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.