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

arXiv: https://arxiv.org/abs/2403.18120 · HTML: https://mlsanity.com/paper/2403.18120/

## Key facts

- Cited by 55 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 33 of its 44 references that are in the map.
- First posted on arXiv 26 Mar 2024.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 30 of 33)

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [PaLM: Scaling Language Modeling with Pathways](https://mlsanity.com/paper/2204.02311/) (2022)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [Training a Helpful and Harmless Assistant with Reinforcement Learning from Human Feedback](https://mlsanity.com/paper/2204.05862/) (2022)
- [The Curious Case of Neural Text Degeneration](https://mlsanity.com/paper/1904.09751/) (2019)
- [WebGPT: Browser-assisted question-answering with human feedback](https://mlsanity.com/paper/2112.09332/) (2021)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks](https://mlsanity.com/paper/2211.12588/) (2022)
- [Atlas: Few-shot Learning with Retrieval Augmented Language Models](https://mlsanity.com/paper/2208.03299/) (2022)
- [REPLUG: Retrieval-Augmented Black-Box Language Models](https://mlsanity.com/paper/2301.12652/) (2023)
- [Automatic Chain of Thought Prompting in Large Language Models](https://mlsanity.com/paper/2210.03493/) (2022)
- [PAL: Program-aided Language Models](https://mlsanity.com/paper/2211.10435/) (2022)
- [Decomposed Prompting: A Modular Approach for Solving Complex Tasks](https://mlsanity.com/paper/2210.02406/) (2022)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Self-critiquing models for assisting human evaluators](https://mlsanity.com/paper/2206.05802/) (2022)
- [Solving General Arithmetic Word Problems](https://mlsanity.com/paper/1608.01413/) (2016)
- [Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoning](https://mlsanity.com/paper/2205.09712/) (2022)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [MathPrompter: Mathematical Reasoning using Large Language Models](https://mlsanity.com/paper/2303.05398/) (2023)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanations](https://mlsanity.com/paper/2205.11822/) (2022)
- [Progressive-Hint Prompting Improves Reasoning in Large Language Models](https://mlsanity.com/paper/2304.09797/) (2023)
- [Internet-augmented language models through few-shot prompting for open-domain question answering](https://mlsanity.com/paper/2203.05115/) (2022)

## Built on by (most cited first, 30 of 55)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification](https://mlsanity.com/paper/2410.05318/) (2024)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [Enhancing Reasoning Capabilities of LLMs via Principled Synthetic Logic Corpus](https://mlsanity.com/paper/2411.12498/) (2024)
- [PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs](https://mlsanity.com/paper/2502.00963/) (2025)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [Theorem Prover as a Judge for Synthetic Data Generation](https://mlsanity.com/paper/2502.13137/) (2025)
- [A Survey on Mathematical Reasoning and Optimization with Large Language Models](https://mlsanity.com/paper/2503.17726/) (2025)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [HYBRIDMIND: Meta Selection of Natural Language and Symbolic Language for Enhanced LLM Reasoning](https://mlsanity.com/paper/2409.19381/) (2024)
- [A Survey on Feedback-based Multi-step Reasoning for Large Language Models on Mathematics](https://mlsanity.com/paper/2502.14333/) (2025)
- [Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability](https://mlsanity.com/paper/2505.23703/) (2025)
- [DAPE V2: Process Attention Score as Feature Map for Length Extrapolation](https://mlsanity.com/paper/2410.04798/) (2024)
- [FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware](https://mlsanity.com/paper/2410.23299/) (2024)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [ProtoReasoning: Prototypes as the Foundation for Generalizable Reasoning in LLMs](https://mlsanity.com/paper/2506.15211/) (2025)
- [Solve-Detect-Verify: Inference-Time Scaling with Flexible Generative Verifier](https://mlsanity.com/paper/2505.11966/) (2025)
- [Efficient PRM Training Data Synthesis via Formal Verification](https://mlsanity.com/paper/2505.15960/) (2025)
- [Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving](https://mlsanity.com/paper/2506.17104/) (2025)
- [Advancing the Scientific Method with Large Language Models: From Hypothesis to Discovery](https://mlsanity.com/paper/2505.16477/) (2025)
- [On Learning Verifiers and Implications to Chain-of-Thought Reasoning](https://mlsanity.com/paper/2505.22650/) (2025)
- [StepProof: Step-by-step verification of natural language mathematical proofs](https://mlsanity.com/paper/2506.10558/) (2025)
- [FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4](https://mlsanity.com/paper/2503.03238/) (2025)

## Abstract (arXiv)

Large language models (LLM), such as Google's Minerva and OpenAI's GPT families, are becoming increasingly capable of solving mathematical quantitative reasoning problems. However, they still make unjustified logical and computational errors in their reasoning steps and answers. In this paper, we leverage the fact that if the training corpus of LLMs contained sufficiently many examples of formal mathematics (e.g. in Isabelle, a formal theorem proving environment), they can be prompted to translate i.e. autoformalize informal mathematical statements into formal Isabelle code -- which can be verified automatically for internal consistency. This provides a mechanism to automatically reject solutions whose formalized versions are inconsistent within themselves or with the formalized problem statement. We evaluate our method on GSM8K, MATH and MultiArith datasets and demonstrate that our approach provides a consistently better heuristic than vanilla majority voting -- the previously best method to identify correct answers, by more than 12% on GSM8K. In our experiments it improves results consistently across all datasets and LLM model sizes. The code can be found at https://github.com/jinpz/dtv.