FaithSieve：基于忠实形式证据的数学证明细粒度评估

# FaithSieve：基于忠实形式证据源的数学证明细粒度评估  
来源：https://arxiv.org/html/2608.26310  
作者：王子宇  
所属机构：北京大学前沿交叉学科研究院  
电子邮箱：[[email protected]](mailto:[email protected])  
戴清明  
所属机构：北京大学数学科学学院  
电子邮箱：[[email protected]](mailto:[email protected])  
吴一山  
所属机构：华为技术有限公司2012实验室理论实验室  
电子邮箱：[[email protected]](mailto:[email protected])  
文再文  
所属机构：北京国际数学研究中心（北京大学）  
电子邮箱：[[email protected]](mailto:[email protected])  

#### 摘要  
大语言模型现已能够生成复杂的、多步骤的数学证明，但如何可靠地判定其正确性并定位早期逻辑错误仍是关键挑战。现有评估方法大多依赖模型生成的自然语言判断，往往忽视局部推理缺口。尽管Lean等形式定理证明器为严格验证提供了路径，但用其评估非正式文本需解决局部性与语义不匹配问题：证明器可能通过证明过于宽泛的目标来绕过局部缺陷，或验证一个偏离原始数学意图的自动形式化命题。为此，我们提出FaithSieve——一个借助Lean的框架，用于对自然语言数学证明进行细粒度评估。FaithSieve将粗粒度证明步骤分解为局部推理单元，提取类型化证明义务，并通过形式化评估代理进行验证。形式化验证受语义对齐评分控制，仅当形式化命题忠实保留了原始主张的上下文、对象和逻辑形式时，才会采纳Lean证据。我们构建了两个经专家验证的数据集：ProofLoc-Olympiad和ProofLoc-University，以评估首个错误定位能力。在包含350道题的Olympiad数据集上，采用GPT-5.4作为主干的FaithSieve达到81.43%的精确首个错误准确率，优于72.29%的直接判断基线。此外，在覆盖六个高级数学领域的200道题ProofLoc-University基准测试中，FaithSieve达到84.5%的精确准确率，而直接判断方法为75.0%。我们的工作表明，将证明分解为细粒度单元并以忠实的形式证据作为依据，能显著提升自然语言推理的可靠评估。

## 1 引言  
大语言模型现可生成多步骤数学证明，但评估这些证明并定位首个逻辑错误仍然困难。此类证明可能省略条件、跳过推导、使用隐含假设，或从早期错误延续至看似合理的结论。因此，可靠评估不仅需检查最终答案，还需验证局部推理步骤。现有的自然语言验证方法已取得重大进展。自我一致性、过程监督、过程奖励模型以及近期关于错误定位的工作（如ProcessBench、Hard2Verify、ProofGrader/ProofBench）为步骤级评估提供了有用基线[Wang et al., 2023, Lightman et al., 2023, Tyen et al., 2024, Zheng et al., 2025, Pandit et al., 2025, Ma et al., 2025]。然而，其证据主要来自基于模型的自然语言推理评分或分类。与此同时，形式推理系统也发展迅速。Lean、mathlib以及DeepSeek-Prover-V2、Seed-Prover、AxiomProver、Aria、M2F等系统表明，许多数学命题现可用形式证据验证[The mathlib Community, 2020, Ren et al., 2025, Chen et al., 2025b, Chen et al., 2025a, Axiom, 2026, Wang et al., 2025a, Wang et al., 2026]。  
将Lean直接用作非正式证明的判官仍面临一个核心障碍：Lean仅验证提交给它的形式命题；即使该命题可证，也不一定忠实表达待检查的证明步骤。自动形式化可能遗漏假设、添加条件、逆转蕴含关系，或将有争议的局部主张重写为不同但可证的命题。因此，形式证据仅当验证目标保持局部且语义上忠实于原始主张时，才对错误定位有用。我们提出FaithSieve，一个借助Lean的自然语言数学证明首个错误定位框架。FaithSieve将粗粒度证明步骤分解为局部边单元（EdgeUnit），从可疑转换中提取类型化证明义务，并结合轻量级检查、Lean验证和语义对齐评分来生成局部证据。Lean不被用作对整个证明的直接判官，而是作为由语义对齐控制的结构化证据源。整体工作流分为三个阶段：定位、验证与合成。定位阶段构建边单元并选择局部转换进行优先检查。验证阶段将这些转换转化为证明义务，并通过形式化与轻量级非形式化检查收集证据。合成阶段将局部证据聚合回原始步骤层级，并预测首个错误步骤。图1展示了该流程。图1：FaithSieve借助Lean进行首个错误定位的工作流概览。我们构建了两个经专家验证的数据集：ProofLoc-Olympiad（包含350道代数与数论问题）和ProofLoc-University（包含200道高等数学问题）。在ProofLoc-Olympiad上，FaithSieve达到81.43%的精确首个错误准确率，而GPT-5.4直接判断基线为72.29%。在ProofLoc-University上，FaithSieve同样明显优于直接判断方法。我们的贡献如下：  
1. **Lean辅助的证明错误定位框架**。我们将局部性与语义忠实性视为应用Lean验证于自然语言证明评估的核心挑战，并提出FaithSieve作为首个错误定位的Lean辅助框架。  
2. **证明状态树分解与类型化义务**。我们引入证明状态树表示，将粗粒度证明步骤分解为局部状态转换，并提取类型化义务以明确每个转换的推理责任。  
3. **语义对齐评分**。我们提出语义对齐分数来衡量Lean命题是否保留了非形式义务的意图，从而仅当形式验证避免偏移或弱化目标时才被采用。  
4. **专家验证的评估数据集**。我们构建了两个覆盖竞赛数学与大学数学的专家验证基准，并表明忠实的局部形式证据优于直接判断基线。

## 2 任务形式化与挑战  
### 2.1 问题形式化  
当大语言模型生成自然语言数学证明时，一个核心挑战不仅是判断整体正确性，还要定位首个错误步骤。BIG-Bench Mistake首次将首个错误定位形式化为显式评估问题，后续工作扩展至数学过程验证与开放式解答[Tyen et al., 2024, Zheng et al., 2025, Pandit et al., 2025]。过程监督与PRMs为步骤级正确性建模提供了进一步背景[Lightman et al., 2023]。我们沿用此形式化，但探究形式验证能否为首个错误定位提供可检查的结构化证据。具体而言，输入为数学问题 \(p\) 和包含 \(n\) 步的自然语言证明 \(\pi=(s_1,\ldots,s_n)\)，系统需输出“正确”或首个错误步骤的索引 \(k\)（其中 \(k\) 对应基准步骤）。我们将首个错误步骤定义为使证明在数学上不可靠的最早步骤；后续错误可能存在但非评估目标。为评估，我们沿用先前首个错误定位工作的标签接口[Tyen et al., 2024, Zheng et al., 2025]，报告二进制准确率与精确准确率。设 \(y, \hat{y} \in \{\texttt{correct}\} \cup \{1,\ldots,n\}\) 分别为金标准标签与系统预测。二进制准确率衡量系统能否正确区分有效证明与无效证明，而精确准确率要求与金标准标签完全匹配：对有效证明为“正确”，对无效证明为正确的首个错误步骤。

### 2.2 基于Lean的验证：前景与挑战  
为超越纯自然语言判官，一个自然方向是使用Lean等证明助手为局部数学命题提供可检查的形式制品。Lean验证可将部分判断从模型分数转化为可验证的证明结果或失败信号。对于代数重写、逻辑蕴含、目标归约、见证验证与案例覆盖，形式验证可能提供比自然语言评分更强的证据。然而，此证据并非无条件可靠：形式验证必须针对正确的局部对象，且该对象必须忠实表达原始自然语言命题。  
**局部性不匹配**。首要困难是确保形式验证针对与自然语言证明相同的局部推理。证明通常由局部推理转换而非单一组成。若证明声称从 \(a\) 推出 \(b\)，再从 \(b\) 推出 \(c\)，仅证明 \(a \to c\) 并不确立两个局部步骤 \(a \to b\) 和 \(b \to c\) 正确。强大的证明器可能直接证明更强或更粗糙的目标，忽略原始证明中的局部错误。因此，形式验证需要分解与定位：粗粒度步骤必须拆解为局部推理单元，且系统需选择验证哪些局部命题。  
**语义不匹配**。第二个困难是确保Lean命题忠实表示原始义务。即使定位后，系统也需将非形式主张转化为形式命题。自动形式化可能遗漏假设、添加条件、逆转蕴含、改变量词、弱化或强化结论，或用不同但可证的命题替代原主张。因此，编译成功或证明成功本身不足为关键；关键问题在于Lean命题是否与原始主张语义对齐。  
这两个不匹配导致两项要求：首先，形式验证应作用于局部推理单元，因此系统需适当分解证明；其次，被验证的Lean命题必须与原始自然语言语义对齐。据此，我们不将Lean用作端到端定理证明器，而是作为条件证据生成器：仅当局部性与忠实性均满足时，形式结果才是强证据。

## 3 定位可验证推理单元  
### 3.1 递归分解为证明状态树  
对于传统思维链证明，COT步骤适合作为标注与输出单位，但通常并非最小推理单元，因为单一步骤常同时包含多个操作：替换、定义展开、引入新事实、目标切换或分支剪枝。若将此类粗粒度步骤直接输入Lean流程，便会遇到第2节讨论的局部性不匹配。因此，我们将COT步骤视为标注单位，而非直接作为逻辑验证单位。为获得细粒度证明，我们首先要求语言模型对原始COT步骤进行预分解，在不改变证明逻辑的前提下移除冗余重复语句，以语义忠实方式获得详细COT。此处强调“忠实”而非“补丁”：原始证明中的结论、变量范围、案例讨论措辞、具体见证与数值计算均须原样保留。Lean证明状态记录特定时刻的可用假设与当前目标，策略将一个证明状态转化为另一个。基于预分解获得的细粒度子步骤，我们借鉴Lean证明状态的状态转换视角，要求语言模型根据自然语言步骤逐步写出证明过程中的所有证明状态与状态转换，构建证明状态树 \(\mathcal{T}=(V,E)\)。  
**证明状态树定义**。每个节点 \(v \in V\) 表示自然语言证明状态 \(S_v=(\Gamma_v, G_v)\)，其中 \(\Gamma_v\) 为当前可用的累积假设，\(G_v\) 为当前待证子目标。以图2中第一步为例，在状态0包含原问题条件和结论后，自然语言证明欲对 \(m\) 的奇偶性进行案例拆分。因此，状态0.0在父状态基础上添加分支假设“\(m\) 为奇数”并保持分支目标 \((n,m)=(1,1)\)；状态0.1添加分支假设“\(m\) 为偶数”并保持分支目标 \((n,m)=(3,2)\)。它们共同对应状态0在不同证明分支中的下一证明状态。每条边 \(e=(v \to v') \in E\) 表示类型为 \(\tau_e\) 的局部推理转换，如实例推导、重写、目标归约、案例拆分或引理引入。每条边记录为边单元 \(u_e\)，作为后续检查与形式验证的基本对象。前述例子中，对应边类型为案例拆分。图2：从证明步骤到证明状态树  
**递归构造**。构建证明状态树时，对于每个预分解子步骤，模型先识别其转换类型 \(\tau_e\)，再定位该子步骤发生的父状态 \(v\)。针对不同转换类型，我们编写了详细的状态转换手册，使LLM能准确生成子状态 \(S_{v'}=(\Gamma_{v'}, G_{v'})\)。例如，若子步骤引入新事实 \(h\)，则更新 \(\Gamma_{v'}=\Gamma_v \cup \{h\}\)；若改变当前目标，则更新 \(G_v\)；若产生多个分支，则生成具有特定条件的多个子节点。图2中的边1即为案例拆分示例：它将状态0拆分为状态0.0与状态0.1，分别对应 \(m\) 为奇数与偶数的情况。