Gramáticas da Incerteza Formal: Quando Confiar em LLMs em Tarefas de Raciocínio Automatizado

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

May 26, 2025

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

cs.AI

Resumo

Modelos de linguagem de grande escala (LLMs) demonstram um potencial notável para democratizar o raciocínio automatizado ao gerar especificações formais. No entanto, existe uma tensão fundamental: LLMs são probabilísticos, enquanto a verificação formal exige garantias determinísticas. Este artigo aborda essa lacuna epistemológica ao investigar de forma abrangente os modos de falha e a quantificação de incerteza (UQ) em artefatos formais gerados por LLMs. Nossa avaliação sistemática de cinco LLMs de ponta revela o impacto específico do domínio da autoformalização baseada em Satisfiability Modulo Theories (SMT) na precisão (variando de +34,8% em tarefas lógicas a -44,5% em tarefas factuais), com técnicas conhecidas de UQ, como a entropia das probabilidades de tokens, falhando em identificar esses erros. Introduzimos uma estrutura de gramática livre de contexto probabilística (PCFG) para modelar as saídas dos LLMs, resultando em uma taxonomia de incerteza refinada. Descobrimos que os sinais de incerteza são dependentes da tarefa (por exemplo, entropia gramatical para lógica, AUROC>0,93). Por fim, uma fusão leve desses sinais permite a verificação seletiva, reduzindo drasticamente os erros (14-100%) com uma abstenção mínima, transformando a formalização impulsionada por LLMs em uma disciplina de engenharia confiável.

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.