通过严格步骤级验证评估研究级数学证明

# 通过严格步骤级验证评估研究级数学证明 来源：https://arxiv.org/html/2606.10799

###### 摘要

大型语言模型（LLMs）在严格验证复杂数学证明方面存在困难。标准的全局评估方法容易遭受“上下文中毒”——表面合理的陈述掩盖了细微的逻辑缺陷，导致幻觉或过度怀疑。为解决此问题，我们从全局评估转向严格的步骤级验证：我们的框架为每个推导步骤维护详细的上下文，并严格限定所应用定理的来源。我们在一个精心策划的对抗性诊断套件上进行评估，该套件包含来自 FirstProof 挑战赛的研究级证明。系统的消融研究表明，这些演绎约束不可或缺，因为无约束的全局提示始终无法定位细微的逻辑错误。除了优于全局评估外，我们的方法从根本上改变了失败分类。错误分析显示，剩余的拒绝并非源于严重的逻辑幻觉，而主要是“迂腐的过度严谨”实例，源于未说明的领域约定，从而有效地揭示了专家基准本身内部的隐含歧义。我们的发现表明，促使代理以谨慎、类似人类数学家的方式组织其验证笔记，可以显著提高其区分严谨证明与有缺陷证明的能力，有潜力强化基座模型尚未很好掌握的前沿数学概念上的代理推理能力，并为未来的自动证明审查系统奠定理论基础。代码和提示可在 GitHub (https://github.com/celainica/A-lightweight-natural-language-proof-verification-agent) 获取。

## 1 引言

大型语言模型（LLMs）和 AI 代理的自我修正与推理能力，随着规模扩展和强化学习而显著提升[7]。在数学领域，代理框架已展现出令人印象深刻的解题结果[8, 14]。然而，在验证研究级数学证明时，当前模型常常出错。标准的全局评估方法容易遭受“上下文中毒”——表面合理的陈述掩盖了细微的虚假论证，导致代理要么幻觉性地认为有效，要么过度怀疑。虽然像 Lean[6] 这样的形式化验证系统提供了绝对保证，但其应用受限于人工构建的基础设施和对手动维护库（如 Mathlib[21]）的严重依赖。这自然限制了当前自动化代理形式化验证高级数学概念的能力。因此，用自然语言验证证明仍然是一个关键的前沿领域。生成非正式证明的细粒度阐述是一个关键桥梁：它不仅有助于人类数学家进行同行评审，也帮助代理系统最终将非正式数学翻译为严谨的形式化代码[23, 13, 3, 24, 25]。至关重要的是，这种对 AI 自我修正的关注，与形式化本身扮演着根本不同的角色。形式化验证系统在最终问责范式上运作，由底层基础设施（如 Lean）或人类专家承担提供绝对正确性保证的责任。相比之下，我们的目标是赋予代理在其探索和生成阶段内在地区分合理推理与错误逻辑的能力。毕竟，代理将不可避免地遇到必须完全依赖纯自然语言推理来构思和发现解决方案的场景。在数学发现高度无约束的搜索空间中，让代理能够识别自身的误步对于修剪死胡同、大幅减少幻觉性或结构性缺陷证明的生成至关重要。最终，我们旨在展示代理推理的一个核心原则：通过强制模型显式且详尽地写出非正式证明的底层细节，我们固有地增强了它发现标准推理中本会被忽略的细微逻辑错误的能力。需要强调的是，为验证我们的方法，我们仅让代理执行阐述过程，而非要求其输出完美无缺、详尽无遗的自然语言证明作为最终结果。因此，我们的目标并非重新发明 de Bruijn 的数学方言（MV）。相反，我们旨在证明，代理——正如人类数学家——利用详细写作这一行为本身来确定哪些结论是真正正确且经过严格证明的。

为实现此目标，我们旨在设计一个代理框架，以人类数学家审阅手稿的严格性来评估证明。这样的系统必须优先考虑**可靠性**（消除对有缺陷证明的错误接受），而非仅仅是完备性，并有效利用**推理时计算**，在推理时间越长时达到更高的清晰度。我们引入了一个关键的方法论转变：**将验证从直接异常检测重新定义为通过严格的步骤级验证进行建设性阐述**。我们并非直接查询 LLM 在全局上下文中发现缺陷——这项任务极易受到上下文中毒和幻觉的影响——而是测试该证明能否被严格且显式地扩展。对于被视为字符串的数学文本 \(S\)，我们将其分解为一个有序的步骤序列 \((s_1, s_2, \dots, s_n)\)，分离出包含逻辑断言的**推导步骤**。“阐述一个步骤”是指将推导步骤 \(s_i\) 扩展为更细粒度的推导字符串 \(s_i'\)，该字符串以自然语言严格保留原始推理轨迹，但显式地展开底层逻辑。因此，异常检测自然地从生成过程中产生：如果代理未能构建有效的 \(s_i'\)，我们就会怀疑 \(s_i\) 存在逻辑缺口或不当的论证。通过强制代理进行阐述，我们以严格的生成约束取代了 LLM 不透明的内部判断[15, 4]。每个阐述的步骤都需要显式地将其应用的定理和逻辑推导置于基础之上，从而减少表面合理性。

为了系统地实施这些约束并确保阐述本身不会引入幻觉，我们将过程植根于一个形式化的描述性框架。具体来说，我们使用一个严格的三元架构对任何推导步骤的逻辑依赖性进行建模：**内部上下文**（\(\Gamma_i\)，包含直接来源于证明文本 \(S\) 的定理、定义和假设）、**外部知识**（\(\Sigma_i\)，包含来自外部文献或已建立领域共识的非平凡陈述），以及**背景理论**（\(\mathcal{T}_i\)，表示句法上推导出该断言所必需的平凡陈述或重写规则）。在操作上，我们将此步骤级验证实现为一个自主的、状态驱动的代理工作流，由固定的提示文件引导。默认情况下，每个推导步骤 \(s_i\) 都会初始化一个保守的局部状态。在每次迭代中，代理尝试阐述剩余的**开放**步骤。基于严格的 \((\Gamma_i, \Sigma_i, \mathcal{T}_i)\) 约束，代理执行特定的状态转换动作：若成功导出阐述，则该步骤转换为**已验证**；相反，若代理识别出明显的逻辑错误，则将其标记为**有缺陷**。为严格防范误报（即迂腐的过度拒绝），任何**有缺陷**的步骤都会触发一个固定的确认阶段：代理尝试确认该错误，如果重新评估后认为该感知到的缺陷已被解决，则可能将状态回滚到**开放**。这个迭代过程受严格的停止标准支配：（1）**接受**：当且仅当所有步骤都达到**已验证**状态时，证明被视为有效；（2）**拒绝**：如果**有缺陷**状态在反思后被明确确认，则立即终止过程并拒绝该证明；（3）**耗尽**：为防止在难以处理的缺口上无限循环，系统在经过连续五次推理恢复且未观察到进展信号后全局停止并拒绝该证明。

为实证验证我们的概念验证并展示其潜在回报，我们构建了一个高度精选的、包含挑战性数学证明的诊断套件。我们专注于小规模样本以确保评估的绝对清晰：每个证明都经过人类专家精心验证，以建立明确的真实标签，将其分类为严格有效或明确无效。具体而言，我们的诊断套件主要基于 **FirstProof** 挑战赛[1, 9, 10]。为建立明确的真实标签，我们收集了经过严格专家评估的证明，获得了一个高度精选的 21 个研究级证明集合，这些证明被明确分类为严格有效或明确无效。这 21 个样本策略性地选自三个权威来源：（1）官方 FirstProof 发布版本，（2）Aletheia 生成的正确证明，以及（3）OpenAI 解决方案的生成结果。通过将我们的评估锚定在这个精确、经过专家验证的套件上，我们可以研究我们的步骤级验证如何有效隔离标准全局评估者始终遗漏的细微推理错误。

在对精选的 21 个证明套件的评估中，我们观察到当前大型语言模型在标准上下文中表现出强大能力：标准全局基线成功识别了 10 个明确无效证明中的 8 个逻辑错误。然而，对全局管道失败的其余 2 个案例的详细分析揭示了一个特定弱点。在这些特定案例中，有缺陷的证明将不正确的数学知识——LLM 不熟悉的知识——包装在结构严谨且看似合理的格式中。这一实证结果突显了证明验证仍然是一项极具挑战性的任务，特别是对于新颖或前沿的数学，LLM 缺乏对所涉特定领域知识的先前熟悉度，容易被听起来正式伪证明所欺骗。为解决此限制，我们在严格的 avg@3 设置下评估了我们的步骤级验证代理，并针对这些特定的对抗性示例补充了多轮实验。通过将推理过程明确植根于 \((\Gamma_i, \Sigma_i, \mathcal{T}_i)\) 约束以追踪外部知识，我们的框架成功隔离了这些伪装的错误，成功拒绝了所有无效证明。此外，在有效证明中，我们的代理仅未能验证 3 个案例。矛盾的是，这些失败恰恰突显了我们框架的严谨性。代理失败并非由于逻辑推理缺陷，而是因为底层基座模型缺乏对高度特定的领域约定的熟悉度，其中某些数学对象默认具有隐含属性。例如，在 FirstProof 数据集的第 7 题中，人类专家自然假设子群 \(\Gamma\) 是显式线性的（因为它是实半单李群的子群，并且按照该特定研究领域的惯例，此类群被视为线性的）[10, 22]。而标准基线只是忽略了这一细微跳跃，对文本一带而过，但我们的代理严格注意到，根据一般定义，实半单李群的子群并不默认是线性的[19]。由于基座模型不熟悉这个既定的领域约定，它保守地拒绝任意将线性假设添加到局部上下文中，最终丧失了验证证明所需的基本条件。这种对比完美地展示了我们的框架强制执行真正的演绎验证，而非表面模式匹配，即使它在面对尚未掌握的领域特定约定时会停止。

总之，我们的主要贡献有三方面：
- **方法论范式转变**：我们将自然语言证明验证从直接的、黑箱的异常检测重新定义为**建设性阐述**。通过新颖的 \((\Gamma_i, \Sigma_i, \mathcal{T}_i)\) 三元架构对推导步骤的逻辑依赖性建模，我们强制模型显式追踪内部上下文、外部知识和背景理论，从而减轻表面模式匹配。
- **自主验证工作流**：我们提出了一个由严格步骤级约束引导的状态驱动代理框架。配备固定的确认阶段和稳健的停止标准，我们的系统优先考虑逻辑可靠性，并有效利用推理时计算来防止困扰全局评估者的“上下文中毒”。
- **通过微基准测试的实证见解**：我们的评估表明，即使高度能力的标准基线仍可能被结构严谨的伪证明所欺骗，但我们的框架在问题集上实现了零错误接受。此外，我们的定性分析揭示了当前验证任务中的一个关键瓶颈：基座模型容易受到未说明的、领域特定的隐含约定的影响。

## 2 相关工作

#### 数学代理

用于数学的代理框架发展迅速，并在研究级数学中产生越来越重要的成果。这些代理可能使用也可能不使用证明助手和形式语言。最近的前沿突破强烈偏向后一种范式：代理完全使用纯自然语言进行探索、推理和证明构建。例如，**Rethlas**[14] 可以作为一个非正式推理代理运行，模仿人类数学工作流程——探索文献并为高级开放问题提出候选自然语言证明。类似地，**Aletheia**[8] 作为一个端到端自然语言研究代理，能够迭代地生成、验证和修改从博士级练习到自主研究论文的解决方案。最近，**OpenAI 的模型**[20] 通过使用高度复杂的纯非正式推理，驳斥了 Erdős 已有 80 年历史的平面单位距离猜想，实现了历史性的里程碑。然而，尽管这些纯自然语言代理具有强大的生成能力，但它们的一个关键弱点是其