🤖 machine learning

OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

本文提出了 OptProver，通过专家迭代数据策展和一种结合困惑度加权与惩罚无效步骤的偏好学习目标，实现了从奥数领域向本科优化数学领域的有效持续训练与领域迁移，并在新构建的 Lean 4 优化基准测试中达到了最先进的性能。

原作者： Chenyi Li, Yanchen Nie, Zhengyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

发布于 2026-04-28

📖 1 分钟阅读☕ 轻松阅读

原作者： Chenyi Li, Yanchen Nie, Zhengyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

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

这是一篇关于人工智能（AI）如何学习“严谨数学”的前沿论文。为了让你轻松理解，我们可以把这个过程想象成**“一个天才奥数选手转行学习大学专业课”**的故事。

1. 背景：天才选手的“职业瓶颈”

想象一下，现在的 AI（比如 GPT 系列）就像是一个**“奥数天才”**。它非常擅长解各种奇奇怪怪、脑筋急转弯式的数学竞赛题（这就是论文里说的 Olympiad-level）。

但是，这个天才有一个致命弱点：他说话虽然好听，但不够严谨。 他能写出看起来很完美的解题步骤，但有时候会“幻觉”出一个不存在的公式，或者在逻辑的微小细节上出错。在数学界，这叫“自然语言证明”；而真正的数学家需要的是“机器可验证的证明”（Formal Theorem Proving），也就是每一步都必须像计算机程序一样，严丝合缝，错一点都不行。

现在，我们想让这个“奥数天才”去学**“最优化理论”**（Optimization）——这是机器学习、工程学和科学计算的基石。这就像是让一个只会做奥数题的孩子，突然去读大学的工程专业。

2. 遇到的困难：跨专业的“水土不服”

当这个天才试图学习“最优化”时，他遇到了两个大麻烦：

“方言”不通（分布偏移）： 奥数题讲究的是“奇招”和“技巧”；而最优化理论讲究的是“定义”和“严谨的逻辑链条”（比如凸性、梯度、收敛性）。这就像是一个只会说“粤语”的天才，突然要去读“德语”专业的书，他发现以前的套路全都不灵了。
“无效努力”陷阱（无效策略）： 这是最难的一点。天才可能会学到一些“看起来很像专业数学”的动作，但这些动作是**“无效动作”**。比如，他可能在证明一个复杂的公式时，做了一个虽然语法正确、但会让问题变得更复杂、甚至走入死胡同的步骤。这就像是在解迷宫，他虽然一直在走，但一直在原地打转，浪费了大量的脑力（计算资源）。

3. 解决方案：OptProver 的“魔鬼训练法”

为了让这个天才真正变成“最优化专家”，研究人员设计了一套名为 OptProver 的训练方案。我们可以把它看作一套**“特训营”**：

第一阶段：自我进化（Expert Iteration）

我们不只是把课本塞给他，而是让他**“边做边学”**。我们给他大量的数学题目，让他自己去尝试证明。如果他成功了，我们就把这段成功的路径记录下来，让他反复背诵、内化。这就像是让学生通过大量的刷题和自我总结，把书本知识变成自己的肌肉记忆。

第二阶段：纠正“无效动作”（Utility-Aware Preference Optimization）

这是本论文最聪明的地方。传统的训练只是告诉 AI“这道题做对了”或“做错了”。但 OptProver 的训练法更进了一步，它会给 AI 的动作打分：

满分动作： 既正确，又能直接通向答案。
零分动作： 语法错误，直接报错。
“坑人”动作（重点惩罚）： 语法完全正确，看起来很专业，但其实是在**“绕圈子”或者“把简单问题复杂化”**。
通过这种方式，AI 学会了不仅要“做对”，还要“高效地做对”，避免在解题时走弯路。

第三阶段：稳住基本功（Perplexity-Weighted DPO）

在学新专业时，天才很容易“学了新知识，忘了旧本事”（这叫灾难性遗忘）。研究人员引入了一种“权重机制”，当 AI 遇到那些它完全看不懂、极其陌生的新知识时，我们会调低这些知识对它大脑的冲击力，防止它因为过度震惊而把以前的奥数逻辑给搞乱了。

4. 最终成果：全能型专家

经过这套魔鬼训练，OptProver 表现得非常出色：

专业课满分： 在专门设计的“最优化测试卷”（OptBench）上，它的表现远超其他同级别的 AI 模型，能解决超过 55% 的难题。
基本功没丢： 它不仅学会了最优化，在以前擅长的奥数题和普通的大学数学题上，表现依然稳健，甚至还有所进步。
逻辑更丝滑： 它不再像以前那样只会“暴力拆解”题目，而是学会了利用现有的数学工具库（Mathlib）进行优雅、简洁的证明。

总结

OptProver 的意义在于： 它证明了我们可以通过一套科学的“特训方案”，让一个擅长“技巧性数学”的 AI，平滑且高效地转型为一名擅长“严谨专业数学”的专家，同时还能保持其原有的聪明才智。这为 AI 学习更深奥、更专业的科学知识开辟了一条成功的道路。

这是一篇关于形式化定理证明（Formal Theorem Proving）领域的研究论文，题为《OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving》。以下是对该论文的详细技术总结：

1. 问题背景与挑战 (Problem)

目前的神经定理证明器（Neural Theorem Provers）主要集中在**奥林匹克数学（Olympiad-level mathematics）领域，但在优化理论（Optimization）**这一本科及研究生阶段的核心数学领域表现不足。

将模型从奥林匹克数学迁移到优化领域面临两个核心挑战：

交互式分布偏移 (Interactive Distribution Shift)： 优化理论依赖于特定的形式化定义（如凸性、最优性条件、算法收敛性）。简单的持续训练（Continual Training）会导致模型学习到新的语法，但却失去了原有的推理启发式策略，产生“看似正确但无助于证明”的无效步骤（Stagnant tactics），从而导致搜索效率低下。
灾难性遗忘 (Catastrophic Forgetting)： 在适应新领域（优化）的特殊语法和定义时，模型往往会丧失在通用数学领域积累的强大推理能力。

2. 核心方法论 (Methodology)

为了解决上述问题，作者提出了 OptProver，其核心是一个稳健的持续训练流水线，包含三个关键技术组件：

A. 基于专家迭代的大规模自我蒸馏 (Large-Scale Self-Distillation via Expert Iteration)

为了缓解由于教材风格与预训练风格不一致导致的分布偏移，作者不直接进行监督微调（SFT），而是采用专家迭代（Expert Iteration, EI）：

利用 Mathlib（数学库）中的定理作为种子，通过当前策略进行大规模搜索。
将搜索到的、经过 Lean 验证器确认的正确轨迹（Trajectories）作为训练数据。
结合自动形式化的教材数据（ $D_{book}$ ）和问题集数据（ $D_{pro}$ ），使模型在学习新知识的同时，通过自我生成的正确路径来保持推理风格的一致性。

B. 效用感知偏好优化 (Utility-Aware Preference Optimization, UAPO)

针对“有效但无用”的步骤（即语法正确但会导致证明进入死胡同的步骤），作者引入了基于验证器反馈的偏好学习：

效用分级： 将证明步骤分为三类：已证明的转换（ $u=2$ ）、无效转换（ $u=0$ ）以及停滞转换（ $u=1$ ）。
惩罚机制： 在构建偏好数据集时，将能够推进证明的步骤设为“优选（Winner）”，而将那些虽然语法正确但导致搜索预算耗尽的“停滞步骤”设为“劣选（Loser）”。这迫使模型避开无效的分支，专注于高效的证明路径。

C. 困惑度加权偏好优化 (Perplexity-Weighted DPO, PW-DPO)

为了解决偏好学习中的数值不稳定问题，作者提出了 PW-DPO：

Token级权重： 计算每个 token 相对于参考模型（Reference Model）的困惑度（Perplexity）。
抑制噪声： 对于高困惑度的 token（通常对应于分布外数据或噪声），通过一个有界的逆困惑度函数降低其在损失函数中的权重。这能防止模型过度拟合低概率的异常数据，从而稳定训练并减轻灾难性遗忘。

3. 主要贡献 (Key Contributions)

提出了新问题定义： 将形式化证明的持续训练定义为一个“交互式分布偏移”问题，并证明了朴素微调的脆弱性。
创新算法： 开发了结合了效用感知（UAPO）与困惑度加权（PW-DPO）的偏好学习框架，显著提升了证明搜索的效率。
构建新基准 (OptBench)： 创建了一个包含 400 个本科水平优化问题的 Lean 4 基准测试集，涵盖基础性质、凸分析和算法分析三个维度。

4. 实验结果 (Results)

领域内表现 (OptBench)： OptProver 在 OptBench 上表现卓越，其 Pass@1 和 Pass@32 达到了 SOTA 水平。通过结合 UAPO 和 PW-DPO（即 PW-UAPO），模型在 OptBench 上的 Pass@32 达到了 55.25%，显著优于同规模的其他模型。
通用能力保持： 在通用数学基准（MiniF2F 和 ProofNet）上，OptProver 没有出现灾难性遗忘。相反，在 ProofNet 上的表现甚至有所提升，证明了其学习到的推理模式具有良好的泛化性。
对比分析： 实验证明，**步进式证明（Step-level proving）**在优化领域远优于全证明生成（Whole-proof generation），因为步进式可以通过交互反馈来弥补领域定义的鸿沟。

5. 研究意义 (Significance)

这项研究为特定领域的自动化定理证明提供了一个成功的范式。它证明了：在处理高度专业化的数学领域时，仅仅依靠增加数据量是不够的，必须通过结合验证器反馈的偏好学习来引导模型学习“高效的推理策略”，而不仅仅是“正确的语法”。这对于未来将 AI 引入更深层次的科学计算和工程优化领域具有重要的指导意义。