juihuichung/awakening-goedel-v2-32b-sft
The awakening-goedel-v2-32b-sft model by juihuichung is a 32 billion parameter Qwen3-based language model fine-tuned on approximately 860,000 Lean-4 proof examples. This model is the supervised fine-tuning (SFT) base from a capability-recovery study, demonstrating strong Lean-4 theorem proving abilities. However, its tool-calling functionality has significantly collapsed, making it unsuitable for tasks requiring external tool use.
Loading preview...
Model Overview
The awakening-goedel-v2-32b-sft is a 32 billion parameter model developed by juihuichung, based on the Qwen3 architecture. It represents the supervised fine-tuning (SFT) stage of the Goedel-Prover-V2-32B project, specifically checkpoint-4000. This model was fine-tuned using approximately 860,000 Lean-4 proof examples, making it a strong performer in Lean-4 theorem proving.
Key Characteristics
- Lean-4 Proving: Demonstrates robust capabilities in generating Lean-4 proofs.
- Tool-Calling Collapse: A notable characteristic is the significant collapse of its tool-calling functionality. It scores BFCL Non-Live 4.6 / Multi-Turn 0.0, with approximately 96% irrelevance in function calls, meaning it largely refuses to use tools.
- Research Context: This model serves as the "before" state in a capability-recovery study, where subsequent agentic replay (e.g.,
awakening-sft-replay100) aims to restore tool-use capabilities.
Use Cases
- Lean-4 Theorem Proving: Ideal for research and applications focused on automated theorem proving within the Lean-4 framework.
- Research on Tool-Use Recovery: Valuable as a baseline model for studies investigating methods to recover or improve tool-calling abilities in fine-tuned language models.
Limitations
- No Tool Use: Due to its collapsed tool-calling ability, this model is not suitable for tasks requiring interaction with external tools or APIs.