Грамматики формальной неопределенности: когда доверять большим языковым моделям в задачах автоматизированного рассуждения

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

May 26, 2025

Авторы: Debargha Ganguly, Vikash Singh, Sreehari Sankar, Biyao Zhang, Xuecen Zhang, Srinivasan Iyengar, Xiaotian Han, Amit Sharma, Shivkumar Kalyanaraman, Vipin Chaudhary

cs.AI

Аннотация

Крупные языковые модели (LLM) демонстрируют значительный потенциал для демократизации автоматизированного рассуждения за счет генерации формальных спецификаций. Однако существует фундаментальное противоречие: LLM являются вероятностными, в то время как формальная верификация требует детерминированных гарантий. В данной статье рассматривается этот эпистемологический разрыв путем всестороннего исследования режимов сбоев и количественной оценки неопределенности (UQ) в формальных артефактах, созданных LLM. Наше систематическое исследование пяти передовых LLM выявляет влияние автоматизации на основе теории удовлетворяемости модулей (SMT) на точность в зависимости от предметной области (от +34,8% в логических задачах до -44,5% в фактологических), при этом известные методы UQ, такие как энтропия вероятностей токенов, не способны выявить эти ошибки. Мы представляем вероятностную контекстно-свободную грамматику (PCFG) для моделирования выходных данных LLM, что позволяет уточнить таксономию неопределенности. Мы обнаруживаем, что сигналы неопределенности зависят от задачи (например, энтропия грамматики для логики, AUROC>0,93). Наконец, легковесное объединение этих сигналов позволяет реализовать выборочную верификацию, значительно сокращая количество ошибок (14-100%) при минимальном воздержании, превращая формализацию на основе LLM в надежную инженерную дисциплину.

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.