[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	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	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 (This Model)	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.

Statement Autoformalization (statement_autoformalization): Given an informal problem and its informal ground-truth answer, the model outputs a corresponding formal statement.
Solution Drafting (solution_drafting): Input an informal problem, its informal ground-truth answer, its informal ground-truth solution, and a corresponding formal statement, and the model outputs a formal solution draft.
Next-Proof-Step Prediction (next_proof_step_prediction): Input the current proof state; the model outputs the next proof step.
Next-Solution-Step Drafting (next_solution_step_drafting): Given an informal problem and a current solution state, the model outputs the next formal solution step draft.

📋 Example

Statement Autoformalization

System Prompt

You are a Lean 4 expert.

User Prompt

Given a natural language math problem and its answer, please generate a corresponding Lean 4 formal statement.
Please add comments highlighting the original parts of the natural language math problem and answer.
Please explicitly use the variable `answer` to indicate the answer in the formal statement.
Please maintain the semantic equivalence between natural language math and Lean 4.
Please assume the following header code has already been executed and do not add any imports or openings.
```lean4
import Mathlib
open BigOperators Real Nat Topology

```

# Problem
"""
Given $2\sin (π-x)+1=0$, find the value of $\cos 2x$.
"""
# Answer
"""
the answer is \frac{1}{2}
"""

Response

# Formal Statement
```lean4
example
(answer : ℝ)
  (x : ℝ)
  -- Given $2\sin (π-x)+1=0$
  (h_eq : 2 * Real.sin (Real.pi - x) + 1 = 0)
  -- Find the value of $\cos 2x$.
  (h_answer : Real.cos (2 * x) = answer)
: -- the answer is $\frac{1}{2}$
answer = 1/2
:= by
```

Solution Drafting

System Prompt

You are a Lean 4 expert.

User Prompt

Given a natural language math problem, its answer, its solution, and its formal statement, please generate a corresponding Lean 4 proof sketch and add comments to highlight the original parts of the natural language math solution.
Please maintain the semantic equivalence between natural language math and Lean 4.
Please only use forward reasoning in the proof, do not use tactics that modify the final goal.
For new hypotheses, please do not prove them and use `sorry` to close them.
Please assume the following header code has already been executed and do not add any imports or openings.
```lean4
import Mathlib
```

# Problem
"""
Given $2\sin (π-x)+1=0$, find the value of $\cos 2x$.
"""
# Answer
"""
the answer is \frac{1}{2}
"""
# Solution
"""
The given equation can be simplified as follows:

$2\sin (π-x)+1=0$

Using the cofunction identity $\sin(π-x)=\sin(x)$, we have:

$2\sin(x)+1=0$

Now, solve for $\sin(x)$:

$\sin(x)=-\frac{1}{2}$

Now, we need to find $\cos 2x$. We can use the double angle identity for cosine:

$\cos 2x = 1 - 2\sin^2 x$

Substitute the value of $\sin x$:

$\cos 2x = 1 - 2(-\frac{1}{2})^2$

Simplify:

$\cos 2x = 1 - 2(\frac{1}{4})$

$\cos 2x = 1 - \frac{1}{2}$

$\cos 2x = \frac{1}{2}$

Thus, the value of $\cos 2x$ is $\boxed{\frac{1}{2}}$.
"""

# Formal Statement
```lean4
example
(answer : ℝ)
  (x : ℝ)
  -- Given $2\sin (π-x)+1=0$
  (h_eq : 2 * Real.sin (Real.pi - x) + 1 = 0)
  -- Find the value of $\cos 2x$.
  (h_answer : Real.cos (2 * x) = answer)
: -- the answer is $\frac{1}{2}$
answer = 1/2
:= by
```

Response

# Formal Proof Draft
```lean4
-- The given equation can be simplified as follows: $2\sin (π-x)+1=0$
have h_given_eq : 2 * Real.sin (Real.pi - x) + 1 = 0 := h_eq

-- 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 := sorry
have h_simplified_eq : 2 * Real.sin x + 1 = 0 := sorry

-- Now, solve for $\sin(x)$: $\sin(x)=-\frac{1}{2}$
have h_sin_x : Real.sin x = -1/2 := sorry

-- Now, we need to find $\cos 2x$. We can use the double angle identity for cosine: $\cos 2x = 1 - 2\sin^2 x$
have h_double_angle : Real.cos (2 * x) = 1 - 2 * (Real.sin x)^2 := sorry

-- Substitute the value of $\sin x$: $\cos 2x = 1 - 2(-\frac{1}{2})^2$
have h_substituted : Real.cos (2 * x) = 1 - 2 * (-1/2)^2 := sorry

-- Simplify: $\cos 2x = 1 - 2(\frac{1}{4})$
have h_simplified : Real.cos (2 * x) = 1 - 2 * (1/4) := sorry

-- $\cos 2x = 1 - \frac{1}{2}$
have h_final_simplification : Real.cos (2 * x) = 1 - 1/2 := sorry

-- $\cos 2x = \frac{1}{2}$
have h_cos_2x : Real.cos (2 * x) = 1/2 := sorry

-- Thus, the value of $\cos 2x$ is $\boxed{\frac{1}{2}}$
have h_answer : answer = 1/2 := sorry

exact h_answer -- submit

```

Next-Proof-Step Prediction

System Prompt

You are a Lean 4 expert.

User Prompt

Generate a tactic that can transform one step from the current tactic state to the 'no goals' tactic state.
Current tactic state:
```
R : Type u
ι : Type v
inst✝⁶ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → LieRingModule L (M i)
inst✝ : ∀ (i : ι), LieModule R L (M i)
x y : L
m : ⨁ (i : ι), M i
⊢ ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
```

Response

refine
  DFinsupp.ext fun _ =>
    ?_
      -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`

Next-Solution-Step Drafting

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 := sorry
```

📚 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}
}