README.md

---
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 `<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)](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) |

<sub>**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).</sub>

## 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](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 `<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**](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.

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

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