バグ検出、パッチ検証、コードレビューといったリポジトリ規模のタスクにAIエージェントを投入するには、大きな技術的ハードルを乗り越える必要があります。主要なボトルネックの1つは、リポジトリごとに動的実行サンドボックスをセットアップする必要があり、これは高価で計算負荷が重いことです。
このオーバーヘッドを回避するために、コードを実行する代わりに大規模言語モデル（LLM）の推論を用いる手法が人気を集めていますが、それでもしばしば未サポートの推測や幻覚につながります。
実行を伴わない推論を改善するために、Metaの研究者は「半形式推論,」という研究を紹介します。これは構造化されたプロンプト手法です。この方法では、AIエージェントに、前提を明示し、具体的な実行経路をたどり、回答を提示する前に形式的な結論を導出することで、論理証明書を埋めることを求めます。
構造化された形式により、エージェントは結論を導く前に証拠を体系的に集め、関数呼び出しに従うことが強制されます。これによりコーディングタスクにおけるLLMの精度が向上し、障害箇所の特定（fault localization）やコードベース質問応答における誤りが大幅に減少します。
コードレビューのタスクでLLMを使う開発者にとって、半形式推論は、実行を伴わない高信頼なセマンティックなコード解析を可能にし、同時にAIコーディングシステムのインフラコストを大きく削減します。
エージェント的コード推論
エージェント的コード推論とは、コードを実行せずにコードベースへ深いセマンティック解析を行うために、ファイルを行き来し、依存関係を追跡し、文脈を反復的に収集することによって、AIエージェントがナビゲートできる能力です。企業向けAIアプリケーションでは、この能力は、複雑なリポジトリ全体にわたる自動バグ検出、包括的なコードレビュー、パッチ検証をスケールさせるうえで不可欠です。そこでは関連する文脈が複数のファイルにまたがります。
業界では現在、実行を伴わないコード検証に対処するための主に2つのアプローチがあります。1つ目は、非構造化されたLLM評価器によって、コードを直接または特化したLLMを報酬モデルとして学習してテスト結果を近似することで検証しようとする方法です。主な欠点は、非構造化された推論に依存している点です。これにより、モデルは明示的な根拠なしにコード挙動について確信に満ちた主張を行えるようになります。構造化された制約がないと、エージェントが関数名のような表面的なパターンに基づいて当て推量するのではなく、徹底的に推論していることを担保するのが難しくなります。
2つ目のアプローチは形式的検証です。これはコードまたは推論を、Lean、Coq、Datalogのような形式的な数学言語へと翻訳し、自動化された証明検査を可能にするものです。厳密である一方、形式的手法ではプログラミング言語の意味論（セマンティクス）を定義する必要があります。これは、複数のフレームワークや言語にまたがる恣意的な企業コードベースでは完全に現実的ではありません。
また既存の手法は、しばしば非常に断片化されており、タスク固有である傾向があります。新しい問題領域ごとに、まったく別のアーキテクチャや専門的な学習が必要になることも多いのです。幅広い汎用の企業向けアプリケーションに求められる柔軟性が欠けています。
半形式推論はどのように機能するか
非構造化された当て推量と、過度に硬直した数学的な証明の間のギャップを埋めるために、Metaの研究者は「半形式推論」と呼ぶ構造化されたプロンプト手法を提案しています。このアプローチは、LLMエージェントにタスク固有の構造化された推論テンプレートを与えます。
これらのテンプレートは、必須の論理証明書として機能します。タスクを完了するには、エージェントは前提を明示し、特定のテストに対する実行経路を追跡し、検証可能な証拠のみに基づいて形式的な結論を導き出さなければなりません。
テンプレートにより、エージェントは判断を下す前に、コードベースから証明（proof）を集めることが求められます。エージェントは、関数の命名規則のような表面的な手がかりに基づいて挙動を推測するのではなく、実際に関数呼び出しやデータフローをステップごとに追わなければなりません。この体系的な証拠収集は、関数名の取り違えといったエッジケースに対処するのに役立ち、裏付けのない主張を避けることにつながります。
半形式推論の実例
研究者らは、3つのソフトウェアエンジニアリング・タスクにわたって半形式推論を評価しました。具体的には、2つのパッチが実行せずに同一のテスト結果を生むかを判定するためのパッチ同等性検証、バグの原因となる正確なコード行を特定するための障害箇所の特定（fault localization）、複雑なコードベースに関するきめ細かなセマンティック理解をテストするためのコード質問応答です。実験では、自律的な検証エージェントとして振る舞うClaude Opus-4.5およびSonnet-4.5モデルを用いました。
チームは、自分たちの構造化された半形式的アプローチを、いくつかのベースラインと比較しました。その中には、標準的な推論が含まれます。標準的推論では、エージェント的モデルに最小限のプロンプトを与え、思考を自由に非構造化の自然言語で説明させます。また、difflibのような従来のテキスト類似度アルゴリズムとも比較しました。
パッチ同等性においては、半形式推論が難しい厳選された例で精度を改善し、標準的推論の78%から88%へと向上しました。テスト仕様が利用可能な現実世界の、エージェント生成パッチを評価する際、半形式推論を用いたOpus-4.5モデルは93%の検証精度を達成し、非構造化の単発ベースライン（86%）とdifflibベースライン（73%）の両方を上回りました。他のタスクでも同様の改善が全般に見られました。
論文では、実世界の例を通じて半形式推論の価値が強調されています。あるケースでは、エージェントがPython Djangoリポジトリ内の2つのパッチを評価します。これらのパッチはいずれも、1000 CEより前の年に対して2桁の年の書式設定を修正しようとします。1つのパッチは、標準の関数としてPythonで使われるものを上書きする、ライブラリ内のカスタムformat()関数を使用しています。
標準的推論のモデルは、これらのパッチを見て、format()がPythonの標準的な組み込み関数を指すものだと仮定し、両方のアプローチが同じ文字列出力を生成すると計算してしまい、誤ってパッチが同等だと宣言します。
半形式推論では、エージェントが実行経路を追跡してメソッド定義を確認します。構造化されたテンプレートに従うことで、ライブラリのファイルの1つの中で、format()という名前が実際にはモジュールレベルのカスタム関数によってシャドーイング（上書き）されていることをエージェントは発見します。エージェントは、コードに渡される入力の属性を前提にすると、このパッチはシステムをクラッシュさせ、もう一方は成功することを、形式的に証明します。
彼らの実験に基づき、研究者らは「LLMエージェントは実行なしでも有意義なセマンティックなコード解析を行え、サンドボックス実行を避けることで、RLトレーニングのパイプラインにおける検証コストを潜在的に削減できる」と示唆しています。
注意点とトレードオフ
半形式推論は大幅な信頼性の改善をもたらしますが、採用する前に企業の開発者は複数の実務上の注意点を考慮する必要があります。明確な計算量とレイテンシのトレードオフがあります。半形式推論は、より多くのAPI呼び出しとトークンを必要とします。パッチ同等性の評価では、半形式推論は標準的な非構造化推論と比べて、約2.8倍の実行ステップを要しました。
また、この手法は必ずしも万能に性能を向上させるわけではありません。特定のタスクにおいてモデルがすでに非常に高い能力を持っている場合には、特にそうです。研究者らがSonnet-4.5モデルをコード質問応答のベンチマークで評価したところ、標準的な非構造化推論だけで既に約85%という高い精度が得られていました。この状況で半形式テンプレートを適用しても、追加の改善は得られませんでした。
さらに、構造化された推論は非常に高い確信を伴う誤った回答を生み出すことがあります。エージェントは、精巧で形式的な証明の連鎖を構築することを強いられるため、調査が深いのに不完全だと、過度に確信してしまうことがあります。あるPythonの評価では、エージェントが有効なエッジケースを見つけるために5つの異なる関数を綿密に追跡しましたが、下流側のコードがすでにその正確な状況を安全に処理していたことを完全に見落としました。強固な証拠の連鎖を構築していたため、極めて高い確信度で誤った結論を提示しました。
また、システムが具体的な証拠に依存することは、コードベースの境界に突き当たったときにも破綻します。基盤となるソースコードが利用できないサードパーティのライブラリを分析する場合、エージェントは関数名に基づいた推測に頼ってしまいます。
そして場合によっては、厳密なプロンプト指示にもかかわらず、モデルが具体的な実行経路を完全には追跡できないことがあります。
最終的に、半形式的な推論は、非構造的な当て推量や幻覚を大幅に減らしますが、それらを完全に排除するわけではありません。
開発者が汲み取るべきこと
この手法はそのまま使えます。モデルのトレーニングや特別なパッケージングは不要です。コード実行を行わないため、LLM環境に追加のツールを組み込む必要はありません。コードレビューのタスクでより高い精度を得るために、推論時により多くの計算量を支払うことになります。
研究者らは、構造化されたエージェント的推論は「古典的な静的解析ツールに対する柔軟な代替手段になり得る。すなわち、分析ロジックを専門のアルゴリズムとして符号化するのではなく、言語やフレームワークをまたいで汎化できる、タスク固有の推論テンプレートを用いてLLMエージェントにプロンプトを与えられる」と示唆しています。
研究者らはプロンプトテンプレートを公開しており、それをそのままアプリケーションに容易に実装できます。プロンプトエンジニアリングが終わったという議論は多いものの、この手法は、よく構造化されたプロンプトからまだどれほどの性能を引き出せるかを示しています。
