Gramáticas de la Incertidumbre Formal: Cuándo Confiar en los LLM en Tareas de Razonamiento Automatizado

Resumen

Los modelos de lenguaje de gran escala (LLMs) muestran un notable potencial para democratizar el razonamiento automatizado mediante la generación de especificaciones formales. Sin embargo, existe una tensión fundamental: los LLMs son probabilísticos, mientras que la verificación formal exige garantías deterministas. Este artículo aborda esta brecha epistemológica mediante una investigación exhaustiva de los modos de fallo y la cuantificación de incertidumbre (UQ) en los artefactos formales generados por LLMs. Nuestra evaluación sistemática de cinco LLMs de vanguardia revela el impacto específico del dominio en la precisión de la autoformalización basada en Teorías de Satisfacción Modular (SMT) (desde +34,8% en tareas lógicas hasta -44,5% en tareas factuales), con técnicas conocidas de UQ, como la entropía de las probabilidades de tokens, que no logran identificar estos errores. Introducimos un marco de gramática libre de contexto probabilística (PCFG) para modelar las salidas de los LLMs, obteniendo una taxonomía refinada de la incertidumbre. Encontramos que las señales de incertidumbre dependen de la tarea (por ejemplo, entropía gramatical para lógica, AUROC>0,93). Finalmente, una fusión ligera de estas señales permite una verificación selectiva, reduciendo drásticamente los errores (14-100%) con una mínima abstención, transformando la formalización impulsada por LLMs en una disciplina de ingeniería confiable.

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.

Gramáticas de la Incertidumbre Formal: Cuándo Confiar en los LLM en Tareas de Razonamiento Automatizado

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

Resumen

Support