Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs

📄 arXiv: 2508.15878v1 📥 PDF

作者: Terry Jingchen Zhang, Wenyuan Jiang, Rongchuan Liu, Yisong Wang, Junran Yang, Ning Wang, Nicole Ni, Yinya Huang, Mrinmaya Sachan

分类: cs.LO, cs.AI, cs.CL, cs.LG

发布日期: 2025-08-21

备注: Accepted to AI4MATH@ICML2025

💡 一句话要点

利用理论计算机科学，可扩展地合成形式化定理证明挑战

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化定理证明 理论计算机科学 自动推理 数据集生成 Lean4

📋 核心要点

  1. 现有形式化定理证明数据集规模有限，阻碍了大型语言模型推理能力的有效评估。
  2. 利用理论计算机科学的算法定义，自动生成具有形式化和非形式化对应关系的定理-证明对。
  3. 在忙碌的海狸和混合布尔算术问题上验证，揭示了现有模型在长篇证明生成方面的不足。

📝 摘要（中文）

形式化定理证明（FTP）已成为评估大型语言模型推理能力的关键基础，能够大规模地自动验证数学证明。然而，由于人工标注的高成本以及经过验证的形式化-非形式化对应关系的挑战性问题的稀缺，进展受到了数据集的限制。我们提出利用理论计算机科学（TCS）作为严格证明问题的可扩展来源，其中算法定义能够自动生成任意数量的挑战性定理-证明对。我们在两个TCS领域展示了这种方法：忙碌的海狸问题（涉及证明图灵机停止行为的界限）和混合布尔算术问题（结合逻辑和算术推理）。我们的框架自动合成具有并行形式化（Lean4）和非形式化（Markdown）规范的问题，从而创建了一个可扩展的管道来生成经过验证的证明挑战。对前沿模型的评估揭示了自动定理证明方面的巨大差距：虽然DeepSeekProver-V2-671B在忙碌的海狸问题上取得了57.5％的成功率，但在混合布尔算术问题上仅取得了12％的成功率。这些结果突显了即使对于计算上易于验证的问题，长篇证明生成的难度，证明了TCS领域对于推进自动推理研究的价值。

🔬 方法详解

问题定义：论文旨在解决形式化定理证明领域中，高质量、大规模数据集匮乏的问题。现有方法依赖于人工标注，成本高昂且难以覆盖足够多的挑战性问题，限制了大型语言模型在定理证明方面的能力提升。

核心思路：论文的核心思路是利用理论计算机科学（TCS）中的问题作为定理证明的来源。TCS问题通常具有明确的算法定义，可以自动生成大量的定理-证明对，并且可以方便地进行形式化验证。通过将TCS问题转化为形式化定理证明的挑战，可以有效地扩展数据集，并为评估和训练大型语言模型的推理能力提供更丰富的资源。

技术框架：该框架包含以下几个主要步骤：1) 选择合适的TCS领域，例如忙碌的海狸问题和混合布尔算术问题；2) 基于TCS问题的算法定义，自动生成定理和证明；3) 将定理和证明分别转化为形式化（Lean4）和非形式化（Markdown）的表示；4) 使用形式化验证工具验证生成的定理-证明对的正确性。整个流程构成一个可扩展的流水线，可以源源不断地生成高质量的定理证明挑战。

关键创新：该论文最重要的技术创新在于将理论计算机科学与形式化定理证明相结合，提出了一种自动生成大规模、高质量定理证明数据集的方法。与传统的人工标注方法相比，该方法具有更高的效率和可扩展性，并且可以生成更具挑战性的问题。

关键设计：论文的关键设计包括：1) 选择具有代表性的TCS问题，例如忙碌的海狸问题和混合布尔算术问题，以覆盖不同类型的推理能力；2) 设计自动化的定理和证明生成算法，确保生成的问题具有一定的难度和复杂性；3) 使用Lean4作为形式化语言，并提供相应的工具将非形式化证明转化为Lean4代码；4) 采用严格的形式化验证流程，确保生成的数据集的正确性和可靠性。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

实验结果表明，即使是目前最先进的模型DeepSeekProver-V2-671B，在混合布尔算术问题上的成功率也仅为12%，远低于在忙碌的海狸问题上的57.5%。这表明即使对于计算上易于验证的问题，长篇证明生成仍然是一个巨大的挑战，突显了该研究提出的数据集的价值。

🎯 应用场景

该研究成果可应用于自动定理证明、程序验证、人工智能安全等领域。通过提供大规模、高质量的定理证明数据集，可以促进大型语言模型在数学推理和逻辑推理方面的能力提升，并为开发更可靠、更安全的AI系统奠定基础。未来，该方法可以扩展到更多的TCS领域，生成更丰富的定理证明挑战。

📄 摘要（原文）

Formal theorem proving (FTP) has emerged as a critical foundation for evaluating the reasoning capabilities of large language models, enabling automated verification of mathematical proofs at scale. However, progress has been constrained by limited datasets due to the high cost of manual curation and the scarcity of challenging problems with verified formal-informal correspondences. We propose leveraging theoretical computer science (TCS) as a scalable source of rigorous proof problems, where algorithmic definitions enable automated generation of arbitrarily many challenging theorem-proof pairs. We demonstrate this approach on two TCS domains: Busy Beaver problems, which involve proving bounds on Turing machine halting behavior, and Mixed Boolean Arithmetic problems, which combine logical and arithmetic reasoning. Our framework automatically synthesizes problems with parallel formal (Lean4) and informal (Markdown) specifications, creating a scalable pipeline for generating verified proof challenges. Evaluation on frontier models reveals substantial gaps in automated theorem proving: while DeepSeekProver-V2-671B achieves 57.5\% success on Busy Beaver problems, it manages only 12\% on Mixed Boolean Arithmetic problems. These results highlight the difficulty of long-form proof generation even for problems that are computationally easy to verify, demonstrating the value of TCS domains for advancing automated reasoning research.