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.