Views
No views yet
| 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 |
next_solution_step_prediction): Input an informal problem and a current solution state; the model outputs the next solution step.You are a Lean 4 expert.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
```
# 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]
}
```
1@inproceedings{
2liu2025bootstrapping,
3title={Bootstrapping Hierarchical Autoregressive Formal Reasoner with Chain-of-Proxy-Autoformalization},
4author={Liu, Qi and Zheng, Xinhao and Xia, Renqiu and Cao, Qinxiang and Yan, Junchi},
5booktitle={The Thirty-ninth Annual Conference on Neural Information Processing Systems},
6year={2025},
7url={https://openreview.net/forum?id=2Xn8h68mP3}
8}