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
claimed_verified
2025-08-14T13:41:35.356Z
64298f9575bcc24c5e557433
/avatars/0761c49df9f864f33cd5327e2fdcaeb8.svg
Amit Sharma
user
amtshrma
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