viai957/proofforge-goedel8b-e2e-smoke-checkpoints

Text Generation • Updated 10 days ago

Note Start here. 2026-10-26: SFT -> DPO -> RLVR on Goedel-Prover-V2-8B, 4x L4. Last checkpoint of each stage, with optimizer state. Showed the whole pipeline runs and resumes. Smoke scale, no benchmark claim.

viai957/proofforge-goedel8b-sft-lora-e2e-smoke

Text Generation • Updated 10 days ago • 35 • 1

Note The final SFT adapter of that run: 320 self-generated, Lean-verified proofs, 80 steps. Parent of the DPO adapter and of both HPO members.

Note The data behind it: 7,803 base-model proof attempts on 980 Goedel-Pset statements, each with its Lean verdict (4,007 valid). Every prompt re-checked token by token: 0 mismatches.

viai957/Goedel-Prover-V2-8B-EI-campaign1-r1

Text Generation • 8B • Updated 10 days ago • 746

Note Context: the Goedel line's real training run. Expert iteration round 1 scored 188/226 on miniF2F-valid, the same as the base. That null, and the move to Nemotron-3-Nano, closed the Goedel line.