AI 拿下 IMO 金牌，但靠的是「反复检查」不是天才
一个纯靠自然语言、不调用任何外部工具的大模型，在 IMO 2026 上拿了 30/42 分，正好压线金牌。它没有用形式化证明器，也没有联网，就是让三个模型互相生成、验证、再修改答案，最后挑一个提交。真正拉开差距的不是模型本身多聪明，而是「迭代验证」这个笨办法——生成一个候选证明，让另一个模型挑错，再改，再挑，循环到时间用完。研究者把训练数据、代码、提交的解答和 200 道新题全开源了。它不是你明天能拿来解数学题的，但它说明一件事：在硬推理上，「多检查几遍」比「换个更聪明的模型」更管用。
📄 原文摘要(英文)
We study how model post-training and test-time inference design affect natural-language proof generation for hard olympiad mathematics. Starting from Nemotron 3 Ultra, we train two specialist checkpoints using supervised fine-tuning and reinforcement learning, and evaluate checkpoint choice, verification, and refinement. Based on these findings, we present an open-model test-time-compute pipeline. The system operates entirely in natural language, with no formal prover, external tools, or internet access. Three Nemotron 3 Ultra checkpoints - the general-availability model and two post-trained specialists - power an iterative search that generates, verifies, and refines candidate proofs; a separate high-compute stage then selects each final submission. The system scored 30 out of 42 points at IMO 2026, reaching the gold-medal threshold. We release the two post-trained checkpoints as well as the training data, the training and inference code, the submitted solutions, and Nemotron-IMO-Bench, a new benchmark of 200 novel olympiad-level problems.