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

85 0 0

文章摘要

近年来，大语言模型（LLM）在数学推理领域取得了显著进展，但在形式化数学证明方面却遇到了瓶颈。尽管LLM能够以超过80%的准确率生成非形式化的解题思路，但在将这些思路转化为机器可验证的严格证明时，成功率骤降至不足8%。这一现象揭示了当前AI数学研究中的一个核心矛盾：在“思考”与“证明”之间，存在一道难以逾越的鸿沟。

现有的一体化或耦合式方案试图在单个模型内集成“思考草稿”与“形式化证明”两个环节，但这种设计存在根本性缺陷。首先，模型的高层“思考”受到了其自身底层“证明”能力的严格束缚，导致推理潜力被扼杀。其次，这些模型普遍采用“可验证奖励的强化学习”（RLVR）进行训练，这种训练范式鼓励模型“走捷径”，放弃深度的、复杂的逻辑构建，转而依赖自动化“战术”进行暴力尝试。实验首次定量证明，这种特化训练会导致模型在通用数学推理上的性能显著下降。

为应对这一挑战，研究提出了一种全新的、基于“解耦”哲学的自动化定理证明框架。该框架由两个独立的、可灵活调度的核心模块构成：“推理器”和“证明器”。推理器选用业界最强大的通用大模型，其唯一任务是不受任何形式化约束地进行最高水平的战略思考，提出解决问题的核心思路，并将其凝练成一系列关键的子目标或引理。证明器则选用最高效的形式化证明模型，其任务是接收推理器提出的引理，并逐一验证它们的正确性。通过这种分工，框架彻底解放了推理器的思考潜力，同时又通过证明器的严格验证保证了每一步的逻辑可靠性。

在一系列极具挑战性的、2000年后的国际数学奥林匹克（IMO）非几何难题上，该框架验证了其有效性。框架成功解决了5道此前所有开源自动化证明器均未能解决的IMO难题，包括IMO 2000 Problem 2、IMO 2005 Problem 3、IMO 2011 Problem 3、IMO 2019 Problem 1和IMO 2020 Problem 2。这是AI在顶尖数学竞赛难题上取得的一次里程碑式的突破，首次证明了通过精巧的框架设计，AI有能力攻克需要深邃人类智慧的数学堡垒。

此外，研究向公众开源了全部成果，包括超过600条由框架生成并成功验证的高质量引理。这些数据集为后续工作解决更多IMO级别的难题提供了一个坚实的基础，无论是对于AI研究者，还是对于人类数学家，都可能带来新的启发。

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