Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908380208037888 |
|---|---|
| author | Ganguly, Debargha Singh, Vikash Sankar, Sreehari Zhang, Biyao Zhang, Xuecen Iyengar, Srinivasan Han, Xiaotian Sharma, Amit Kalyanaraman, Shivkumar Chaudhary, Vipin |
| author_facet | Ganguly, Debargha Singh, Vikash Sankar, Sreehari Zhang, Biyao Zhang, Xuecen Iyengar, Srinivasan Han, Xiaotian Sharma, Amit Kalyanaraman, Shivkumar Chaudhary, Vipin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_20047 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks Ganguly, Debargha Singh, Vikash Sankar, Sreehari Zhang, Biyao Zhang, Xuecen Iyengar, Srinivasan Han, Xiaotian Sharma, Amit Kalyanaraman, Shivkumar Chaudhary, Vipin Computation and Language Artificial Intelligence Logic in Computer Science Software Engineering 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. |
| title | Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks |
| topic | Computation and Language Artificial Intelligence Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2505.20047 |