Goedel-Code-Prover-8B, developed by Zenan Li et al., is an 8 billion parameter model based on Qwen3-8B, specialized in Lean 4 proof generation and decomposition for code correctness verification. It excels at breaking down complex formal specifications into smaller, manageable lemmas and then composing these to prove the target theorem. This model is primarily designed for automated theorem proving within a decompose-then-verify scaffolding, aiming to generate complete, verifiable proofs without manual intervention.
Loading preview...
Goedel-Code-Prover-8B Overview
Goedel-Code-Prover-8B is an 8 billion parameter model, built upon the Qwen3-8B architecture, specifically fine-tuned for Lean 4 theorem proving and proof decomposition. Developed by Zenan Li et al., this model's core innovation lies in its ability to hierarchically search for proofs by breaking down complex formal problems into smaller, more manageable lemmas.
Key Capabilities
- Proof Decomposition: Automatically analyzes a Lean 4 formal problem and decomposes it into a series of small, self-contained lemmas.
- Theorem Proving: Generates complete Lean 4 proofs by composing the introduced lemmas, aiming for proofs without any
sorrystatements. - Code Verification: Designed to integrate into a decompose-then-verify workflow, where generated proofs can be compiled and checked for correctness against a Lean 4 server.
- Reinforcement Learning: Utilizes GRPO reinforcement learning with online Lean 4 verification rewards to enhance proof generation quality.
Good for
- Automating the verification of code correctness using Lean 4 formal specifications.
- Assisting in the creation of complex mathematical and software proofs by providing a structured decomposition approach.
- Researchers and developers working with formal methods and theorem proving in the Lean 4 ecosystem.
For more technical details, refer to the associated paper: Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification.