用大语言模型求解不等式证明

用大语言模型求解不等式证明

Solving Inequality Proofs with Large Language Models

https://arxiv.org/pdf/2506.07927v2

摘 要
不等式证明在众多科学与数学领域中至关重要，它考验着高级推理能力，例如发现紧致界（tight bounds）和策略性地应用定理。这使其成为大语言模型（LLMs）面临的一个独特而具有挑战性的前沿任务，所提供的洞见超越了一般的数学问题求解。然而，该领域的进展受到现有数据集的制约——这些数据集往往稀缺、合成生成，或形式过于僵化。我们通过提出一种非正式但可验证的任务形式来应对这一挑战，将不等式证明重新表述为两个可自动检验的子任务：界估计（bound estimation）与关系预测（relation prediction）。在此基础上，我们发布了 IneqMath——一个由专家精心整理的奥林匹克级别不等式数据集，包含一个测试集和一个训练语料库，后者配有逐步解答和定理标注。我们还开发了一种新颖的“大语言模型作为评判者”（LLM-as-judge）评估框架，该框架结合了一个最终答案评判者与四个步骤级评判者，专门用于检测常见的推理缺陷。在 IneqMath 上对 29 个主流大语言模型的系统评估揭示了一个令人惊讶的现实：即使是最先进的模型（如 o1），在步骤级严格审查下整体准确率也低于 10%；相较于仅考虑最终答案等价性时的准确率，这一数字最多下降了 65.5%。这种差距暴露了当前大语言模型在演绎链条上的脆弱性，以及在“找到答案”与“构建严谨证明”之间的关键鸿沟。扩大模型规模或增加测试时计算资源对整体证明正确性的提升作用有限。相反，我们的研究结果指出了若干有前景的研究方向，例如定理引导的推理（theorem-guided reasoning）和自我精炼（self-refinement）。

1 引言
数学不等式在分析、优化和概率论等诸多领域中具有基础性地位，其应用遍及科学建模、经济学以及竞赛数学。证明一个不等式是一项复杂的工作，不仅需要计算能力，更要求一种精妙的综合能力：包括发现紧致界（tight bounds）的直觉、策略性地选择与应用经典定理（例如均值-几何平均不等式 AM-GM、柯西-施瓦茨不等式 Cauchy-Schwarz）的洞察力，以及精确的符号变换能力。这些能力是高级数学推理的标志，使不等式证明区别于一般的数学问题求解。因此，若能实现这一过程的自动化，将产生广泛影响：可为自动定理证明器（ATPs）提供缺失的引理，加速形式化验证流程，并为通用推理系统提供一个极具挑战性的测试平台。

然而，尽管大语言模型（如 DeepSeek-R1 [14] 和 OpenAI o3 [48]）以及自动定理证明器本身 [16, 18, 26, 34, 50, 75] 已取得显著进展，不等式证明的自动化仍然是一个充满挑战的前沿问题。阻碍大语言模型在该领域能力提升的一个主要瓶颈是缺乏合适的基准数据集。现有资源在多个方面存在不足：通用 ATP 数据集如 MiniF2F [82] 和 ProofNet [7] 中包含的不等式数量极少；合成数据集如 INT [64] 和 AIPS [63] 虽具规模，但由于基于模板生成，可能缺乏结构多样性；而人工整理的数据集如 ChenNEQ [8] 则通常规模过小，难以支撑大规模训练。

更根本的是，大多数现有数据集采用完全形式化的表示方式，将问题和证明编码在 Lean [11] 或 Isabelle [42] 等形式系统中。虽然形式化数学推理能提供正确性保证，且是重要的研究方向，但大语言模型是在海量自然语言语料上训练而成，往往展现出强大的非形式化推理能力。这表明，即使模型难以应对形式化证明器严苛的语法要求，它们仍可能以非形式化的方式解决问题。因此，我们的工作旨在探索并评估这种非形式化能力，通过聚焦更贴近人类直觉、更接近数学发现初期（通常结构较松散）的推理模式，来补充当前形式化数学人工智能的研究。

为弥合形式严谨性与直观解题之间的鸿沟，我们提出了一种非正式但可验证的任务形式（§2）。我们不要求模型在形式系统内生成完全可机器检验的证明，而是将不等式问题重新表述为两个具体且可自动验证的子任务：(i) 界估计（Bound estimation）——确定能使不等式成立的最大（或最小）常数 C C；(ii) 关系预测（Relation prediction）——判断两个表达式之间成立的关系（>、≥、=、≤ 或 <）。这两个任务均可使用自然语言和 LaTeX 表达，由大语言模型逐步求解，其最终答案（一个常数或一个关系符号）可被自动验证。这种方式保留了不等式证明的创造性本质，同时避免了形式化证明辅助工具带来的沉重开销。

基于这一任务形式，我们发布了 IneqMath（§3）——首个完全以非正式语言编写的、大规模奥林匹克级别不等式数据集。测试集包含 200 道原创题目，均由国际数学奥林匹克（IMO）级别奖牌得主精心设计并审核，确保其原创性与难度。训练语料库包含 1,252 道题目，源自高等教材，先由大语言模型自动重写为我们定义的两个子任务形式，再经人类专家细致审校。一个关键特点是，每道训练题最多配有四条逐步解答路径，为训练大语言模型的细粒度推理提供了丰富数据。此外，76.8% 的训练题目标注了与其解法相关的 83 个命名定理，涵盖 29 个类别。如表 2 所示，IneqMath 在规模、多样性以及与人类式非形式化解题方法的对齐程度上，均超越了以往资源。

然而，仅得出正确最终答案是不够的，推理过程本身必须可靠。为此，我们提出了一个 “大语言模型作为评判者”（LLM-as-judge）的评估框架（§4）。该框架包含一个高精度的最终答案评判者，用于验证答案等价性；并辅以四个专门的步骤级评判者，用于评估推理步骤的合理性。这些步骤级评判者旨在检测我们在预实验中识别出的常见推理缺陷：过度依赖玩具案例（toy case examples）、未处理的逻辑漏洞、未经论证的数值近似，以及数值计算错误。在人工标注的开发集解答上验证表明，这些评判者具有高可靠性（平均 F1 > 0.9），为大规模审查大语言模型生成证明的演绎完整性提供了可扩展的方法。

我们在 29 个主流大语言模型上进行了系统评估（§5），涵盖从通用聊天模型到先进推理模型，包括开源与闭源系统。如图 1 所示，关键结果如下：尽管专用推理模型（如 o1 [45]）在最终答案准确率上优于通用聊天模型（如 GPT-4o [43]），但这种优势在步骤级审查下往往大幅削弱。一旦我们的评判者逐条检查推理步骤，整体准确率最多骤降 65.5%。事实上，即便是表现最佳的模型（如 o1），其整体准确率也低于 10%（见表 4），暴露出其演绎链条的脆弱性，以及“找到答案”与“构建严谨证明”之间的显著差距。

我们的深入研究（§5.3）表明：尽管模型规模增大与最终答案准确率提升呈正相关，但对整体准确率的影响有限（例如 o1 的整体准确率仅为 8.0%）。同样，通过延长推理链来增加测试时计算资源，在整体正确性上的收益也迅速递减（例如，当 o1 的最大输出 token 数从 5K 增至 40K 时，其整体准确率仍维持在 8.0%；而 o3 [48] 的准确率则在约 31% 处趋于饱和）。这些发现表明，当前的模型扩展策略不足以支撑 IneqMath 中所需的稳健演绎推理。

相反，我们探索了若干有前景的改进策略：例如定理引导推理（theorem-guided reasoning）——通过提供“黄金定理”（golden theorems），可使 o3-mini [47] 的整体准确率最高提升 11%；以及批评者引导的自我精炼（critic-guided self-refinement）——例如 Gemini 2.5 Pro [22] 的整体准确率实现了 5% 的绝对提升。

综上所述，本工作做出四项核心贡献：

1. 提出一种不等式证明的非形式化重构方法，将任务分解为两个可验证的子任务（§2）；
2. 发布 IneqMath——一个由专家整理的奥林匹克级别不等式基准测试集，以及一个富含逐步解答和定理标注的训练语料库（§3）；
3. 开发了一个模块化的 LLM-as-judge 框架，可严格评估最终答案与证明步骤的合理性（§4）；
4. 开展了一项系统的实证研究（§5），揭示了大语言模型性能与数学严谨性之间的显著差距，并指明了未来研究的方向。

2 任务形式化：一种非正式视角

然而，这种形式化方法要求使用者具备专业工具的使用经验；而自然语言中的非正式证明虽然更符合直觉，却因其非结构化的特性而难以自动验证。

为应对这些挑战，我们提出一种非正式视角，将不等式证明问题重新表述为两个可验证的子任务：界估计（bound estimation）与关系预测（relation prediction）。

这些子任务之所以被选用，是因为它们在数学问题求解中频繁出现，能够简化评估流程，并且关键在于，它们保留了原始不等式证明问题所固有的核心推理挑战。一个理想的 LLM 解答不仅应给出正确的最终答案，还应呈现清晰、逻辑严谨且完整的推导过程，包括策略性地应用定理、准确的符号操作与计算，以及对所有关键步骤的充分论证。

3 IneqMath：不等式问题数据集
本节描述 IneqMath 的数据整理过程及其关键统计信息。IneqMath 是一个新颖的不等式问题集合，旨在支持以非正式视角来求解和证明不等式。

测试数据整理。为减少来自常见来源（如教材、竞赛和在线资源）的污染——这些内容可能已存在于大语言模型的训练语料中——我们委托国际数学奥林匹克（IMO）级别的奖牌得主专门设计全新的不等式题目。这些题目随后由另一个独立专家小组进行严格评审，并仅在全体一致确认其可解性、推理合理性及标准答案正确性后才被采纳。专家认为较简单的题目被排除在测试集之外（转用于开发集），以确保测试集具有较高难度。为进一步说明污染程度有限，我们还在 §C.8 中对测试集进行了记忆性探测（memorization probe）。相关数据整理工具详见 §A.2。我们还搭建了一个在线评测网站¹，为社区提供公平的评估平台。

关键统计信息。如表 1 所示，IneqMath 数据集包含用于基准测试的 200 道测试题、100 道带公开标准答案的开发题，以及 1,252 道训练题，后者在界估计和关系预测两个子任务之间平均分配。每道训练题均配有逐步解答，最多包含四条不同解法；其中 76.8%（即 962 道）标注了相关定理。该数据集涵盖了 29 个类别中的 83 个命名定理，其分布情况见图 2。测试题示例见 §A.4。

与现有数据集的比较。如表 2 所总结，IneqMath 的突出特点在于：(1) 提供由专家精心整理的训练集和测试集；(2) 提供丰富的标注信息，包括逐步解答和 83 个有明确依据的定理；(3) 采用一种非正式且易于使用的不等式证明格式，通过界估计和关系预测两个子任务进行表述，并借助 LLM-as-judge 框架进行评估。这一设计弥合了形式化证明系统与直观数学推理之间的鸿沟，使 IneqMath 成为推动大语言模型在问题求解与定理证明能力方面发展的独特资源。

潜在污染声明。为确保评估的严谨性，IneqMath 测试集由 IMO 级别的奖牌得主专门设计，包含全新题目，以最大程度减少大语言模型在预训练阶段接触过相关内容的可能性。各类模型在该测试集上的普遍不佳表现（§5.2），尤其是在整体准确率方面（该指标要求每一步推理都正确），强烈表明该基准确实构成了显著的推理挑战，无论模型是否对底层数学概念存在一定程度的熟悉。因此，我们相信 IneqMath 测试集能够有效探测模型在解决新问题方面的能力，我们关于当前大语言模型在严谨不等式证明方面存在局限性的结论是稳健的。

4 面向不等式求解的细粒度非正式评判器
IneqMath 数据集的测试部分构成我们的基准，包含 200 道奥林匹克级别的不等式题目，对人类和当前的大语言模型均构成挑战。在此场景下，传统评估方法存在不足：专家人工标注虽准确，但劳动成本过高；而字符串匹配或数值等价性等自动化技术则无法捕捉逐步推理的正确性——而这正是不等式求解的核心要素。

为解决这一问题，我们提出一种细粒度的 LLM-as-judge 框架（如图 3 所示），包括一个用于验证预测答案的最终答案评判者（§4.1）和四个专门针对常见推理缺陷的步骤级评判者（§4.2）。只有当一个解答通过全部五个评判者的检验时，才被视为整体正确。如表 3 所示，这些评判者与人工标注高度一致（F1 = 0.93），为手动评估提供了一种可扩展且可靠的替代方案。

4.1 最终答案评判者

4.2 四个步骤级评判者

逻辑漏洞评判者（Logical Gap Judge）。IneqMath 的不等式问题常涉及多步推导（如代数变换、约束优化、函数变换），需要明确的论证支持。然而，大语言模型往往跳过关键推理步骤，或在无依据的情况下直接断言结论（例如，直接给出最优界而不提供推导过程）。现有步骤级评估方法 [68] 能评估有效性与冗余性，但对这类逻辑遗漏缺乏细粒度判断。我们的逻辑漏洞评判者通过标记缺失的过渡步骤、无依据的断言以及模糊的推导（特别是在涉及不等式变换或界估计的步骤中）来解决此问题（详见 §B.3）。

4.3 评判器有效性验证

整体性 LLM 评判基线。为凸显我们专用评判系统的设计动机，我们首先评估一种启发式的 LLM-as-judge 基线方法。该方法提示一个通用大语言模型，对 IneqMath 解答的整体正确性进行综合判断，同时考虑最终答案的准确性以及 §4.2 中所述四类推理缺陷的步骤级合理性。如图 4 所示，在 80 个经人工标注的开发集样例上构建的混淆矩阵表明，这种朴素方法与人类标注的一致性很差，凸显了其在本领域严谨评估中的不可靠性。

细粒度评判器的性能。相比之下，我们提出的五位专用评判器组合与人类评估高度一致。图 5 展示了在同一开发集上每位评判器的混淆矩阵。最终答案评判者（使用 GPT-4o-mini）实现了近乎完美的对齐，而四个步骤级评判者（根据性能与成本的平衡选定，详见 §B.6）也表现出高保真度。这证实了：将复杂的评估任务分解为有针对性的子问题，可使大语言模型成为可靠的评估工具。

评判器分歧的定性分析。尽管整体表现优异（总体 F1 = 0.93，见表 3），LLM-as-judge 的评估并非完美无缺。鉴于学界对基于 LLM 的评估普遍存在疑虑，我们对评判器判断与人工标注不一致的失败案例进行了定性分析。详细示例见 §B.7。这些案例表明，尽管我们的 LLM 评判器非常有效，但在涉及专家级数学推理所特有的深度与细微理解时，仍可能面临挑战。

5 IneqMath 实验

5.1 实验设置

我们在 IneqMath 测试集的不等式问题上，对 29 个主流大语言模型进行了系统性评估。所评估的模型涵盖两类：通用聊天模型（包括开源和闭源模型）以及专为复杂、多步问题求解设计的专用推理大语言模型。

所有模型均在零样本（zero-shot）设置下进行提示，输入包含问题陈述和指令：“请以清晰、严谨且逻辑严密的步骤解答该问题”，以鼓励模型生成详细推理过程。模型的输出由我们提出的 LLM-as-judge 框架（§4）进行评估。

我们报告以下三项关键指标：

• Answer Acc（答案准确率）：衡量预测答案的正确性，由最终答案评判者（§4.1）验证。
• Step Acc（步骤准确率）：汇总由四个专用步骤级评判者（§4.2）判定的各推理步骤的正确性，这些评判者针对常见的推理缺陷。
• Overall Acc（整体准确率）：主要评估指标，仅当解答同时满足最终答案正确且所有推理步骤无瑕疵（即通过全部五个评判者）时，才视为正确。

因此，只有当模型通过逻辑有效的推理步骤得出正确最终答案，并通过所有评判者的审查时，其回答才被视为完全正确（Overall Acc）。更多实验设置细节见 §C.1。

5.2 主要评估结果

表 4 展示了所评估大语言模型在 IneqMath 上的性能。我们的分析揭示了当前大语言模型在不等式证明能力方面的若干关键洞见：

1. 推理型大语言模型具有更高的最终答案准确率。例如，o1（答案准确率 62.5%）和 Grok 3 mini（71.5%）在识别正确最终答案方面显著优于通用聊天模型（如 GPT-4o 的 37.5%、Grok 3 的 54.5%）。这表明专用架构或训练方法提升了模型搜索并找到最终答案的能力。
2. 步骤级审查暴露出性能的急剧下降。答案准确率的优势往往掩盖了底层推理缺陷。一旦对推理步骤进行评估，整体准确率便大幅下滑。例如，Grok 3 mini 的准确率下降了 65.5%（从 71.5% 的答案准确率降至 6.0% 的整体准确率），o3-mini 下降了 53.0%。这种显著差距凸显了大语言模型生成的演绎链条的脆弱性。
3. 构建严谨证明仍是一大挑战。即便是顶尖模型如 o1，其整体准确率也较低（8.0%）。许多大型模型尽管具备中等水平的答案准确率，整体表现依然不佳（例如 Grok 3 的整体准确率仅为 3.5%）。这表明，在“找到一个看似合理的答案”与“构建数学上严谨、逐步推导的证明”之间存在根本性鸿沟。

5.3 深入研究

错误解答分析。如表 4 所示（其中报告了整体准确率、最终答案准确率以及四类步骤级错误的平均错误率），大语言模型生成解答中最常见的步骤级错误是逻辑漏洞（各模型平均失败率达 85.0%）和基于玩具案例的无根据泛化（59.7%）。数值近似错误（26.9%）和计算错误（6.8%）虽较少见，但仍具显著影响。对错误解答的详细检查（见 §C.2.1–§C.2.4 中的示例）突显了这些普遍存在的错误模式——即使模型得出了正确的最终答案，这些错误也常常破坏整个证明的严谨性。除步骤级错误外，大语言模型在复杂问题上也难以得出正确最终答案（§C.2.5），表明其在定理应用和符号操作方面面临更深层次的挑战。

模型规模的缩放规律。图 6 展示了仅评估最终预测答案正确性时，大语言模型的最终答案准确率如何随模型规模增长。随着模型规模增大，答案准确率稳步提升，体现出一种经验性的缩放规律：更大的模型更擅长推断正确的界和不等式关系。然而，当考虑整体准确率（即同时要求答案正确和中间推理步骤有效）时，这一趋势不再成立，如图 7 所示。在此情况下，缩放曲线趋于平缓，表明仅靠增加模型规模不足以消除逐步推理中的错误。

测试时计算的缩放规律。延长测试时计算、允许更长的推理链，是解决复杂问题的常用策略 [14]。我们通过调整推理型大语言模型的最大生成 token 数，研究了其对 IneqMath 整体准确率的影响。图 8 显示，尽管像 Gemini 2.5 Pro 和 o3 这样的模型在初期随着 token 数增加而有所提升，但其性能增益很快趋于饱和（例如，超过 20K tokens 后）。这表明，单纯增加计算预算对于获得严谨且步骤正确的证明所能带来的收益递减，凸显出仅靠延长“思考过程”是远远不够的，亟需更有效的推理机制。

5.4探索改进策略

以相关定理作为提示（hints）。为评估基于定理的提示效果，我们在模型求解一个包含 40 道题目的测试子集时，为其提供来自 IneqMath 训练语料中最常出现的 top-k 个定理。如图 9 所示，对于较弱的模型（例如 Grok 3 mini、o3-mini、o4-mini），提供一到两个此类定理反而会降低其整体准确率，这可能是因为模型误用了这些定理，或被潜在不相关的信息干扰。相反，更强的模型（如 Gemini 2.5 Pro）则能从这些提示中获益，表明高级推理能力对于有效利用此类指导至关重要。这些结果既凸显了定理引导推理（theorem-guided reasoning）的潜力，也强调了亟需更精细的定理检索机制（例如 RAG [28, 24]），以可靠地提升大语言模型在不等式证明中的表现。详细实验见 §C.4。

通过批评者反馈实现自我改进。已有研究表明，让大语言模型对其自身推理进行批判并修订，可提升其在复杂任务上的表现 [78, 57]。为探究这一方法是否适用于不等式证明，我们从 IneqMath 中随机抽取了 40 道测试题，并执行了一轮自我批判（self-critique）。如图 10 所示，自我批判持续提升了模型性能——例如，Gemini 2.5 Pro 的整体准确率从 43% 提高至 48%。这一上升趋势表明，自我批判是一种有前景的、无需外部监督的方法，可有效增强大语言模型在不等式推理中的逻辑严谨性与解答质量。更多细节见 §C.5。

6 相关工作

不等式与定理证明的数据集。提升大语言模型在不等式证明方面能力的主要瓶颈之一是缺乏合适的数据集。现有资源在多个方面存在不足：通用自动定理证明器（ATP）数据集如 MiniF2F [82] 和 ProofNet [7] 中包含的不等式数量极少；合成数据集如 INT [64] 和 AIPS [63] 虽具规模，但由于基于模板生成，往往缺乏结构多样性；而人工整理的数据集如 ChenNEQ [8] 通常规模过小，难以支撑大规模训练。更根本的是，大多数现有数据集 [80, 59, 73, 29, 58, 26] 采用完全形式化的表示方式，将问题和证明编码在 Lean [11] 或 Isabelle [42] 等系统中。尽管形式化数学推理能提供正确性保证，且是重要的研究方向，但大语言模型是在海量自然语言语料上训练而成，通常展现出强大的非形式化推理能力。因此，我们的 IneqMath 采取一种非正式视角，将不等式证明问题重新表述为两个可验证的子任务——界估计（bound estimation）与关系预测（relation prediction）。IneqMath 中的问题均由 IMO 级别奖牌得主专家设计并审核。其他非形式化推理数据集 [49, 39, 23, 37] 通常缺乏标注的解答、定理引用或相应的训练数据。为弥补这些空白，IneqMath 引入了 1,252 道用于训练的不等式问题，每道题均标注了与其解法相关的定理，并最多包含四步的逐步解答。

不等式与定理证明的方法。不等式证明十分复杂，需要识别紧致界的直觉、策略性地运用定理，以及精确的符号操作。传统的自动定理证明器（ATPs）主要在 Lean [11] 或 Isabelle [42] 等形式系统内运行，要求问题和证明以专用语言进行编码。受大语言模型在数学推理方面能力的启发 [81]，近期大量工作聚焦于将 LLM 与这些形式化 ATP 集成。这些方法通常将定理证明建模为马尔可夫决策过程（MDP），训练 LLM 在形式系统中选择合适的策略（tactics）和前提以构建证明 [1, 9, 62, 16, 18, 26, 34, 61, 72]。例如，Goedel-Prover [35] 利用大规模 Lean 语料库训练模型进行策略预测，从而实现端到端的形式化证明生成。其他方法则结合树搜索技术，在形式框架内探索前提的搜索空间 [65, 31, 70, 71]。

大语言模型在海量自然语言语料上的训练使其在非形式化推理方面具有优势——这更接近人类解决问题的方式。这揭示了一种利用此类非形式化能力的新机遇。我们的工作脱离了形式化范式，提出了一种非正式但可验证的不等式证明框架，旨在对大语言模型在类人问题求解中的表现进行基准测试与提升，并探索如定理引导推理和自我精炼等改进策略。

用于数学问题求解的 LLM-as-judge 方法。可靠评估数学问题求解不仅需要判断最终答案的正确性，还需评估每一步推理的逻辑合理性，这对自动化系统而言是一项重大挑战。传统方法往往不足：专家人工标注劳动密集且难以扩展至大规模评估 [49, 39]；而字符串匹配或数值等价性等自动化技术则忽略了逐步证明正确性的关键方面 [25, 23, 37, 38]。尽管大语言模型作为评判者（LLM-as-judge）已展现出潜力，其在细粒度、步骤级数学判断方面的能力仍在发展中。例如，现有的步骤级 LLM 评判器 [68, 17] 可能评估步骤的一般有效性，但往往缺乏识别细微推理缺陷的粒度。类似地，EIC-Math [30] 等框架虽提供宽泛的错误类别，却可能遗漏多步推导中微妙但关键的问题。为应对这些局限，并有效评估不等式求解等非形式化数学证明，我们的 LLM-as-judge 框架结合了一个最终答案评判者与四个专门针对常见错误的步骤级评判者：玩具案例过度泛化、逻辑漏洞、未经论证的数值近似，以及数值计算错误。

7 结论

综上所述，我们提出了一种非正式但可验证的不等式证明任务形式化方法，将其分解为界估计（bound estimation）与关系预测（relation prediction）两个子任务。基于此，我们发布了 IneqMath——一个由专家精心整理的奥林匹克级别不等式基准数据集，其训练语料库包含逐步解答和定理标注。我们还开发了一种新颖的 LLM-as-judge 评估框架，包含一个最终答案评判者和四个步骤级评判者，从而实现对模型推理过程的严格评估。

我们对多种主流大语言模型的全面评估揭示了一个关键差距：尽管大语言模型可能在最终答案准确率上表现较高，但在步骤级审查下，这一指标最多骤降 65.5%，即便是顶尖模型如 o1，其整体准确率也低于 10%。这一差距暴露了当前大语言模型在构建严谨数学证明时所依赖的演绎链条的脆弱性。

此外，我们发现单纯扩大模型规模或增加测试时计算资源对整体证明正确性的提升作用有限。相反，我们的研究结果指出了若干有前景的研究方向，例如定理引导推理（theorem-guided reasoning）和自我精炼（self-refinement）。

原文链接：https://arxiv.org/pdf/2506.07927v2