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

要約

大規模な言語モデル（LLMS）は、正式な仕様を生成することにより、自動化された推論を民主化するための顕著な約束を示しています。
ただし、基本的な緊張が存在します。LLMは確率的であり、正式な検証は決定論的保証を要求します。
このペーパーでは、LLMが生成した正式なアーティファクトにおける故障モードと不確実性の定量化（UQ）を包括的に調査することにより、この認識論的ギャップに対処します。
5つのフロンティアLLMの体系的な評価により、満足度モジュロ理論（SMT）ベースのオートフォーマル化のドメイン固有の精度に対するドメイン固有の影響（論理タスクの +34.8％から事実のものの-44.5％まで）が明らかになり、これらのエラーを特定するために誤って誤っている確率のエントロピーのような既知のUQ技術があります。
LLM出力をモデル化するために、確率的コンテキストのない文法（PCFG）フレームワークを導入し、洗練された不確実性分類法を生み出します。
不確実性シグナルはタスクに依存していることがわかります（たとえば、論理の文法エントロピー、AUROC> 0.93）。
最後に、これらの信号の軽量の融合により、選択的検証が可能になり、最小限の棄権でエラー（14-100％）を大幅に削減し、LLM駆動型の形式化を信頼できるエンジニアリング分野に変換します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google