GLM-5.3 is live. Run Z.ai's latest model on Friendli Model APIs. Try it today ➜
lm-provers
Available on FriendliAI
Run this model inference on single tenant GPU with unmatched speed and reliability at scale.
Model Details
Model Provider
lm-provers
Model Tree
lm-provers/QED-Nano-SFT
Input Modalities
Output Modalities
Supported Functionality
QED-Nano is a 4B parameter model explicitly post-trained to strengthen its proof-writing capabilities. Despite its small size, QED-Nano achieves an impressive 40% score on the challenging IMO-ProofBench benchmark (+20% over the Qwen3 base model), matching the performance of GPT-OSS-120B from OpenAI. With an agent scaffold that scales inference-time compute to over 1M tokens per problem, QED-Nano approaches the performance of Gemini-3-Pro. Crucially, the same agentic scaffold on the base model (Qwen3-4B-Thinking-2507) barely improves performance.
QED-Nano is based on Qwen/Qwen3-4B-Thinking-2507, and was post-trained via a combination of supervised fine-tuning and reinforcement learning with a reasoning cache (to be able to train for continual improvement with our agentic scaffold at test time) on a mixture of Olympiads proof problems from various public sources.
For more details refer to our blog post: https://huggingface.co/spaces/lm-provers/qed-nano-blogpost
python
from transformers import AutoModelForCausalLM, AutoTokenizer model_name = "lm-provers/QED-Nano"device = "cuda" # for GPU usage or "cpu" for CPU usage # load the tokenizer and the modeltokenizer = AutoTokenizer.from_pretrained(model_name)model = AutoModelForCausalLM.from_pretrained( model_name,).to(device) # prepare the model inputprompt = "Generate a rigorous proof to the following question: is \sqrt{2} rational or irrational?"messages_think = [ {"role": "user", "content": prompt}] text = tokenizer.apply_chat_template( messages_think, tokenize=False, add_generation_prompt=True,)model_inputs = tokenizer([text], return_tensors="pt").to(model.device) # Generate the outputgenerated_ids = model.generate(**model_inputs, max_new_tokens=32768) # Get and decode the outputoutput_ids = generated_ids[0][len(model_inputs.input_ids[0]) :]print(tokenizer.decode(output_ids, skip_special_tokens=True))[!TIP] We recommend setting
temperature=0.6andtop_p=0.95in the sampling parameters.
You can use vLLM and SGLang to deploy the model in an API compatible with OpenAI format.
bash
python -m sglang.launch_server --model-path lm-provers/QED-Nanobash
vllm serve lm-provers/QED-NanoIn this section, we report the evaluation results of QED-Nano on IMO-ProofBench, ProofBench, and IMO-AnswerBench. All evaluations except those on IMO-AnswerBench are reported as avg@3 unless stated otherwise.
| Model | IMO-ProofBench | ProofBench | IMO-AnswerBench |
|---|---|---|---|
| Qwen3-4B-Thinking-2507 | 20.4 (2.6) | 19.5 (0.9) | 55.8 |
| QED-Nano-SFT | 39.5 (2.9) | 33.3 (0.5) | 57.5 |
| QED-Nano | 40.0 (0.6) | 44.9 (3.4) | 67.5 |
| QED-Nano (Agent) | 54.0 (3.7) | 54.4 (2.4) | - |
| Qwen3-30B-A3B-Thinking-2507 | 27.6 (1.0) | 26.1 (2.4) | 67.0 |
| Qwen3-235B-A22B-Thinking-2507 | 34.1 (0.7) | 33.7 (1.1) | 70.5 |
| Nomos-1 | 40.3 (3.5) | 28.3 (3.9) | 49.0 |
| GPT-OSS-20B | 38.3 (1.2) | 38.4 (3.9) | 61.5 |
| GPT-OSS-120B | 43.1 (3.2) | 47.5 (1.7) | 70.5 |
| DeepSeek-Math-V2 | 57.9 (2.0) | 60.6 (0.1) | 75.8 |
| Gemini 3 Pro | 58.7 (2.9) | 66.7 (3.1) | 83.2 |
QED-Nano is a domain-specific model that is designed for one thing and one thing only: proving theorems. Using as a general assistant will likely produce nonsense outside of this domain. These models should be used as assistive tools rather than definitive sources of information. Users should always verify important information and critically evaluate any generated content.
QED-Nano is a joint collaboration between the research teams at CMU, ETH Zurich, Numina, and Hugging Face. Below is a list of the individual contributors and their affiliations:
Amrith Setlur, Yuxiao Qu, Ian Wu, and Aviral Kumar
Jasper Dekoninck
Jia Li
Edward Beeching and Lewis Tunstall
from transformers import AutoModelForCausalLM, AutoTokenizer model_name = "lm-provers/QED-Nano"device = "cuda" # for GPU usage or "cpu" for CPU usage # load the tokenizer and the modeltokenizer = AutoTokenizer.from_pretrained(model_name)model = AutoModelForCausalLM.from_pretrained( model_name,).to(device) # prepare the model inputprompt = "Generate a rigorous proof to the following question: is \sqrt{2} rational or irrational?"messages_think = [ {"role": "user", "content": prompt}] text = tokenizer.apply_chat_template( messages_think, tokenize=False, add_generation_prompt=True,)model_inputs = tokenizer([text], return_tensors="pt").to(model.device) # Generate the outputgenerated_ids = model.generate(**model_inputs, max_new_tokens=32768) # Get and decode the outputoutput_ids = generated_ids[0][len(model_inputs.input_ids[0]) :]print(tokenizer.decode(output_ids, skip_special_tokens=True))