EPFL-LARA/lean-world-model-qwen3-4b-grpo
The EPFL-LARA/lean-world-model-qwen3-4b-grpo is a 4 billion parameter Qwen3-based model developed by EPFL-LARA, specifically designed for generating Lean proofs. This model incorporates predicted goal states and compiler diagnostics within inline comments, and supports repair attempts within a single response. It is optimized for formal theorem proving, offering a specialized solution for generating and refining Lean 4 code.
Loading preview...
Lean World-Model Prover — Qwen3-4B
This model, developed by EPFL-LARA, is a 4 billion parameter Qwen3-based language model specifically engineered for formal theorem proving in Lean 4. It operates as a "world-model" (WM4) and has undergone a GRPO (Goal-Reinforced Proof Optimization) stage, enabling it to generate Lean proofs with advanced features.
Key Capabilities
- Lean Proof Generation: Generates Lean 4 code to solve mathematical theorems, replacing
sorrystatements with complete proofs. - Contextual Feedback: Provides predicted goal states and compiler diagnostics directly within inline comments (
/- <feedback> ... </feedback> -/) in the generated proof. - Proof Repair: Supports iterative repair attempts within a single response, allowing the model to refine proofs based on feedback.
- High Context Length: Utilizes a 32,768-token context window, accommodating complex theorem statements and proof structures.
Good For
- Automated Theorem Proving: Ideal for researchers and developers working on automating proof generation in Lean 4.
- Educational Tools: Can be used to assist students and practitioners in understanding proof structures and compiler feedback.
- Lean 4 Development: Useful for generating initial proof candidates or suggesting improvements for existing Lean 4 codebases.
This model is particularly suited for tasks requiring precise, verifiable mathematical proofs and offers a specialized approach to interacting with the Lean 4 theorem prover.