---
title: "Theorem Prover as a Judge for Synthetic Data Generation (2025)"
description: "Synthetic math data for LLMs often contains solutions whose final answer is right but whose… 67 references, cited by 8 papers here."
authors: ["Joshua Ong Jun Leang", "Giwon Hong", "Wenda Li", "Shay B. Cohen"]
year: 2025
venue: "Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)"
source: "https://aclanthology.org/2025.acl-long.1448/"
doi: "10.18653/v1/2025.acl-long.1448"
licence: "CC BY 4.0 (ACL Anthology)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/leang-2025-theorem-prover-as-judge-synthetic/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/leang-2025-theorem-prover-as-judge-synthetic/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/9/) / Theorem Prover as a Judge for Synthetic Data Generation

# Theorem Prover as a Judge for Synthetic Data Generation

**Authors:** [Joshua Ong Jun Leang](https://md.research.elamur.ai/free/en/authors/joshua-ong-jun-leang/), [Giwon Hong](https://md.research.elamur.ai/free/en/authors/giwon-hong/), [Wenda Li](https://md.research.elamur.ai/free/en/authors/wenda-li/) and [Shay B. Cohen](https://md.research.elamur.ai/free/en/authors/shay-b-cohen/) · **Year:** 2025 · **Venue:** [Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)](https://md.research.elamur.ai/free/en/venues/acl/) ([ACL 2025](https://md.research.elamur.ai/free/en/venues/acl/2025/)) · **Publisher:** [Association for Computational Linguistics](https://md.research.elamur.ai/free/en/publishers/association-for-computational-linguistics/) · **Licence:** [CC BY 4.0 (ACL Anthology)](https://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://aclanthology.org/2025.acl-long.1448/) · [PDF](https://aclanthology.org/2025.acl-long.1448.pdf) · [DOI 10.18653/v1/2025.acl-long.1448](https://doi.org/10.18653/v1/2025.acl-long.1448) · [OpenAlex](https://openalex.org/W4412889765)

**Citations:** 1 citations (OpenAlex, 2026-10-14) · [8](https://md.research.elamur.ai/free/en/papers/leang-2025-theorem-prover-as-judge-synthetic/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Synthetic math data for LLMs often contains solutions whose final answer is right but whose intermediate steps are wrong. LLM-as-a-Judge filtering can be biased, and translating solutions into a formal prover often produces code that fails to run. The authors address this with three parts.

- **Iterative autoformalisation:** Lean error messages are fed back to the model so it can repair its formal code.
- **TP-as-a-Judge:** a pipeline that generates questions and answers with LLMs and then has the Lean prover check both, step by step.
- **RLTPF:** prover verdicts take the place of human preference labels in an RLHF-style setup, which combines SFT with DPO.

Questions are created by reverse question-answering, seeded with examples from GSM8K and MATH. Two GPT-4o variants solve each question, and their verified or refuted answers determine how each sample is used in training. With only 3,508 samples, the approach improves several 7–8B open models on arithmetic and word-problem benchmarks. The authors report results competitive with models trained on far larger datasets. The work suggests that formal verification of reasoning steps can replace both human annotation and costly search-based data curation.

## Key points
- Allowing up to five repair rounds raised the share of Lean formalisations that execute successfully from 60% to 87%.
- Question checking has four stages:
  - symbolic rewriting with CoMAT;
  - Lean autoformalisation;
  - Auto-Informalisation back into natural language with gpt-4o;
  - an Alignment Check comparing the result against the original question.
- Answers come from gpt-4o and chatgpt-4o-latest and are sorted as follows:
  - both verified → SFT;
  - one verified and one refuted → DPO;
  - both refuted → discarded.
- Reported gains include +5.56% for Mistral-7B on MultiArith, +6.00% for Llama-2-7B on SVAMP, and +3.55% for Llama-3.1-8B on AQUA. On SIMQA, Llama-3.1-8B scored 83.75% when SFT used only verified data, versus 79.60% when SFT used all data.
- The code is released at github.com/joshuaongg21/RLTPF. Stated limitations:
  - coverage is restricted to algebra, counting/probability, and problem solving;
  - iterative formalisation is computationally expensive;
  - scaling beyond 8B models is difficult.

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

## Institutions

- [University of Edinburgh](https://md.research.elamur.ai/free/en/universities/university-of-edinburgh/) — University, Edinburgh, United Kingdom · 359 works · 77,352 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 16,667 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 16,194 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 252 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,426 works

## Cite

Cite as: Joshua Ong Jun Leang, Giwon Hong, Wenda Li and Shay B. Cohen. 2025. Theorem Prover as a Judge for Synthetic Data Generation. Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers).

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{leang2025theorem,
  title = {{Theorem Prover as a Judge for Synthetic Data Generation}},
  author = {Joshua Ong Jun Leang, Giwon Hong, Wenda Li and Shay B. Cohen},
  booktitle = {Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)},
  year = {2025},
  doi = {10.18653/v1/2025.acl-long.1448},
  url = {https://doi.org/10.18653/v1/2025.acl-long.1448}
}
```

- [← previous The Mirage of Model Editing: Revisiting Evaluation in the Wild](https://md.research.elamur.ai/free/en/papers/yang-2025-mirage-model-editing-revisiting-evaluation/)
- [next → Thinking Out Loud: Do Reasoning Models Know When They're Right?](https://md.research.elamur.ai/free/en/papers/zeng-2025-thinking-out-loud-do-reasoning/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/9/)

## References

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

1. Nishant Balepur, Feng Gu, Abhilasha Ravichander, Shi Feng, Jordan Boyd-Graber, and Rachel Rudinger. 2024. Reverse question answering: Can an LLM write a question so hard (or bad) that it can’t answer? ArXiv preprint, abs/2410.15512. [find](https://scholar.google.com/scholar?q=Nishant+Balepur%2C+Feng+Gu%2C+Abhilasha+Ravichander%2C+Shi+Feng%2C+Jordan+Boyd%2DGraber%2C+and+Rachel+Rudinger%2E+2024%2E+Reverse+question+answering%3A+Can+an+LLM+write+a+question+so+hard+%28or+bad%29+that+it+can%E2%80%99t+answer%3F)
2. Zhangqian Bi, Yao Wan, Zheng Wang, Hongyu Zhang, Batu Guan, Fangxin Lu, Zili Zhang, Yulei Sui, Xuanhua Shi, and Hai Jin. 2024. Iterative refinement of project-level code context for precise code generation with compiler feedback. ArXiv preprint, abs/2403.16792. [find](https://scholar.google.com/scholar?q=Zhangqian+Bi%2C+Yao+Wan%2C+Zheng+Wang%2C+Hongyu+Zhang%2C+Batu+Guan%2C+Fangxin+Lu%2C+Zili+Zhang%2C+Yulei+Sui%2C+Xuanhua+Shi%2C+and+Hai+Jin%2E+2024%2E+Iterative+refinement+of+project%2Dlevel+code+context+for+precise+code+gener)
3. Bradley Brown, Jordan Juravsky, Ryan Ehrlich, Ronald Clark, Quoc V Le, Christopher Ré, and Azalia Mirhoseini. 2024. [Large language monkeys: Scaling inference compute with repeated sampling](https://md.research.elamur.ai/free/en/papers/brown-2024-large-language-monkeys-scaling-inference/). ArXiv preprint, abs/2407.21787.
4. Davide Castelvecchi. 2021. Mathematicians welcome computer-assisted proof in ‘grand unification’theory. Nature, 595(7865):18–19. [find](https://scholar.google.com/scholar?q=Davide+Castelvecchi%2E+2021%2E+Mathematicians+welcome+computer%2Dassisted+proof+in+%E2%80%98grand+unification%E2%80%99theory%2E+Nature%2C+595%287865%29%3A18%E2%80%9319%2E)
5. Guoxin Chen, Minpeng Liao, Chengxi Li, and Kai Fan. 2024. [Alphamath almost zero: Process supervision without process](https://md.research.elamur.ai/free/en/papers/chen-2024-alphamath-almost-zero-process-supervision/). In Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, December 10 - 15, 2024.
6. Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W Cohen. 2022. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks. ArXiv preprint, abs/2211.12588. [find](https://scholar.google.com/scholar?q=Wenhu+Chen%2C+Xueguang+Ma%2C+Xinyi+Wang%2C+and+William+W+Cohen%2E+2022%2E+Program+of+thoughts+prompting%3A+Disentangling+computation+from+reasoning+for+numerical+reasoning+tasks%2E+ArXiv+preprint%2C+abs%2F2211%2E12588%2E)
7. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. 2021. [Training verifiers to solve math word problems](https://md.research.elamur.ai/free/en/papers/cobbe-2021-training-verifiers-solve-math-word/). ArXiv preprint, abs/2110.14168.
8. Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer. [find](https://scholar.google.com/scholar?q=Leonardo+De+Moura+and+Nikolaj+Bj%C3%B8rner%2E+2008%2E+Z3%3A+An+efficient+SMT+solver%2E+In+International+conference+on+Tools+and+Algorithms+for+the+Construction+and+Analysis+of+Systems%2C+pages+337%E2%80%93340%2E+Springer%2E)
9. Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. Springer. [find](https://scholar.google.com/scholar?q=Leonardo+De+Moura%2C+Soonho+Kong%2C+Jeremy+Avigad%2C+Floris+Van+Doorn%2C+and+Jakob+von+Raumer%2E+2015%2E+The+lean+theorem+prover+%28system+description%29%2E+In+Automated+Deduction%2DCADE%2D25%3A+25th+International+Conference)
10. Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. 2024. [The Llama 3 herd of models](https://md.research.elamur.ai/free/en/papers/grattafiori-2024-llama-3-herd-models/). ArXiv preprint, abs/2407.21783.
11. Manuel Eberl, Anthony Bordg, Lawrence C Paulson, and Wenda Li. 2024. Formalising half of a graduate textbook on number theory (short paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Schloss Dagstuhl–Leibniz-Zentrum für Informatik. [find](https://scholar.google.com/scholar?q=Manuel+Eberl%2C+Anthony+Bordg%2C+Lawrence+C+Paulson%2C+and+Wenda+Li%2E+2024%2E+Formalising+half+of+a+graduate+textbook+on+number+theory+%28short+paper%29%2E+In+15th+International+Conference+on+Interactive+Theorem+Pro)
12. Zhibin Gou, Zhihong Shao, Yeyun Gong, Yelong Shen, Yujiu Yang, Nan Duan, and Weizhu Chen. 2024a. [CRITIC: large language models can self-correct with tool-interactive critiquing](https://md.research.elamur.ai/free/en/papers/gou-2023-critic-large-language-models-self/). In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. Open-Revi…
13. Zhibin Gou, Zhihong Shao, Yeyun Gong, Yelong Shen, Yujiu Yang, Minlie Huang, Nan Duan, and Weizhu Chen. 2024b. [Tora: A tool-integrated reasoning agent for mathematical problem solving](https://md.research.elamur.ai/free/en/papers/gou-2023-tora-tool-integrated-reasoning-agent/). In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. Op…
14. WT Gowers, Ben Green, Freddie Manners, and Terence Tao. 2023. On a conjecture of marton. ArXiv preprint, abs/2311.05762. [find](https://scholar.google.com/scholar?q=WT+Gowers%2C+Ben+Green%2C+Freddie+Manners%2C+and+Terence+Tao%2E+2023%2E+On+a+conjecture+of+marton%2E+ArXiv+preprint%2C+abs%2F2311%2E05762%2E)
15. Xinyu Guan, Li Lyna Zhang, Yifei Liu, Ning Shang, Youran Sun, Yi Zhu, Fan Yang, and Mao Yang. 2025. [rstar-math: Small LLMs can master math reasoning with self-evolved deep thinking](https://md.research.elamur.ai/free/en/papers/guan-2025-rstar-math-small-llms-can/). ArXiv preprint, abs/2501.04519.
16. Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. 2025. [Deepseek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning](https://md.research.elamur.ai/free/en/papers/deepseek-ai-2025-deepseek-r1-incentivizing-reasoning-capability/). ArXiv preprint, abs/2501.12948.
17. Chaoqun He, Renjie Luo, Yuzhuo Bai, Shengding Hu, Zhen Leng Thai, Junhao Shen, Jinyi Hu, Xu Han, Yujie Huang, Yuxiang Zhang, et al. 2024. [Olympiadbench: A challenging benchmark for promoting AGI with olympiad-level bilingual multimodal scientific problems](https://md.research.elamur.ai/free/en/papers/he-2024-olympiadbench-challenging-benchmark-promoting-agi/). ArXiv preprint, abs/2402.14008.
18. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. [Measuring mathematical problem solving with the math dataset](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-mathematical-problem-solving-math/). ArXiv preprint, abs/2103.03874.
19. Edward J. Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. 2022. [Lora: Low-rank adaptation of large language models](https://md.research.elamur.ai/free/en/papers/hu-2021-lora-low-rank-adaptation-large/). In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net.
20. Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. 1997. The Coq proof assistant a tutorial. Rapport Technique, 178. [find](https://scholar.google.com/scholar?q=G%C3%A9rard+Huet%2C+Gilles+Kahn%2C+and+Christine+Paulin%2DMohring%2E+1997%2E+The+Coq+proof+assistant+a+tutorial%2E+Rapport+Technique%2C+178%2E)
21. Aaron Hurst, Adam Lerer, Adam P Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, AJ Ostrow, Akila Welihinda, Alan Hayes, Alec Radford, et al. 2024. [GPT-4o system card](https://md.research.elamur.ai/free/en/papers/openai-2024-gpt-4o-system-card/). ArXiv preprint, abs/2410.21276.
22. Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, et al. 2024. [OpenAI o1 system card](https://md.research.elamur.ai/free/en/papers/openai-2024-openai-o1-system-card/). ArXiv preprint, abs/2412.16720.
23. Albert Q Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, et al. 2023a. Mistral 7b. ArXiv preprint, abs/2310.06825. [find](https://scholar.google.com/scholar?q=Albert+Q+Jiang%2C+Alexandre+Sablayrolles%2C+Arthur+Mensch%2C+Chris+Bamford%2C+Devendra+Singh+Chaplot%2C+Diego+de+las+Casas%2C+Florian+Bressand%2C+Gianna+Lengyel%2C+Guillaume+Lample%2C+Lucile+Saulnier%2C+et+al%2E+2023a%2E+Mis)
24. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023b. [Draft, sketch, and prove: Guiding formal theorem provers with informal proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). In The Eleventh International Conference on Learning Representations, ICL…
25. Dongwei Jiang, Marcio Fonseca, and Shay Cohen. 2024. LeanReasoner: Boosting complex logical reasoning with lean. In Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), pages 7497–7510,… [find](https://scholar.google.com/scholar?q=Dongwei+Jiang%2C+Marcio+Fonseca%2C+and+Shay+Cohen%2E+2024%2E+LeanReasoner%3A+Boosting+complex+logical+reasoning+with+lean%2E+In+Proceedings+of+the+2024+Conference+of+the+North+American+Chapter+of+the+Association+)
26. Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. 2022. [Large language models are zero-shot reasoners](https://md.research.elamur.ai/free/en/papers/kojima-2022-large-language-models-zero-shot/). In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, Novemb…
27. Joshua Ong Jun Leang, Aryo Pradipta Gema, and Shay B Cohen. 2024. [Comat: Chain of mathematically annotated thought improves mathematical reasoning](https://md.research.elamur.ai/free/en/papers/leang-2025-comat-chain-mathematically-annotated-thought/). ArXiv preprint, abs/2410.10336.
28. Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, et al. 2024a. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face repository, 13:9. [find](https://scholar.google.com/scholar?q=Jia+Li%2C+Edward+Beeching%2C+Lewis+Tunstall%2C+Ben+Lipkin%2C+Roman+Soletskyi%2C+Shengyi+Huang%2C+Kashif+Rasul%2C+Longhui+Yu%2C+Albert+Q+Jiang%2C+Ziju+Shen%2C+et+al%2E+2024a%2E+Numinamath%3A+The+largest+public+dataset+in+ai4mat)
29. Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. 2024b. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2024,… [find](https://scholar.google.com/scholar?q=Zenan+Li%2C+Yifan+Wu%2C+Zhaoyu+Li%2C+Xinming+Wei%2C+Xian+Zhang%2C+Fan+Yang%2C+and+Xiaoxing+Ma%2E+2024b%2E+Autoformalize+mathematical+statements+by+symbolic+equivalence+and+semantic+consistency%2E+In+Advances+in+Neural+)
30. Percy Liang, Rishi Bommasani, Tony Lee, Dimitris Tsipras, Dilara Soylu, Michihiro Yasunaga, Yian Zhang, Deepak Narayanan, Yuhuai Wu, Ananya Kumar, et al. 2022. Holistic evaluation of language models. ArXiv preprint, abs/2211.09110. [find](https://scholar.google.com/scholar?q=Percy+Liang%2C+Rishi+Bommasani%2C+Tony+Lee%2C+Dimitris+Tsipras%2C+Dilara+Soylu%2C+Michihiro+Yasunaga%2C+Yian+Zhang%2C+Deepak+Narayanan%2C+Yuhuai+Wu%2C+Ananya+Kumar%2C+et+al%2E+2022%2E+Holistic+evaluation+of+language+models%2E+)
31. Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. 2024. Lean-star: Learning to interleave thinking and proving. ArXiv preprint, abs/2407.10040. [find](https://scholar.google.com/scholar?q=Haohan+Lin%2C+Zhiqing+Sun%2C+Yiming+Yang%2C+and+Sean+Welleck%2E+2024%2E+Lean%2Dstar%3A+Learning+to+interleave+thinking+and+proving%2E+ArXiv+preprint%2C+abs%2F2407%2E10040%2E)
32. Wang Ling, Dani Yogatama, Chris Dyer, and Phil Blunsom. 2017. Program induction by rationale generation: Learning to solve and explain algebraic word problems. In Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 158–167, Vancouver… [find](https://scholar.google.com/scholar?q=Wang+Ling%2C+Dani+Yogatama%2C+Chris+Dyer%2C+and+Phil+Blunsom%2E+2017%2E+Program+induction+by+rationale+generation%3A+Learning+to+solve+and+explain+algebraic+word+problems%2E+In+Proceedings+of+the+55th+Annual+Meetin)
33. Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, et al. 2024a. Process-driven autoformalization in lean 4. ArXiv preprint, abs/2406.01940. [find](https://scholar.google.com/scholar?q=Jianqiao+Lu%2C+Yingjia+Wan%2C+Zhengying+Liu%2C+Yinya+Huang%2C+Jing+Xiong%2C+Chengwu+Liu%2C+Jianhao+Shen%2C+Hui+Jin%2C+Jipeng+Zhang%2C+Haiming+Wang%2C+et+al%2E+2024a%2E+Process%2Ddriven+autoformalization+in+lean+4%2E+ArXiv+prepri)
34. Zimu Lu, Aojun Zhou, Houxing Ren, Ke Wang, Weikang Shi, Junting Pan, Mingjie Zhan, and Hongsheng Li. 2024b. Mathgenie: Generating synthetic data with question back-translation for enhancing mathematical reasoning of llms. ArXiv preprint, abs/2402.16352. [find](https://scholar.google.com/scholar?q=Zimu+Lu%2C+Aojun+Zhou%2C+Houxing+Ren%2C+Ke+Wang%2C+Weikang+Shi%2C+Junting+Pan%2C+Mingjie+Zhan%2C+and+Hongsheng+Li%2E+2024b%2E+Mathgenie%3A+Generating+synthetic+data+with+question+back%2Dtranslation+for+enhancing+mathematic)
35. Liangchen Luo, Yinxiao Liu, Rosanne Liu, Samrat Phatale, Harsh Lara, Yunxuan Li, Lei Shu, Yun Zhu, Lei Meng, Jiao Sun, et al. 2024. [Improve mathematical reasoning in language models by automated process supervision](https://md.research.elamur.ai/free/en/papers/luo-2024-improve-mathematical-reasoning-language-models/). ArXiv preprint, abs/2406.06592.
36. Qing Lyu, Shreya Havaldar, Adam Stein, Li Zhang, Delip Rao, Eric Wong, Marianna Apidianaki, and Chris Callison-Burch. 2023. [Faithful chain-of-thought reasoning](https://md.research.elamur.ai/free/en/papers/lyu-2023-faithful-chain-thought-reasoning/). In Proceedings of the 13th International Joint Conference on Natural Language Processing and the 3rd Conference of the Asia-Pacific Chapter…
37. Iman Mirzadeh, Keivan Alizadeh, Hooman Shahrokhi, Oncel Tuzel, Samy Bengio, and Mehrdad Farajtabar. 2024. [Gsm-symbolic: Understanding the limitations of mathematical reasoning in large language models](https://md.research.elamur.ai/free/en/papers/mirzadeh-2024-gsm-symbolic-understanding-limitations-mathematical/). ArXiv preprint, abs/2410.05229.
38. Niklas Muennighoff, Zitong Yang, Weijia Shi, Xiang Lisa Li, Li Fei-Fei, Hannaneh Hajishirzi, Luke Zettlemoyer, Percy Liang, Emmanuel Candès, and Tatsunori Hashimoto. 2025. [s1: Simple test-time scaling](https://md.research.elamur.ai/free/en/papers/muennighoff-2025-s1-simple-test-time-scaling/). ArXiv preprint, abs/2501.19393.
39. Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. 2023. [LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers](https://md.research.elamur.ai/free/en/papers/olausson-2023-linc-neurosymbolic-approach-logical-reasoning/). In Proceedings of the 2023 Conference on Empirical Methods in Natural Lan…
40. Team OLMo, Pete Walsh, Luca Soldaini, Dirk Groeneveld, Kyle Lo, Shane Arora, Akshita Bhagia, Yuling Gu, Shengyi Huang, Matt Jordan, et al. 2025. 2 olmo 2 furious. ArXiv preprint, abs/2501.00656. [find](https://scholar.google.com/scholar?q=Team+OLMo%2C+Pete+Walsh%2C+Luca+Soldaini%2C+Dirk+Groeneveld%2C+Kyle+Lo%2C+Shane+Arora%2C+Akshita+Bhagia%2C+Yuling+Gu%2C+Shengyi+Huang%2C+Matt+Jordan%2C+et+al%2E+2025%2E+2+olmo+2+furious%2E+ArXiv+preprint%2C+abs%2F2501%2E00656%2E)
41. Sungjin Park, Xiao Liu, Yeyun Gong, and Edward Choi. 2024. Ensembling large language models with process reward-guided tree search for better complex reasoning. ArXiv preprint, abs/2412.15797. [find](https://scholar.google.com/scholar?q=Sungjin+Park%2C+Xiao+Liu%2C+Yeyun+Gong%2C+and+Edward+Choi%2E+2024%2E+Ensembling+large+language+models+with+process+reward%2Dguided+tree+search+for+better+complex+reasoning%2E+ArXiv+preprint%2C+abs%2F2412%2E15797%2E)
42. Arkil Patel, Satwik Bhattamishra, and Navin Goyal. 2021. [Are NLP models really able to solve simple math word problems?](https://md.research.elamur.ai/free/en/papers/patel-2021-are-nlp-models-really-able/) In Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, pages 2080–2094, Online. Associat…
43. Lawrence C Paulson. 1994. Isabelle: A generic theorem prover. Springer. [find](https://scholar.google.com/scholar?q=Lawrence+C+Paulson%2E+1994%2E+Isabelle%3A+A+generic+theorem+prover%2E+Springer%2E)
44. Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. 2024. Improving autoformalization using type checking. ArXiv preprint, abs/2406.07222. [find](https://scholar.google.com/scholar?q=Auguste+Poiroux%2C+Gail+Weiss%2C+Viktor+Kunc%CC%8Cak%2C+and+Antoine+Bosselut%2E+2024%2E+Improving+autoformalization+using+type+checking%2E+ArXiv+preprint%2C+abs%2F2406%2E07222%2E)
45. Xin Quan, Marco Valentino, Louise A Dennis, and André Freitas. 2024. [Verification and refinement of natural language explanations through llm-symbolic theorem proving](https://md.research.elamur.ai/free/en/papers/quan-2024-verification-refinement-natural-language-explanations/). ArXiv preprint, abs/2405.01379.
46. Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher D. Manning, Stefano Ermon, and Chelsea Finn. 2023. [Direct preference optimization: Your language model is secretly a reward model](https://md.research.elamur.ai/free/en/papers/rafailov-2023-direct-preference-optimization-language-model/). In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Sy…
47. Subhro Roy and Dan Roth. 2015. [Solving general arithmetic word problems](https://md.research.elamur.ai/free/en/papers/roy-2015-solving-general-arithmetic-word-problems/). In Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pages 1743–1752, Lisbon, Portugal. Association for Computational Linguistics.
48. Swarnadeep Saha, Xian Li, Marjan Ghazvininejad, Jason Weston, and Tianlu Wang. 2025. Learning to plan & reason for evaluation with thinking-llm-as-a-judge. ArXiv preprint, abs/2501.18099. — [arXiv:2501.18099](https://arxiv.org/abs/2501.18099) [find](https://scholar.google.com/scholar?q=Swarnadeep+Saha%2C+Xian+Li%2C+Marjan+Ghazvininejad%2C+Jason+Weston%2C+and+Tianlu+Wang%2E+2025%2E+Learning+to+plan+%26+reason+for+evaluation+with+thinking%2Dllm%2Das%2Da%2Djudge%2E+ArXiv+preprint%2C+abs%2F2501%2E18099%2E+%E2%80%94+%5BarXiv%3A250)
49. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, et al. 2024. [Deepseekmath: Pushing the limits of mathematical reasoning in open language models](https://md.research.elamur.ai/free/en/papers/shao-2024-deepseekmath-pushing-limits-mathematical-reasoning/). ArXiv preprint, abs/2402.03300.
50. Andreas Stephan, Dawei Zhu, Matthias Aßenmacher, Xiaoyu Shen, and Benjamin Roth. 2024. [From calculation to adjudication: Examining llm judges on mathematical reasoning tasks](https://md.research.elamur.ai/free/en/papers/stephan-2024-calculation-adjudication-examining-llm-judges/). ArXiv preprint, abs/2409.04168.
51. Zhengyang Tang, Xingxing Zhang, Benyou Wang, and Furu Wei. 2024. Mathscale: Scaling instruction tuning for mathematical reasoning. In Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024. OpenReview.net. [find](https://scholar.google.com/scholar?q=Zhengyang+Tang%2C+Xingxing+Zhang%2C+Benyou+Wang%2C+and+Furu+Wei%2E+2024%2E+Mathscale%3A+Scaling+instruction+tuning+for+mathematical+reasoning%2E+In+Forty%2Dfirst+International+Conference+on+Machine+Learning%2C+ICML+202)
52. The Mistral AI Team. 2024. Mathstral-7b-v0.1. [https://huggingface.co/mistralai/Mathstral-7B-v0.1](https://huggingface.co/mistralai/Mathstral-7B-v0.1). [↗](https://huggingface.co/mistralai/Mathstral-7B-v0.1)
53. Shubham Toshniwal, Wei Du, Ivan Moshkov, Branislav Kisacanin, Alexan Ayrapetyan, and Igor Gitman. 2024. Openmathinstruct-2: Accelerating ai for math with massive open-source instruction data. ArXiv preprint, abs/2410.01560. [find](https://scholar.google.com/scholar?q=Shubham+Toshniwal%2C+Wei+Du%2C+Ivan+Moshkov%2C+Branislav+Kisacanin%2C+Alexan+Ayrapetyan%2C+and+Igor+Gitman%2E+2024%2E+Openmathinstruct%2D2%3A+Accelerating+ai+for+math+with+massive+open%2Dsource+instruction+data%2E+ArXiv+pr)
54. Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, et al. 2023. [Llama 2: Open foundation and fine-tuned chat models](https://md.research.elamur.ai/free/en/papers/touvron-2023-llama-2-open-foundation-fine/). ArXiv preprint, abs/2307.09288.
55. Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. 2024a. Lego-prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, ICLR 2… [find](https://scholar.google.com/scholar?q=Haiming+Wang%2C+Huajian+Xin%2C+Chuanyang+Zheng%2C+Zhengying+Liu%2C+Qingxing+Cao%2C+Yinya+Huang%2C+Jing+Xiong%2C+Han+Shi%2C+Enze+Xie%2C+Jian+Yin%2C+Zhenguo+Li%2C+and+Xiaodan+Liang%2E+2024a%2E+Lego%2Dprover%3A+Neural+theorem+proving)
56. Ke Wang, Houxing Ren, Aojun Zhou, Zimu Lu, Sichun Luo, Weikang Shi, Renrui Zhang, Linqi Song, Mingjie Zhan, and Hongsheng Li. 2024b. [Mathcoder: Seamless code integration in llms for enhanced mathematical reasoning](https://md.research.elamur.ai/free/en/papers/wang-2023-mathcoder-seamless-code-integration-llms/). In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienn…
57. Peiyi Wang, Lei Li, Zhihong Shao, Runxin Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. 2024c. [Math-shepherd: Verify and reinforce llms step-by-step without human annotations](https://md.research.elamur.ai/free/en/papers/wang-2024-math-shepherd-verify-reinforce-llms/). In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Pape…
58. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. 2022. [Chain-of-thought prompting elicits reasoning in large language models](https://md.research.elamur.ai/free/en/papers/wei-2022-chain-thought-prompting-elicits-reasoning/). In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processi…
59. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. 2024. [Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/). ArXiv preprint, abs/2405.14333.
60. Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, and Wynne Hsu. 2024. [Faithful logical reasoning via symbolic chain-of-thought](https://md.research.elamur.ai/free/en/papers/xu-2024-faithful-logical-reasoning-symbolic-chain/). ArXiv preprint, abs/2405.18357.
61. An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, et al. 2024a. Qwen2. 5-math technical report: Toward mathematical expert model via self-improvement. ArXiv preprint, abs/2409.12122. — [Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement](https://md.research.elamur.ai/free/en/papers/yang-2024-qwen2-5-math-technical-report/)
62. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. 2024b. Formal mathematical reasoning: A new frontier in ai. ArXiv preprint, abs/2412.16075. [find](https://scholar.google.com/scholar?q=Kaiyu+Yang%2C+Gabriel+Poesia%2C+Jingxuan+He%2C+Wenda+Li%2C+Kristin+Lauter%2C+Swarat+Chaudhuri%2C+and+Dawn+Song%2E+2024b%2E+Formal+mathematical+reasoning%3A+A+new+frontier+in+ai%2E+ArXiv+preprint%2C+abs%2F2412%2E16075%2E)
63. Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T. Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. 2024. [Metamath: Bootstrap your own mathematical questions for large language models](https://md.research.elamur.ai/free/en/papers/yu-2023-metamath-bootstrap-your-own-mathematical/). In The Twelfth International Conference on Learning Representations, ICLR 2024, Vie…
64. Zheng Yuan, Hongyi Yuan, Chengpeng Li, Guanting Dong, Keming Lu, Chuanqi Tan, Chang Zhou, and Jingren Zhou. 2023. [Scaling relationship on learning mathematical reasoning with large language models](https://md.research.elamur.ai/free/en/papers/yuan-2023-scaling-relationship-learning-mathematical-reasoning/). ArXiv preprint, abs/2308.01825.
65. Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah D. Goodman. 2022. [Star: Bootstrapping reasoning with reasoning](https://md.research.elamur.ai/free/en/papers/zelikman-2022-star-bootstrapping-reasoning-reasoning/). In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022.
66. Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric P. Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. 2023. [Judging llm-as-a-judge with mt-bench and chatbot arena](https://md.research.elamur.ai/free/en/papers/zheng-2023-judging-llm-judge-mt-bench/). In Advances in Neural Information Processing Systems 36: A…
67. Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, and Yuhuai Wu. 2024. Don’t trust: Verify - grounding LLM quantitative reasoning with autoformalization. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. O… [find](https://scholar.google.com/scholar?q=Jin+Peng+Zhou%2C+Charles+Staats%2C+Wenda+Li%2C+Christian+Szegedy%2C+Kilian+Q%2E+Weinberger%2C+and+Yuhuai+Wu%2E+2024%2E+Don%E2%80%99t+trust%3A+Verify+%2D+grounding+LLM+quantitative+reasoning+with+autoformalization%2E+In+The+Twelfth)

*Updated 1 November 2026*