首次证明了通过精巧的框架设计，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）。这些引理是纯粹的数学陈述，是连接高层智慧与底层逻辑的桥梁。