| --- |
| license: apache-2.0 |
| base_model: allenai/Olmo-3.1-32B-Think |
| tags: |
| - math |
| - theorem-proving |
| - olmo3 |
| language: |
| - en |
| --- |
| |
| # Proof Pilot — intermediate 32B checkpoints |
|
|
| Intermediate model checkpoints for the AIMO Proof Pilot submission, one subdirectory per step |
| of the Stage 2 "Final Pipeline" report. Code: [proof-pilot-codes](https://github.com/ycchen-tw/proof-pilot-codes). |
| Final deployment artifacts (OPD step-200 target, GPTQ-w4a16, DFlash drafts) live in |
| [proof-pilot-deploy-bundle](https://huggingface.co/ycchen/proof-pilot-deploy-bundle). |
|
|
| Lineage: OLMo 3.1 32B Think → DeepSeek-V4 tokenizer transplant → attention-sink calibration → |
| SFT → offline soft distillation (forward KL on DeepSeek-V4-Flash hidden states) → proof-agent |
| continuation distillation → agentic on-policy distillation (OPD). |
|
|
| | Subdirectory | Report step | Contents | |
| |---|---|---| |
| | `step01-olmo32b-deepseektok/` | 1 | OLMo 3.1 32B Think body with DeepSeek-V4 vocabulary (centered-OMP transplant), bf16 | |
| | `step02-olmo32b-deepseektok-sink/` | 2 | Step 1 + calibrated explicit attention sinks; custom modeling code and `sink_provenance.json` | |
| | `step04-sft-stage1-32b/` | 4 | Supervised 32B checkpoint (step 5,317, ~22.3B packed tokens, trailing loss ≈0.44) | |
| | `step05-yarn256k-config/` | 5 | Config-only YaRN-256k variant of step 4 (same weights; YaRN factor 8→32, attention factor 1.347, max position 262,144) | |
| | `step07-softdistill-32b-config/` | 7 | Training config of the initial soft-distilled checkpoint; identical weights are public as `soft-distill-32b-deploy` in the deploy bundle | |
| | `step09-softdistill-v2test-32b/` | 9 | Final proof-agent soft-distilled 32B (2 epochs, final loss 0.114) — student init for OPD and target for DFlash | |
| | `step10-opd-32b-s150/` | 10 | OPD step-150 checkpoint; the released step-200 target is `opd-32b-deploy` in the deploy bundle. NOTE: this directory uses the serving layout (legacy `rope_scaling` keys, hybrid-SWA fields, no bundled custom modeling code) — load it with SGLang/the deploy stack, not stock `transformers` | |
|
|
| All full checkpoints are consolidated bf16 safetensors with config, tokenizer, and chat template. |
| The 65 GB checkpoints load with `trust_remote_code` where custom `olmo3_sink` modeling code is present. |
|
|
| Optimizer states and distributed (resumable) training checkpoints are not published. |
| Teacher hidden-state corpora are not published; their manifests and extraction metadata are in |
| [proof-pilot-datasets](https://huggingface.co/datasets/ycchen/proof-pilot-datasets). |
|
|
