腾讯AI Lab 提出解耦推理新框架，破解IMO 数学难题

首次证明了通过精巧的框架设计，AI有能力攻克需要深邃人类智慧的数学堡垒。

本文探讨了当前大语言模型（LLM）在自动化定理证明（ATP）领域面临的核心困境——强大的非形式化推理能力与孱弱的形式化证明能力之间的巨大鸿沟。为弥合这一鸿沟，我们提出了一种全新的“解耦推理与证明”框架。本研究由腾讯AI Lab完成，主要作者为梁振文和宋林峰。

论文题目：Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

论文地址：[2507.06804] Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

项目主页及开源数据：https://tencent-imo.github.io/

01
背景与动机：AI数学能力的巨大鸿沟

近年来，以大语言模型为代表的通用人工智能在数学推理领域取得了长足进步。然而，当面对需要绝对逻辑严谨性的形式化数学证明时，AI的能力却遭遇了瓶颈。这一现象揭示了当前AI数学研究中的一个核心矛盾，也是其“阿喀琉斯之踵”：

在“思考”与“证明”之间，存在一道难以逾越的鸿沟。

最近在顶尖数学竞赛难题（如Putnam）上的大规模评测鲜明地印证了这一点：最强大的LLM（如Gemini 2.5 Pro）能够以超过80%的准确率生成非形式化的解题思路，展现出惊人的数学直觉与推理能力。然而，当要求最先进的形式化证明器（Prover）将这些思路转化为机器可验证的严格证明时，成功率骤降至不足8%。

AI似乎成了一个“聪明的空想家”——它能想到解法，却无法严格地证明它。现有SOTA证明器（如DeepSeek-Prover-v2）试图通过在单一模型内融合“思考”（生成草稿）与“证明”（生成代码）来解决此问题。但我们的研究发现，这种“耦合”设计存在根本性缺陷：它强迫强大的“思考者”去迁就能力有限的“证明者”，从而扼杀了AI真正的数学潜能。这正是为何即便是最前沿的模型，也始终未能攻克任何一道2000年后的国际数学奥林匹克（IMO）难题。

02
核心洞见：训练范式导致推理能力退化

为应对这一挑战，目前最前沿的工作（如DeepSeek-Prover-v2, Kimina）普遍采用一种“一体化”或“耦合式”的方案，即在单个模型内部集成“思考草稿”与“形式化证明”两个环节。它们试图让模型先生成高层思路，再据此产出形式化代码。

然而，我们的研究发现，这种看似直观的设计存在一个根本性的缺陷：它让模型“带着镣铐跳舞”。具体而言，这种耦合架构导致了两个严重问题：

1.推理潜力被扼杀：模型的高层“思考”受到了其自身底层“证明”能力的严格束缚。为了确保后续能顺利生成可通过验证的代码，模型不敢提出那些真正具有创造性、但形式化难度较高的“奇招”，其所谓的“规划”能力因此退化。

2.训练范式导致能力退化：这些模型普遍采用“可验证奖励的强化学习”（RLVR）进行训练，即只根据最终代码是否编译成功来给予奖励。这种“成王败寇”式的粗暴信号，实际上在鼓励模型“走捷径”——放弃深度的、复杂的逻辑构建，转而依赖ring, omega等自动化“战术”（tactics）进行暴力尝试。我们的实验首次定量证明：这种特化训练，会导致模型在通用数学推理（如MATH, AIME基准）上的性能显著下降，即为了“证明”，牺牲了“推理”。

3.这些问题共同导致了现有方法无法真正利用LLM那高达80%的推理潜力，在面对国际数学奥林匹克（IMO）等真正需要“灵光一闪”的难题时，屡战屡败。

03
解耦框架：让“战略家”与“精算师”各司其职

基于上述诊断，我们提出了一种全新的、基于“解耦 (Decoupling)”哲学的自动化定理证明框架。我们认为，与其强迫一个模型同时扮演好“战略家”和“士兵”两个角色，不如让最优秀的人才各司其职。我们的框架由两个独立的、可灵活调度的核心模块构成：

1.“推理器”（The Reasoner）：我们选用业界最强大的通用大模型（如GPT-4o, Gemini 1.5 Pro）作为推理器。它的唯一任务，就是不受任何形式化约束地进行最高水平的战略思考，提出解决问题的核心思路，并将其凝练成一系列关键的子目标或引理（Lemmas）。这些引理是纯粹的数学陈述，是连接高层智慧与底层逻辑的桥梁。

2.“证明器”（The Prover）：我们选用最高效的形式化证明模型（如DeepSeek-Prover-v2）作为证明器。它的任务是接收推理器提出的引理，并像一个专注的工匠一样，逐一验证它们的正确性。

通过这种“战略家出谋划策，实干家验证执行”的分工，我们的框架彻底解放了推理器的思考潜力，同时又通过证明器的严格验证保证了每一步的逻辑可靠性。

04
里程碑式的实验结果

我们在一系列极具挑战性的、2000年后的IMO非几何难题上验证了我们框架的有效性。结果是突破性的：

我们的框架成功解决了5道此前所有开源自动化证明器均未能解决的IMO难题。包括：

lIMO 2000 Problem 2

lIMO 2005 Problem 3

lIMO 2011 Problem 3

lIMO 2019 Problem 1

lIMO 2020 Problem 2

这是AI在顶尖数学竞赛难题上取得的一次里程碑式的突破，首次证明了通过精巧的框架设计，AI有能力攻克需要深邃人类智慧的数学堡垒。

05
开源贡献与总结

除了方法上的创新，我们深知推动整个社区发展的重要性。为此，我们向公众开源了本次研究的全部成果：

我们为大量DeepSeek-Prover-V2 671B等模型无法独立证明的IMO难题，提供了超过600条由我们的框架生成并成功验证的高质量引理。我们相信，这个数据集将为后续工作解决更多IMO级别的难题提供一个坚实的基础，无论是对于AI研究者，还是对于人类数学家，都可能带来新的启发。

本研究首次系统性地揭示并解决了AI在形式化数学证明中“思考”与“证明”能力失衡的核心矛盾。我们提出的“解耦”框架，不仅在实践中取得了前所未有的成果，也为未来构建更强大、更具洞察力的人工智能系统提供了一条全新的、充满希望的路径。

总结

本研究由腾讯AI Lab完成。我们不仅提出了一个全新的、有效的自动化定理证明框架，更重要的是，我们深刻揭示了当前领域发展的核心矛盾，并为如何弥合“非形式化推理”与“形式化证明”之间的鸿沟提供了一条清晰可行的道路。通过将“思考的艺术”与“验证的科学”解耦，我们成功解决了5道顶尖IMO难题。

未经「AI科技评论」授权，严禁以任何方式在网页、论坛、社区进行转载！

公众号转载请先在「AI科技评论」后台留言取得授权，转载时需标注来源并插入本公众号名片。