FM-Pochi-32B
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.
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):
1./download_models.sh step225 # fetches opd-32b-bf16-step-225 (+ DFlash draft)
2./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
solutions.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.
Related repositories
- Inference code / harness: GitHub repository
- Sibling
deploy checkpoint + DFlash draft: HuggingFace repository
- Base model (continued training from):
allenai/Olmo-3.1-32B-Think
Acknowledgements
We thank the
Fields Model Initiative and
LLMC NII for providing the resources that made this work
possible.