--- license: apache-2.0 base_model: - allenai/Olmo-3.1-32B-Think pipeline_tag: text-generation language: - en tags: - olmo - mathematics - olympiad - theorem-proving - reasoning - imo --- # 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**](https://huggingface.co/allenai/Olmo-3.1-32B-Think), with an **attention-sink** modification and a transplanted **DeepSeek tokenizer**, and is trained to emit a long ` … ` 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)](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot/tree/main/imo_2026_eval) | step-225, `high` budget | [solutions.csv](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot/blob/main/imo_2026_eval/raw/imo2026-step225-budget-high-tournament_submission.csv) | | **IMO 2025** | **30 / 42 — Silver medal** | GPT-5.6-sol | step-225, `high` budget | [solutions.csv](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot/blob/main/benchmarks/imo-2025/solutions.csv) | | **IMO-ProofBench-V2** | **66.4%** (mean **4.65 / 7**) | GPT-5.6-sol | step-225, `medium` budget | [solutions.csv](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot/blob/main/benchmarks/imo-proofbench-v2/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](https://matharena.ai) `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](https://arxiv.org/abs/2511.01846). All numbers use the generate–verify–refine harness (see **Inference** below), not single-shot decoding. Details in [Evaluation](#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 ` … ` block, then the solution. ## Training Starting from [OLMo 3.1 32B Think](https://huggingface.co/allenai/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 `` 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**](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot) 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): ```bash ./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](https://huggingface.co/fieldsmodelorg/Olmo-3.1-32B-Think-OPD-ProofPilot). ## 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`](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot/blob/main/imo_2026_eval/raw/imo2026-step225-budget-high-tournament_submission.csv); per-problem [`scores.csv`](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot/blob/main/imo_2026_eval/scores.csv) and full commentary are in [`imo_2026_eval/`](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot/tree/main/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](https://matharena.ai) `imo_2025` **checkpoint markschemes**. The proofs, per-problem scores, and the reproducible grading prompts are in [`benchmarks/imo-2025/solutions.csv`](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot/blob/main/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](https://arxiv.org/abs/2511.01846) (Luong et al., 2025). Full solutions and per-problem scores: [`benchmarks/imo-proofbench-v2/solutions.csv`](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot/blob/main/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](https://github.com/google-deepmind/superhuman/tree/main/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](https://github.com/fieldsmodelorg/AIMO-Proof-Pilot) - **Sibling `deploy` checkpoint + DFlash draft:** [HuggingFace repository](https://huggingface.co/fieldsmodelorg/Olmo-3.1-32B-Think-OPD-ProofPilot) - **Base model (continued training from):** [`allenai/Olmo-3.1-32B-Think`](https://huggingface.co/allenai/Olmo-3.1-32B-Think) ## Acknowledgements We thank the [Fields Model Initiative](https://www.fieldsmodel.org/) and [LLMC NII](https://llmc.nii.ac.jp/en/) for providing the resources that made this work possible.