mlsanityData to 14 Oct 2026

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

arXiv 2403.18120 ↗First posted 26 Mar 2024cs.AI cs.CL cs.LGcited by 55

On the map: LLM reasoning → Mathematical reasoning

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.

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.

Builds on

33 of 44 references.

Closest ancestors · 2

Same direction, newest first

  1. 2023MathPrompter: Mathematical Reasoning using Large Language Models4 Mar
  2. 2022Solving Quantitative Reasoning Problems with Language Models29 Jun

Other references · 31

  1. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,399
  2. 2020Language Models are Few-Shot Learnerscited by 32,419
  3. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
  4. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  5. 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,708
  6. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  7. 2022PaLM: Scaling Language Modeling with Pathwayscited by 5,326
  8. 2022Large Language Models are Zero-Shot Reasonerscited by 4,374
  9. 2023Toolformer: Language Models Can Teach Themselves to Use Toolscited by 4,182
  10. 2022Training a Helpful and Harmless Assistant with Reinforcement Learning from Human Feedbackcited by 3,720
  11. 2019The Curious Case of Neural Text Degenerationcited by 2,916
  12. 2021WebGPT: Browser-assisted question-answering with human feedbackcited by 1,745
19 more
  1. 2022Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Taskscited by 1,076
  2. 2022Atlas: Few-shot Learning with Retrieval Augmented Language Modelscited by 952
  3. 2023REPLUG: Retrieval-Augmented Black-Box Language Modelscited by 792
  4. 2022Automatic Chain of Thought Prompting in Large Language Modelscited by 688
  5. 2022PAL: Program-aided Language Modelscited by 652
  6. 2022Decomposed Prompting: A Modular Approach for Solving Complex Taskscited by 558
  7. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  8. 2022Self-critiquing models for assisting human evaluatorscited by 380
  9. 2016Solving General Arithmetic Word Problemscited by 360
  10. 2022Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoningcited by 334
  11. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  12. 2022Autoformalization with Large Language Modelscited by 263
  13. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  14. 2022Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanationscited by 159
  15. 2023Progressive-Hint Prompting Improves Reasoning in Large Language Modelscited by 147
  16. 2022Internet-augmented language models through few-shot prompting for open-domain question answeringcited by 131
  17. 2018A Survey on Semantic Parsingcited by 62
  18. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  19. 2022Towards a Mathematics Formalisation Assistant using Large Language Modelscited by 22

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2024: 13; 2025: 33; 2026: 9.

55 papers.

Sort:

By area:

  1. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  2. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 68
  3. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 59
  4. 2024Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verificationcited by 40
  5. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 35
  6. 2024Enhancing Reasoning Capabilities of LLMs via Principled Synthetic Logic Corpuscited by 29
  7. 2025PDE-Controller: LLMs for Autoformalization and Reasoning of PDEscited by 23
  8. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  9. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 21
  10. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 21
  11. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 16
  12. 2025Theorem Prover as a Judge for Synthetic Data Generationcited by 14
38 more
  1. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  2. 2025Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalizationcited by 12
  3. 2024HYBRIDMIND: Meta Selection of Natural Language and Symbolic Language for Enhanced LLM Reasoningcited by 11
  4. 2025A Survey on Feedback-based Multi-step Reasoning for Large Language Models on Mathematicscited by 11
  5. 2025Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capabilitycited by 11
  6. 2024DAPE V2: Process Attention Score as Feature Map for Length Extrapolationcited by 10
  7. 2024FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardwarecited by 10
  8. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Predictioncited by 10
  9. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 10
  10. 2025ASSESS: A Semantic and Structural Evaluation Framework for Statement Similaritycited by 10
  11. 2025ProtoReasoning: Prototypes as the Foundation for Generalizable Reasoning in LLMscited by 9
  12. 2025Solve-Detect-Verify: Inference-Time Scaling with Flexible Generative Verifiercited by 8
  13. 2025Efficient PRM Training Data Synthesis via Formal Verificationcited by 8
  14. 2025Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Provingcited by 8
  15. 2025Advancing the Scientific Method with Large Language Models: From Hypothesis to Discoverycited by 7
  16. 2025On Learning Verifiers and Implications to Chain-of-Thought Reasoningcited by 6
  17. 2025StepProof: Step-by-step verification of natural language mathematical proofscited by 6
  18. 2025FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4cited by 5
  19. 2025Step-Wise Formal Verification for LLM-Based Mathematical Problem Solvingcited by 5
  20. 2024Improving Arithmetic Reasoning Ability of Large Language Models through Relation Tuples, Verification and Dynamic Feedbackcited by 4
  21. 2025Thinking Machines: Mathematical Reasoning in the Age of LLMscited by 4
  22. 2025Towards Verified Code Reasoning by LLMscited by 4
  23. 2025Self-Adjust Softmaxcited by 3
  24. 2025Translating Informal Proofs into Formal Proofs Using a Chain of Statescited by 3
  25. 2026Do We Need Frontier Models to Verify Mathematical Proofs?cited by 3
  26. 2024Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Taskscited by 2
  27. 2025Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solvingcited by 2
  28. 2025Creativity or Brute Force? Using Brainteasers as a Window into the Problem-Solving Abilities of Large Language Modelscited by 2
  29. 2025Argument-Based Consistency in Toxicity Explanations of LLMscited by 2
  30. 2025Improving Autoformalization Using Direct Dependency Retrievalcited by 2
  31. 2026Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofscited by 2
  32. 2024Expanding Search Space with Diverse Prompting Agents: An Efficient Sampling Approach for LLM Mathematical Reasoningcited by 1
  33. 2025KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignmentcited by 1
  34. 2025LLMs and their Limited Theory of Mind: Evaluating Mental State Annotations in Situated Dialoguecited by 1
  35. 2026Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Treescited by 1
  36. 2026Automating Formal Verification with Reinforcement Learning and Recursive Inferencecited by 1
  37. 2026The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalizationcited by 1
  38. 2026Groundability, Not Scale Alone: When Weak Reviewers Can Audit Strong Coding Agentscited by 1

50 most cited of 55 All 55 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2025Autoformalization in the Era of Large Language Models: A Survey
  2. 2024Not All Votes Count! Programs as Verifiers Improve Self-Consistency of Language Models for Math Reasoning
  3. 2025Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning
  4. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
  5. 2025FMC: Formalization of Natural Language Mathematical Competition Problems
  6. 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
  7. 2024Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
  8. 2026Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs