File size: 2,548 Bytes
2925c01 3345aa0 2925c01 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 | ---
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).
|