Olmo-3.1-32B-Think-OPD-IMO

A 32B fully open-source reasoning model fine-tuned for writing mathematics proofs. It continues training from AllenAI's OLMo 3.1 32B Think, with an attention-sink modification and a transplanted DeepSeek tokenizer, and is trained to emit a long <think> … </think> reasoning trace followed by a complete written solution. The recommended checkpoint is opd-32b-bf16-step-225 ("step-225").

Training cutoff — no IMO 2026 contamination. Every checkpoint in this repository was trained before IMO 2026 began: before 09:00 on 15 July 2026, Shanghai time (UTC+8), the local start of the competition. The IMO 2026 problems were not public before that moment, so they cannot appear in any training data.

Benchmark	Result	Grader	Setting	Solutions
IMO 2026	21 / 42 — Bronze medal	Human expert (ex-IMO)	step-225, `high` budget	submission.csv
IMO 2025	30 / 42 — Silver medal	GPT-5.6-sol	step-225, `high` budget	solutions.csv
IMO-ProofBench-V2	66.4% (mean 4.65 / 7)	GPT-5.6-sol	step-225, `medium` budget	solutions.csv

_{Grader — IMO 2026 solutions were graded per-problem by human experts
(former IMO competitors) against broad IMO standards. IMO 2025 is scored by
GPT-5.6-sol (xhigh) against the MathArena imo_2025
checkpoint markschemes — full marks (7 points) for a complete proof by any method, partial credit
for genuine checkpoints, 0 for a wrong answer; IMO-ProofBench-V2
by the same autograder following the ProofAutoGrader protocol of
arXiv:2511.01846. All numbers use the
generate–verify–refine harness (see Inference below), not single-shot decoding.
Details in Evaluation.}

Checkpoints in this repository

Each sub-folder is a self-contained BF16 checkpoint (config + safetensors). Point your loader at the sub-folder, not the repo root.

Sub-folder	What it is
`opd-32b-bf16-step-225`	Recommended. Strongest single-step checkpoint; all reported numbers use this.
`opd-32b-bf16-step-125` … `-250`	Individual training-step checkpoints (125, 150, 175, 200, 225, 250).
`opd-32b-bf16-merged-*`	Weight-averaged ("model-soup") checkpoints over a range of steps.

If you only want the best model, download opd-32b-bf16-step-225.

Architecture

A dense decoder-only transformer derived from OLMo 3.1 32B (Think), with two modifications relative to stock OLMo:

Attention sink — per-head learned attention-sink logits (the Olmo3Sink variant). The inference stack must apply the attention-sink patch. Loading the weights in an unpatched runtime silently produces wrong numerics (no sinks).
DeepSeek tokenizer — the original OLMo tokenizer is replaced with DeepSeek's, with the embedding / LM-head re-fit accordingly.

Other properties: BF16 weights, 262,144-token context, "Think" reasoning format (a <think> … </think> block, then the solution.

Training

Starting from OLMo 3.1 32B Think, the model is adapted and then distilled for proof writing against a DeepSeek-V4-Flash teacher:

Base adaptation — transplant the DeepSeek tokenizer (embeddings re-fit) and add the learnable attention sink, so the OLMo body runs in DeepSeek's token space with stable long-context attention.
Stage-1 SFT — supervised fine-tuning to establish proof behaviour: formatting, mathematical style, and long-form <think> traces (~20 B tokens, max length 12,288).
Full-vocab soft distillation — offline distillation against the teacher's full next-token distribution: teacher hidden states are stored and the full-vocab logits reconstructed through the LM head, then KL/JSD to the student. Context length is raised to 128 k.
Full-vocabulary OPD — the final on-policy distillation stage matches the teacher's full next-token distribution (as in step 3), not just its sampled or top-k outputs.

The model is trained to play every role in the inference harness — prover, verifier, refiner and selector.

Inference

Inference code (harness + Docker): inference harness on GitHub

Because of the attention-sink modification, run this model through the provided harness (patched SGLang) rather than a stock loader. The repository ships a self-contained Docker image and a scheduler.sh launcher that apply the required Olmo3Sink patch at boot; a hand-rolled python -m sglang.launch_server that bypasses them runs unpatched and produces wrong outputs.

The reported numbers come from a generate–verify–refine harness (best-of-N proving → self-verification → refinement, with an optional LLM final-solution selector), configured by the checkpoint × budget presets config-model-step225-budget-{medium,high,xhigh}.yaml:

Preset	proofs/round	verifications/proof	top	refine parents × reviews	rounds
`medium`	32	16	8	4 × 3	4
`high`	64	32	16	4 × 3	8
`xhigh`	128	64	32	4 × 3	8

Quick start (from the harness repo, on an 8×H200 node):

./download_models.sh step225                        # fetches opd-32b-bf16-step-225 (+ DFlash draft)
./scheduler.sh config-model-step225-budget-xhigh.yaml /workspace/runs/step225-xhigh

Optional DFlash speculative-decoding draft and the sibling deploy checkpoint live in a separate HuggingFace repository.

Evaluation

IMO 2026

step-225 at the high budget, graded per-problem by human experts (former IMO competitors) against broad IMO standards (no markscheme was available). The proofs are the tournament submission.csv; per-problem scores.csv and full commentary are in imo_2026_eval/.

P1	P2	P3	P4	P5	P6	Total
7	0	0	7	7	0	21 / 42

Medal boundaries this year were Bronze 16 / Silver 23 / Gold 29, so 21 is a Bronze, just short of Silver. xhigh reruns independently reproduced P1, P4 and P5 at 7 each.

IMO 2025

step-225 at the high budget, on all 6 problems, scored 0–7 by GPT-5.6-sol (xhigh) using the MathArena imo_2025 checkpoint markschemes. The proofs, per-problem scores, and the reproducible grading prompts are in benchmarks/imo-2025/solutions.csv (the markscheme is embedded in the prompts, so re-running them reproduces the scores).

P1	P2	P3	P4	P5	P6	Total
7	7	2	7	7	0	30 / 42

The 2025 medal boundaries were Bronze 19 / Silver 28 / Gold 35, so 30 is a Silver — the model clears the Silver cut-off on IMO 2025.

Full marks (7): P1, P2, P4, P5 are complete rigorous proofs — including P2, solved by a full coordinate-geometry computation (a valid alternative to the synthetic solution; the route OpenAI and Gemini also took). A complete proof by any method earns 7.
Partial (P3 = 2): the correct answer (c = 4) and a valid construction, but the upper-bound crux — the identity-function branch — is "closed" by a false step, so only the construction checkpoint is earned.
Zero (P6 = 0): a wrong final answer (4048; the correct answer is 2112).

This is an LLM grade (GPT-5.6-sol + independent verification), not human coordination.

IMO-ProofBench-V2

step-225 at the medium budget, on all 60 problems (30 Basic + 30 Advanced), scored 0–7 by the GPT-5.6-sol autograder following the ProofAutoGrader prompt of arXiv:2511.01846 (Luong et al., 2025). Full solutions and per-problem scores: benchmarks/imo-proofbench-v2/solutions.csv.

Subset	Problems	Mean / 7	% of max
Overall	60	4.65	66.4%
Basic	30	6.45	92.1%
Advanced	30	2.84	40.6%

Numbers are averaged from 8 LLM gradings (grader self-consistency is high — 57/60 unanimous across 4 LLM judges). Please note that IMO-ProofBench-V2 results are usually graded using Gemini-2.5-Pro in previous literature, but we find GPT-5.6-Sol to be more precise and strict.

_{Benchmark problems, reference solutions and grading guidelines from
google-deepmind/superhuman/imobench
(CC-BY 4.0).}

Intended use and limitations

Intended use: research on olympiad-level mathematical reasoning and automated proof generation. Designed to be driven by the generate–verify–refine harness.
Limitations: weak on hard combinatorics/geometry and on problems requiring synthetic (non-computational) geometry; can produce fluent-but-wrong "hallucinated rigor" (fabricated load-bearing steps). Proofs should be independently verified.
Reproducibility: the IMO'2026 and IMO-ProofBench-V2 results are stable accross multiple inference runs.