Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks

TL;DR

This paper investigates the limitations of LLMs in formal reasoning, proposing a probabilistic grammar framework to better quantify uncertainty and improve reliability in automated formalization tasks.

Contribution

It introduces a PCFG-based uncertainty modeling approach and a fusion method for selective verification, enhancing trustworthiness of LLM-generated formal artifacts.

Findings

Uncertainty signals are task-dependent, with high AUROC scores.

SMT-based autoformalization improves logical task accuracy by up to 34.8%.

Error reduction of 14-100% with minimal abstention.

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.