迈向通过解耦推理和证明解决更具挑战性的IMO问题

形式语言中的自动化定理证明 (ATP) 是人工智能面临的一项基础性挑战。尽管大型语言模型 (LLM) 取得了显著进展，但其强大的非形式化推理能力与薄弱的正式证明性能之间仍存在巨大差距。最近的研究表明，在 PutnamBench 等基准测试中，非形式化准确率超过 80%，而正式证明的成功率仍低于 8%。我们认为，这种差距之所以存在，是因为当前最先进的证明器通过将推理和证明紧密耦合，在训练范式中无意中惩罚了深度推理，而倾向于浅层、基于策略的解决方案。为了弥合这一根本性差距，我们提出了一种新颖的框架，将高级推理与低级证明生成解耦。我们的方法利用了两个独立的专业模型：一个强大的通用推理器 (Reasoner) 用于生成多样化、策略性的子目标引理，以及一个高效的证明器 (Prover) 用于严格验证这些引理。这种模块化设计释放了模型的全部推理潜力，并避免了端到端训练的弊端。我们在 2000 年后国际数学奥林匹克 (IMO) 难题的挑战性集合上评估了我们的方法，此前没有任何开源证明器在此类问题集上报告过成功。我们的解耦框架成功解决了其中 5 个问题，标志着在异常困难的数学挑战上实现自动化推理迈出了重要一步。为了促进未来的研究，我们发布了针对各种 IMO 问题生成的和已验证的引理的完整数据集，可在 https://tencent-imo.github.io/ 获取。