論文「Can LLMs Perform Synthesis?」の技術的サマリー

この論文は、大規模言語モデル（LLM）が、記号論理に基づく従来のプログラム合成ツール（Symbolic Tools）と比較して、形式仕様からプログラムを合成する能力においてどの程度優れているか、あるいは劣っているかを検証した研究です。

以下に、問題設定、手法、主要な貢献、実験結果、および意義について詳細をまとめます。

1. 問題設定と背景

プログラム合成の目標は、与えられた正しさの仕様（Correctness Specification）を満たすシステムを自動的に生成することです。これまで、この分野は「記号的アプローチ（Symbolic Approaches）」（例：反例誘導合成、記法誘導合成など）が主流でした。しかし、近年の LLM のコード生成能力の飛躍的向上により、「LLM 単体で、あるいは LLM を中心としたアプローチで、形式仕様に基づくプログラム合成が可能か？」という問いが生じました。

本研究では、LLM が「その場（Out-of-the-box）」で、追加学習や RAG（検索拡張生成）なしに、形式仕様から正しいプログラムを生成できる能力を、最先端の記号ツールと比較評価することを目的としています。

2. 評価対象ドメインとツール

研究では、以下の 4 つの異なる合成ドメインで評価を行いました。

1. LTL 反応的合成 (LTL Reactive Synthesis): 線形時相論理（LTL）の仕様を満たす有限状態機械（FSM）の合成。
   • 対比ツール: ltlsynt (SYNTCOMP 2025 の優勝ツール)
2. 記法誘導合成 (Syntax-Guided Synthesis, SyGuS): 文法と仕様の両方を満たすプログラムの合成。
   • 対比ツール: cvc5 (SMT ソルバ)
3. 分散プロトコル合成 (Distributed Protocol Synthesis): TLA+ によるスケッチ（穴埋め）の完成。
   • 対比ツール: PolySemist
4. 再帰的プログラム合成 (Recursive Program Synthesis): ACL2s 言語による再帰関数のスケッチ完成。
   • 対比ツール: Cataclyst

評価対象の LLM:

• Qwen-2.5-Coder-32B-Instruct: 320 億パラメータのオープンソースモデル（NVIDIA H200 GPU 上で実行）。
• GPT-5: 商用の最先端モデル（OpenAI API 経由）。パラメータ数は非公開だが、GPT-3 の 1750 億を大幅に上回ると推測される。

3. 手法と実験設計

公平な比較を行うため、以下の手法を採用しました。

3.1 比較の公平性とリソース配分

• ハードウェアの非対称性: 記号ツールは CPU 上で、LLM は GPU（Qwen）またはクラウド（GPT-5）上で実行されるため、完全なハードウェア対称性は不可能です。
• 時間制約の統一: 各ベンチマークに対して、記号ツールと LLM ツールチェーンの両方に10 分（再帰合成は 15 分）のタイムアウトを適用しました。
• 反復戦略 (ILST):
  • Qwen: 正解が見つかるかタイムアウトするまで、検証器（Verifier）でチェックし、失敗した場合は再度プロンプトを送信する「反復ループ（Iterate-LLM-until-solution-or-timeout）」を実行します。ただし、過去の失敗例や反例をプロンプトに含めることはせず（神経記号的ループではない）、LLM 単体の能力を評価します。
  • GPT-5: 公平性を保つため、1 回のみクエリを実行し、その結果を検証します（反復は行いません）。

3.2 検証プロセス

LLM が生成したコードは、それぞれのドメインに対応する形式検証ツール（nuXmv, Z3, TLC, ACL2s 等）で正しさが検証されます。構文エラーや意味論的な誤り（仕様違反）が発見された場合は失敗とみなされます。

4. 主要な実験結果

4.1 解決されたベンチマーク数

• LTL 合成: 記号ツール（ltlsynt）が 396/433 を解決し、圧倒的に優位でした。GPT-5 は一部で記号ツールを上回るケースもありましたが、全体としては劣るか同等でした。Qwen は 50 件程度しか解決できませんでした。
• SyGuS: 記号ツール（cvc5）が 137/148 を解決。GPT-5 は 143/148 と cvc5 をわずかに上回る結果となりました。Qwen は 96 件でした。
• 分散プロトコル合成: 記号ツール（PolySemist）が 140/171 を解決。GPT-5 は 136 件、Qwen は 102 件でした。
• 再帰的プログラム合成: 記号ツール（Cataclyst）が 41/42 を解決。GPT-5 も 41 件を解決し同等の性能を示しましたが、Qwen は 39 件でした。

総括: どのドメインにおいても、記号ツールは Qwen よりも多くのベンチマークを解決しました。GPT-5 は LTL 合成を除く他の 3 つのドメインで記号ツールと同等か、わずかに上回る性能を示しましたが、LTL 合成では記号ツールに劣りました。

4.2 実行時間

• 記号ツールの優位性: 記号ツールは、GPT-5 が稼働するより強力なハードウェア（GPU/クラウド）上で実行されているにもかかわらず、すべてのドメインで GPT-5 よりも高速でした。
  • LTL 合成では、記号ツールは GPT-5 よりも 2 桁以上速いケースがありました。
  • SyGuS 合成でも、記号ツールは GPT-5 よりも 1 桁以上速かったです。
• Qwen の遅延: Qwen は反復ループを行うため、失敗したケースではタイムアウトまで時間を消費し、成功したケースでも平均実行時間は記号ツールより長い傾向にありました（再帰合成ドメインを除く）。

4.3 構文と文法遵守

• GPT-5: 構文エラーや文法違反が非常に少なく、高い品質のコードを生成しました。
• Qwen: 構文エラー（括弧の不一致、無効な演算子など）や、指定された文法/スケッチに準拠しない出力が多く見られました。特に再帰的プログラム合成では、失敗の半数以上が構文問題に起因していました。
• 反復の欠点: Qwen は同じ誤った解決策を何度も生成する傾向があり、トークン制限やコンテキストウィンドウの制約により、過去の失敗例をプロンプトに含めて修正を促すことが困難でした。

4.4 コスト

• GPT-5 の実験全体のコストは、LTL 合成で約 44 ドル、SyGuS で約 2.6 ドル、TLA+ で約 20 ドル、再帰合成で約 0.8 ドルでした。記号ツールはランタイムコストがほぼゼロであるのに対し、LLM は計算リソースと API コストがかかります。

5. 結論と意義

5.1 結論

1. LLM 単体での合成能力: 現在の LLM（GPT-5 や Qwen）は、特定のドメイン（特に SyGuS や再帰合成）では記号ツールと同等の性能を発揮しますが、LTL 反応的合成のような複雑な論理合成では記号ツールに劣ります。
2. 効率性の欠如: LLM は、記号ツールに比べて実行時間が非常に長く、コストも高いです。これは、LLM が確率的にサンプリングを繰り返すのに対し、記号ツールが体系的に探索を行うためです。
3. 構文の信頼性: 記号ツールは「構築による正しさ（Correctness by Construction）」を保証し、構文エラーを発生させませんが、LLM は構文エラーや文法違反を頻繁に犯します。
4. 反復の限界: 検証フィードバックを与えずに LLM を反復させる手法（ILST）は、LLM が同じ誤りを繰り返す傾向があるため、効率的ではありません。

5.2 意義と提言

• ポートフォリオアプローチの推奨: LLM と記号ツールは互いに補完的です。LLM が解決できるが記号ツールが解決できないケース、およびその逆のケースが存在するため、実用的には両者を並列実行するポートフォリオアプローチが最も効果的であることが示唆されました。
• ハイブリッド手法の必要性: LLM を単独で使うのではなく、記号ツールや検証器と組み合わせた「神経記号的（Neurosymbolic）」アプローチや、LLM を探索のヒューリスティックとして活用するハイブリッド手法こそが、将来のプログラム合成の鍵となるでしょう。
• 評価基準の明確化: 本研究は、LLM のコード生成能力を「形式仕様を満たすか」という厳密な基準で評価し、単なるコード生成ベンチマークとは異なる視点を提供しました。

総じて、LLM はプログラム合成の分野において有望なツールですが、現時点では「記号ツールを置き換えるもの」ではなく、「記号ツールを補完するもの」として位置づけるべきであり、そのためにはより高度な統合技術の開発が必要であるという結論に至っています。