Grammaires de l'incertitude formelle : Quand faire confiance aux LLM dans les tâches de raisonnement automatisé
Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
May 26, 2025
Auteurs: Debargha Ganguly, Vikash Singh, Sreehari Sankar, Biyao Zhang, Xuecen Zhang, Srinivasan Iyengar, Xiaotian Han, Amit Sharma, Shivkumar Kalyanaraman, Vipin Chaudhary
cs.AI
Résumé
Les grands modèles de langage (LLM) montrent un potentiel remarquable pour démocratiser le raisonnement automatisé en générant des spécifications formelles. Cependant, une tension fondamentale existe : les LLM sont probabilistes, tandis que la vérification formelle exige des garanties déterministes. Cet article aborde cet écart épistémologique en étudiant de manière exhaustive les modes de défaillance et la quantification de l'incertitude (UQ) dans les artefacts formels générés par les LLM. Notre évaluation systématique de cinq LLM de pointe révèle l'impact spécifique au domaine de l'autoformalisation basée sur les théories de satisfiabilité modulo (SMT) sur la précision (allant de +34,8 % pour les tâches logiques à -44,5 % pour les tâches factuelles), avec des techniques d'UQ connues comme l'entropie des probabilités de tokens échouant à identifier ces erreurs. Nous introduisons un cadre de grammaire hors contexte probabiliste (PCFG) pour modéliser les sorties des LLM, produisant une taxonomie raffinée de l'incertitude. Nous constatons que les signaux d'incertitude dépendent de la tâche (par exemple, l'entropie grammaticale pour la logique, AUROC>0,93). Enfin, une fusion légère de ces signaux permet une vérification sélective, réduisant considérablement les erreurs (14-100 %) avec une abstention minimale, transformant ainsi la formalisation pilotée par les LLM en une discipline d'ingénierie fiable.
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.