Elamur Research⌕
☰
home / papers / 2025 / ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

Paper · 2025 · Guoxin Chen, Jing Wu, Xinjie Chen et al.

Summary

Autoformalization turns natural-language math problems into Lean statements that a machine can check. Current LLMs usually produce code that compiles, but the statements often change the problem's meaning. The authors argue this happens because models translate in one shot and never review their own output. ReForm makes the model work in a loop instead: it drafts a Lean 4 statement, critiques whether the draft matches the original problem, and revises until it is satisfied. Training starts with SFT on reflective trajectories gathered by a multi-agent pipeline. It continues with PBSO, a reinforcement-learning algorithm that rewards both the final statement and the quality of the intermediate critiques. PBSO caps the accumulated returns so training stays stable. Across four benchmarks, ReForm beats the strongest baselines by 22.6 points on average. The authors also release ConsistencyCheck, an expert-labeled benchmark showing that LLM judges are reasonably reliable and that humans often make formalization mistakes too. This matters because formal theorem provers depend on faithful problem statements.

Key points

  • Evaluation: ReForm-8B and ReForm-32B were tested on miniF2F, ProofNet, Putnam, and AIME2025. They were compared with Goedel-Prover-V2 (8B/32B), Kimina-7B, and GPT-5, and gained 22.6 percentage points on average over the strongest baseline.
  • PBSO: It assigns rewards at different positions in a sequence. Critique steps receive an auxiliary reward, and the final answer receives the task reward. Each step's return is a discounted sum of future rewards, clipped to the reward range. This keeps critiques from becoming shallow or hallucinated.
  • ConsistencyCheck: The benchmark contains 859 expert-annotated items for testing whether a model can judge if a Lean statement matches its source problem.
  • Human error rates: Annotators found semantic errors in 16.4% of miniF2F and 38.5% of ProofNet human-written formal statements.
  • LLM judge accuracy: The best frontier LLM judges are correct about 85.8% of the time. This is well within the margin needed to trust ReForm's gains, yet it also shows that even this simpler classification task remains imperfect.

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 5The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 worksComputational Theory and Mathematics · 252 works

Cite

Cite as Guoxin Chen, Jing Wu, Xinjie Chen, Wayne Xin Zhao, Ruihua Song, Chengxi Li, Kai Fan, Dayiheng Liu and Minpeng Liao. 2025. ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization. arXiv:2510.24592.

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

@misc{chen2025reform,
  title = {{ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization}},
  author = {Guoxin Chen, Jing Wu, Xinjie Chen, Wayne Xin Zhao, Ruihua Song, Chengxi Li, Kai Fan, Dayiheng Liu and Minpeng Liao},
  year = {2025},
  doi = {10.48550/arxiv.2510.24592},
  eprint = {2510.24592},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2510.24592}
}

References

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

  1. Alon Albalak, Duy Phung, Nathan Lile, Rafael Rafailov, Kanishk Gandhi, Louis Castricato, Anikait Singh, Chase Blagden, Violet Xiang, Dakota Mahan, et al. Big-math: A large-scale, high-quality math dataset for reinforcement learning in language models. arXiv preprint arXiv:2502.17387, 2025. find
  2. Anthropic. Claude 3.7 sonnet and claude code. https://www.anthropic.com/news/ claude-3-7-sonnet, February 2025. ↗
  3. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023.
  4. Guoxin Chen, Minpeng Liao, Chengxi Li, and Kai Fan. Alphamath almost zero: Process supervision without process. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024a. URL https://openreview.net/forum?id=VaXnxQ3UKo. ↗
  5. Guoxin Chen, Minpeng Liao, Chengxi Li, and Kai Fan. Step-level value preference optimization for mathematical reasoning. arXiv preprint arXiv:2406.10858, 2024b. find
  6. Guoxin Chen, Zile Qiao, Xuanzhong Chen, Donglei Yu, Haotian Xu, Wayne Xin Zhao, Ruihua Song, Wenbiao Yin, Huifeng Yin, Liwen Zhang, et al. Iterresearch: Rethinking long-horizon agents via markovian state reconstruction. arXiv preprint arXiv:2511.07327, 2025a. — [arXiv:2511.07327](https://arxiv.org/abs/2511.07327) find
  7. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23726, 2025b. find
  8. Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In International Conference on Automated Deduction, pp. 378–388. Springer, 2015. find
  9. Bofei Gao, Feifan Song, Zhe Yang, Zefan Cai, Yibo Miao, Qingxiu Dong, Lei Li, Chenghao Ma, Liang Chen, Runxin Xu, et al. Omni-math: A universal olympiad level mathematic benchmark for large language models. arXiv preprint arXiv:2410.07985, 2024.
  10. Google. Gemini 2.5 pro. https://deepmind.google/technologies/gemini/pro/, April 2025. ↗
  11. Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. 2025.
  12. Chuanyang Han, Pu Huang, Yixuan Wang, Yutao Chen, Sheng Zhang, and Li Song. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2404.14813, 2024. find
  13. Zhiwei He, Tian Liang, Jiahao Xu, Qiuzhi Liu, Xingyu Chen, Yue Wang, Linfeng Song, Dian Yu, Zhenwen Liang, Wenxuan Wang, et al. Deepmath-103k: A large-scale, challenging, decontaminated, and verifiable mathematical dataset for advancing reasoning. arXiv preprint arXiv:2504.11456, 2025. find
  14. Aaron Hurst, Adam Lerer, Adam P. Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, AJ Ostrow, Akila Welihinda, Alan Hayes, Alec Radford, Aleksander Madry, Alex Baker-Whitcomb, Alex Beutel, Alex Borzunov, Alex Carney, Alex Chow, Alex Kirillov, Alex Nichol, Alex Paino, Alex Renzin, Alex Tachard Pass… — GPT-4o System Card
  15. InternLM Team. Internlm: A multilingual language model with progressively enhanced capabilities. arXiv preprint arXiv:2307.16135, 2023. — [arXiv:2307.16135](https://arxiv.org/abs/2307.16135) find
  16. Albert Qiaochu Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023. find
  17. Sheng Jiayi, Lyu Luna, Jin Jikai, Xia Tony, Gu Alex, Zou James, and Lu Pan. Solving inequality proofs with large language models. arXiv preprint arXiv:2506.07927, 2025. — [arXiv:2506.07927](https://arxiv.org/abs/2506.07927) find
  18. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939, 2024. find
  19. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025a. find
  20. Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613, 2025b. find
  21. OpenAI. Gpt-5 is here. https://openai.com/gpt-5/, August 2025. ↗
  22. OpenCompass. AIME 2025 Benchmark. opencompass/AIME2025, 2025. https://huggingface.co/datasets/ ↗
  23. Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, et al. Criticlean: Critic-guided reinforcement learning for mathematical formalization. arXiv preprint arXiv:2507.06181, 2025.
  24. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. In International Conference on Machine Learning, pp. 7872–7882. PMLR, 2020.
  25. Zile Qiao, Guoxin Chen, Xuanzhong Chen, Donglei Yu, Wenbiao Yin, Xinyu Wang, Zhen Zhang, Baixuan Li, Huifeng Yin, Kuan Li, et al. Webresearcher: Unleashing unbounded reasoning capability in long-horizon agents. arXiv preprint arXiv:2509.13309, 2025. — [arXiv:2509.13309](https://arxiv.org/abs/2509.13309) find
  26. Qwen. QwQ: Reflect deeply on the boundaries of the unknown. Hugging Face, 2024. find
  27. Alexander A Razborov and Steven Rudich. Natural proofs. In Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, pp. 204–213, 1994. find
  28. ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
  29. John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06347, 2017. find
  30. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. 2024.
  31. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. Advances in Neural Information Processing Systems, 37: 11545–11569, 2024. find
  32. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025a. find
  33. Weixun Wang, Shaopan Xiong, Gengru Chen, Wei Gao, Sheng Guo, Yancheng He, Ju Huang, Jiaheng Liu, Zhendong Li, Xiaoyang Li, et al. Reinforcement learning optimization for large-scale learning: An efficient and user-friendly scaling library. 2025b. find
  34. Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, and Tiancheng Zhang. Autoformalization in the era of large language models: A survey. arXiv preprint arXiv:2505.23486, 2025.
  35. Yilun Wu, Albert Q Jiang, Wenda Li, Mateja Jamnik, Guillaume Lample, and M Rabe. Autoformalization with large language models. Transactions on Machine Learning Research, 2023.
  36. 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
  37. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Zheng Yuan, Wenwei Zhang, Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via critic-guided search. In 2nd AI for Math Workshop@ ICML 2025, 2025. find
  38. Jiaxuan Xie, Chengwu Liu, Ye Yuan, Siqi Li, Zhiping Xiao, and Ming Zhang. Fmc: Formalization of natural language mathematical competition problems. arXiv preprint arXiv:2507.11275, 2025. — [arXiv:2507.11275](https://arxiv.org/abs/2507.11275) find
  39. 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.
  40. 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, 2024b.
  41. An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, et al. Qwen3 technical report. arXiv preprint arXiv:2505.09388, 2025.
  42. 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:21573– 21612, 2023.
  43. 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. Advances in Neural Information Processing Systems, 37:105848–105863, 2024. find
  44. Qiying Yu, Zheng Zhang, Ruofei Zhu, Yufeng Yuan, Xiaochen Zuo, Yu Yue, Tiantian Fan, Gaohong Liu, Lingjun Liu, Xin Liu, et al. Dapo: An open-source llm reinforcement learning system at scale. 2025a.
  45. Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al. Formalmath: Benchmarking formal mathematical reasoning of large language models. arXiv preprint arXiv:2505.02735, 2025b. find
  46. Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, Zhenwen Liang, Zhuosheng Zhang, Rui Wang, et al. Deeptheorem: Advancing llm reasoning for theorem proving through natural language and reinforcement learning. arXiv preprint arXiv:2505.23754, 2025. — [arXiv:2505.23754](https://arxiv.org/abs/2505.23754) find
  47. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021.
  48. 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/chen-2025-reform-reflective-autoformalization-prospective-bounded/