🤖 machine learning

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

该论文提出了一种名为“编译即压缩”的框架，通过利用编译器将多样化证明尝试映射为紧凑结构化失败模式的特性，结合基于显式验证器反馈的局部修正树搜索，在显著降低测试时计算成本的同时，有效提升了不同规模大语言模型在形式化定理证明中的性能，并在 PutnamBench 基准测试中取得了优于同类模型的成果。

原作者： Guchan Li, Rui Tian, Hongning Wang

发布于 2026-04-22

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Guchan Li, Rui Tian, Hongning Wang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇文章介绍了一种让 AI 数学证明助手变得更聪明、更高效的新方法。我们可以把它想象成教一个刚学编程的学生如何“从错误中学习”，而不是让他每次都从头开始重做。

以下是用通俗易懂的语言和生动的比喻对这篇论文核心内容的解读：

1. 核心问题：AI 证明数学题太“烧脑”了

现在的 AI（大语言模型）在解数学证明题时，虽然很厉害，但有个大毛病：太费资源。

现状：为了证明一个定理，AI 往往需要尝试成千上万次（就像一个人为了打开一把锁，试了 1000 把钥匙都不对，它不会总结规律，而是继续盲目试第 1001 把）。
后果：这需要巨大的计算量，就像为了做一道菜，把整个厨房都拆了重装一样，成本太高，速度太慢。

2. 核心洞察：编译器是“超级压缩师”

论文发现了一个有趣的现象：编译器（检查代码错误的工具）其实是个“信息压缩大师”。

比喻：想象一下，学生写了一万种不同的错误代码（输入空间巨大），但编译器给出的错误提示（输出空间）却非常少，只有几十种固定的“错误类型”。
- 比如，不管你是少写了一个分号，还是变量名拼错了，编译器可能都只报“找不到标识符”。
- 不管你是逻辑错了还是公式错了，编译器可能都报“目标未解决”。
启示：这意味着，虽然错误的代码千奇百怪，但导致错误的“原因”却是有规律的。AI 不需要记住每一句错误的代码，只需要学会如何修复这几十种“错误类型”即可。

3. 解决方案：编译即压缩（Compile to Compress）

作者提出了一种**“学习修正”（Learning-to-Refine）**的新框架。

比喻：从“盲目试错”到“对症下药”

以前的做法（直接生成）：
就像让一个厨师每次做菜失败后，把整道菜倒掉，重新买食材、重新切菜、重新炒一遍。这非常浪费，而且如果第一次切菜手法不对，后面怎么炒都没用。
现在的做法（修正框架）：
当菜炒糊了（代码报错），厨师（AI）会看厨师长（编译器）给的提示：“火太大了”或者“盐放多了”。
- 厨师不需要重头开始，而是直接针对“火太大”这个错误进行微调（把火关小）。
- 如果下次又“盐放多了”，厨师就能立刻反应过来：“哦，又是这个老毛病，下次少放点盐”。
- 关键点：AI 学会了根据编译器的“错误报告”来局部修补代码，而不是每次都重写整个证明过程。

4. 具体怎么做？（三个步骤）

冷启动（收集错题本）：
先让 AI 试着做题，收集它做错的题目和编译器给出的错误提示。然后，用更聪明的 AI（如 Claude）来写“解题思路”，告诉它：“看到这个错误，你应该这样改”。这就形成了一本**“错题修正手册”**。
专家迭代（反复练习）：
让 AI 拿着这本手册不断练习。它做错了 -> 看手册 -> 修正 -> 再试。在这个过程中，AI 不仅学会了怎么解题，更学会了怎么根据错误提示快速修 bug。
智能搜索（价值引导）：
在考试（测试）时，AI 面临两个选择：
- A. 重新想一个新的证明（广度搜索）。
- B. 修改刚才那个失败的证明（深度搜索）。
- 作者训练了一个“小助手”（价值函数），它能判断：“这个错误看起来很有希望修好，还是直接放弃重开比较好？”
- 比喻：就像探险家，如果前面的路只是被一棵树挡住了（小错误），就砍树继续走；如果前面是悬崖（大错误），就立刻换条路走。这样能最快地找到宝藏（正确答案）。

5. 成果如何？

效果显著：在著名的数学竞赛（如 Putnam）测试中，这种方法让中等规模的 AI 模型表现达到了世界顶尖水平，甚至超过了那些需要巨大算力的超级模型。
省钱省力：它不需要 AI 记住长长的历史对话，也不需要巨大的计算资源，就能把解题能力翻倍。

总结

这篇论文的核心思想就是：不要试图让 AI 记住所有正确的答案，而是让它学会如何根据“错误报告”快速修正错误。

就像教孩子骑自行车，与其让他摔倒了就换一辆新车重新骑，不如教他：“刚才摔倒是因为车把歪了，下次扶正一点就行”。通过这种**“编译即压缩”**的智慧，AI 证明定理变得更加高效、聪明且经济。

论文技术总结：Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

1. 研究背景与问题 (Problem)

形式化定理证明（Formal Theorem Proving）是人工智能推理领域的核心挑战之一。近年来，大型语言模型（LLM）在该领域展现出巨大潜力，但现有的最先进方法（SOTA）通常面临严重的可扩展性瓶颈：

计算成本高昂：为了获得高性能，现有方法往往依赖大规模的测试时计算（Test-time Compute），例如通过大量的推理 rollout（多轮尝试）或极长的上下文窗口来累积历史证明尝试。
反馈利用不足：现有的编译器反馈（Compiler Feedback）通常被简化为二元的成功/失败信号，或者仅作为纯文本的错误信息。这忽略了编译器输出中蕴含的丰富结构化信息。
上下文膨胀：依赖多轮自我修正（Self-correction）会导致模型必须处理不断增长的交互历史，导致上下文窗口迅速膨胀，限制了在固定计算预算下的探索深度。

核心洞察：作者观察到，尽管 Lean 证明程序的输入空间是组合爆炸且无限的，但编译器（Compiler）将这些多样化的证明尝试映射到了一个紧凑的、结构化的失败模式集合中。即，许多语法不同但语义错误的证明会触发相同的编译器错误信息。

2. 方法论 (Methodology)

论文提出了一种名为**“编译即压缩”（Compile to Compress）的学习 - 细化（Learning-to-Refine）**框架，旨在利用编译器输出的结构化特性来高效地引导证明搜索。

2.1 核心概念：维度压缩与失败模式驱动

编译器作为维度压缩器：编译器将高维的 Lean 程序空间投影到低维的编译器消息空间。不同的错误程序往往对应相同的错误签名（Error Signatures）。
失败模式驱动的细化（Failure-Mode Driven Refinement）：模型学习基于编译器错误类型（而非具体的程序语法）进行修正。这意味着模型可以将从一个错误模式中学到的修正策略泛化到其他具有相同错误结构的证明尝试中。
分布链（Chain of Distributions, CoD）：
- 传统的直接生成是从单一固定分布 $D_{direct}$ 中采样。
- 细化过程则形成了一条条件分布链 $\{D_{refine}(\cdot | c_i, \Phi(c_i), p)\}$ 。每一步修正都基于当前的失败状态（程序 $c_i$ + 错误信息 $\Phi(c_i)$ + 问题 $p$ ），动态调整采样分布，从而能够探索那些初始分布中概率极低（Out-of-Distribution, OOD）的正确解区域。

2.2 技术实现流程

冷启动数据合成（Cold-Start Data Synthesis）：
- 利用强大的 LLM（如 Claude-3.7-Sonnet）分析初始证明失败时的编译器错误，生成详细的“思考（Thought）”轨迹，解释如何从错误代码修正到正确代码。
- 构建包含“问题 + 错误代码（嵌入编译器消息）+ 思考过程 + 修正后代码”的训练数据。
- 通过监督微调（SFT）让基础证明器学会自我修正。
专家迭代（Expert Iteration）：
- 在 SFT 基础上，让模型在训练集上进行多轮自我修正，直到找到正确解或预算耗尽。
- 将成功的修正轨迹转化为新的监督信号，进行迭代训练。这使得模型能够适应自身在修正过程中产生的新的错误分布。
测试时搜索策略（Test-Time Search Strategy）：
- 马尔可夫过程：每一步细化仅依赖当前状态，无需维护长历史，大幅降低上下文长度。
- 树搜索：将证明过程建模为树搜索。
  - 直接生成对应广度优先搜索（BFS）。
  - 细化旧尝试对应深度优先搜索（DFS）。
- 价值引导（Value-Guided Search）：训练一个神经价值模型（Value Function），评估当前节点（证明状态）的潜在成功概率。
  - 利用成对偏好学习（Pairwise Preference Learning）训练价值模型：成功路径上的状态优于失败路径，且更接近最终解的状态优于早期状态。
  - 在搜索时，根据价值模型的预测概率进行 Softmax 采样，优先探索高潜力的分支。

3. 关键贡献 (Key Contributions)

理论视角创新：首次将编译器视为形式化证明搜索空间的“维度压缩器”，揭示了编译器错误消息作为结构化反馈在指导 LLM 推理中的核心作用。
提出 Learning-to-Refine 框架：设计了一套完整的从数据合成、SFT 到专家迭代的训练流程，将复杂的推理能力蒸馏为通用的“生成 + 修正”策略。
引入分布链（CoD）机制：证明了基于反馈的迭代修正能够动态改变采样分布，有效跳出局部最优，探索 OOD 的正确解，解决了传统方法依赖长上下文和大量 rollouts 的问题。
价值引导的搜索策略：结合神经价值模型，实现了在直接生成和迭代细化之间的自适应平衡，显著提高了搜索效率。

4. 实验结果 (Results)

论文在多个基准测试（MiniF2F, ProofNet, MathOlympiadBench, PutnamBench）上进行了广泛评估，使用了 Kimina-8B 和 Goedel-32B 作为基座模型。

性能提升：
- 在 PutnamBench（高难度数学竞赛题）上，该方法在同等计算预算下取得了SOTA 性能。
- Goedel-32B 版本解决了 110 个问题，超越了所有同规模（~32B）的现有方法（包括 Ax-Prover 和原始 Goedel-V2）。
- Kimina-8B 版本解决了 25 个问题，在 ~8B 参数规模模型中排名第一。
- 相比基线模型，在 ProofNet 和 PutnamBench 上实现了超过 50% 的相对提升。
效率与可扩展性：
- 在固定测试时预算（如 256 次采样）下，表现优于依赖更大模型或更长推理时间的系统。
- 消融实验表明，性能提升主要源于“细化（Refinement）”机制本身，而非仅仅是更多的训练数据。
分布分析：
- 通过统计检验（Energy Distance Test）证实，细化过程产生的程序分布与直接生成分布显著不同，验证了 CoD 假设。
- 可视化显示，细化过程能够引导模型离开初始的密集簇，探索新的程序空间区域。

5. 意义与影响 (Significance)

范式转变：提出了一种无需依赖海量计算资源即可提升定理证明能力的可扩展范式。通过“压缩”错误空间，将昂贵的试错过程转化为高效的针对性修正。
通用性：该框架与模型无关（Model-Agnostic），可应用于不同规模的 LLM，且随着模型参数和计算预算的增加，性能呈现一致的提升趋势。
未来方向：为下一代“验证器引导（Verifier-Guided）”的推理系统奠定了基础。虽然目前主要针对符号定理证明，但其利用结构化反馈进行分布调整的思想，对处理具有弱反馈或噪声反馈的复杂推理任务具有启发意义。

总结：这篇论文通过深入挖掘编译器输出的结构化信息，提出了一种高效、可扩展的定理证明增强框架。它证明了通过“学习如何修正”而非单纯“学习如何生成”，可以显著突破现有 LLM 在形式化推理中的性能瓶颈，为构建更智能、更高效的数学推理系统提供了新的技术路径。