「自動推論」の記事一覧

• 形式的不確実性の文法：LLMによる自動推論の信頼性評価

  2025-05-27 02:27

  科学・技術

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

• 柔軟な証明支援ツールの開発

  2025-05-10 10:41

  科学・技術

  著者は、推定の自動検証ツールを改良し、対話型で柔軟な証明支援ツールへと進化させた。Lean風のインターフェースを持ち、Pythonのsympyを利用して線形不等式や漸近推定を処理できる。ユーザーは高レベルの「戦術」を指定し、ツールが計算を行う。今後は関数空間ノルムの評価や不等式の導入も視野に入れており、さらなる拡張が期待される。実装はGitHub上で公開されており、数理解析や論理に関心のある開発者に有用だ。