---
license: apache-2.0
language:
- en
base_model:
- deepseek-ai/DeepSeek-R1-0528-Qwen3-8B
---
# OPC-R1-8B
We introduce the Open Proof Corpus (OPC)—the world’s first large-scale, open-source dataset of human-verified solutions to advanced mathematics problems. With over 5,000 solutions spanning 1,000+ challenging problems, the OPC is specifically designed for broad applicability and downstream usage in proof generation research and is the first to include a substantial number of correct, LLM-generated solutions to problems from prestigious mathematics competitions such as the USAMO and IMO.
Leverage OPC to tackle pressing research questions in automated proof generation:
(1) How do natural language and formal proof generation compare?
(2) How often do models that produce correct final answers truly reason their way to valid proofs?
(3) By what margin do best-of-n selection methods improve proof quality?
Building on this breakthrough resource, we present **OPC-R1-8B** - an open-source model for proof correctness judging that matches state-of-the-art performance. OPC-R1-8B outperforms the majority of leading closed-source models, reaching an impressive 88.1% accuracy on verifying LLM-generated proofs.
## Introduction
**OPC-R1-8B** is a specialized, open-source model fine-tuned for proof evaluation. We finetuned *DeepSeek R1 Distill Qwen3 8B (05/28)* using GRPO reward signals from judgment accuracy, using the "LLM-as-judge" prompt detailed in our paper.
## Usage
You can run our model following the example below:
```python
from transformers import AutoModelForCausalLM, AutoTokenizer
model_name = "INSAIT-Institute/OPC-R1-8B"
# load the tokenizer and the model
tokenizer = AutoTokenizer.from_pretrained(model_name)
model = AutoModelForCausalLM.from_pretrained(
model_name,
torch_dtype="auto",
device_map="auto"
)
# prepare the model input
problem = "Compute the number of real solutions of the equation $x^2 + 2x + 2 = 0$."
solution = "The equation can be factored in as $x^2 + 2x + 2 = (x+1)^2 + 1$. Because $(x+1)^2 \\geq 0$, then $x^2 + 2x + 2 \\geq 1 > 0$. Therefore, there are \\boxed{0} real solutions."
prompt = ""
messages = [
{"role": "user", "content": prompt.format(problem=problem, solution=solution)}
]
text = tokenizer.apply_chat_template(
messages,
tokenize=False,
add_generation_prompt=True,
enable_thinking=True
)
model_inputs = tokenizer([text], return_tensors="pt").to(model.device)
# conduct text completion
generated_ids = model.generate(
**model_inputs,
max_new_tokens=32768
)
output_ids = generated_ids[0][len(model_inputs.input_ids[0]):].tolist()
content = tokenizer.decode(output_ids, skip_special_tokens=True).strip("\n")
print("content:", content)
```
You can also run the model using the inference pipeline in our GitHub repository.
## Evaluation results
To benchmark LLMs as judges for proofs, we took 293 solutions from the OPC containing human-labeled ground truths. **OPC-R1-8B** achieves a 88.1% maj@5 accuracy, matching the top-performing **Gemini 2.5 Pro**, and outperforming all other closed- and open-source alternatives.
| **Judge** | **pass@1** | **maj@5** | **Cost (USD)** |
|--------------------|:----------:|:---------:|:--------------:|
| Human | 90.4 | - | N/A |
| Gemini 2.5 Pro | 85.4 | 88.1 | 135.47 |
| **OPC-R1-8B** | 83.8 | 88.1 | N/A |
| o4-mini | 83.8 | 85.3 | 29.57 |
| o3 | 83.1 | 84.3 | 93.3 |
| Qwen3 235B-A22B | 81.8 | 84.6 | 3.79 |
| DeepSeek R1 (05/28)| 80.9 | 82.6 | 27.35 |
| DeepSeek R1 Distill 8B| 70.7 | 71.3 | N/A |
| Qwen3-8B | 64.4 | 63.6 | N/A |
## Dataset
We have open-sourced the OPC dataset, where we answer many open questions regarding the LLMs’ proof capabilities.
| **Dataset** | **Download** |
| :-----------------------------: | :----------------------------------------------------------: |
| OPC | [🤗 HuggingFace](https://huggingface.co/datasets/INSAIT-Institute/OPC) |
## License
**OPC-R1-8B** is released under the permissive Apache 2.0 license.
## Citation
```
@article{openproofcorpus2025,
title={The Open Proof Corpus: A Large-Scale Human Study of LLM Proofs},
author={Jasper Dekoninck and Ivo Petrov and Kristian Minchev and Mislav Balunovic and Martin Vechev and Miroslav Marinov, Maria Drencheva and Lyuba Konova and Milen Milenov Shumanov and Kaloyan Tsvetkov and Nikolay Drenchev and Lazar D. Todorov and Kalina Nikolova and Nikolay Georgiev and Vanesa Kalinkova and Margulan Ismoldayev},
journal={arXiv},
year={2025},
}
```
