Grammars of Formal Uncertainty: When to Trust LLMs in Automated
  Reasoning Tasks
Authors: name: Debargha Ganguly; name: Vikash Singh; name: Sreehari Sankar; name: Biyao Zhang; name: Xuecen Zhang; name: Srinivasan Iyengar; name: Xiaotian Han; name: Amit Sharma; name: Shivkumar Kalyanaraman; name: Vipin Chaudhary
Published: 2025-05-26 14:34:04

Abstract: 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.