用于自动证明验证的伪形式化

arXiv:2605.20531v3 公告类型：replace-cross 摘要：可靠地验证证明仍然是训练和评估 AI 系统进行高难度数学推理的瓶颈。使用 Lean 等语言编写的完全形式化证明易于验证，因为它们具有明确无歧义且模块化的特点。大多数证明，尤其是由 AI 系统编写的证明，都不具备这两种特性；而在许多前沿数学场景中，将它们转换为形式化语言仍然颇具挑战。我们提出伪形式化（Pseudo-Formalization，PF），这是一种证明格式，既能保留形式化证明的模块化和精确性，又具备自然语言的灵活性。伪形式化证明被分解为相互独立的模块，每个模块都用自然语言陈述其前提、结论和证明。为了验证普通自然语言证明的正确性，LLM 将其转换为伪形式化证明，然后独立验证每个模块；我们将这一算法称为区块验证（Block Verification，BV）。我们在涵盖奥林匹克数学和研究级数学的两个基准上评估了 PF+BV；在错误发现的精确率和召回率方面，它均帕累托支配了 LLM-as-judge 基线。为支持未来研究，我们发布了研究级证明验证基准 ArxivMathGradingBench。