---
title: "Don't Trust — paper by Zhou et al. (2024) — summary and ideas"
description: "The paper proposes Don't Trust: Verify (DTV), which uses autoformalization to check solutions. 46 references, cited by 42 papers here."
authors: ["Jin Peng Zhou", "Charles Staats", "Wenda Li", "Christian Szegedy", "Kilian Q. Weinberger", "Yuhuai Wu"]
year: 2024
venue: "arXiv:2403.18120"
source: "https://arxiv.org/abs/2403.18120"
doi: "10.48550/arxiv.2403.18120"
arxiv: "2403.18120"
licence: "CC BY 4.0 (arXiv)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/zhou-2024-don-t-trust-verify-grounding/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/zhou-2024-don-t-trust-verify-grounding/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/9/) / Don't Trust: Verify — Grounding LLM Quantitative Reasoning with Autoformalization

# Don't Trust: Verify — Grounding LLM Quantitative Reasoning with Autoformalization

**Authors:** [Jin Peng Zhou](https://md.research.elamur.ai/free/en/authors/jin-peng-zhou/), [Charles Staats](https://md.research.elamur.ai/free/en/authors/charles-staats/), [Wenda Li](https://md.research.elamur.ai/free/en/authors/wenda-li/), [Christian Szegedy](https://md.research.elamur.ai/free/en/authors/christian-szegedy/), [Kilian Q. Weinberger](https://md.research.elamur.ai/free/en/authors/kilian-q-weinberger/) and [Yuhuai Wu](https://md.research.elamur.ai/free/en/authors/yuhuai-wu/) · **Year:** 2024 · **Venue:** arXiv:2403.18120 · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2403.18120) · [PDF](https://arxiv.org/pdf/2403.18120v1) · [DOI 10.48550/arxiv.2403.18120](https://doi.org/10.48550/arxiv.2403.18120) · [arXiv 2403.18120](https://arxiv.org/abs/2403.18120) · [OpenAlex](https://openalex.org/W4393299873)

**Citations:** 3 citations (OpenAlex, 2026-10-14) · [42](https://md.research.elamur.ai/free/en/papers/zhou-2024-don-t-trust-verify-grounding/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
LLMs such as Minerva and GPT-3.5 can produce step-by-step solutions to math word problems, but these often contain arithmetic slips or unjustified logical jumps. Majority voting over sampled solutions helps, yet the most frequent answer is not always right. The paper proposes Don't Trust: Verify (DTV), which uses autoformalization to check solutions.

For each sampled solution, an LLM is few-shot prompted to do two things:
- turn the problem plus the extracted answer into an Isabelle theorem;
- turn the natural-language reasoning into a formal proof sketch.

An automated theorem prover then tries to fill the low-level gaps step by step. Symbolic and neural filters discard unfaithful statement translations, such as vacuous ones. Majority voting is then applied only to the solutions that pass verification.

DTV needs no training. It was tested on GSM8K, three MATH subsets and MultiArith, and it beat plain majority voting across all datasets and model sizes. This shows that formal verifiers can make LLM quantitative reasoning more reliable even when only natural-language data is available.

## Key points
- DTV outperforms majority voting by more than 12% on GSM8K. Results use 64 samples per problem, and the method also works with fewer samples.
- On MATH Number Theory, with Minerva 62B solutions:
  - single sample: 12.2%
  - majority voting: 23.7%
  - DTV with Minerva 62B formalization: 31.9%
  - DTV with GPT-3.5 formalization: 36.1%
- When GPT-3.5 generates both the solutions and their formalizations, DTV reaches 49.4%, compared with 41.0% for majority voting.
- Keeping only verified solutions sharply raises the share of correct answers. For Number Theory it rises from 24.3% to 50.5% (Minerva 62B) or 62.3% (GPT-3.5). Algebra and Prealgebra show similar gains.
- The formal environment is Isabelle, and code is released at github.com/jinpz/dtv.

*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 · 395 works · 81,691 citations
- [Cornell University](https://md.research.elamur.ai/free/en/universities/cornell-university/) — University, Ithaca, United States · 139 works · 65,295 citations

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,959 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,789 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (2): [🧠 Language models & pretraining](https://md.research.elamur.ai/free/en/topics/language-models/) · 4,145 works · [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: 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. arXiv:2403.18120.

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

```bibtex
@misc{zhou2024don,
  title = {{Don't Trust: Verify — Grounding LLM Quantitative Reasoning with Autoformalization}},
  author = {Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger and Yuhuai Wu},
  year = {2024},
  doi = {10.48550/arxiv.2403.18120},
  eprint = {2403.18120},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2403.18120}
}
```

- [← previous Cross-Lingual Knowledge Editing in Large Language Models](https://md.research.elamur.ai/free/en/papers/wang-2024-cross-lingual-knowledge-editing-large/)
- [next → GLoRe: When, Where, and How to Improve LLM Reasoning via Global and Local Refinements](https://md.research.elamur.ai/free/en/papers/havrilla-2024-glore-where-improve-llm-reasoning/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/9/)

## References

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

1. Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. [Towards a mathematics formalisation assistant using large language models](https://md.research.elamur.ai/free/en/papers/agrawal-2022-mathematics-formalisation-assistant-large-language/). arXiv preprint arXiv:2211.07524, 2022.
2. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. [Proofnet: Autoformalizing and formally proving undergraduate-level mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). arXiv preprint arXiv:2302.12433, 2023.
3. Yuntao Bai, Andy Jones, Kamal Ndousse, Amanda Askell, Anna Chen, Nova DasSarma, Dawn Drain, Stanislav Fort, Deep Ganguli, Tom Henighan, et al. Training a helpful and harmless assistant with reinforcement learning from human feedback. arXiv preprint arXiv:2204.05862, 2022. [find](https://scholar.google.com/scholar?q=Yuntao+Bai%2C+Andy+Jones%2C+Kamal+Ndousse%2C+Amanda+Askell%2C+Anna+Chen%2C+Nova+DasSarma%2C+Dawn+Drain%2C+Stanislav+Fort%2C+Deep+Ganguli%2C+Tom+Henighan%2C+et+al%2E+Training+a+helpful+and+harmless+assistant+with+reinforcem)
4. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997. [find](https://scholar.google.com/scholar?q=Bruno+Barras%2C+Samuel+Boutin%2C+Cristina+Cornes%2C+Judicae%CC%88l+Courant%2C+Jean%2DChristophe+Filliatre%2C+Eduardo+Gimenez%2C+Hugo+Herbelin%2C+Gerard+Huet%2C+Cesar+Munoz%2C+Chetan+Murthy%2C+et+al%2E+The+Coq+proof+assistant+refe)
5. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. [Language models are few-shot learners](https://md.research.elamur.ai/free/en/papers/brown-2020-language-models-few-shot-learners/). Advances in neural information processing systems, 33:1877–1901, 2020.
6. Davide Castelvecchi et al. Mathematicians welcome computer-assisted proof in ‘grand unification’theory. Nature, 595(7865):18–19, 2021. [find](https://scholar.google.com/scholar?q=Davide+Castelvecchi+et+al%2E+Mathematicians+welcome+computer%2Dassisted+proof+in+%E2%80%98grand+unification%E2%80%99theory%2E+Nature%2C+595%287865%29%3A18%E2%80%9319%2C+2021%2E)
7. Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W. Cohen. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks, 2022. [find](https://scholar.google.com/scholar?q=Wenhu+Chen%2C+Xueguang+Ma%2C+Xinyi+Wang%2C+and+William+W%2E+Cohen%2E+Program+of+thoughts+prompting%3A+Disentangling+computation+from+reasoning+for+numerical+reasoning+tasks%2C+2022%2E)
8. Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, et al. [Palm: Scaling language modeling with pathways](https://md.research.elamur.ai/free/en/papers/chowdhery-2022-palm-scaling-language-modeling-pathways/). arXiv preprint arXiv:2204.02311, 2022.
9. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. [Training verifiers to solve math word problems](https://md.research.elamur.ai/free/en/papers/cobbe-2021-training-verifiers-solve-math-word/). arXiv preprint arXiv:2110.14168, 2021.
10. Antonia Creswell, Murray Shanahan, and Irina Higgins. Selection-inference: Exploiting large language models for interpretable logical reasoning, 2022. [find](https://scholar.google.com/scholar?q=Antonia+Creswell%2C+Murray+Shanahan%2C+and+Irina+Higgins%2E+Selection%2Dinference%3A+Exploiting+large+language+models+for+interpretable+logical+reasoning%2C+2022%2E)
11. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 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, pp. 378–388. [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+The+lean+theorem+prover+%28system+description%29%2E+In+Automated+Deduction%2DCADE%2D25%3A+25th+International+Conference+on+Au)
12. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. [Bert: Pre-training of deep bidirectional transformers for language understanding](https://md.research.elamur.ai/free/en/papers/devlin-2019-bert-pre-training-deep-bidirectional/). arXiv preprint arXiv:1810.04805, 2018.
13. Yao Fu, Hao Peng, Ashish Sabharwal, Peter Clark, and Tushar Khot. [Complexity-based prompting for multi-step reasoning](https://md.research.elamur.ai/free/en/papers/fu-2022-complexity-based-prompting-multi-step/), 2023.
14. Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. Pal: Program-aided language models. arXiv preprint arXiv:2211.10435, 2022. [find](https://scholar.google.com/scholar?q=Luyu+Gao%2C+Aman+Madaan%2C+Shuyan+Zhou%2C+Uri+Alon%2C+Pengfei+Liu%2C+Yiming+Yang%2C+Jamie+Callan%2C+and+Graham+Neubig%2E+Pal%3A+Program%2Daided+language+models%2E+arXiv+preprint+arXiv%3A2211%2E10435%2C+2022%2E)
15. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. [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 arXiv:2103.03874, 2021. [https://github.com/albertqjiang/Portal-to-ISAbelle](https://github.com/albertqjiang/Portal-to-ISAbelle) [↗](https://github.com/albertqjiang/Portal-to-ISAbelle)
16. Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. [The curious case of neural text degeneration](https://md.research.elamur.ai/free/en/papers/holtzman-2019-curious-case-neural-text-degeneration/). arXiv preprint arXiv:1904.09751, 2019.
17. Shima Imani, Liang Du, and Harsh Shrivastava. [Mathprompter: Mathematical reasoning using large language models](https://md.research.elamur.ai/free/en/papers/imani-2023-mathprompter-mathematical-reasoning-large-language/). arXiv preprint arXiv:2303.05398, 2023.
18. Gautier Izacard, Patrick Lewis, Maria Lomeli, Lucas Hosseini, Fabio Petroni, Timo Schick, Jane Dwivedi-Yu, Armand Joulin, Sebastian Riedel, and Edouard Grave. [Atlas: Few-shot learning with retrieval augmented language models](https://md.research.elamur.ai/free/en/papers/izacard-2022-atlas-few-shot-learning-retrieval/). arXiv preprint arXiv, 2208, 2022.
19. Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pp. 378–392, 2021. [find](https://scholar.google.com/scholar?q=Albert+Qiaochu+Jiang%2C+Wenda+Li%2C+Jesse+Michael+Han%2C+and+Yuhuai+Wu%2E+Lisa%3A+Language+models+of+isabelle+proofs%2E+In+6th+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+pp%2E+378%E2%80%93392%2C+2021%2E)
20. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timoth’ee Lacroix, Yuhuai Wu, and Guillaume Lample. [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 International Conference on Learning Representations, 2023. URL [https://doi.…](https://doi.…) [↗](https://doi.…)
21. Jaehun Jung, Lianhui Qin, Sean Welleck, Faeze Brahman, Chandra Bhagavatula, Ronan Le Bras, and Yejin Choi. [Maieutic prompting: Logically consistent reasoning with recursive explanations](https://md.research.elamur.ai/free/en/papers/jung-2022-maieutic-prompting-logically-consistent-reasoning/). In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, pp. 1266–1279, Abu Dha…
22. Aishwarya Kamath and Rajarshi Das. A survey on semantic parsing. arXiv preprint arXiv:1812.00978, 2018. — [arXiv:1812.00978](https://arxiv.org/abs/1812.00978) [find](https://scholar.google.com/scholar?q=Aishwarya+Kamath+and+Rajarshi+Das%2E+A+survey+on+semantic+parsing%2E+arXiv+preprint+arXiv%3A1812%2E00978%2C+2018%2E+%E2%80%94+%5BarXiv%3A1812%2E00978%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1812%2E00978%29)
23. Tushar Khot, Harsh Trivedi, Matthew Finlayson, Yao Fu, Kyle Richardson, Peter Clark, and Ashish Sabharwal. [Decomposed prompting: A modular approach for solving complex tasks](https://md.research.elamur.ai/free/en/papers/khot-2022-decomposed-prompting-modular-approach/), 2023.
24. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pp. 207–22… [find](https://scholar.google.com/scholar?q=Gerwin+Klein%2C+Kevin+Elphinstone%2C+Gernot+Heiser%2C+June+Andronick%2C+David+Cock%2C+Philip+Derrin%2C+Dhammika+Elkaduwe%2C+Kai+Engelhardt%2C+Rafal+Kolanski%2C+Michael+Norrish%2C+et+al%2E+sel4%3A+Formal+verification+of+an+os)
25. Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. [Large language models are zero-shot reasoners](https://md.research.elamur.ai/free/en/papers/kojima-2022-large-language-models-zero-shot/). Advances in neural information processing systems, 35: 22199–22213, 2022.
26. Angeliki Lazaridou, Elena Gribovskaya, Wojciech Stokowiec, and Nikolai Grigorev. [Internet-augmented language models through few-shot prompting for open-domain question answering](https://md.research.elamur.ai/free/en/papers/lazaridou-2022-internet-augmented-language-models-through/). arXiv preprint arXiv:2203.05115, 2022.
27. Aitor Lewkowycz, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. [Solving quantitative reasoning problems with language models](https://md.research.elamur.ai/free/en/papers/lewkowycz-2022-solving-quantitative-reasoning-problems-language/). In Alic…
28. Reiichiro Nakano, Jacob Hilton, Suchir Balaji, Jeff Wu, Long Ouyang, Christina Kim, Christopher Hesse, Shantanu Jain, Vineet Kosaraju, William Saunders, et al. [Webgpt: Browser-assisted question-answering with human feedback](https://md.research.elamur.ai/free/en/papers/nakano-2021-webgpt-browser-assisted-question-answering/). arXiv preprint arXiv:2112.09332, 2021.
29. Tobias Nipkow, Markus Wenzel, and Lawrence Charles Paulson. Isabelle/hol: A proof assistant for higher-order logic. 2002. [find](https://scholar.google.com/scholar?q=Tobias+Nipkow%2C+Markus+Wenzel%2C+and+Lawrence+Charles+Paulson%2E+Isabelle%2Fhol%3A+A+proof+assistant+for+higher%2Dorder+logic%2E+2002%2E)
30. OpenAI. Introducing chatgpt. URL — [GPT-4 Technical Report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/) [https://openai.com/blog/chatgpt](https://openai.com/blog/chatgpt). OpenAI. Gpt-4 technical report, 2023. [↗](https://openai.com/blog/chatgpt)
31. Lawrence C Paulsson and Jasmin C Blanchette. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Proceedings of the 8th International Workshop on the Implementation of Logics (IWIL-2010), Yogyakarta, Indonesia. EPiC, volume 2, 2012. [find](https://scholar.google.com/scholar?q=Lawrence+C+Paulsson+and+Jasmin+C+Blanchette%2E+Three+years+of+experience+with+sledgehammer%2C+a+practical+link+between+automatic+and+interactive+theorem+provers%2E+In+Proceedings+of+the+8th+International+Wo)
32. Subhro Roy and Dan Roth. arXiv:1608.[01413, 2016](https://md.research.elamur.ai/free/en/papers/roy-2015-solving-general-arithmetic-word-problems/).
33. Solving general arithmetic word problems. arXiv preprint William Saunders, Catherine Yeh, Jeff Wu, Steven Bills, Long Ouyang, Jonathan Ward, and Jan Leike. [Self-critiquing models for assisting human evaluators](https://md.research.elamur.ai/free/en/papers/saunders-2022-self-critiquing-models-assisting-human/). arXiv preprint arXiv:2206.05802, 2022.
34. Timo Schick, Jane Dwivedi-Yu, Roberto Dessı̀, Roberta Raileanu, Maria Lomeli, Luke Zettlemoyer, Nicola Cancedda, and Thomas Scialom. [Toolformer: Language models can teach themselves to use tools](https://md.research.elamur.ai/free/en/papers/schick-2023-toolformer-language-models-can-teach/). arXiv preprint arXiv:2302.04761, 2023.
35. Weijia Shi, Sewon Min, Michihiro Yasunaga, Minjoon Seo, Rich James, Mike Lewis, Luke Zettlemoyer, and Wen-tau Yih. [Replug: Retrieval-augmented black-box language models](https://md.research.elamur.ai/free/en/papers/shi-2023-replug-retrieval-augmented-black-box/). arXiv preprint arXiv:2301.12652, 2023.
36. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13, pp. 3–20. [find](https://scholar.google.com/scholar?q=Christian+Szegedy%2E+A+promising+path+towards+autoformalization+and+general+artificial+intelligence%2E+In+Intelligent+Computer+Mathematics%3A+13th+International+Conference%2C+CICM+2020%2C+Bertinoro%2C+Italy%2C+July)
37. Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. [Exploration of neural machine translation in autoformalization of mathematics in mizar](https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/). In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 85–98, 2020.
38. Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, and Denny Zhou. [Self-consistency improves chain of thought reasoning in language models](https://md.research.elamur.ai/free/en/papers/wang-2022-self-consistency-improves-chain-thought/). arXiv preprint arXiv:2203.11171, 2022.
39. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed H. Chi, Quoc V Le, and Denny Zhou. Chain of thought prompting elicits reasoning in large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Proce… — [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/)
40. Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. [Naturalprover: Grounded mathematical proof generation with language models](https://md.research.elamur.ai/free/en/papers/welleck-2022-naturalprover-grounded-mathematical-proof-generation/), 2022.
41. Freek Wiedijk. Formal proof sketches. Lecture notes in computer science, 3085:378–393, 2004. [find](https://scholar.google.com/scholar?q=Freek+Wiedijk%2E+Formal+proof+sketches%2E+Lecture+notes+in+computer+science%2C+3085%3A378%E2%80%93393%2C+2004%2E)
42. Freek Wiedijk. Formal proof–getting started. 2008. [find](https://scholar.google.com/scholar?q=Freek+Wiedijk%2E+Formal+proof%E2%80%93getting+started%2E+2008%2E)
43. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). Advances in Neural Information Processing Systems, 35:32353–32368, 2022.
44. Zhuosheng Zhang, Aston Zhang, Mu Li, and Alex Smola. [Automatic chain of thought prompting in large language models](https://md.research.elamur.ai/free/en/papers/zhang-2022-automatic-chain-thought-prompting-large/). arXiv preprint arXiv:2210.03493, 2022.
45. Chuanyang Zheng, Zhengying Liu, Enze Xie, Zhenguo Li, and Yu Li. [Progressive-hint prompting improves reasoning in large language models](https://md.research.elamur.ai/free/en/papers/zheng-2023-progressive-hint-prompting-improves-reasoning/), 2023.
46. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. [Minif2f: a cross-system benchmark for formal olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). arXiv preprint arXiv:2109.00110, 2021.

*Updated 3 November 2026*