FM-Pochi-32B-IMO26

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.

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:

1. 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.
2. 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).
3. 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.
4. 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:

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 solutions.csv; per-problem scores.csv and full commentary are in imo_2026_eval/.

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).

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.

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.