Instructions to use purewhite42/AR_CoPA_Cycle1 with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use purewhite42/AR_CoPA_Cycle1 with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="purewhite42/AR_CoPA_Cycle1")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# Load model directly
from transformers import AutoTokenizer, AutoModelForMultimodalLM

tokenizer = AutoTokenizer.from_pretrained("purewhite42/AR_CoPA_Cycle1")
model = AutoModelForMultimodalLM.from_pretrained("purewhite42/AR_CoPA_Cycle1")
messages = [
    {"role": "user", "content": "Who are you?"},
]
inputs = tokenizer.apply_chat_template(
	messages,
	add_generation_prompt=True,
	tokenize=True,
	return_dict=True,
	return_tensors="pt",
).to(model.device)

outputs = model.generate(**inputs, max_new_tokens=40)
print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:]))

Notebooks
Google Colab
Kaggle
Local Apps Settings

vLLM

How to use purewhite42/AR_CoPA_Cycle1 with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "purewhite42/AR_CoPA_Cycle1"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "purewhite42/AR_CoPA_Cycle1",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/purewhite42/AR_CoPA_Cycle1

SGLang

How to use purewhite42/AR_CoPA_Cycle1 with SGLang:

Install from pip and serve model

# Install SGLang from pip:
pip install sglang
# Start the SGLang server:
python3 -m sglang.launch_server \
    --model-path "purewhite42/AR_CoPA_Cycle1" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "purewhite42/AR_CoPA_Cycle1",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker images

docker run --gpus all \
    --shm-size 32g \
    -p 30000:30000 \
    -v ~/.cache/huggingface:/root/.cache/huggingface \
    --env "HF_TOKEN=<secret>" \
    --ipc=host \
    lmsysorg/sglang:latest \
    python3 -m sglang.launch_server \
        --model-path "purewhite42/AR_CoPA_Cycle1" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "purewhite42/AR_CoPA_Cycle1",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use purewhite42/AR_CoPA_Cycle1 with Docker Model Runner:
```
docker model run hf.co/purewhite42/AR_CoPA_Cycle1
```

[NeurIPS'25] Bootstrapping Hierarchical Autoregressive Formal Reasoner with Chain-of-Proxy-Autoformalization

Qi Liu, Xinhao Zheng, Renqiu Xia, Qinxiang Cao, Junchi Yan* (* indicates corresponding author)

School of Computer Science & School of Artificial Intelligence, Shanghai Jiao Tong University

Shanghai Innovation Institute

Please refer to the 📺GitHub repo and 📃Paper for more details.

📈 Performance

Cycle	Method	FormalMath500		MiniF2F-Solving
		Solved% ↑	Budget ↓	Solved % ↑	Budget ↓
1	BFS (This Model)	9.52% ± 0.57%	28139 ± 104	9.64% ± 1.66%	27712 ± 339
1	WG	18.78% ± 0.22%	18456 ± 92	24.95% ± 1.09%	18853 ± 454
1	WG $(K_W=16)$	21.78% ± 0.12%	35391 ± 153	28.83% ± 0.77%	35895 ± 487
1	AR (This Model)	34.39% ± 0.78%	20860 ± 233	44.41% ± 0.34%	17814 ± 140
1	H-BFS	13.32% ± 1.47%	27777 ± 360	12.25% ± 1.47%	27479 ± 203
1	H-WG	36.77% ± 0.86%	17039 ± 461	47.30% ± 1.01%	16303 ± 388
1	H-WG $(K_W=16)$	40.04% ± 0.50%	32134 ± 226	51.08% ± 0.44%	30357 ± 212
1	HAR	43.65% ± 1.35%	18432 ± 344	55.50% ± 0.46%	15069 ± 143
2	HAR	44.09% ± 0.54%	18273 ± 116	56.58% ± 0.92%	14754 ± 269

⚙️ Usage

We recommend using vLLM to serve the model locally.

This model is SFTed for the following tasks with 🤗purewhite42/CoPA_Dataset.

Next-Solution-Step Prediction (next_solution_step_prediction): Input an informal problem and a current solution state; the model outputs the next solution step.

📋 Example

Next-Solution-Step Prediction

System Prompt

You are a Lean 4 expert.

User Prompt

Given a natural language math problem and the current solution state, please generate the next solution step.
Please use comments to plan and reason in natural language and deductive reasoning to derive the answer.
Assume `Mathlib` is imported.
# Informal Problem
"""
Given $2\sin (π-x)+1=0$, find the value of $\cos 2x$.
"""
# Current Solution State
```lean4
case h.mp
answer x : ℝ
h_eq : 2 * Real.sin (Real.pi - x) + 1 = 0
h_answer : Real.cos (2 * x) = answer
h_given_eq : 2 * Real.sin (Real.pi - x) + 1 = 0
⊢ ?w
```

Response

# Next Solution Step
```lean4
-- Using the cofunction identity $\sin(π-x)=\sin(x)$, we have: $2\sin(x)+1=0$
have h_cofunction : Real.sin (Real.pi - x) = Real.sin x := by {
simp [Real.sin_pi_sub]
}
```

📚 Citation

If you find our work useful in your research, please cite

@inproceedings{
liu2025bootstrapping,
title={Bootstrapping Hierarchical Autoregressive Formal Reasoner with Chain-of-Proxy-Autoformalization},
author={Liu, Qi and Zheng, Xinhao and Xia, Renqiu and Cao, Qinxiang and Yan, Junchi},
booktitle={The Thirty-ninth Annual Conference on Neural Information Processing Systems},
year={2025},
url={https://openreview.net/forum?id=2Xn8h68mP3}
}