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