---
library_name: transformers
license: apache-2.0
language:
- en
base_model:
- Qwen/Qwen3-4B-Thinking-2507
---

# QED-Nano

![logo.png](https://huggingface.co/lm-provers/QED-Nano/resolve/main/logo.png)


##  Table of Contents

1. [Model Summary](#model-summary)
2. [How to use](#how-to-use)
3. [Evaluation](#evaluation)
4. [Training](#training)
5. [Limitations](#limitations)
6. [License](#license)

## Model Summary

QED-Nano is a 4B parameter language model designed to push the theorem-proving boundaries of small models. It was post-trained to solve Olympiad-level proof problems by continually improving at test-time. When we scale test-time compute for our model, we get QED-Nano (Agent) which outperforms several much larger open source models (notably GPT-OSS-120B, Qwen3-235B-Thinking), and comes close to matching Gemini-3-Pro model on the challenging IMOProofBench benchmark:

![imoproofbench.png](https://huggingface.co/lm-provers/QED-Nano/resolve/main/imoproofbench.png)

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 reasoning cache on a mixture of Olympiads proof problems from various sources. 

## How to use

```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 model
tokenizer = AutoTokenizer.from_pretrained(model_name)
model = AutoModelForCausalLM.from_pretrained(
    model_name,
).to(device)

# prepare the model input
prompt = "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 output
generated_ids = model.generate(**model_inputs, max_new_tokens=32768)

# Get and decode the output
output_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.6` and `top_p=0.95` in the sampling parameters.


### Agentic Usage

[Add link to scaffolds?]

### vLLM and SGLang

You can use vLLM and SGLang to deploy the model in an API compatible with OpenAI format.

#### SGLang

```bash
python -m sglang.launch_server --model-path lm-provers/QED-Nano
```

#### vLLM

```bash
vllm serve lm-provers/QED-Nano
```

## Evaluation

In this section, we report the evaluation results of QED-Nano. All evaluations are reported as avg@3 unless stated otherwise, and we use [CODEBASE] to run them. 

We highlight the best score in bold and underline the second-best score.

[ADD TABLE]

## Training

### Model

- **Architecture:** Transformer decoder
- **Precision:** bfloat16

### Software & hardware

- **GPUs:** 80 H100
- **Training Framework:** [ADD CODE]
- **Evaluation framework:** [ADD CODE]

### Open resources
Here is an infographic with all the training details 
- The datasets used for post-training can be found in this [collection](https://huggingface.co/collections/lm-provers/qed-nano). 
- The training and evaluation configs and code can be found in the [ADD CODE]
- The SFT checkpoint is available at [ADD LINK]


## Limitations

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.

## License
[Apache 2.0](https://www.apache.org/licenses/LICENSE-2.0)

## Citation