mlsanityData to 14 Oct 2026

Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks

arXiv 2505.20047 ↗First posted 26 May 2025cs.CL cs.AI cs.LOcited by 10

On the map: LLM reasoning → Test-time compute and efficient thinking

Abstract (arXiv)

Large language models (LLMs) show remarkable promise for democratizing automated reasoning by generating formal specifications. However, a fundamental tension exists: LLMs are probabilistic, while formal verification demands deterministic guarantees. This paper addresses this epistemological gap by comprehensively investigating failure modes and uncertainty quantification (UQ) in LLM-generated formal artifacts. Our systematic evaluation of five frontier LLMs reveals Satisfiability Modulo Theories (SMT) based autoformalization's domain-specific impact on accuracy (from +34.8% on logical tasks to -44.5% on factual ones), with known UQ techniques like the entropy of token probabilities failing to identify these errors. We introduce a probabilistic context-free grammar (PCFG) framework to model LLM outputs, yielding a refined uncertainty taxonomy. We find uncertainty signals are task-dependent (e.g., grammar entropy for logic, AUROC>0.93). Finally, a lightweight fusion of these signals enables selective verification, drastically reducing errors (14-100%) with minimal abstention, transforming LLM-driven formalization into a reliable engineering discipline.

Key facts. Cited by 10 papers in the map (data through 14 Oct 2026). Placed in Test-time compute and efficient thinking, one of 17 directions in LLM reasoning. Builds on 79 of its 103 references that are in the map. First posted on arXiv 26 May 2025.

Builds on

79 of 103 references.

Closest ancestors · 1

Same direction, newest first

  1. 2022Language Models (Mostly) Know What They Know11 Jul

Other references · 78

  1. 2020Language Models are Few-Shot Learnerscited by 32,419
  2. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
  3. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  4. 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,708
  5. 2015Dropout as a Bayesian Approximation: Representing Model Uncertainty in Deep Learningcited by 4,448
  6. 2022Large Language Models are Zero-Shot Reasonerscited by 4,374
  7. 2016Simple and Scalable Predictive Uncertainty Estimation using Deep Ensemblescited by 3,926
  8. 2022Emergent Abilities of Large Language Modelscited by 2,512
  9. 2022Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Taskscited by 1,076
  10. 2023Can LLMs Express Their Uncertainty? An Empirical Evaluation of Confidence Elicitation in LLMscited by 974
  11. 2023Semantic Uncertainty: Linguistic Invariances for Uncertainty Estimation in Natural Language Generationcited by 819
  12. 2023Just Ask for Calibration: Strategies for Eliciting Calibrated Confidence Scores from Language Models Fine-Tuned with Human Feedbackcited by 812
38 more
  1. 2023SelfCheckGPT: Zero-Resource Black-Box Hallucination Detection for Generative Large Language Modelscited by 810
  2. 2022Teaching Models to Express Their Uncertainty in Wordscited by 751
  3. 2021Did Aristotle Use a Laptop? A Question Answering Benchmark with Implicit Reasoning Strategiescited by 743
  4. 2021A Survey of Uncertainty in Deep Neural Networkscited by 680
  5. 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoningcited by 391
  6. 2020Simple and Principled Uncertainty Estimation with Deterministic Deep Learning via Distance Awarenesscited by 389
  7. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  8. 2020BatchEnsemble: An Alternative Approach to Efficient Ensemble and Lifelong Learningcited by 371
  9. 2022Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thoughtcited by 337
  10. 2020ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Languagecited by 324
  11. 2023Generating with Confidence: Uncertainty Quantification for Black-box Large Language Modelscited by 293
  12. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  13. 2023Mathematical Capabilities of ChatGPTcited by 268
  14. 2022Autoformalization with Large Language Modelscited by 263
  15. 2022FOLIO: Natural Language Reasoning with First-Order Logiccited by 235
  16. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  17. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  18. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 168
  19. 2023LM-Polygraph: Uncertainty Estimation for Language Modelscited by 131
  20. 2022Quantifying Aleatoric and Epistemic Uncertainty in Machine Learning: Are Conditional Entropy and Mutual Information Appropriate Measures?cited by 125
  21. 2023Quantifying Uncertainty in Answers from any Language Model and Enhancing their Trustworthinesscited by 122
  22. 2024GTBench: Uncovering the Strategic Reasoning Limitations of LLMs via Game-Theoretic Evaluationscited by 120
  23. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  24. 2023Decomposing Uncertainty for Large Language Models through Input Clarification Ensemblingcited by 114
  25. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 109
  26. 2023SatLM: Satisfiability-Aided Language Models Using Declarative Promptingcited by 102
  27. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 98
  28. 2023SAC3: Reliable Hallucination Detection in Black-Box Language Models via Semantic-aware Cross-check Consistencycited by 90
  29. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 82
  30. 2018Quantifying Uncertainties in Natural Language Processing Taskscited by 79
  31. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  32. 2023Selectively Answering Ambiguous Questionscited by 66
  33. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 55
  34. 2024Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalizationcited by 55
  35. 2023Active Learning Principles for In-Context Learning with Large Language Modelscited by 54
  36. 2024Overconfidence is Key: Verbalized Uncertainty Evaluation in Large Language and Vision-Language Modelscited by 54
  37. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  38. 2019A Comprehensive guide to Bayesian Convolutional Neural Network with Variational Inferencecited by 51

50 most cited of 78 All 78 (JSON)

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 2; 2026: 8.

10 papers.

  1. 2026Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verificationcited by 4
  2. 2026FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Leancited by 4
  3. 2026Trust The Typicalcited by 3
  4. 2026Path-Lock Expert: Separating Reasoning Mode in Hybrid Thinking via Architecture-Level Separationcited by 3
  5. 2025ATA: A Neuro-Symbolic Approach to Implement Autonomous and Trustworthy Agentscited by 2
  6. 2026Towards Generation-Efficient Uncertainty Estimation in Large Language Modelscited by 2
  7. 2026Context Determines Optimal Architecture in Materials Segmentationcited by 1
  8. 2025Towards Trustworthy Multi-Turn LLM Agents via Behavioral Guidancecited by 0
  9. 2026The System Hallucination Scale (SHS): A Minimal yet Effective Human-Centered Instrument for Evaluating Hallucination-Related Behavior in Large Language Modelscited by 0
  10. 2026Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoningcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2026Embedding Perturbation may Better Reflect Intermediate-Step Uncertainty in LLM Reasoning
  2. 2025Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving
  3. 2026SELFDOUBT: Uncertainty Quantification for Reasoning LLMs via the Hedge-to-Verify Ratio
  4. 2026Can We Trust LLM's Logic? Quantifying Uncertainty, Coherence, and Robustness via a Graph-Based Framework
  5. 2025Reasoning Under Uncertainty: Exploring Probabilistic Reasoning Capabilities of LLMs
  6. 2025ReliableMath: Benchmark of Reliable Mathematical Reasoning on Large Language Models
  7. 2025Probabilistic Soundness Guarantees in LLM Reasoning Chains
  8. 2024Improving Self Consistency in LLMs through Probabilistic Tokenization