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.