技术摘要：用于自然语言数学推理的风险控制型 Lean-as-Judge

1. 问题陈述

本文探讨了利用形式化证明助手（特别是 Lean）作为大型语言模型（LLM）生成的自然语言数学推理的评判者所面临的挑战。虽然成功的 Lean 证明为形式化陈述提供了强有力的正面证据，但缺乏证明则是一个模棱两可的信号。证明失败可能表明数学答案不正确，但也可能源于形式化类型错误、缺失库事实或证明搜索超时。

现有方法常将证明失败视为负面正确性信号，从而冒着将数学错误与形式化覆盖不足相混淆的风险。作者识别出一种“覆盖悬崖”现象：形式化选择的可信度高度依赖于能够成功形式化并证明的候选答案比例。当覆盖率高时，形式化选择非常准确；当覆盖率低时，该信号变得不可靠。

核心问题在于确定下游系统应何时信任形式化 Lean 信号，以及何时将该信号视为超出覆盖范围（即未解决）而非错误，同时为被接受的答案提供有限样本风险保证。

2. 方法论：COVCAL

作者提出了COVCAL（Coverage-Calibrated Lean，覆盖校准型 Lean），这是一种基于覆盖诊断来决定是否接受形式化答案或放弃的风险控制型选择包装器。

2.1 部分观测框架

该系统将形式化流程视为一种部分观测机制。它并不观测每个候选答案的真伪，而仅观测：

1. 哪些归一化答案类达到了良构的 Lean 陈述（类型覆盖）。
2. 其中哪些类成功获得了证明（证明覆盖）。
3. 最高权重的已证明类与最高权重的未解决竞争对手之间的权重差（形式化边距）。

答案类被定义为一组表示相同最终答案的候选字符串（例如 $1/2$、$0.5$、$2/4$）。未形式化或未证明的类被视为未解决，而非自动错误。

2.2 覆盖诊断

COVCAL 针对给定问题 $x$ 计算四个关键指标：

• 类型覆盖 ($C_{typ}$)：达到良构 Lean 陈述（状态为 proved、typechecked 或 timeout）的候选类的总权重。
• 证明覆盖 ($C_{prf}$)：获得内核检查证明的候选类的总权重。
• 未解决竞争对手质量 ($R_{unres}$)：未获得证明的最高权重答案类的权重。
• 形式化边距 ($M$)：最高权重已证明类的权重与未解决竞争对手质量之间的差值。

2.3 选择与认证

COVCAL 仅在满足基于阈值 $(\tau_{typ}, \tau_{prf}, \tau_M)$ 的预声明规则时，才接受最高权重的已证明类。如果规则未满足，系统将放弃（或回退到非形式化方法，如自一致性）。

为确保可靠性，COVCAL 采用有限样本选择风险认证。它保证以 $1-\delta$ 的概率，被接受答案的选择风险（错误率）不超过 $\epsilon$。提出了两种认证机制：

1. Bonferroni 机制：在校准集上搜索阈值网格，并应用并集界校正（$\delta/|T|$）以应对多重比较。这种方法较为保守，需要高密度的信号才可行。
2. Dev-then-Cal 机制：在独立开发集上选择阈值，并在校准集上使用单个 Clopper-Pearson 界（$\delta$）进行一次认证。这种方法样本效率更高，但要求开发数据与校准数据严格分离。

2.4 理论极限

本文证明，如果没有覆盖诊断（即仅依赖证明的存在性），若存在未解决的、不等价的竞争对手类，则无法推导出任何非平凡的单点正确性证书。缺失形式化证据并非数学谬误的证据，而是未解决状态的证据。

3. 主要贡献

1. 覆盖悬崖特征化：在 MATH-500 数据集上，作者证明，在高证明覆盖率下，“证明获胜”的答案有 96% 是正确的，而在低覆盖率下仅为 20%。这确立了 Lean 证明仅在覆盖率和边距较高时才可靠。
2. 信号稀疏性与忠实度：形式化信号是稀疏且不完善的。一个 7B 自动形式化器仅为 28% 的问题证明了一个类。此外，人工审计显示，这些证明中仅约 43% 忠实于原始问题（其余为平凡恒等式或真实但无关的陈述）。
3. COVCAL 方法：一种在部分观测下认证风险的选择性预测框架。它明确处理了证明失败的不对称性，并为被接受的预测提供了有限样本保证。
4. 形式化器依赖的可行性：本文证明，证书可行性受自动形式化覆盖率的支配。7B 形式化器产生的信号过于稀疏，无法满足保守的 Bonferroni 机制（拒绝了所有 20 个自举分区），而证明专用形式化器（Goedel-Prover-V2-8B）实现了 79% 的覆盖率，使得该方法在 17/20 个分区上可行。

4. 实验结果

实验在 MATH-500 的过滤子集（378 个示例）上进行，使用 Qwen2.5-Math-7B 进行生成，并使用各种形式化器进行自动形式化。

• 基线性能：仅使用自一致性在不放弃的情况下达到 91% 的准确率。
• COVCAL 性能：
  • 在使用 7B 形式化器的Bonferroni 机制下，由于信号过于稀疏无法满足严格的并集界，该方法拒绝了所有输入（0/20 个分区）。
  • 在使用 7B 形式化器的Dev-then-Cal 机制下，12/20 个分区获得认证。被接受的比例约为 21%，被接受答案为 0.93 的准确率。
  • 使用 Goedel-Prover-V2-8B（专用形式化器）时，证明覆盖率上升至 79%。Bonferroni 机制在 17/20 个分区上变得可行，接受约 48% 的问题，被接受答案的准确率为 0.98。
• 忠实度审计：对 45 个分层示例的人工审计显示，虽然 73.6% 的已证明陈述是非平凡且正确的，但只有 43% 忠实于问题陈述。许多“已证明”的陈述是真实的侧面事实或平凡恒等式，未能捕捉问题的约束条件。

5. 意义与主张

本文主张，其主要贡献在于精确阐述了在风险控制下，何时以及使用何种形式化器可以信任部分形式化信号，而非单纯提高原始准确率。

• 风险控制优于原始准确率：由于自一致性本身已达到 91% 的准确率，COVCAL 的价值在于为其接受的答案子集提供证书，区分“已验证”与“未解决”，而非区分“正确”与“错误”。
• 处理部分观测：该工作将形式化验证重新框架化为一种选择性预测问题，其中缺失的证明被视为未解决的候选项，从而防止因形式化失败而将正确的推理错误标记为错误。
• 对专业化的依赖：结果表明，原始模型规模不能替代专业化。证明专用形式化器在证明覆盖率方面显著优于更大的通用模型，而覆盖率是可认证风险控制的关键约束。

作者总结道，COVCAL 充当了使用 Lean 作为评判者的保守接口：仅当自动形式化器覆盖了足够多的答案质量以支持风险证书时，它才是可行且信息丰富的，但它并不保证所有答案都经过验证。