Grammars of Formal Uncertainty: When to Trust LLMs in Automated
  Reasoning Tasks
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.
683596d32bb7489b50c2831c
Debargha Ganguly
claimed_verified
2025-05-28T08:59:32.141Z
61deb0a302496c6d78da4ade
/avatars/1d31be74c0e6c983860d94846b4d3770.svg
Debargha Ganguly
user
Debargha
683596d32bb7489b50c2831d
Vikash Singh
claimed_verified
2025-06-03T08:51:02.258Z
6702352c547acbd64cddf31e
/avatars/37fbacb299f217505b2a03549128f10d.svg
Vikash Singh
user
optimusPrimeBee
683596d32bb7489b50c2831e
Sreehari Sankar
683596d32bb7489b50c2831f
Biyao Zhang
683596d32bb7489b50c28320
Xuecen Zhang
683596d32bb7489b50c28321
Srinivasan Iyengar
683596d32bb7489b50c28322
Xiaotian Han
683596d32bb7489b50c28323
Amit Sharma
683596d32bb7489b50c28324
Shivkumar Kalyanaraman
683596d32bb7489b50c28325
Vipin Chaudhary
Grammars of Formal Uncertainty: When to Trust LLMs in Automated
  Reasoning Tasks
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.
This research explores uncertainty quantification in large language models for generating formal specifications, introducing a PCFG framework to improve error detection and selective verification.
large language models (LLMs) formal verification satisfiability modulo theories (SMT) autoformalization uncertainty quantification (UQ) entropy probabilistic context-free grammar (PCFG) grammar entropy AUROC