StepProof：自然语言数学证明的逐步验证
计算机科学中的逻辑
2025-07-01 v2 人工智能
摘要
交互式定理证明器（ITP）是对数学证明进行自底向上形式化验证的强大工具，但其缺乏自然语言接口仍是显著的局限。近期大型语言模型（LLM）的进步增强了对自然语言输入的理解，为自动化形式化——即将自然语言证明翻译为可被验证的形式证明——提供了可能。尽管如此，现有自动化形式化方法仅限于验证完整证明，缺乏对更细粒度、句子级验证的能力。为填补这一空白，我们提出StepProof，一种专为粒粒级验证设计的新型自动化形式化方法。StepProof将完整证明拆分为多个可验证子证明，实现句子级验证。实验结果表明，StepProof在证明成功率和效率上显著优于传统方法。此外，我们发现，对自然语言证明进行少量手动调整以适应逐级验证，可进一步提升StepProof在自动化形式化中的性能。
引用
@article{arxiv.2506.10558,
title = {StepProof: Step-by-step verification of natural language mathematical proofs},
author = {Xiaolin Hu and Qinghua Zhou and Bogdan Grechuk and Ivan Y. Tyukin},
journal= {arXiv preprint arXiv:2506.10558},
year = {2025}
}