uw-math-ai/gAPRIL-w-exp
uw-math-ai/gAPRIL-w-exp is an 8 billion parameter LoRA finetune of Goedel-Prover-V2-8B, developed by uw-math-ai. This model specializes in Lean 4 proof repair, generating natural-language explanations for errors, suggesting fixes, and providing corrected proofs. It was trained on the APRIL dataset, comprising 260K paired erroneous/correct Lean proofs with compiler diagnostics and LLM-generated explanations. Its primary strength lies in jointly repairing Lean proofs and explaining the underlying issues.
Loading preview...
Overview
uw-math-ai/gAPRIL-w-exp is an 8 billion parameter model developed by uw-math-ai, specifically designed for Lean 4 proof repair with natural-language explanations. It is a LoRA finetune of the Goedel-Prover-V2-8B base model, trained on the comprehensive APRIL dataset.
Key Capabilities
- Joint Proof Repair and Explanation: Given an erroneous Lean proof and compiler feedback, the model diagnoses the failure, suggests a fix, and provides a corrected proof, all while generating a human-interpretable explanation.
- Lean 4 Specific: Optimized for Lean 4.22.0-rc4, making it highly relevant for developers working with this proof assistant.
- Performance: Achieves a single-shot proof repair accuracy (pass@1) of 34.6% on the full APRIL test set, outperforming the base Goedel-8B (15.5%) and Goedel-32B (26.8%) models. While joint explanation training slightly reduces repair accuracy compared to a repair-only variant (36.7%), it provides valuable diagnostic insights.
Good For
- Automated Lean Proof Debugging: Developers needing to automatically identify and correct errors in Lean 4 proofs.
- Educational Tools: Generating explanations for proof failures, aiding in understanding and learning Lean 4.
- Augmenting Other Models: Providing human-interpretable diagnostics that can be used to enhance other proof-related AI systems.
- Research in Formal Verification: Exploring the intersection of LLMs and formal methods, particularly in proof repair and explanation generation.