GLM-5.3 is live. Run Z.ai's latest model on Friendli Model APIs. Try it today ➜
EPFL-LARA
Available on FriendliAI
Run this model inference on single tenant GPU with unmatched speed and reliability at scale.
Model Details
Model Provider
EPFL-LARA
Model Tree
Qwen/Qwen3-8B-Base
Input Modalities
Output Modalities
Supported Functionality
Load the published weights from the Hub and generate on your GPU:
bash
pip install 'transformers==4.57.3' accelerate torchhf download EPFL-LARA/lean-world-model-qwen3-8b-reasoning-grpo example_transformers.py inference.py prompt_utils.py Example.lean --local-dir lean-world-model-qwen3-8b-reasoning-grpocd lean-world-model-qwen3-8b-reasoning-grpopython example_transformers.pyThe included Example.lean is the input; replace it with your own imports,
context, and theorem ending in by sorry:
lean4
import Mathlib theorem demo (n : ℕ) : n + 0 = n := by sorryThe complete Transformers example is:
python
from pathlib import Path import torchfrom transformers import AutoModelForCausalLM, AutoTokenizer, set_seed from inference import build_prompt MODEL_ID = 'EPFL-LARA/lean-world-model-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.
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:
lean4
import Mathlib -- Theorem: For any natural number n, n + 0 = ntheorem demo (n : ℕ) : n + 0 = n := by -- Use the reflexivity of equality to show that n + 0 equals n /- <feedback> -- proof state: n : ℕ ⊢ n + 0 = n </feedback> -/ simp [Nat.add_zero]text
[Problem Restatement] For every natural number \(n\), adding zero to \(n\) leaves it unchanged: \[n+0=n.\] [Useful Observations] - The statement is the basic identity law for addition.- It holds for every natural number, including \(0\).- No special assumptions or case distinctions are needed.- The natural way to prove it is to recognize that \(0\) is the additive identity. [Reasoning Path] The claim says that if we start with any natural number \(n\), then adjoining zero to it does not change the value. This is one of the defining properties of zero in the natural numbers: zero is the neutral element for addition. So the proof is immediate. We take an arbitrary natural number \(n\), and use the fact that adding zero to any number returns that same number. There is no need to transform the expression, introduce another variable, or split into cases. The equality is true by the basic arithmetic identity for addition. [Key Derivation] For any natural number \(n\), \[n+0 = n.\] This is exactly the additive identity law. [Proof Type] Direct proof by the identity property of zero in natural-number addition. [Formal Anchors] The Lean proof uses the standard simplification fact: ```lean4Nat.add_zero n``` which states that for every natural number \(n\), ```lean4n + 0 = n``` The proof is completed by simplification: ```lean4simp [Nat.add_zero]``` [Final Solution] Let \(n\) be any natural number. By the defining property of zero as the additive identity, adding zero to a number does not change it. Therefore, \[n+0=n.\] Since this holds for every natural number \(n\), the claim is proved. Here is the complete Lean 4 proof annotated with Lean 4 compiler feedback blocks: ```lean4import Mathlib -- Theorem: For any natural number n, n + 0 = ntheorem demo (n : ℕ) : n + 0 = n := by -- Use the reflexivity of equality to show that n + 0 equals n /- <feedback> -- proof state: n : ℕ ⊢ n + 0 = n </feedback> -/ simp [Nat.add_zero]```Full response · Input/output JSON · Lean proof
For multiple samples and longer output budgets:
bash
pip install 'vllm==0.12.0'hf download EPFL-LARA/lean-world-model-qwen3-8b-reasoning-grpo inference.py prompt_utils.py Example.lean --local-dir lean-world-model-qwen3-8b-reasoning-grpopython lean-world-model-qwen3-8b-reasoning-grpo/inference.py lean-world-model-qwen3-8b-reasoning-grpo/Example.lean --samples 1The 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.
The reasoning with feedback 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:
text
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, annotated with Lean 4 compiler feedback blocks in the form `/- <feedback> ... </feedback> -/` at the appropriate locations. If a previous attempt failed, first give [Error Analysis], [Revised Reasoning] and [Updated Proof Plan], then provide the corrected solution, annotated with Lean 4 compiler feedback blocks in the form `/- <feedback> ... </feedback> -/` at the appropriate locations.The requested informal-solution sections precede the Lean proof. A repair begins with [Error Analysis], [Revised Reasoning], and [Updated Proof Plan].
Proofs appear in lean4 code fences with /- <feedback> ... </feedback> -/ comments containing predicted goal states and diagnostics. A response can contain successive corrected proof attempts.
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.
pip install 'transformers==4.57.3' accelerate torchhf download EPFL-LARA/lean-world-model-qwen3-8b-reasoning-grpo example_transformers.py inference.py prompt_utils.py Example.lean --local-dir lean-world-model-qwen3-8b-reasoning-grpocd lean-world-model-qwen3-8b-reasoning-grpopython example_transformers.pyimport Mathlib theorem demo (n : ℕ) : n + 0 = n := by sorryfrom pathlib import Path import torchfrom transformers import AutoModelForCausalLM, AutoTokenizer, set_seed from inference import build_prompt MODEL_ID = 'EPFL-LARA/lean-world-model-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="")import Mathlib -- Theorem: For any natural number n, n + 0 = ntheorem demo (n : ℕ) : n + 0 = n := by -- Use the reflexivity of equality to show that n + 0 equals n /- <feedback> -- proof state: n : ℕ ⊢ n + 0 = n </feedback> -/ simp [Nat.add_zero][Problem Restatement]For every natural number \(n\), adding zero to \(n\) leaves it unchanged:\[n+0=n.\][Useful Observations]- The statement is the basic identity law for addition.- It holds for every natural number, including \(0\).- No special assumptions or case distinctions are needed.- The natural way to prove it is to recognize that \(0\) is the additive identity.[Reasoning Path]The claim says that if we start with any natural number \(n\), then adjoining zero to it does not change the value. This is one of the defining properties of zero in the natural numbers: zero is the neutral element for addition.So the proof is immediate. We take an arbitrary natural number \(n\), and use the fact that adding zero to any number returns that same number. There is no need to transform the expression, introduce another variable, or split into cases. The equality is true by the basic arithmetic identity for addition.[Key Derivation]For any natural number \(n\),\[n+0 = n.\]This is exactly the additive identity law.[Proof Type]Direct proof by the identity property of zero in natural-number addition.[Formal Anchors]The Lean proof uses the standard simplification fact:```lean4Nat.add_zero n```which states that for every natural number \(n\),```lean4n + 0 = n```The proof is completed by simplification:```lean4simp [Nat.add_zero]```[Final Solution]Let \(n\) be any natural number. By the defining property of zero as the additive identity, adding zero to a number does not change it. Therefore,\[n+0=n.\]Since this holds for every natural number \(n\), the claim is proved.Here is the complete Lean 4 proof annotated with Lean 4 compiler feedback blocks:```lean4import Mathlib-- Theorem: For any natural number n, n + 0 = ntheorem demo (n : ℕ) : n + 0 = n := by -- Use the reflexivity of equality to show that n + 0 equals n /- <feedback> -- proof state: n : ℕ ⊢ n + 0 = n </feedback> -/ simp [Nat.add_zero]```pip install 'vllm==0.12.0'hf download EPFL-LARA/lean-world-model-qwen3-8b-reasoning-grpo inference.py prompt_utils.py Example.lean --local-dir lean-world-model-qwen3-8b-reasoning-grpopython lean-world-model-qwen3-8b-reasoning-grpo/inference.py lean-world-model-qwen3-8b-reasoning-grpo/Example.lean --samples 1Solve 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, annotated with Lean 4 compiler feedback blocks in the form `/- <feedback> ... </feedback> -/` at the appropriate locations. If a previous attempt failed, first give [Error Analysis], [Revised Reasoning] and [Updated Proof Plan], then provide the corrected solution, annotated with Lean 4 compiler feedback blocks in the form `/- <feedback> ... </feedback> -/` at the appropriate locations.