Research map / Large language models / Agents, code and math
Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes Don't Trust: Verify (DTV), which uses few-shot LLM autoformalization into Isabelle plus automated theorem proving to filter informal solutions before majority voting on math word problems.
Problem
Majority voting over sampled LLM solutions often selects a wrong answer, and LLM reasoning contains unjustified logical and computational errors; a better verification heuristic is needed for quantitative reasoning.
Approach
Autoformalize each informal problem (with extracted answer) and solution into Isabelle, verify with Sledgehammer and tactics, keep only verified solutions for majority voting, and use vacuous-statement and self-critique filters to reduce unfaithful formalizations. Training-free, few-shot prompting only.
Key results
- DTV with GPT-3.5 formalization reaches 68.2% average solve rate versus 61.5% for majority voting with Minerva 62B.
- On GSM8K, DTV with GPT-3.5 formalization reaches 79.4% versus 67.2% for majority voting (more than 12 points).
- DTV improves over majority voting across Minerva 8B, 62B and 540B on Number Theory, GSM8K and MultiArith.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| autoformalize and verify sampled solutions instead of majority voting | Minerva 62B solutions · GSM8K | problem solve rate: 67.2% -> 71.4% | Helped |
| autoformalize and verify sampled solutions instead of majority voting | Minerva 62B solutions · MATH Number Theory | problem solve rate: 23.7% -> 31.9% | Helped |
| use GPT3.5 for statement formalization rather than Minerva 62B | DTV with Minerva 62B informal solutions · GSM8K | problem solve rate: 71.4% -> 79.4% | Helped |
| add formal solution sketches (ablation) | DTV with Minerva 62B · MATH Number Theory | problem solve rate: 29.2% -> 31.9% | Helped |
| add vacuous statement filter (ablation) | DTV with Minerva 62B · MATH Number Theory | problem solve rate: 30.7% -> 31.9% | Helped |
| add self-critique filter (ablation) | DTV with Minerva 62B · MATH Prealgebra | problem solve rate: 58.4% -> 61.0% | Helped |
| increase informal solution model size from Minerva 8B to Minerva 540B | DTV Formalization with Minerva 62B · MATH Number Theory | problem solve rate: 23.0% -> 40.2% | Helped |
| increase informal solution model size from Minerva 8B to Minerva 540B | Majority Voting · GSM8K | problem solve rate: 27.7% -> 75.6% | Helped |
| use GPT-3.5 for informal solutions and formalization instead of Minerva 62B | DTV · MATH Number Theory | problem solve rate: 36.1% -> 49.4% | Helped |
Surprising findings
- Autoformalization by Minerva 62B, a model trained mainly on natural language math, still improves over majority voting, and using larger-model informal solutions with a weaker formalizer also helps.
Limitations
- Requires a theorem proving environment supporting the problem domain; geometry and probability poorly supported in Isabelle, so those MATH categories were excluded.
- LLM translation errors can produce unfaithful formal statements (e.g., natural-number subtraction pitfalls).
- Self-critique filter can reject faithful statements and miss unfaithful ones.
Experimental setup
Datasets: GSM8K MATH MultiArith
Benchmarks: GSM8K MATH Number Theory MATH Algebra MATH Prealgebra MultiArith
Metrics: problem solve rate
Baselines: single sample majority voting
Builds on: chain-of-thought prompting Minerva Portal-to-Isabelle self-consistency majority voting
Closest papers by meaning
- Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (NeurIPS 2024 · similarity 0.89)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.89)
- HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs (ICML 2026 · similarity 0.88)
- Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (ICML 2025 · similarity 0.87)
- MathArena: Evaluating LLMs on Uncontaminated Math Competitions (NeurIPS 2025 · similarity 0.87)
- Step-by-Step Reasoning for Math Problems via Twisted Sequential Monte Carlo (ICLR 2025 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.