8.2 KiB
library_name, pipeline_tag, base_model, base_model_relation, language, tags, datasets
| library_name | pipeline_tag | base_model | base_model_relation | language | tags | datasets | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| transformers | text-generation | Qwen/Qwen3-8B-Base | finetune |
|
|
|
Lean Standard Prover — Qwen3-8B
Paper model: S8 + reasoning · Stage: After informal reasoning
Generates complete Lean proofs from theorem statements using the standard prover response format. This variant writes an informal reasoning plan before each proof attempt.
Hugging Face Transformers
Load the published weights from the Hub and generate on your GPU:
pip install 'transformers==4.57.3' accelerate torch
hf download EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo example_transformers.py inference.py prompt_utils.py Example.lean --local-dir lean-standard-prover-qwen3-8b-reasoning-grpo
cd lean-standard-prover-qwen3-8b-reasoning-grpo
python example_transformers.py
The included Example.lean is the input; replace it with your own imports,
context, and theorem ending in by sorry:
import Mathlib
theorem demo (n : ℕ) : n + 0 = n := by sorry
The complete Transformers example is:
from pathlib import Path
import torch
from transformers import AutoModelForCausalLM, AutoTokenizer, set_seed
from inference import build_prompt
MODEL_ID = 'EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo'
source = Path("Example.lean").read_text(encoding="utf-8")
prompt = build_prompt(source)
tokenizer = AutoTokenizer.from_pretrained(MODEL_ID)
model = AutoModelForCausalLM.from_pretrained(
MODEL_ID, dtype=torch.bfloat16, device_map="auto", attn_implementation="sdpa",
).eval()
inputs = tokenizer(prompt, return_tensors="pt", add_special_tokens=False).to(model.device)
prompt_length = inputs["input_ids"].shape[1]
budget = min(2048, 32768 - prompt_length)
if budget <= 0:
raise ValueError("The prompt must leave room for a proof in the 32,768-token context.")
set_seed(0)
with torch.inference_mode():
output = model.generate(
**inputs, max_new_tokens=budget, do_sample=True,
temperature=0.3, top_p=0.95, top_k=0, min_p=0.0,
repetition_penalty=1.0, num_beams=1,
pad_token_id=tokenizer.pad_token_id,
)
response = tokenizer.decode(output[0, prompt_length:], skip_special_tokens=True)
print(response, end="")
build_prompt supplies this checkpoint's exact raw completion prompt.
Tokenization uses add_special_tokens=False; the context budget is 32,768
tokens. This compact example allows up to 2,048 generated tokens and prints
only the generated response.
Example output
Recorded with the script above on an H100 in BF16, using seed 0, temperature 0.3, and top-p 0.95. This is the extracted final proof, checked with Lean 4.15 and Mathlib:
import Mathlib
theorem demo (n : ℕ) : n + 0 = n := by
induction n with
| zero => rfl
| succ n ih => simp_all
Full generated response
[Problem Restatement]
For every natural number \(n\), adding zero to \(n\) leaves \(n\) unchanged. In symbols, the claim is
\[
n + 0 = n.
\]
This is one of the basic properties of addition on the natural numbers.
[Useful Observations]
1. **Zero is the additive identity.** In any algebraic structure with addition, the element \(0\) is defined by the property that adding it to any element does not change that element. For natural numbers, this is exactly the statement \(n + 0 = n\).
2. **Natural numbers are built recursively.** The natural numbers are generated from \(0\) by repeatedly applying the successor operation. This means any proof about all natural numbers can be reduced to checking the base case \(n = 0\) and then verifying that the property is preserved when moving from \(n\) to \(n+1\).
3. **The successor case is immediate.** If we already know \(n + 0 = n\), then adding one more zero gives \((n+1) + 0 = n+1\). This is just the same identity applied to the successor of \(n\).
[Reasoning Path]
To prove \(n + 0 = n\) for all natural numbers, we use the recursive definition of the natural numbers.
- **Base case:** When \(n = 0\), the statement becomes \(0 + 0 = 0\), which is true by the definition of addition.
- **Inductive step:** Assume the statement holds for some natural number \(n\), i.e., \(n + 0 = n\). We must show it holds for \(n+1\), i.e., \((n+1) + 0 = n+1\). But \((n+1) + 0\) is just \(n+1\) by the definition of addition, so the statement is true for \(n+1\) as well.
Since both the base case and the inductive step are immediate, the identity holds for every natural number \(n\).
[Key Derivation]
The entire derivation is captured by the two equations:
\[
0 + 0 = 0,
\]
and
\[
(n+1) + 0 = n+1.
\]
These are exactly the base and successor cases of the recursive definition of addition on natural numbers.
[Proof Type]
This is a direct proof by induction on the natural number \(n\).
[Formal Anchors]
The Lean proof uses induction on \(n\):
```lean4
induction n with
| zero => rfl
| succ n ih => ...
```
The base case is closed by reflexivity (`rfl`), and the successor case follows from the induction hypothesis (`ih`) together with the simplifier (`simp`), which uses the recursive definition of addition.
[Final Solution]
We prove that \(n + 0 = n\) for every natural number \(n\) by induction.
- For \(n = 0\), we have \(0 + 0 = 0\), which is true.
- Assume \(n + 0 = n\). Then \((n+1) + 0 = n+1\), which is also true.
By induction, \(n + 0 = n\) for all natural numbers \(n\).
The complete typechecked Lean 4 proof is:
```lean4
import Mathlib
theorem demo (n : ℕ) : n + 0 = n := by
induction n with
| zero => rfl
| succ n ih => simp_all
```
Full response · Input/output JSON · Lean proof
vLLM
For multiple samples and longer output budgets:
pip install 'vllm==0.12.0'
hf download EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo inference.py prompt_utils.py Example.lean --local-dir lean-standard-prover-qwen3-8b-reasoning-grpo
python lean-standard-prover-qwen3-8b-reasoning-grpo/inference.py lean-standard-prover-qwen3-8b-reasoning-grpo/Example.lean --samples 1
The vLLM runner uses the same raw prompt. Its default temperature is 0.3
for one sample and 0.7 for 32 samples; top-p is 0.95. Output tokens fit
within the context remaining after the prompt. Use --print-prompt to
inspect the exact input without loading weights.
Prompt template
The reasoning template follows evaluate_prover_model_run.py.
Replace the placeholder with the imports, context, and theorem ending in
by sorry, and keep the final newline:
Solve the following problem with Lean 4 code and explanatory comments:
```lean4
{formal_statement_with_imports}
```
Replace every sorry statement with an appropriate proof. Before writing any Lean code, give an informal solution with the sections [Problem Restatement], [Useful Observations], [Reasoning Path], [Key Derivation], [Proof Type], [Formal Anchors] and [Final Solution]. Then provide the complete solution in the lean4 code block. If a previous attempt failed, first give [Error Analysis], [Revised Reasoning] and [Updated Proof Plan], then provide the corrected solution.
Expected response
The requested informal-solution sections precede the Lean proof. A repair begins with [Error Analysis], [Revised Reasoning], and [Updated Proof Plan].
The response contains a complete proof in a lean4 code fence, together with explanatory text or comments.
Use the last complete Lean code block as the final proof candidate for Lean verification. The vLLM runner returns the full response, extracted lean_code, and finish_reason as JSONL.