Lean 融合理论计算机科学：形式-非形式配对中的可扩展定理证明挑战合成
计算机科学中的逻辑
2026-05-19 v2 人工智能
计算与语言
机器学习
摘要
形式化定理证明（FTP）已成为评估大语言模型推理能力的关键基础，使其能够大规模自动验证数学证明。然而，由于手动精细校订成本高昂以及缺乏具备验证形式-非形式对应关系的具有挑战性的问题，进展受到限制。我们提出利用理论计算机科学（TCS）作为严谨证明问题的可扩展来源，其中算法定义使我们能够自动生成任意数量具有挑战性的定理-证明对。我们在两个 TCS 领域进行了演示：一个是 Busy Beaver 问题，涉及证明图灵机停机行为的下界；另一个是混合布尔算术问题，组合逻辑与算术推理。我们的框架自动合成具有平行形式（Lean4）和非形式（Markdown）规格的问题，创建可扩展的用于生成经验证证明挑战的管道。在前沿模型上进行评估，揭示了自动化定理证明中的显著差距：尽管 DeepSeekProver-V2-671B 在 Busy Beaver 问题上实现了 57.5% 的成功率，但在混合布尔算术问题上仅为 12%。这些结果凸显了即使对于计算容易验证的问题，长形式证明生成也具有挑战性，表明 TCS 领域对于推动自动推理研究具有重要价值。
引用
@article{arxiv.2508.15878,
title = {Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs},
author = {Terry Jingchen Zhang and Wenyuan Jiang and Rongchuan Liu and Yisong Wang and Junran Yang and Ning Wang and Nicole Ni and Yinya Huang and Mrinmaya Sachan},
journal= {arXiv preprint arXiv:2508.15878},
year = {2026}
}
备注
Accepted to AI4MATH@ICML2025