让大模型逐句验证数学证明，提升自动形式化准确率。
StepProof: Step-by-step verification of natural language mathematical proofs
- 将完整证明拆解为可验证子步骤，实现逐句检查。
- 实验显示成功率和效率显著优于传统方法。
- 微调自然语言表述可进一步提升验证效果。
交互式定理证明器（ITPs）能将数学证明严格验证至公理层级，但缺乏自然语言接口是其主要局限。近年来大语言模型（LLMs）提升了对自然语言的理解能力，推动了自动形式化——将自然语言证明转化为可验证的正式证明。然而现有方法仅支持完整证明的验证，无法进行细粒度的句子级验证。为此，我们提出 StepProof，一种面向细粒度、分步验证的新型自动形式化方法。StepProof 将完整证明分解为多个可验证的子证明，实现句子级别的验证。实验结果表明，与传统方法相比，StepProof 显著提升了证明成功率与验证效率。此外，我们发现对自然语言证明进行微调以适配步骤级验证，能进一步增强 StepProof 的自动形式化性能。
原文摘要 · Abstract (English)
Interactive theorem provers (ITPs) are powerful tools for the formal verification of mathematical proofs down to the axiom level. However, their lack of a natural language interface remains a significant limitation. Recent advancements in large language models (LLMs) have enhanced the understanding of natural language inputs, paving the way for autoformalization - the process of translating natural language proofs into formal proofs that can be verified. Despite these advancements, existing autoformalization approaches are limited to verifying complete proofs and lack the capability for finer, sentence-level verification. To address this gap, we propose StepProof, a novel autoformalization method designed for granular, step-by-step verification. StepProof breaks down complete proofs into multiple verifiable subproofs, enabling sentence-level verification. Experimental results demonstrate that StepProof significantly improves proof success rates and efficiency compared to traditional methods. Additionally, we found that minor manual adjustments to the natural language proofs, tailoring them for step-level verification, further enhanced StepProof's performance in autoformalization.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。