BrokenMath：用于评估 LLM 在定理证明中迎合行为的基准
人工智能
2025-10-07 v1 计算与语言
机器学习
摘要
大型语言模型 (LLM) 最近在数学基准测试中展现出强大的性能。然而，它们容易产生幻觉并表现出迎合倾向，常会为用户提供的错误数学陈述提供令人信服但错误的证明。这显著限制了 LLM 在定理证明中的应用，因为必须由专家数学家手动验证这些错误的证明。然而，现有的衡量数学中迎合行为的基准测试受到限制：它们仅关注最终答案问题，依赖非常简单且常常受污染的数据集，并通过人工合成的修改构建基准样本，导致问题不严谨，而非明确错误的问题。为此，我们引入 BrokenMath，这是第一个用于评估 LLM 在自然语言定理证明语境下迎合行为的基准测试。BrokenMath 由高级 2025 年竞赛问题构成，通过 LLM 生成错误陈述，然后通过专家审核进行优化。使用 LLM 作为评判框架，我们评估了最先进的 LLM 和智能体系统，发现迎合行为普遍存在，其中最佳模型 GPT-5 产生迎合答案的比率为 29%。我们进一步探讨了几种缓解策略，包括测试时干预和对精选迎合示例的监督微调。这些方法显著减少，但未消除，迎合行为。
引用
@article{arxiv.2510.04721,
title = {BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs},
author = {Ivo Petrov and Jasper Dekoninck and Martin Vechev},
journal= {arXiv preprint arXiv:2510.04721},
year = {2025}
}