用伪形式化让AI证明可验证，提升数学推理可信度
Pseudo-Formalization for Automatic Proof Verification
- 将自然语言证明拆成自包含模块，每块含前提、结论和证明
- 在奥数与前沿数学题上，错误检测的精准率与召回率均超越纯LLM判断
- 适合需要可靠数学证明验证的研究者与AI系统开发者
可靠的证明验证仍是训练和评估人工智能系统在高难度数学推理任务上的瓶颈。完全形式化的证明（如使用Lean语言）因无歧义且模块化而易于验证，但大多数证明，尤其是由AI生成的，缺乏这些特性，且在前沿数学场景中难以转化为形式语言。我们提出伪形式化（Pseudo-Formalization, PF），一种兼具形式化证明的模块化与精确性，同时保留自然语言灵活性的证明格式。伪形式化证明被分解为自包含模块，每个模块以自然语言陈述其前提、结论和证明过程。为验证普通自然语言证明的正确性，我们利用大模型将其转换为伪形式化表示，并独立验证每个模块，该算法称为块验证（Block Verification, BV）。我们在涵盖奥数与研究级数学的两个基准上评估了PF+BV，结果表明其在错误发现的精度与召回率上均对齐或优于基于大模型的评判基线。为支持后续研究，我们发布了研究级数学证明验证基准ArxivMathGradingBench。
原文摘要 · Abstract (English)
Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most proofs, particularly those written by AI systems, have neither property, and translating them into formal languages remains challenging in many frontier math settings. We propose Pseudo-Formalization (PF), a proof format that captures the modularity and precision of formal proofs while retaining the flexibility of natural language. A Pseudo-Formal proof is decomposed into self-contained modules, each stating its premises, conclusion, and proof in natural language. To verify the correctness of a regular natural language proof, an LLM translates it to Pseudo-Formal and then verifies each module independently, an algorithm we call Block Verification (BV). We evaluate PF+BV on two benchmarks spanning olympiad and research-level mathematics, where it pareto-dominates LLM-as-judge baselines on error-finding precision and recall. To support future work, we release our research-level proof verification benchmark ArxivMathGradingBench.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。