苏黎世联邦理工发现：AI定理证明竟被理论计算机科学难题“打回原形”！——揭示大模型推理能力的致命短板

苏黎世联邦理工发现：AI定理证明竟被理论计算机科学难题“打回原形”！——揭示大模型推理能力的致命短板 Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs

引用格式: Terry Jingchen Zhang, Wenyuan Jiang, Rongchuan Liu, Yisong Wang, Junran Yang, Ning Wang, Nicole Ni, Yinya Huang, Mrinmaya Sachan. Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs. arXiv:2508.15878.

论文内容解析

这篇由苏黎世联邦理工学院（ETH Zurich）团队发表的论文，探讨了一个看似简单但极具挑战性的问题：如何有效评估大型语言模型（LLM）在数学定理证明方面的真实推理能力。传统上，研究人员使用人工整理的数学问题数据集来测试模型，但这种方法存在两个主要问题：一是数据集规模有限，二是容易被模型在训练时“见过”类似题目，导致测试结果失真。

核心创新：用理论计算机科学自动生成无限难题

论文提出了一个革命性的思路：利用理论计算机科学（TCS）中的经典问题，自动生成无限多的定理证明挑战。具体来说，他们选择了两个著名的TCS问题领域：

1. 1. Busy Beaver（忙碌海狸）问题 ：这是一个关于图灵机停机问题的变种。简单来说，就是找到一个给定状态数的图灵机，在空白纸带上运行最多步数后停机。这个问题在计算理论中是不可判定的，意味着没有通用算法能解决所有情况。论文通过参数化生成不同复杂度的Busy Beaver机器，从简单的64个机器（N=1）到极其复杂的42亿个机器（N=4），创造了可调节难度的证明挑战。

2. 2. 混合布尔算术（MBA）问题 ：这类问题结合了算术运算（加、减、乘）和位运算（与、或、异或等），常用于密码学和软件混淆技术。例如，一个简单的表达式x+y可以被重写为(x XOR y) + 2*(x AND y)，使得表面看起来复杂但数学等价。论文通过算法生成这样的等式，要求模型证明其等价性。

论文设计了一个三阶段的自动化框架：

• • 问题模块 ：定义可参数化的问题，如Busy Beaver的状态数或MBA的变量数。

• • 真值生成 ：使用算法方法确定正确答案。例如，对于Busy Beaver，通过模拟图灵机运行BB(N)+1步来判定是否停机。

• • 模板合成 ：使用专家设计的模板，同时生成形式化（Lean4）和非形式化（Markdown）的问题描述，确保语义严格对齐。这意味着每个问题都有精确的数学定义和自然语言解释，避免了人工标注的误差和成本。

论文测试了多个前沿模型，包括OpenAI的o3和o4-mini、DeepSeek-Prover系列等，结果令人震惊：

• • 在Busy Beaver问题上，最好的模型DeepSeek-Prover-v2-671B仅达到57.5%的成功率，而其他模型如OpenAI-o4-mini只有27.5%。

• • 在MBA问题上，性能更差：DeepSeek-Prover-v2-671B仅管理12%的成功率，而许多模型（如DeepSeek-R1）完全失败（0%）。

• • 关键发现：模型在单个推理步骤上表现近乎完美（98.88%准确率），但在组合这些步骤成完整证明时却崩溃。这暴露了模型在全局策略规划上的根本缺陷——它们擅长“局部推理”但缺乏“整体证明构建”能力。

论文深入分析了模型的错误类型：

• • 幻觉（67.27%） ：模型使用不存在的定理或战术，如试图用“归纳法”证明无关问题。

• • 战术误用（23.22%） ：过度依赖自动化战术（如aesop或bv_decide），而不理解其适用条件，导致搜索失败。

• • 自愿放弃（4.88%） ：模型直接输出“sorry”（Lean中表示放弃的标记），显示指令遵循失败。

• • 类型不匹配（4.47%） ：由于Lean的类型系统，模型生成表达式类型错误。

这些错误表明，当前模型更像是在“语法层面”操纵符号，而非真正理解数学推理。例如，一个模型在MBA证明中堆砌了多个引理却盲目调用ring战术，最终失败，反映出对战术适用性的无知。

实际影响与未来方向

这项研究不仅揭示了LLM在定理证明中的局限性，还提出了一个可扩展、抗污染的评估框架。通过TCS问题的算法生成，研究人员可以创建无限的新挑战，避免数据集污染问题。论文呼吁社区进一步探索理论计算机科学与形式化证明的结合，以推动自动化推理的发展。

评分

9/10分

这篇论文质量极高，具有以下优点：

• • 创新性 ：首次将理论计算机科学问题系统用于定理证明评估，解决了数据集稀缺和污染问题。

• • 严谨性 ：通过自动化管道生成形式化-非形式化对，确保数学精确性，且实验设计详细（如步骤级分解）。

• • 实用性 ：结果揭示了当前模型的根本缺陷，为未来研究提供了明确方向。

• • 可重复性 ：代码和框架开源，便于社区使用和扩展。

唯一的小缺点是实验部分稍显技术化，可能对非专业读者理解造成一定障碍，但整体不影响其突出贡献。