uw-math-ai/gAPRIL-wo-exp
uw-math-ai/gAPRIL-wo-exp is an 8 billion parameter LoRA fine-tuned variant of Goedel-Prover-V2-8B, developed by uw-math-ai. This model specializes in Lean 4 proof repair, directly correcting erroneous proofs given compiler feedback. It is optimized for single-shot repair accuracy by training exclusively on the repair objective without explanation supervision, achieving 36.7% pass@1 on the APRIL test set. Its primary use is to automatically fix errors in Lean proofs.
Loading preview...
uw-math-ai/gAPRIL-wo-exp: Lean Proof Repair (Repair Only)
This model is an 8 billion parameter LoRA fine-tune of the Goedel-Prover-V2-8B base model, developed by uw-math-ai. It is specifically designed for Lean 4 proof repair, taking an erroneous Lean proof and compiler feedback to directly produce a corrected proof.
Key Capabilities & Features
- Proof Repair Specialization: Exclusively trained on the repair objective using the APRIL dataset, which contains 260K paired erroneous/correct Lean proofs with compiler diagnostics.
- High Single-Shot Accuracy: Achieves a 36.7% pass@1 accuracy on the full APRIL test set for proof repair, outperforming its base model (15.5%) and a 32B Goedel variant (26.8%).
- No Explanation Supervision: Unlike its counterpart gAPRIL-w-exp, this model maximizes repair accuracy by not generating human-interpretable diagnostics or explanations, focusing solely on the corrected proof output.
- Context Length: Supports a context length of 32768 tokens, allowing for comprehensive proof analysis.
When to Use This Model
This model is ideal for automated systems or developers who require direct, high-accuracy correction of Lean 4 proofs without the need for accompanying explanations. It excels in scenarios where the primary goal is to fix the proof efficiently and effectively, leveraging compiler feedback to generate the corrected code block.