FrenzyMath/REAL-Prover
REAL-Prover by FrenzyMath is a 7.6 billion parameter retrieval-augmented, stepwise theorem prover for Lean 4, built upon Qwen2.5-Math-7B. It features a retrieval module (Leansearch-PS) to fetch relevant theorems from the Lean math library, enhancing its formal reasoning capabilities. With a context length of 131072 tokens, this model is specifically designed for advanced mathematical reasoning and proof generation within the Lean formal system.
Loading preview...
REAL-Prover: Retrieval Augmented Lean Prover
REAL-Prover, developed by FrenzyMath, is a 7.6 billion parameter language model specifically engineered for formal mathematical reasoning within the Lean 4 theorem prover. Built on Qwen2.5-Math-7B, it integrates a novel retrieval-augmented generation pipeline to enhance its proof-generating capabilities.
Key Capabilities
- Retrieval-Augmented Reasoning: Utilizes a retrieval module, Leansearch-PS, to dynamically fetch relevant theorems from the Lean math library, significantly improving the quality and accuracy of generated proofs.
- Stepwise Theorem Proving: Designed to generate proofs in a step-by-step manner, making the reasoning process more transparent and verifiable.
- Custom Training: Fine-tuned using a specialized pipeline and dataset, including data synthesized in an interactive environment (Jixia-interactive).
- Comprehensive Evaluation: Assessed on established benchmarks like ProofNet and a newly proposed benchmark, FATE-M, to validate its performance in formal mathematics.
Good for
- Automated Theorem Proving in Lean 4: Ideal for researchers and developers working on automating proof generation within the Lean 4 ecosystem.
- Mathematical Research: Supports advanced mathematical reasoning tasks requiring formal verification.
- Developing AI for Formal Systems: Provides a robust foundation for exploring retrieval-augmented approaches in symbolic AI and formal methods.