Elamur Research⌕
☰
home / papers / 2024 / HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving

HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving

Paper · 2024 · Yang Li, Dong Du, Linfeng Song et al.

Summary

Formal theorem proving in LEAN4 remains difficult for language models. The search space is enormous, and there is little supervised data: mathlib4 provides only about 50k theorems with tactics. HunyuanProver addresses this by fine-tuning the Hunyuan 7B model with two components. The first is a low-cost, iterative data pipeline. An autoformalizer converts tens of millions of natural-language math problems into LEAN statements. The prover then repeatedly attempts the unsolved statements with best-first search and is retrained on the proofs it finds through rejection finetuning. The second component is critic-guided tree search at inference time. The authors compare best-first search (BFS) with an adapted ηMCTS, guided by three critics: policy confidence, a process reward model (PRM), and a new distance critic that estimates how many steps remain. The best setup, BFS with the distance critic, reaches 68.4% on miniF2F-test. This beats the previous best of 65.9% while using a smaller search budget. The results suggest that scaling synthetic data, selecting it carefully, and training explicit critics all matter for step-level provers.

Key points

  • Autoformalization data: The autoformalizer was trained on 130k NL–LEAN pairs, 50k from lean workbook and 80k from MMA. Translating these into Chinese doubled the set. The model turned 30M internal problems into about 20M valid LEAN statements, and NuminaMath CoT was also used as a source.
  • Iterative prover training: More than 10 rounds of proving and rejection finetuning produced over 20M tactic-level examples, roughly a 40× expansion. Diversity came from two sources: turning the final states of unfinished proofs into new statements, and adding harder Olympiad-style inequalities.
  • Search and critics: ηMCTS was modified in three ways: the simulation step was removed, K tactics are sampled per expansion, and each node's expansion budget adapts to its importance. Node selection uses UCB. The PRM is trained on ±1 labels indicating whether a proof was reached. The distance critic predicts both the exact number of remaining steps and a range for it, organized as a balanced binary tree.
  • Main results:
    • HunyuanProver v16 with BFS and the distance critic scores 68.4% on miniF2F-test, using a 600×8×400 budget.
    • The previous best, InternLM2.5-StepProver+BFS+CG, scores 65.9% with a 256×32×600 budget.
    • On v16, the distance critic adds 3.6 points over BFS with policy confidence (64.8% → 68.4%).
    • The system solves four IMO problems: 1960 P2, 1962 P2, 1964 P2, and 1983 P6.
  • Data selection effect: Accuracy gains flattened when training data grew from about 2.75B tokens (v8) to 4.25B (v12). Dropping easy examples from early iterations after v12 improved accuracy again.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksComputational Theory and Mathematics · 252 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,426 works

Cite

Cite as Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang and Haitao Mi. 2024. HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving. arXiv:2412.20735.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2412.20735 · arXiv 2412.20735

@misc{li2024hunyuanprover,
  title = {{HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving}},
  author = {Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang and Haitao Mi},
  year = {2024},
  doi = {10.48550/arxiv.2412.20735},
  eprint = {2412.20735},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2412.20735}
}

References

20 references, 10 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Aaron Hurst, Adam Lerer, Adam P Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, AJ Ostrow, Akila Welihinda, Alan Hayes, Alec Radford, et al. Gpt-4o system card. arXiv preprint arXiv:2410.21276, 2024.
  2. Albert Qiaochu Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization, 2024. URL https://openreview.net/forum?id=QqdloE1QH2. ↗
  3. Jia LI, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu, Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample, and Stanislas Polu. Numinamath. [https://huggingface. co/AI-MO/NuminaMath-CoT](https://github.c… find
  4. Haohan Lin, Zhiqing Sun, Sean Welleck, and Yiming Yang. Lean-star: Learning to interleave thinking and proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024. find
  5. Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, and Dongmei Zhang. Wizardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct. arXiv preprint arXiv:2308.09583, 2023.
  6. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pp. 625–635.
  7. LC PAULSON. Isabelle: A generic theorem prover. Lecture Notes in Computer Science, 828, 1994. find
  8. Ye Tian, Baolin Peng, Linfeng Song, Lifeng Jin, Dian Yu, Haitao Mi, and Dong Yu. Toward self-improvement of llms via imagination, searching, and criticizing. In Proceedings of Neurips 2024, 2024. find
  9. Ante Wang, Linfeng Song, Ye Tian, Baolin Peng, Dian Yu, Haitao Mi, Jinsong Su, and Dong Yu. Litesearch: Efficacious tree search for llm. arXiv preprint arXiv:2407.00320, 2024a. — [arXiv:2407.00320](https://arxiv.org/abs/2407.00320) find
  10. Chaojie Wang, Yanchen Deng, Zhiyi Lyu, Liang Zeng, Jujie He, Shuicheng Yan, and Bo An. Q*: Improving multi-step reasoning for llms with deliberative planning. arXiv preprint arXiv:2406.14283, 2024b. find
  11. Peiyi Wang, Lei Li, Zhihong Shao, Runxin Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. Math-shepherd: Verify and reinforce llms step-by-step without human annotations. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp…
  12. Chenrui Wei, Mengzhou Sun, and Wei Wang. Proving olympiad algebraic inequalities without human demonstrations, 2024. URL https://openreview.net/forum?id=8kFctyli9H. ↗
  13. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024. find
  14. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024a.
  15. Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-… — DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
  16. Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024c.
  17. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024.
  18. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024. find
  19. Longhui Yu, Weisen Jiang, Han Shi, YU Jincheng, Zhengying Liu, Yu Zhang, James Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models. In The Twelfth International Conference on Learning Representations, 2024.
  20. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/