Grammatiche dell'Incertezza Formale: Quando Fidarsi dei Modelli Linguistici nei Compiti di Ragionamento Automatico

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

May 26, 2025

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

cs.AI

Abstract

I grandi modelli linguistici (LLM) mostrano un notevole potenziale nel democratizzare il ragionamento automatizzato attraverso la generazione di specifiche formali. Tuttavia, esiste una tensione fondamentale: gli LLM sono probabilistici, mentre la verifica formale richiede garanzie deterministiche. Questo articolo affronta questo divario epistemologico attraverso un'indagine completa delle modalità di fallimento e della quantificazione dell'incertezza (UQ) negli artefatti formali generati dagli LLM. La nostra valutazione sistematica di cinque LLM all'avanguardia rivela l'impatto specifico del dominio dell'autoformalizzazione basata su Teorie di Soddisfacibilità Modulo (SMT) sull'accuratezza (da +34,8% nei compiti logici a -44,5% in quelli fattuali), con tecniche note di UQ come l'entropia delle probabilità dei token che non riescono a identificare questi errori. Introduciamo un framework di grammatica libera dal contesto probabilistica (PCFG) per modellare gli output degli LLM, ottenendo una tassonomia raffinata dell'incertezza. Troviamo che i segnali di incertezza sono dipendenti dal compito (ad esempio, entropia grammaticale per la logica, AUROC>0,93). Infine, una fusione leggera di questi segnali consente una verifica selettiva, riducendo drasticamente gli errori (14-100%) con un minimo di astensione, trasformando la formalizzazione guidata dagli LLM in una disciplina ingegneristica affidabile.

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.