엔비디아는 1.5TB VRAM 요구사항을 활용해 AI 컴퓨팅 독점 지위를 공고히 하면서 IMO 검증 레시피를 공개했다.

On September 9, NVIDIA unveiled the complete mathematical reasoning system powering Nemotron 3 Ultra at the 2026 International Mathematical Olympiad (IMO). The system ultimately scored 30 out of 42 points, surpassing that year’s gold medal threshold of 29. Throughout the competition, the model generated proofs exclusively in natural language, without invoking formal provers like Lean, external tools, or web search. However, the significance of this release extends beyond the score. NVIDIA simultaneously open-sourced the two math-specialist checkpoints supporting the 30-point result, along with the supervised fine-tuning (SFT) and reinforcement learning (RL) training datasets, inference code, training recipes, competition submission proofs, and 200 newly curated Nemotron-IMO-Bench problems. In essence, what was published is not merely a stronger standalone mathematical model, but an end-to-end pipeline spanning training to competition inference. Nemotron 3 Ultra serves as the foundational base; the subsequent specialist models, large-scale proof search, model verification, and multi-round rewriting collectively form the complete chain that elevates performance to the gold standard.

Two days later, on September 11, 25 Fields Medalists—including Terence Tao, Peter Scholze, and Maryna Viazovska—issued a joint statement criticizing the accelerating pace of AI-generated mathematical publications, noting that proof verification, methodological clarification, and reproducibility studies consistently lag due to insufficient time. Against this backdrop, NVIDIA’s open-source approach stands out for deliberately preserving the underlying models, data, inference workflows, and computational costs required to achieve an IMO gold-level result.

The technical architecture begins with a deliberate departure from repeatedly sampling a single Nemotron 3 Ultra checkpoint. Instead, NVIDIA trained two math specialists exhibiting distinctly different behaviors. A core design principle within Nemotron is aligning post-training directly with downstream search operations. The SFT dataset incorporates not only complete proofs but also extensive trajectories of proof modification, verification, and re-verification. Consequently, the trained models learn not only how to generate proofs from scratch but also how to diagnose flaws in partially written or locally erroneous drafts and continue refining along the original trajectory. When integrated into the search system, this capability fundamentally alters computational resource utilization. High-difficulty mathematical problems rarely exist in a binary state of solvable or unsolvable; numerous candidates occupy an intermediate zone where the structural framework is nearly viable, failing only on specific lemmas, boundary conditions, or derivation closures. A model capable only of restarting would re-enter the entire proof space upon each failure, whereas a model trained for modification treats existing proofs as intermediate states, effectively preserving valid structures discovered in prior computations.

The RL specialist addresses a separate layer: adjusting the selection probability of different proof pathways. The proof space for IMO-level problems is exceptionally sparse. While a model may possess localized capabilities required to solve certain problem types, correct combinatorial arrangements constitute only a tiny fraction of the generation distribution. Simply increasing sampling volume might eventually encounter the correct pathway, but if most samples remain clustered in similar regions, expanded compute yields minimal gains in actual coverage. RL here recalibrates the generation distribution based on successful and failed trajectories. Approaches that successfully close proofs receive higher weights, while choices that repeatedly drive the model into dead ends are suppressed. This does not invent new mathematical knowledge; it reallocates the frequency at which the model’s existing capabilities manifest. Together, the base, SFT, and RL checkpoints establish three distinct problem-solving priors. This divergence is critical for downstream search, as effectiveness depends on effective sample diversity rather than raw output volume. If a single model continuously generates 200 proofs, most revolving around identical constructions, 200 texts do not equate to 200 independent pathways. Higher candidate correlation diminishes the informational yield of additional compute. Introducing differently post-trained checkpoints actively shifts the sampling distribution, directing computational resources into alternative proof spaces. NVIDIA’s experiments confirm this: extending sampling of a single RL model yields rapidly diminishing returns, whereas integrating the SFT expert significantly expands problem coverage under comparable generation budgets. Thus, post-training here transcends mere single-model capability enhancement. SFT enables iterative proof modification, RL modulates the emergence frequency of high-value pathways, and multi-checkpoint deployment reduces candidate correlation. Collectively, they address how finite inference compute can maximize proof route coverage—a prerequisite for the subsequent 384 initial generations to function effectively. Highly repetitive candidates would render even expansive search pools ineffective.

Following the initial batch of 384 proofs per problem, the actual search process commences. These first-round answers are not treated as endpoints but are deposited into a continuously updated proof pool. Upon verification, each proof falls into one of three categories: fully accepted, directionally viable but requiring patching, or low strategic value. Rather than discarding the latter two categories outright, the system retains higher-scoring proofs and feeds verifier-identified issues back to the model for targeted refinement. This step fundamentally transforms the nature of the inference loop. Conventional multi-sampling repeatedly restarts from zero, generating mutually independent outputs with no memory. Nemotron’s proof pool, conversely, preserves historical computation. It tracks where each pathway stands, what failures occurred, and which components remain usable, feeding this context directly into subsequent search rounds. Verifier feedback functions as a directional signal. Natural language proofs lack continuous, differentiable objective functions, preventing direct gradient-based navigation akin to neural network training. Grading comments serve as an approximation, indicating precisely where the current proof diverges from an acceptable solution, allowing refinement to target localized gaps. Consequently, multi-round rewriting is not mere cosmetic polishing. Each iteration spawns multiple new candidates that re-enter the global proof pool, competing alongside prior pathways. Proofs sustaining high evaluations attract sustained compute investment; those failing to resolve critical vulnerabilities after several refinement cycles gradually lose expansion opportunities. This architecture simultaneously achieves search breadth and depth. The initial hundreds of proofs map the search space, while subsequent multi-round refinements allow near-correct pathways to advance incrementally without constant restarts. This distinguishes Nemotron from naive brute-force sampling, which relies on continuous extraction from a fixed distribution. Here, dynamic compute allocation responds directly to emerging candidate quality.

Nevertheless, this search methodology faces inherent constraints. Unlike chess or Go, mathematical proof generation lacks an explicit rule system. In Go, move legality is instantly verifiable, and game outcomes are deterministically resolved. Natural language mathematics offers no such low-cost validation. A proof may proceed flawlessly for dozens of steps before employing a non-existent symmetry in the final line, or a seemingly abrupt step may nonetheless rest on a valid overarching mathematical intuition. Consequently, the verifier in Nemotron does more than score outputs; it actively dictates compute routing. Paths deemed worthy of retention receive continued refinement opportunities; paths marked as complete trigger early search termination. Verification errors thus transcend mere scoring bias; they directly shape subsequent search trajectories. As search scale expands, the verifier’s influence on overall outcomes intensifies proportionally.

To minimize the risk of erroneously accepted proofs, NVIDIA set an exceptionally high acceptance threshold: two specialists independently verify the same proof, and unanimous agreement is required for acceptance. This design aligns with the system’s cost structure. Misclassifying a correct proof incurs primarily compute overhead, as the system can simply retry; misclassifying an incorrect proof carries heavier consequences, potentially halting search prematurely on a false answer. The system therefore tolerates a higher false-rejection rate to secure a lower false-acceptance rate. Experimental results confirm that raising the threshold markedly reduces erroneous acceptances, albeit at the cost of blocking numerous valid proofs. If the challenge were solely about threshold calibration, the trade-off would simply balance compute expenditure against error rates. Nemotron, however, exposes a deeper structural limitation: verification judgments are not statistically independent. Although the SFT, RL, and base variants undergo distinct post-training, they share the identical Nemotron 3 Ultra foundation. They inherit highly similar knowledge structures, conceptual representations, and reasoning heuristics. When errors stem from random oversights, repeated checks mitigate risk; when errors originate from shared understanding blind spots, incremental verification yields sharply diminishing returns. The paper cites a proof involving permutation symmetry containing easily constructible counterexamples, yet all three checkpoints repeatedly failed to identify the critical flaw. The issue is not insufficient scrutiny, but highly correlated errors across models. If evaluators derive from disparate architectures, one’s blind spot may be compensated by another’s; if they share extensive training and representation structures, multiple evaluators may simultaneously endorse the same false premise. Increased voting consensus stabilizes internal agreement, but this stability does not automatically translate to heightened mathematical credibility.

Case 6 further illustrates this asymmetry. After the system committed substantial compute to generate a novel proof, internal verification still withheld approval, yet human reviewers identified substantial correct content warranting partial credit. This reveals dual verifier biases: shared blind spots permit incorrect proofs to pass with high confidence, while overly conservative thresholds suppress valuable proofs. The subsequent technical hurdle, therefore, lies not merely in training a stronger mathematical referee, but in engineering verification components with maximally divergent error profiles. Deploying different base models for cross-checking, dedicated counterexample generators to actively probe critical steps, symbolic systems for mechanically verifiable algebraic relations, and formal provers for localized propositions collectively reduces the probability of simultaneous component failure at identical logical junctures. At this stage, generation and verification exhibit fundamentally different scaling dynamics. Generation expands through additional models, larger search pools, and deeper refinement chains; verification confronts error correlation. Continuously adding checks from the same model class yields faster plateauing.

With the two expert checkpoints, SFT and RL datasets, inference code, RL recipe, submission proofs, and 200 Nemotron-IMO-Bench problems publicly available, the 30/42 score is reducible to a transparent set of system variables. External teams can manipulate checkpoint combinations, sampling budgets, verifier thresholds, and refinement depths to observe performance shifts. Yet this remains worlds apart from fully replicating the 30-point run. The 550-billion-parameter model, terabyte-scale VRAM requirements, and thousands of GB200 GPU-hours constitute a formidable hardware barrier. Furthermore, NVIDIA’s official documentation explicitly notes that the complete post-training chain for Nemotron 3 Ultra’s base variant is not fully reproducible, with certain intermediate teacher and MOPD checkpoints remaining closed. Nevertheless, the IMO pipeline has laid bare a critical reality: proof generation can scale indefinitely through increased proposals and test-time compute, whereas verification currently lacks an equally stable scaling trajectory. The next formidable challenge is decoupling verifier errors from generator correlations.

Dissecting this event reveals a stark truth: despite fully open recipes, eight B200 GPUs and 1,464 hours of extended compute remain an impenetrable wall, excluding 99 percent of global university laboratories. This “observable yet unaffordable” reality serves as a preview for future AI for Science (AI4S) competitions. Code equity has been achieved, but compute sovereignty remains monopolized by a handful of tech giants. NVIDIA’s strategy illuminates a new collaborative paradigm for scientific discovery. Historically, mathematicians operated as solitary performers. In the era of brute-force inference, AI corporations burn millions in electricity to systematically flatten tedious, repetitive, and massively voluminous logical possibilities. This does not signal the obsolescence of mathematicians, but rather their functional displacement: from “seekers of evidence” to “judges of logic.” NVIDIA’s report demonstrates profound respect for fundamental research not through the 30-point metric, but through a clear signal to academia: compute can handle the most grueling, repetitive labor, but the final adjudication of truth and logical consistency must rely on human intuition. Perhaps this represents the most dignified response from technology conglomerates to basic research in the brute-compute era.

Returning to the opening metaphor, the historical “Edict of Extension” succeeded by distributing benefits to neutralize resistance. Today, NVIDIA distributes the dividends of an IMO gold medal globally through open sourcing, yet inadvertently channels every participant into an NVIDIA-hardware-defined search and inference paradigm. When researchers attempt to replicate this success using the published blueprints, they quickly realize that their only viable path forward is to purchase additional NVIDIA GPUs.

References: https://arxiv.org/pdf/2609.10712 | https://mathandai.org/

Original reporting by Zheng Jiamei | Edited by Cen Feng | Published by Leifeng Wang