EPFL-LARA/lean-standard-prover-qwen3-8b-sft
EPFL-LARA/lean-standard-prover-qwen3-8b-sft is an 8 billion parameter model developed by EPFL-LARA, fine-tuned to generate complete Lean proofs from theorem statements. Built on the Qwen3 architecture, it utilizes a 32,768-token context window and outputs proofs in the standard Lean prover response format. This model is specifically designed for formal theorem proving in Lean 4, providing automated proof generation for mathematical and logical statements.
Loading preview...
Overview
EPFL-LARA/lean-standard-prover-qwen3-8b-sft is an 8 billion parameter language model developed by EPFL-LARA, specifically fine-tuned for automated theorem proving in Lean 4. It generates complete Lean proofs from given theorem statements, adhering to the standard prover response format. This model is built upon the Qwen3 architecture and supports a substantial context length of 32,768 tokens, allowing for complex theorem statements and detailed proof generation.
Key Capabilities
- Lean Proof Generation: Generates full Lean 4 proofs from theorem statements, including necessary imports and context.
- Standard Format Adherence: Produces output in the expected format for Lean provers, making it directly usable for verification.
- High Context Window: Utilizes a 32,768-token context, accommodating lengthy problem descriptions and proof steps.
- Integration with Transformers and vLLM: Provides clear examples and scripts for deployment with popular inference libraries.
Good for
- Automated Theorem Proving: Researchers and developers working on formal verification and mathematical proofs in Lean 4.
- Proof Assistant Automation: Assisting users of the Lean proof assistant by generating initial or complete proofs.
- Educational Tools: Creating tools for learning formal methods and theorem proving by demonstrating proof structures.
- Research in AI for Mathematics: Exploring the capabilities of LLMs in generating verifiable mathematical proofs.