大規模言語モデル（LLM）は形式仕様の自動生成に有望ですが、確率的出力と決定論的検証とのギャップが課題です。本論文は、LLMが形式的推論で誤る要因と、不確実性の定量化手法の効果を検証しました。SAT/SMT問題においては分野依存の精度変動が顕著で、既存のエントロピー指標などでは誤りを十分に検出できませんでした。そこで、出力を確率文脈自由文法（PCFG）でモデル化し、文法エントロピーなどの新たな指標を提案。これにより選択的検証で誤り率を最大100%削減する方法を示しました。