形式的な不確実性の文法：自動推論タスクにおけるLLMの信頼性判断基準

要旨

大規模言語モデル（LLMs）は、形式的仕様を生成することで自動推論の民主化に大きな可能性を示しています。しかし、根本的な矛盾が存在します。LLMsは確率的である一方、形式的検証は決定論的な保証を要求します。本論文は、LLMが生成する形式的成果物における失敗モードと不確実性定量化（UQ）を包括的に調査することで、この認識論的ギャップに取り組みます。5つの最先端LLMを系統的に評価した結果、Satisfiability Modulo Theories（SMT）ベースの自動形式化が、タスク領域に特異的な精度への影響（論理タスクでは+34.8%、事実タスクでは-44.5%）を持つことが明らかになりました。また、トークン確率のエントロピーといった既知のUQ手法では、これらのエラーを特定できないことも判明しました。我々は、LLMの出力をモデル化するための確率的文脈自由文法（PCFG）フレームワークを導入し、洗練された不確実性の分類体系を構築しました。その結果、不確実性のシグナルはタスク依存性が高いこと（例えば、論理タスクでは文法エントロピー、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.

形式的な不確実性の文法：自動推論タスクにおけるLLMの信頼性判断基準

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

要旨

Support