Grammatiken formaler Unsicherheit: Wann man LLMs bei automatisierten Schlussfolgerungsaufgaben vertrauen sollte

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

May 26, 2025

Autoren: Debargha Ganguly, Vikash Singh, Sreehari Sankar, Biyao Zhang, Xuecen Zhang, Srinivasan Iyengar, Xiaotian Han, Amit Sharma, Shivkumar Kalyanaraman, Vipin Chaudhary

cs.AI

Zusammenfassung

Große Sprachmodelle (LLMs) zeigen bemerkenswertes Potenzial, automatisierte Schlussfolgerungen durch die Generierung formaler Spezifikationen zu demokratisieren. Allerdings besteht ein grundlegender Widerspruch: LLMs sind probabilistisch, während formale Verifizierung deterministische Garantien erfordert. Diese Arbeit adressiert diese erkenntnistheoretische Lücke, indem sie systematisch Fehlermodi und Unsicherheitsquantifizierung (UQ) in LLM-generierten formalen Artefakten untersucht. Unsere systematische Auswertung von fünf führenden LLMs zeigt den domänenspezifischen Einfluss der Satisfiability Modulo Theories (SMT)-basierten Autoformalisation auf die Genauigkeit (von +34,8 % bei logischen Aufgaben bis -44,5 % bei faktischen), wobei bekannte UQ-Techniken wie die Entropie der Token-Wahrscheinlichkeiten diese Fehler nicht identifizieren können. Wir führen ein probabilistisches kontextfreies Grammatik (PCFG)-Framework ein, um LLM-Ausgaben zu modellieren, was zu einer verfeinerten Unsicherheitstaxonomie führt. Wir stellen fest, dass Unsicherheitssignale aufgabenabhängig sind (z. B. Grammatikentropie für Logik, AUROC>0,93). Schließlich ermöglicht eine leichte Fusion dieser Signale eine selektive Verifizierung, die Fehler drastisch reduziert (14-100 %) bei minimaler Zurückhaltung und verwandelt die LLM-gestützte Formalisierung in eine zuverlässige Ingenieursdisziplin.

English

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.