juihuichung/awakening-goedel-v2-32b-sft

awakening-goedel-v2-32b-sft

The collapsed SFT base of the capability-recovery study "Minimal Agentic Replay Recovers Tool Use in Formal-Math Fine-Tuned LLMs" (COLM 2026): Qwen3-32B fine-tuned on ~860k Lean-4 proof examples (the SFT stage of Goedel-Prover-V2-32B, checkpoint-4000). Strong Lean-4 prover, but tool-calling has fully collapsed: BFCL Non-Live 4.6 / Multi-Turn 0.0, ~96% irrelevance (refuses essentially every function call). Qwen3-32B, its original base, scores 89.4 / 46.4.

This is the "before" model of the study — 100 agentic traces (awakening-sft-replay100) recover Non-Live to 83.8.

Related

• —Code, data manifests, training recipes, eval scripts: github.com/juihuichung/awakening
• —Training data: juihuichung/awakening-data
• —Models: awakening-goedel-v2-32b-sft · awakening-goedel-v2-32b-rl · awakening-sft-replay100 · awakening-rl-replay100