Blame for README.md

---
license: apache-2.0
library_name: align
pipeline_tag: text-generation
language:
- en
tags:
- post-training
- rlhf
- sft
- dpo
- ppo
- grpo
- cispo
- expert-iteration
- lean4
- theorem-proving
- formal-verification
- fsdp2
- mixture-of-experts
- code
datasets:
- viai957/lean-prover-data
- Goedel-LM/Goedel-Pset-v1
- HangHor/RL-Goedel-Pset-Level-4-5
- SphereLab/FormalMATH-All
- iiis-lean/NuminaMath-LEAN-Sol
- nvidia/Nemotron-Math-Proofs-v1
model-index:
- name: align (harness) / Goedel-Prover-V2-8B baseline and expert-iteration campaign1
  results:
  - task:
      type: text-generation
      name: Lean 4 whole-proof generation
    dataset:
      type: minif2f
      name: miniF2F-test (244, Lean 4.9.0-rc1, statements from Goedel-Prover-V2 dataset/minif2f.jsonl)
      split: test
    metrics:
    - type: pass@8
      name: Goedel-Prover-V2-8B base, pass@8, n=8, cap 16,384 (align harness)
      value: 78.7
    - type: pass@1
      name: Goedel-Prover-V2-8B base, pass@1, n=8, cap 16,384 (align harness)
      value: 62.1
    - type: pass@32
      name: Goedel-Prover-V2-8B base, pass@32, n=32, cap 40,960 (align harness)
      value: 82.8
  - task:
      type: text-generation
      name: Lean 4 whole-proof generation
    dataset:
      type: minif2f
      name: miniF2F-valid (226)
      split: validation
    metrics:
    - type: pass@8
      name: Goedel-Prover-V2-8B base, solved@8, n=8, cap 30,000
      value: 83.2
    - type: pass@8
      name: align expert iteration round 1, solved@8, n=8, cap 30,000
      value: 83.2
    - type: pass@8
      name: align expert iteration round 3, solved@8, n=8, cap 30,000
      value: 81.9
---

# align: a torch-only post-training stack with a Lean 4 verifier in the loop

`align` is a post-training library (SFT, DPO, PPO, GRPO / Dr.GRPO / DAPO-clip, CISPO, expert iteration) whose
runtime dependencies are only `torch`, `triton`, `numpy` and `safetensors`. It contains a strict Lean 4 proof
verifier, FSDP2 training with coordinated stop/resume, a dropless MoE (OLMoE) and a Qwen3 model path. This repository is
a **code snapshot**, not a model checkpoint. The measured results below come from running this code on one 4-GPU box.

> Headline (measured, 2026-10-24 to 2026-10-26): three rounds of verifier-filtered expert iteration on
> Goedel-Prover-V2-8B produced **no measurable gain** on miniF2F-valid. Solved@8 went 188 (base) → 188 → 187 → 185 of 226.
> Base vs round 3 has an exact McNemar p of 0.51. Treat this card as a record of the engineering and of a negative
> result, not as a SOTA claim.

## 1. TL;DR product sheet

| | |
|---|---|
| What it is | Post-training library + Lean 4 verifier + evaluation harness (code snapshot; git bundle with full history) |
| Code in this repo | `code/` = working tree at commit `f8dfa503` (2026-10-19, see `COMMIT`); `align.bundle` = full git history |
| Runtime deps | `torch`, `triton`, `numpy`, `safetensors` only. An AST firewall test enforces this (`tests/test_dependency_firewall.py`). vLLM and W&B run in separate venvs under `extras/` and only exchange files with the trainer. |
| Algorithms implemented | SFT (masked CE, global token-mean); DPO (`sigmoid`, `ipo`, `sigmoid_norm`, `dpop`) with precomputed reference log-probs; PPO with LoRA, a value head, GAE and PRM step rewards (`clip_delta`); GRPO (vendored from open-instruct, Dr.GRPO constant denominator, DAPO clip-higher, ρ correction); CISPO + FP32 LM head; single-turn Lean RL (`cispo` / `dr_grpo` / `ei`); expert iteration with weight averaging |
| Models exercised | Goedel-Prover-V2-8B (Qwen3, 8.19B; LoRA r64), OLMoE-1B-7B-0125 (6.92B MoE; full FT), tiny Mistral/OLMoE test models |
| Verifier | Lean 4.9.0-rc1 + Mathlib `d1d1e4b7` + REPL `v4.9.0-rc1`. Accepts 177/178 known-good proofs and 0/61 adversarial ones; a naive compile-only check accepts 51/61. |
| Best measured eval (base model through this harness) | Goedel-Prover-V2-8B on miniF2F-test: pass@8 78.7% (192/244) at a 16k cap; pass@32 82.8% (202/244) at a 40k cap. The published figure is 84.6% pass@32. |
| Trained-model result | Expert iteration, 3 rounds (LoRA SFT on 374-442 self-generated verified proofs per round): no gain on miniF2F-valid (section 6) |
| Compute | One host with 4 GPUs of 23 GB each, connected over PCIe with no NVLink. Campaign1 stage markers record 27.2 box-hours across 3 rounds (round-1 generation not included). |
| Licence | Apache-2.0 (code). Third-party data licences are in section 10. |

## 2. Library details and mechanism

* **Model code:** dense Mistral and Qwen3 (with QK-norm and GQA), plus OLMoE (dropless top-k MoE). The MoE combine is
  fixed-order: see the bug in section 7. Parity with transformers: OLMoE fp32 max |Δlogit| is 1.4e-5 to 3.0e-5,
  with top-1 agreement 74/74 and router top-8 sets 100% on all 16 layers.
* **Trainer:** FSDP2 with bf16 params and fp32 reduce-scatter. The optimizer is an in-repo block-wise 8-bit AdamW
  (`adamw8bit`) with per-rank optimizer files. A SIGTERM or wall-clock stop halts every rank at the same
  optimizer-step boundary. Checkpoints are fsynced and checked for completeness. Distinct exit codes 80-83 survive
  `torchrun` through `HALT.json`, and `scripts/supervise.py` relaunches the run after a crash.
* **Rollout:** vLLM in `extras/vllm_rollout` with its own venv; the trainer exchanges JSONL with it. There is also a
  native paged-KV engine (CPU-validated only).
* **Verifier (`align/verify/lean/`):** a strict layer (lexical gate, exact statement match, axiom whitelist
  `{propext, Classical.choice, Quot.sound}`, header checks), a REPL pool with memory and time caps, and a 180 s budget
  per proof. Timeouts, crashes and memory kills count as "no signal" and are never scored as failures.

```mermaid
flowchart LR
  subgraph Data
    P[Problem JSONL<br/>HF-streamed pool<br/>decontaminated] --> S[select_by_band<br/>pass-rate band 0..0.75]
  end
  subgraph Rollout["extras/vllm_rollout (own venv)"]
    G[lean_gen.py<br/>vLLM TP=4, T=1.0, top_p 0.95]
  end
  subgraph Verify["align/verify/lean"]
    V[strict verifier<br/>Lean 4.9.0-rc1, 180 s<br/>axiom whitelist, statement match]
  end
  subgraph Train["align/train + align/rl (torch only)"]
    SFT[SFT: LoRA r64, adamw8bit, FSDP2]
    RL[GRPO / CISPO / PPO<br/>Dr.GRPO denominator, rho-correction]
    DPO[DPO: fused chunked kernel,<br/>precomputed ref log-probs]
  end
  AVG[weight average<br/>0.7 ft + 0.3 base]
  E[eval_report.py<br/>pass@k, cluster bootstrap,<br/>exact McNemar]
  S --> G --> V
  V -- accepted proofs --> SFT --> AVG --> G
  V -- rewards --> RL
  AVG --> E
```

```mermaid
flowchart TB
  T[torchrun x4] --> R0[rank 0..3: Trainer]
  R0 -->|every boundary: MAX-reduce stop / non-finite flags| B{stop?}
  B -- no --> O[adamw8bit step, grad clip 1.0, tripwires]
  B -- yes --> C[checkpoint: model.safetensors + optimizer_rank r.pt + RNG, fsync, completeness check]
  C --> H[HALT.json exit 80-83 or 143]
  H --> SUP[supervise.py: relaunch only after a non-HALT crash that made progress]
  SUP --> T
```

## 3. Training data

This is a library card, so the data listed here is the data of the measured runs.

| Use | Source (HF id) | Licence | Rows used | Notes |
|---|---|---|---|---|
| EI campaign pool | `viai957/lean-prover-data:problems/train_pool.jsonl` | mixed, per row | 1,992 kept of 2,000 read | 8 dropped for informal overlap with a protected benchmark |
| EI campaign pool | `viai957/lean-prover-data:supply/screen_v1.jsonl` | mixed, per row | 3,948 kept of 4,000 read | 49 informal overlaps and 3 duplicates dropped |
| Pool by origin | goedel-pset-v1 1,992; rl-goedel-pset-l45 997; numinamath-lean-sol 989; nemotron-math-proofs-v1 989; formalmath-all 973 | MIT / MIT / Apache-2.0 / CC-BY-SA-4.0 / MIT | 5,940 total | `runs/campaign1/pool.jsonl` |
| Protected (never selected) | miniF2F-test, MOBench | MIT / own | - | `protected_problems` in the round manifests; the EI driver refuses test-split selection |
| Model selection | miniF2F-valid | MIT | 226 | all stop decisions use this split |
| OLMoE smoke | PRM800K SFT shards from nano-mistral-o1, re-tokenized | MIT | 320 rows, 640-968 tokens | control-plane test only |

**SFT data per EI round:** up to 4 of the shortest verified proofs per problem, from n=8 samples at a 16k cap. The
selection order is in-band (0 < p ≤ 0.75), then unmeasured, then never-solved (at most 60), truncated at 300 problems.

| Round | in-band selected | unmeasured selected | never-solved selected | SFT rows | problems with rows | completion tokens | prompt tokens |
|---|---|---|---|---|---|---|---|
| 1 | 115 | 185 | 0 | 442 | 135 | 1,642,463 | 111,922 |
| 2 | 107 | 193 | 0 | 374 | 120 | 1,377,760 | 97,007 |
| 3 | 96 | 204 | 0 | 398 | 127 | 1,523,369 | 96,571 |

No never-solved statement was ever selected, because in-band plus unmeasured problems always filled the 300 slots.

## 4. Training procedure

### Objectives as implemented

**SFT** (`align/train/sft_loss.py`, `loss_normalization = "global_token_mean"`). The loss mask $m_t$ zeroes prompt and
pad tokens. The denominator is all-reduced over the accumulation window and over ranks:

$$\mathcal{L}_{\text{SFT}}=-\frac{1}{\sum_{r,w,t} m_t}\sum_{r,w,t} m_t \log \pi_\theta(y_t\mid x,y_{<t})$$

**DPO** (`align/kernels/fused_dpo.py`). With $\Delta=(\log\pi_\theta(y_w)-\log\pi_\theta(y_l))-(\log\pi_{\text{ref}}(y_w)-\log\pi_{\text{ref}}(y_l))$
and reference log-probs precomputed as constants:

$$\mathcal{L}_{\text{DPO}}=-\log\sigma(\beta\Delta),\qquad \mathcal{L}_{\text{DPOP}}=-\log\sigma\big(\beta(\Delta-\lambda\max(0,\log\pi_{\text{ref}}(y_w)-\log\pi_\theta(y_w)))\big)$$

The defaults are $\beta=0.1$, $\lambda=50$ (`dpop` is a tripwire response, not the primary variant), and an optional
chosen-side NLL term.

**GRPO / Dr.GRPO** (`align/rl/grpo_loss.py`, vendored from allenai/open-instruct @ 8759c91). Advantages are centred
within each group and not divided by the standard deviation: $A_i=r_i-\frac1G\sum_j r_j$. With $\rho_t=\pi_\theta/\pi_{\text{old}}$:

$$\mathcal{L}=-\frac{1}{C}\sum_{i,t}\min\!\big(\rho_t A_i,\ \text{clip}(\rho_t,1-\epsilon_{l},1+\epsilon_{h})A_i\big)+\beta\,\widehat{\text{KL}}$$

$C$ is a constant global denominator (prompts × G × max_len). The defaults are $\epsilon_l=0.2$ and $\epsilon_h=0.272$
(DAPO clip-higher). The A3 gate requires $\beta=0$ and refuses to launch otherwise, except $\beta=10^{-4}$ under the explicit `allow_kl_ablation` flag (the pre-registered collapse-response ablation). A stop-gradient engine-mismatch
factor $\pi^{\text{train}}_{\text{old}}/\pi^{\text{infer}}_{\text{old}}$ is applied and masked.

**CISPO** (`align/rl/cispo.py`, MiniMax-M1 Eq. 4-5). The clipped importance weight is a stop-gradient constant, so no
token's gradient is zeroed. There is no KL term. An optional FP32 LM head (chunked and checkpointed) reduces the
mismatch between sampler and trainer:

$$\mathcal{L}_{\text{CISPO}}=-\frac1C\sum_{i,t}\text{sg}\big(\min(\rho_t,1+\epsilon_h)\big)\,A_{i,t}\log\pi_\theta(o_{i,t}\mid q,o_{i,<t})$$

**PPO with process rewards** (`align/ppo/`, ported from mistral-prm-ppo). The objective is a clipped surrogate
(cliprange 0.2) plus a clipped value loss (0.2) plus a k3 KL. GAE uses separate $\lambda_{\text{actor}}$ and
$\lambda_{\text{critic}}$, and $\gamma=1$ is enforced. PRM step scores $p_j$ are shaped with `clip_delta`:
$c_j=\min(p_j-\eta,0)$, $d_j=c_j-c_{j+1}$ (potential-based), with $\eta$ an absolute probability (0.80 in the draft
config).

**Expert iteration (campaign1, `scripts/p2/expert_iteration.py`).** Each round $k$ runs four steps:
1. Select problems by pass-rate band.
2. Sample n=8 proofs at a 16k cap and verify them.
3. Run LoRA SFT on the verified proofs.
4. Average the weights against the original base: $W_{k}=0.7\,W^{\text{ft}}_{k}+0.3\,W_{0}$.

The run stops on a **regression**, when solved@8 is at or below the best so far minus 3 (`max_regress`). It also
stops on a **plateau**, when each of the last 2 rounds fails to beat the earlier best by at least 2 problems
(`min_gain`, `patience`). Campaign1 stopped after round 3 on regression (185 ≤ 188 − 3) and kept round 1.

### Hyperparameters (campaign1 SFT, `configs/p2_sft.toml` + round manifests)

| Parameter | Value |
|---|---|
| Base | Goedel-LM/Goedel-Prover-V2-8B @ `dfd02e62` (Qwen3, 8,190,735,360 params, 36 layers) |
| Adapter | LoRA r=64, α=128, dropout 0. Targets: q,k,v,o,gate,up,down. 175M trainable params (2.1%) |
| Optimizer | adamw8bit, lr 2e-5, betas (0.9, 0.95), wd 0, clip 1.0 |
| Schedule | 10% warmup, cosine to 0, 2 epochs; 28 / 24 / 27 optimizer steps (rounds 1/2/3) |
| Batch | micro-batch 1 × seq_len 18,432 tokens (packed token budget), grad_accum 2, 4 ranks → 8 micro-batches per step |
| Precision / parallelism | bf16, FSDP2, sdpa attention, per-rank optimizer state |
| Weight averaging | ft_weight 0.7, anchored to the original base |
| Eval | miniF2F-valid, n=8, cap 30,000, T=1.0, top_p 0.95, seed 0, verifier budget 180 s |

### Compute (stage markers in `runs/campaign1/ei/round_0*/round_manifest.json`)

| Round | train (s) | gen+verify (s) | eval (s) | export+average (s) | total (h) |
|---|---|---|---|---|---|
| 1 | 2,223 | 55* | 13,110 | 450 | 4.40 |
| 2 | 1,977 | 21,868 | 14,645 | 369 | 10.80 |
| 3 | 2,168 | 24,778 | 15,825 | 416 | 12.00 |

\*Round-1 generation ran during earlier failed attempts and is not in the marker. Recorded total: 27.2 h.

Hardware: 4 GPUs of 23 GB each over PCIe, with no NVLink. NCCL uses the SHM transport at about 4 GB/s.
`docs/MEASUREMENTS.md` records the GPUs as A10G (sm_86) on 2026-10-12. A project note dated 2026-10-25 records an
`nvidia-smi` reading of L4 (sm_89). The campaign manifests do not record the GPU model.

## 5. Training curves

![EI SFT curves](figures/sft_curves_ei_rounds.png)

*Figure 1. LoRA SFT for EI rounds 1-3. Left: token-mean CE, averaged over the 4 ranks per micro-step. Middle:
learning rate actually applied. Right: pre-clip gradient norm at optimizer steps. Source: the local W&B history
`runs/campaign1/wandb/wandb/run-20261023_212613-0ca1a6eafc40/run-0ca1a6eafc40.wandb` (keys `sft/*`, 632 rows =
158 micro-steps × 4 ranks). The checkpoint directories were pruned after export, so W&B is the only surviving log.*

The loss is low from the first step, because the data is the model's own verified output: the rank-mean is
0.18 / 0.15 / 0.11 at the first micro-step of rounds 1/2/3. The loss is noisy within an epoch and does not trend
down. The gradient norm stays between 0.017 and 0.034, so the clip at 1.0 never binds.

![OLMoE smoke](figures/olmoe_sft_smoke.png)

*Figure 2. OLMoE-1B-7B-0125 full-FT smoke run on 4 GPUs (FSDP2, adamw8bit, load balancing off, lr 1e-5,
16,384 padded tokens per step): mean loss per optimizer step and pre-clip gradient norm. Values are transcribed
from `docs/MEASUREMENTS.md` section (g). The raw `history.jsonl` files were deleted with the checkpoints. This run
tests the control plane and makes no claim about convergence.*

No RL (GRPO / CISPO / PPO) or DPO run has been executed with this code on GPUs, so there are no reward, KL or clip-fraction curves.

## 6. Evaluation

### 6.1 Harness validation: base model on miniF2F-test (244)

![miniF2F-test baseline](figures/minif2f_test_baseline_passk.png)

*Figure 3. Goedel-Prover-V2-8B through the align harness. Sources: `docs/evidence/p2_baseline_2026-10-13/report.md`
and `docs/evidence/sota_repro_2026-10-14/report.md`. The dashed line is the published 84.6% pass@32
(`docs/SOTA_TARGETS.md`).*

| Run | n/problem | cap | pass@1 [95% cluster bootstrap] | pass@2 | pass@4 | pass@8 | pass@32 | length-capped | mean tokens |
|---|---|---|---|---|---|---|---|---|---|
| base16k | 8 | 16,384 | 62.1% [57.0, 67.3] | 70.1% | 75.4% | 78.7% (192/244) | n/a | 5.8% | 4,921 |
| base40k_n32 | 32 | 40,960 | 62.8% [57.9, 67.7] | n/a | n/a | 79.7% | 82.8% (202/244) | 2.3% | 5,669 |

Our pass@32 is 202/244 and the published figure is 84.6% (≈207/244). The gap is 5 problems. 391 of 7,808 samples hit
the 180 s verifier timeout, while the published compile budget is 300 s. A re-check of timed-out samples at 300 s
accepted 0 of the first 82, so the baseline stays at 202.

### 6.2 Hill-climbing: expert iteration on miniF2F-valid (226)

![hill climb](figures/hillclimb_ei_minif2f_valid.png)

*Figure 4. Solved@8 (Wilson 95%) and pass@1 (cluster bootstrap over problems, 2,000 resamples, seed 0), all at
n=8, cap 30,000. Sources: `runs/campaign1/ei/round_0{1,2,3}/eval/ver_n8_c30000.jsonl` and the base run
`ProofForge/runs/p5_eval/base/ver_n8_c30000.jsonl` (run 2026-10-26 with the same `lean_gen.py`, sampling args and
prompt render hash `83d0bbb9…`). The only verifier-config difference is the worker count (2 vs 8).*

| Model | solved@8 [Wilson 95%] | pass@1 [bootstrap 95%] | pass@2 | pass@4 |
|---|---|---|---|---|
| Base Goedel-Prover-V2-8B | 188/226 = 83.2% [77.8, 87.5] | 71.8% [66.6, 77.0] | 77.6% | 80.7% |
| EI round 1 | 188/226 = 83.2% [77.8, 87.5] | 71.9% [67.0, 76.7] | 78.2% | 81.6% |
| EI round 2 | 187/226 = 82.7% [77.3, 87.1] | 71.1% [65.9, 76.2] | 77.2% | 80.5% |
| EI round 3 | 185/226 = 81.9% [76.3, 86.3] | 72.0% [66.9, 76.8] | 77.9% | 80.5% |

Paired solved@8 comparisons (exact two-sided McNemar on the 226 problems):

| Comparison | only A | only B | p |
|---|---|---|---|
| base vs r1 | 2 | 2 | 1.00 |
| r1 vs r2 | 3 | 2 | 1.00 |
| r2 vs r3 | 5 | 3 | 0.73 |
| base vs r3 | 6 | 3 | 0.51 |

![pass@k valid](figures/passk_minif2f_valid.png)

*Figure 5. Unbiased pass@k (n=8) on miniF2F-valid for the base and each EI round, from the same verification files as Figure 4.*

### 6.3 Verifier quality

![verifier ceiling](figures/lean_verifier_ceiling.png)

*Figure 6. Pre-registered ceiling test, 2026-10-12 (`docs/evidence/lean_ceiling_2026-10-12/registered.log`,
`result.json`, table sha256 `61636c71…`).*

| Check | Result |
|---|---|
| Known-good accepted (Lean-workbook-proofs slice) | 177/178 = 99.44%, Wilson 95% [96.89, 99.90]. The one miss is a 180 s timeout. |
| Adversarial accepted | 0/61. A naive compile-only check accepts 51/61. |
| Frozen verifier `f1dd9e78` (2026-10-19) | 178/179 known-good (`docs/SOTA_PLAN.md` 4.3; the artefact is untracked) |
| Throughput, 8 warm workers | 0.57 proofs/s on unique statements (p50 1.97 s, p90 21.4 s); 4.38 proofs/s in the GRPO shape (12 statements × 8 samples) |
| vs Kimina Lean server, 741 items (`docs/results/kimina_agreement_report.json`) | 485/485 strict accepts pass Kimina as well. Kimina compile-only passes 40 adversarial items that strict rejects. 0 Kimina false rejects. Kimina is not adopted: the gated pipeline is about 52% slower. |

### 6.4 Systems measurements (`docs/MEASUREMENTS.md`)

![MoE dispatch](figures/moe_dispatch_bench.png)

*Figure 7. One MoE layer at OLMoE shape (E=64, top-8, d=2048, bf16), forward+backward median of 10 runs, from
`docs/MEASUREMENTS.md` section (c). `torch._grouped_mm` takes the fallback path on sm_86 and is only 1.06-1.13× faster than the loop.*

| Measurement | Value |
|---|---|
| 2-rank FSDP2 + adamw8bit, SIGTERM to one rank, then resume | Final params bit-identical (0 of 2,885,888 elements differ). A negative control with swapped optimizer shards is detected. |
| NaN on one rank | Both ranks halt with exit 81 within about 1.3 s, with no NCCL hang |
| OLMoE-1B-7B, 4-GPU FSDP2 SFT | 14.79 s per micro-step; 277 padded tok/s; 0.53 TFLOP/s per GPU. 92% of the step is NCCL over SHM. |
| OLMoE SIGTERM, supervisor relaunch, resume | Max |Δloss| 3.3e-3 against a run-to-run floor of 2.9e-3 (tolerance 1.09e-2). Identical batch rows on all 320 rank×micro-step pairs (4 ranks × 80 micro-steps). |
| Qwen3-8B LoRA SFT throughput (`configs/p2_sft.toml`) | 2,152 padded tok/s at 16,384-token micro-batches; 15.84 GiB allocated peak |
| vLLM generation, TP=4 (`docs/evidence/p2_baseline_2026-10-13/gen_minif2f_c16384.jsonl.manifest.json`) | 876 tok/s end to end on the 16k miniF2F-test baseline: 9,605,934 tokens, 1,952 samples in 10,966 s (3.05 h) |

## 7. Results discussion and lessons

* **Expert iteration on a strong prover was flat.** Round 1 matched the base exactly at solved@8 (188 vs 188,
  2 discordant each way), and later rounds drifted down without significance. Three explanations are consistent
  with the data, and none is tested in isolation: (a) the SFT data was the model's own short verified proofs, mostly
  on problems it already solved; (b) never-solved problems were never selected (0 in every round); (c) the 0.7/0.3
  weight averaging toward the base damps any change. The flat result led the plan to drop more rounds and move to
  repair/feedback arms.
* **A real nondeterminism bug that only real weights could show.** bf16 `index_add_` atomics in the MoE combine
  picked different expert sets on identical inputs: 5 of 5 repeats were distinct, and the step-1 grad norm was
  under-reported by up to 2.7×. A fixed-order combine with fp32 accumulation fixed it, and repeats became bit-identical.
* **Silent rank duplication.** Dense `sft.py` / `pretrain.py` gave every rank the same batches, so 4 GPUs trained like 1.
  This is fixed with a `DistributedBatchSampler`. Before the fix, multi-GPU dense SFT results from this tree are invalid.
* **Scheduler bug in the predecessor.** The predecessor trainer (nano-mistral-o1) logged a decaying LR but never
  applied it. All of its runs used a constant LR. align applies the scheduled LR and has a test that pins it, so align
  runs are not LR-comparable to nano-mistral-o1 runs.
* **This PCIe box is comm-bound.** FSDP costs 24× / 10× / 5.6× the compute time at 1k / 4k / 8k-token micro-batches.
  The cheapest fix is a larger micro-batch, not custom GEMM kernels.
* **Evaluation protocol matters at the 1-3 problem scale.** Protocol choices are about the same size as the effects
  measured: on miniF2F-test, the cap alone (16k vs 40k) moves pass@8 from 78.7% to 79.7%, about 2 problems, while the EI
  effects were 0-3 problems. A 300 s re-check of 82 samples that timed out at 180 s recovered none.

## 8. Intended use, limitations, risks

* **Intended use:** research on verifier-in-the-loop post-training for Lean 4 provers on small clusters, and as a
  reference implementation of the listed objectives with tests (168 entries in `code/tests/` at the shipped snapshot; 1,608 CPU tests passed at
  `654c20c`, per the repo README).
* **Not measured:** GRPO, CISPO, PPO and DPO on GPUs with this tree; multi-turn Lean RL; the native paged-KV and TP
  engines on GPU; `kill -9` during a save; expert parallelism end to end; full-parameter fine-tuning of a 7-8B dense model (campaign1 used LoRA); LBL-on versus LBL-off.
* **Limitations:** the PPO config has unresolved `[TBD]` fields, and the PRM checkpoint it needs does not exist.
  GRPO resume is not wired into `scripts/grpo.py`. Distinct ranks still write to the same `history.jsonl` (rank-local
  logging). There is no OS sandbox on the default verifier path: a sandbox exists, but it is not wired in.
* **Risks:** a Lean verifier can be fooled. The adversarial set is 61 items, and an upstream kernel issue
  (lean4#14576) has not been tested against this pin. Do not treat "accepted" as a proof of correctness without
  independent re-checking.
* **Host safety:** the jobs assume `scripts/hostguard.py` cgroup caps. Running them without the caps on a shared box can OOM it.

## 9. Reproducibility

```bash
git clone align.bundle align && cd align        # or use code/ (commit f8dfa503); see the campaign note below
uv venv .venv && uv pip install -e ".[dev]"     # torch, triton, numpy, safetensors, pytest
.venv/bin/python -m pytest tests/ -q -m "not gpu and not oracle and not slow"

# Lean toolchain (Lean 4.9.0-rc1, Mathlib d1d1e4b7, REPL v4.9.0-rc1)
bash scripts/lean_setup.sh
.venv/bin/python scripts/lean_ceiling_test.py           # verifier ceiling (pre-registered table)

# Baseline eval (vLLM in its own venv)
.venv/bin/python scripts/p2/launch_baseline.py ...      # see docs/P2.md
.venv/bin/python scripts/p2/eval_report.py ...          # pass@k, bootstrap, McNemar

# Expert iteration campaign (4 GPUs). REQUIRES commit >= de55434 -- NOT in this snapshot.
# scripts/p2/campaign.sh was added after f8dfa503 (in 2eb6baa), so this line will not run from code/.
bash scripts/p2/campaign.sh                             # wraps scripts/p2/expert_iteration.py, configs/p2_sft.toml
```

| Item | Value |
|---|---|
| Code snapshot in this repo | `f8dfa503f15d4498f43a6e7e579d450f0869bc95` (2026-10-19) |
| Code that produced campaign1 | local tree at or after `de55434` (2026-10-24; the fix that let round-1 train). Not in this snapshot: re-upload needed. Local HEAD at card time: `4a6a9f6`. |
| Pre-registration | `docs/PREREG_SOTA.md`, `docs/evidence/prereg/prereg_sota_v1.json` (file sha256 `172b0c48…`); bundle digest `58bb39ed…` recorded in `prereg_sota_v1.sha256.txt` (OpenTimestamped, `.ots`) |
| Model revisions | Goedel-Prover-V2-8B `dfd02e62`; OLMoE-1B-7B-0125 `9b0c1aa8` |
| Raw hashes | `docs/evidence/*/raw_sha256.txt` |

Note: the HF snapshot predates the campaign1 code and results. Run outputs (`runs/`) are not in this repository.

## 10. Related repositories, licence, citation

* Expert-iteration checkpoints: [Goedel-Prover-V2-8B-EI-campaign1-r1](https://huggingface.co/viai957/Goedel-Prover-V2-8B-EI-campaign1-r1),
  [-r2](https://huggingface.co/viai957/Goedel-Prover-V2-8B-EI-campaign1-r2), [-r3](https://huggingface.co/viai957/Goedel-Prover-V2-8B-EI-campaign1-r3)
* Data: [viai957/lean-prover-data](https://huggingface.co/datasets/viai957/lean-prover-data)
* Predecessors (the code that align consolidates): [nano-mistral-o1-sft](https://huggingface.co/viai957/nano-mistral-o1-sft),
  [nano-mistral-o1-dpo-arm-a](https://huggingface.co/viai957/nano-mistral-o1-dpo-arm-a), [nano-mistral-o1-dpo-arm-b](https://huggingface.co/viai957/nano-mistral-o1-dpo-arm-b),
  [nano-mistral-o1-grpo-stageb-step48](https://huggingface.co/viai957/nano-mistral-o1-grpo-stageb-step48),
  [mistral-7b-v0.3-prm800k-prm-ppo-math](https://huggingface.co/viai957/mistral-7b-v0.3-prm800k-prm-ppo-math)
* Downstream: [Goedel-Prover-V2-8B-VLG-planner-sft-lora](https://huggingface.co/viai957/Goedel-Prover-V2-8B-VLG-planner-sft-lora)

**Licence.** Code is Apache-2.0 (`code/LICENSE`); attributions are in `code/NOTICE`. The GRPO loss is vendored from
allenai/open-instruct (Apache-2.0). Statement sources: Goedel-Pset-v1 and RL-Goedel-Pset-Level-4-5 are MIT;
FormalMATH-All is MIT; NuminaMath-LEAN-Sol is Apache-2.0; **Nemotron-Math-Proofs-v1 is CC-BY-SA-4.0 (share-alike)**.
Goedel-Prover-V2-8B is Apache-2.0. miniF2F is MIT and is used for evaluation only.

```bibtex
@misc{align2026,
  title        = {align: a torch-only post-training stack with a Lean 4 verifier in the loop},
  author       = {viai957},
  year         = {2026},
  howpublished = {\url{https://huggingface.co/viai957/align}},
  note         = {Code snapshot f8dfa503; expert-iteration campaign1 results (negative)}
}
```