大概过了一遍论文，整体的思路就是目前非常主流的llm as a verifier方法。这种方法的基本假设是，判断一个数学证明是否正确需要的能力是远小于真做出一个题的，所以只需要不是特别多的人类专家标注，就能训练出一个不错的“判卷模型”，即认为现有llm在判卷上有足够强的泛化能力。然后只需把这个“判卷模型”作为奖励模型，用已经成熟的强化学习方法不断训练改进解题模型即可，直到解题模型达到 imo 金牌水平的解题能力。我估计 openai 和 deepmind 也是通过相同的思路构建等效 imo 金牌解题水平的模型。
这里需要指出的一点是，论文中达成 imo 金牌解题水平需要依赖“扩展测试时计算”，计算量和成本远超现有落地模型产品的级别。我觉得在国内高中数学联赛二试题目上的 1 pass 测试结果（论文中的图1）更有参考价值：
可以看出，在类似于官网使用 Deepseek 等主流大模型的“正常推理成本”的条件下，目前最好的一批模型在高联二试题的正确率也就一半左右，应该离 imo 金牌水平有明显差距 （gemini 3 pro和 gpt-5.1 在写这篇论文的时候估计还没有发布，不过据我亲自的测试和周围人的反馈，差距不会特别大）。不过比较令人惊讶的是，没有多模态能力的 deepseek 模型在经过强化学习后做平面几何题也能有还行的正确率。另外组合题的正确率是最低的，这倒是比较符合直觉，因为组合题确实容易出的非常难的题。。。
不管怎么说，AI 数学确实已经取得了巨大的进步，不过对于未来将AI用于解决真正前沿的数学问题，我还是怀疑 llm as a verifier 的思路是否能走通。毕竟对于那些前沿问题相关的学术论文，看懂证明并判断是否正确也是相当困难的，有时候人类专家审稿就得花几个月甚至几年的时间，意味着相关的数据从底层上还是很难大量获取。这一点还是和围棋AI基于大量规则内自对弈产生数据的强度学习不一样。所以我认为AI math乃至 AI for science可能还有很长的一段路要走。不管怎么说，现在已经发展到需要 AI 解决真正困难问题的时代了。