Research map / Large language models / Agents, code and math
Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
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.
Models LLM-generated SMT-LIB programs as samples from a PCFG fitted to the SMT-LIB grammar, derives 25 grammar-based uncertainty metrics, and fuses them for selective verification of LLM autoformalization errors.
Problem
LLM-generated formal artifacts (SMT-LIB programs) are probabilistic and error-prone, yet standard token-level uncertainty methods fail to flag autoformalization errors before passing them to a solver.
Approach
Fits a PCFG over parse trees of ensembles of LLM-sampled SMT-LIB programs (using the SMT-LIB grammar as structure) and derives grammar-level uncertainty metrics (entropy, spectral radius, rule-distribution statistics) plus self-consistency signals, then fuses them with a lightweight ensemble for selective verification.
Key results
- SMT-based autoformalization changes accuracy by +34.8% on ProofWriter for one model and -44.5% on FOLIO, showing task-dependent benefit.
- Grammar entropy from PCFGs reaches AUROC 0.9301 for o3-mini on ProofWriter predicting ground-truth correctness.
- An ensemble fusion achieves AUROC 0.9949 for o3-mini on ProofWriter and reduces error rates by 14-100% with minimal abstention.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Generate SMT-LIB and solve with Z3 instead of direct text reasoning | o3-mini · StrategyQA | accuracy: 0.7828 -> 0.7980 | Helped |
| Generate SMT-LIB and solve with Z3 instead of direct text reasoning | LLMs · StrategyQA | accuracy: 0.8292 -> 0.6720; 0.8580 -> 0.7760; 0.7188 -> 0.5360; 0.6760 -> 0.4500 | Mixed |
| Generate SMT-LIB and solve with Z3 instead of direct text reasoning | LLMs · ProntoQA | accuracy: 1.0000 -> 0.9980; 1.0000 -> 0.4501; 0.9939 -> 0.7440; 0.9820 -> 0.9000 | Hurt |
| Generate SMT-LIB and solve with Z3 instead of direct text reasoning | LLMs · ProofWriter | accuracy: 0.8893 -> 0.9418; 0.8057 -> 0.5800; 0.9423 -> 0.4935; 0.4900 -> 0.6660; 0.4060 -> 0.7540 | Mixed |
| Generate SMT-LIB and solve with Z3 instead of direct text reasoning | LLMs · FOLIO | accuracy: 0.9450 -> 0.5000; 0.9333 -> 0.5961; 0.9252 -> 0.5200; 0.9010 -> 0.5625; 0.9017 -> 0.7321 | Hurt |
| Combine uncertainty metrics with a learned Ensemble ML predictor | PCFG-based error detection · StrategyQA (o3-mini) | AUROC: 0.7448 -> 0.7850 | Helped |
| Use grammar entropy to predict SMT correctness | o3-mini · ProofWriter | AUROC: 0.9301 | Helped |
| Increase sampling temperature (ablation) | LLM SMT-LIB generation and induced PCFG · Temperature-varied SMT generation | grammar entropy | Helped |
| Increase sampling temperature (ablation) | LLM SMT-LIB generation and induced PCFG · Temperature-varied SMT generation | spectral radius | Mixed |
| Increase sampling temperature (ablation) | LLM SMT-LIB generation and induced PCFG · Temperature-varied SMT generation | NSUI | No clear effect |
| Increase sampling temperature (ablation) | LLM SMT-LIB generation and induced PCFG · Temperature-varied SMT generation | average rules per non-terminal | Helped |
| Increase sampling temperature (ablation) | LLM SMT-LIB generation and induced PCFG · Temperature-varied SMT generation | kurtosis | Hurt |
Surprising findings
- Token-level entropy and perplexity fail to identify autoformalization errors, performing near chance on several tasks.
- Metrics with high discriminative ability often show poor calibration (e.g., ECE 0.4419 for grammar entropy on StrategyQA-style analysis).
Limitations
- Evaluation uses only 100 samples per configuration in several settings, limiting statistical reliability.
- The theoretical coverage guarantee relies on a loosely justified typical-set argument and union bound.
- Some results (e.g., DeepSeek R1 SMT on ProofWriter) are from partial runs and excluded from interpretation.
Experimental setup
Datasets: StrategyQA ProntoQA ProofWriter FOLIO
Benchmarks: StrategyQA ProntoQA ProofWriter FOLIO
Metrics: accuracy AUROC AURC ECE Brier score
Baselines: token entropy perplexity self-consistency text Ensemble Average
Builds on: probabilistic context-free grammars self-consistency SAT-LM
Closest papers by meaning
- TokUR: Token-Level Uncertainty Estimation for Large Language Model Reasoning (ICLR 2026 · similarity 0.88)
- Does Reasoning Emerge? Examining the Probabilities of Causation in Large Language Models (NeurIPS 2024 · similarity 0.87)
- Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (ICML 2025 · similarity 0.87)
- RvLLM: LLM Runtime Verification with Domain Knowledge (NeurIPS 2025 · similarity 0.87)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.87)
- CRANE: Reasoning with constrained LLM generation (ICML 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.