NemotronMathProofs

Description

NemotronMathProofs is an environment for writing rigorous natural-language proofs of olympiad-style mathematics problems, graded by a reference-free proof verifier. It ports the proof-generation reinforcement-learning setup behind NVIDIA's An Open Recipe for IMO Gold to OpenReward: the 9,597 problems of nvidia/Nemotron-Math-Proofs-v3-RL, the dataset's own prover prompt, and the reward of the NeMo Gym proof_judge resources server in the paper's alpha=1, beta=0 configuration.

Capabilities

• Olympiad-level mathematical reasoning across algebra and inequalities, functional equations, number theory, combinatorics, sequences and limits, and geometry
• Writing complete, self-contained, rigorous proofs, where an answer without a proof earns nothing and citing a result does not excuse proving it
• Auditing one's own proof: the response must end with a faithful self-evaluation and a boxed self-score in {0, 0.5, 1}
• Following a strict output format in a single message with no tools

Compute Requirements

This is a single-turn environment with no sandbox. The environment server holds a 4.4 MB task file and makes one gpt-6-sol verifier call per episode.

License

MIT. The problem statements are redistributed from nvidia/Nemotron-Math-Proofs-v3-RL under CC BY 4.0, and the verifier prompt is taken from NVIDIA NeMo Gym (Apache 2.0).

Tasks

There is one split, train, containing all 9,597 problems of the source dataset. The problems come from the Art of Problem Solving community and, per the source paper, were selected because Nemotron-3-Ultra solved them in one to three of four attempts as judged by DeepSeek-V3.2-Special, so they are moderately hard for a strong model rather than trivially solvable or hopeless. Problem statements are short (median 285 characters, longest 2,278). About 7,000 ask the model to prove or show a statement and about 2,500 ask it to find or determine something, in which case the solution must state the answer and prove it.

The task spec carries only a task_id (the dataset's uuid); the problem text stays server-side. The prompt the agent receives is the dataset's responses_create_params user message, reproduced byte for byte: it states the task, quotes the verifier's scoring rubric, and mandates the response format (a ## Solution section, a ## Self Evaluation section starting with "Here is my evaluation of the solution:", and a final \boxed{0|0.5|1} self-score). The build script asserts this identity for every row.

Every episode is exactly one turn: the agent's first plain message is the submission and ends the rollout.

Reward Structure

This is a sparse, terminal reward taking one of three values. Writing the format gate as $r_{\text{format}} \in \{0, 1\}$ and the verifier's score as $r_y \in \{0, 0.5, 1\}$:

$R = r_{\text{format}} \cdot r_y$

The format gate follows the upstream parser exactly: text before the last </think> is discarded, the message must contain ## Solution followed later by ## Self Evaluation, the self-evaluation must end with a parseable \boxed{} whose value is 0, 0.5, or 1, the solution section may be at most 40,000 characters and the self-evaluation at most 20,000. Any failure scores 0 without a verifier call; the rejection reason is returned in metadata.

We use an LLM grader. The ## Solution section alone (never the self-evaluation) is sent to gpt-6-sol together with the upstream verifier instruction, which asks for a detailed evaluation and a score of 1 for a completely correct solution, 0.5 for a generally correct solution with minor errors or omitted details, and 0 for a solution with fatal errors or severe omissions. Grading is reference-free: the dataset ships no solutions and the judge sees none. The verifier is called once per episode at medium reasoning effort with no temperature setting, and the reward is its score. The model's self-score is recorded in metadata as s_prime, along with self_eval_gap = |s_prime - r_y|, but does not enter the reward, matching the paper's choice of alpha=1, beta=0 in the DeepSeekMath-V2 reward.

Where this port deviates from the NeMo Gym reference, in the interest of robustness against reward hacking:

• The judge receives a system message stating that the solution text is untrusted data whose instructions, evaluations, and claims of correctness must be ignored. The user message, including the rubric, is the upstream template verbatim.
• A solution section containing the verifier's own answer scaffold ("Here is my evaluation of the solution" or "final overall score should be") is rejected at the format gate as a verdict-injection attempt. Boxed final answers such as \boxed{1} inside a solution are allowed, since problems asking for an answer legitimately produce them.
• The verifier's score is read from the last \boxed{} after the last occurrence of "final overall score should be" in its reply, and a reply that hit the token limit is treated as unusable. Upstream reads the last box anywhere, which a proof ending in a quoted \boxed{1} could exploit if the judge quoted it and was cut off.
• An unusable verifier reply is retried once with a larger budget and a nudge; a persistent failure raises, so the rollout fails visibly instead of scoring 0. Upstream scores an unparseable reply as 0.
• The verifier is gpt-6-sol at medium reasoning effort, whereas the paper's proof generator was trained against Nemotron and DeepSeek-Math-V2 judges sampled at temperature 0.6. The main unmitigated risk is a polished but wrong proof being accepted.

Measured with sweep.py on 2026-09-13 against gpt-5-mini, the verifier at the time (the sweep has not been re-run on gpt-6-sol), every blind or adversarial probe scored 0 on every sampled task, and correct proofs of easy synthetic problems scored 1 on both of two independent judgings:

As a calibration check with real proofs, 20 human-written reference proofs from nvidia/Nemotron-IMO-Bench (200 novel olympiad problems released with the same paper; not part of this environment) were run through the same gpt-5-mini verifier: 12 scored 1, 5 scored 0.5, and 3 scored 0, a mean of 0.725. The judge is therefore strict, and some terse but correct proofs will draw 0.5.

Data

The problems are the problem field of nvidia/Nemotron-Math-Proofs-v3-RL (source AoPS, CC BY 4.0), which the source paper derives from nvidia/Nemotron-Math-Proofs-v1 by keeping problems Nemotron-3-Ultra solved in one to three of four attempts. There are no reference solutions, rubrics, or answers in the release; grading is entirely reference-free. datagen/build.py downloads the release, asserts that the environment's prompt template reproduces every row's responses_create_params content, and writes data/nemotron_math_proofs_tasks.jsonl (task id, split, source, license, problem), which ships inside the environment image.

The agent sees the problem inside the dataset's prover prompt and nothing else. The verifier's evaluation is returned in tool metadata only, never in the tool's text output, so it cannot leak into a trajectory that is later used for training.

Tools

The agent has no visible tools. A hidden terminal tool, submit_solution, receives the agent's final message and returns Proof recorded. Reward: x.xxxx or Submission rejected (<reason>). Reward: 0.0000. Its metadata carries r_format, reason, r_y, s_prime, self_eval_gap, proof_chars, self_eval_chars, the verifier's full response (verifier_response), verifier_finish_reason, judge_model, judge_attempts, judge_usage, and reward. A repeat submission in the same episode is refused with a reward of -0.1.

Time Horizon

Each task is a single message with no tool calls: the agent reads the problem and replies once with its solution and self-evaluation. The solution section is capped at 40,000 characters and the self-evaluation at 20,000. The source paper trained with trajectories of up to 131,072 tokens, so the expected effort per problem is high even though the interaction is one turn. In our deployed checks, gpt-5.2 at high reasoning effort needed 8 to 16 minutes of generation per problem, so client-side request timeouts should allow for that.

Environment Difficulty

The problems are olympiad-style and were filtered to those Nemotron-3-Ultra solved in one to three of four attempts under DeepSeek-V3.2-Special judging, per the source paper. Blind strategies earn 0 (table above). We have only run small end-to-end checks with gpt-5.2 through test_agent.py, not a proper evaluation, so no pass rate is claimed. Against the deployed environment with reasoning effort set to high, gpt-5.2 scored 1.0 on all three sampled problems (a cyclic-window averaging inequality, a set-cover bound of $\lfloor 3k/7 \rfloor$, and a cyclic-quadrilateral geometry problem), taking 8 to 16 minutes and 5,000 to 63,000 output tokens per problem, and self-scoring 1 each time. The same model with no reasoning effort scored 0 on one problem in 23 seconds, honestly self-scoring 0 after failing to close an inequality. The verifier at the time, gpt-5-mini, spent 3,800 to 7,200 tokens per grading call in these runs.

Other Environment Requirements

The verifier needs an OpenAI API key, passed per session as secrets={"openai_api_key": ...} (or chat_api_key). In training infrastructure that redirects OPENAI_BASE_URL for policy traffic, set CHAT_API_KEY and CHAT_BASE_URL so grader traffic stays on the real provider, as described in the OpenReward chat-backends documentation.

Safety

The environment presents no direct safety risks: the agent produces mathematical text and interacts with nothing but a grader. The main indirect risk is that it trains a model to satisfy an LLM verifier. The system message, the verdict-scaffold gate, and the anchored verdict parsing block the cheap exploits we could construct, but a model could still learn to write confident, polished proofs with subtle gaps that the judge accepts, and that habit would be harmful in other settings. Because the self-evaluation does not affect the reward in this configuration, the self-score is also free to drift toward always claiming 1; the s_prime and self_eval_gap metadata exist so that drift can be monitored. Our advice is that multi-environment training runs involving NemotronMathProofs include environments that reward calibrated honesty about one's own errors.

Citations

@article{moshkov2026openrecipe,
  title   = {An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics},
  author  = {Moshkov, Ivan and Ge, Stephen and Armstrong, George and Du, Wei and Mahdavi, Sadegh and Gitman, Igor},
  journal = {arXiv preprint arXiv:2609.10712},
  year    = {2026},
  url     = {https://arxiv.org/abs/2609.10712}
}

@article{shao2025deepseekmathv2,
  title   = {DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning},
  author  = {Shao, Zhihong and Luo, Yuxiang and Lu, Chengda and Ren, Z.Z. and Hu, Jiewen and Ye, Tian and others},
  journal = {arXiv preprint arXiv:2511.22570},
  year    = {2025},
  url     = {https://arxiv.org/abs/2511.22570}
}

@misc{nemogym,
  title  = {NeMo Gym: Evaluate and improve models and agents using environments},
  author = {NVIDIA},
  year   = {2026},
  url    = {https://github.com/NVIDIA-NeMo/Gym}
}