LLM2SMT: Building an SMT Solver with Zero Human-Written Code

この論文は、人間のコードを一切書かずに LLM コーディングエージェントが QF_UF 形式の完全な SMT ソルバーを構築し、その性能が SMT-LIB ベンチマークで競合するレベルであることを示したケーススタディです。

要約

「人間がコードを 1 行も書かない」SMT ソルバーの誕生

～AI 職人が「論理の探偵」をゼロから作り上げた物語～

この論文は、**「人工知能（LLM）が、人間の手を全く借りずに、自分自身で『論理を解くための道具（SMT ソルバー）』を作れるのか？」**という挑戦的な実験の記録です。

まるで、職人（人間）が一切の設計図や道具を与えずに、ただ「いい感じに作って」と頼むだけで、見習い職人（AI）が完璧な時計を完成させるような話です。

---

1. 何を作ったの？（SMT ソルバーとは？）

まず、作られたのは**「SMT ソルバー」というものです。
これを「超能力を持った論理探偵」**と想像してみてください。

• 探偵の任務: 「A は B と同じ、B は C と同じ、でも A は C と違う」のような、一見矛盾しているような複雑な条件の羅列を渡されます。
• 探偵の能力: 「これは矛盾している（答え：NO）」か、「矛盾していない、こういう組み合わせなら成立する（答え：YES）」を瞬時に見抜きます。
• この実験の成果: 人間が 1 行もコードを書かずに、この「探偵」を AI だけで作りました。しかも、その探偵は「証明（なぜその答えに至ったかの証拠）」も Lean という言語で書き出すことができます。

2. 実験のプロセス：AI 職人の「試行錯誤」

人間は「SMT ソルバーを作って」という**「最低限の注文」**だけを出しました。詳細はすべて AI に任せたのです。しかし、最初は AI も失敗しました。

• 最初の失敗: AI は「論理のつなぎ方（AND や OR）」を完全に忘れていました。まるで、料理を頼んだのに「塩も砂糖も入れない」状態です。
• 修正: 人間が「そこはこうだよ」とヒントを出すと、AI はすぐに直しました。
• 面白いエピソード: AI は最初、自分専用の「簡単な探偵」を作ろうとしましたが、人間が「プロの探偵（CaDiCaL という既存のツール）を使って」と指示すると、すぐにそれに切り替えました。

重要な発見:
AI はバグ（ミス）を見つけるのが得意ですが、「なぜミスが起きたか」を自分で見つけるのは苦手でした。そこで人間は、AI に「ランダムな問題を出して、他の探偵と答えを比べる（フェージング）」という**「自動テスト」**の仕組みを作らせました。これにより、AI は「あ、ここが間違っていた」と自分で気づき、修正できるようになりました。

3. 最大の難関：「ダイヤモンド問題」と証明

実験で最も面白かったのは、**「ダイヤモンド問題」**という特殊なパズルへの対応です。

• パズルの例: 「A=B または A=C」かつ「B=D または C=D」という条件が何重にも絡み合っている状態です。
• AI の工夫: 人間が「このパズルを解くには、前もって条件を整理する（前処理）必要がある」とヒントを出しただけで、AI は**「各分岐で共通する結論（A=D など）を先に導き出しておけば、爆発的に増える組み合わせを回避できる！」**という高度な戦略を自力で編み出しました。まるで、迷路の入り口で「ここを通ればゴールに直結する」という地図を自分で描いたようなものです。

さらに、**「証明（Lean 言語での証拠）」を出す作業は最も難しかったです。
AI は「答え」は出せても、「なぜそう言えるのか」を、厳格なルール（Lean）に従って説明するのが苦手でした。人間が「このように証明を書け」という「お手本」**を見せないと、AI は「証明の書き方」を理解できませんでした。

4. 結果：プロと張り合えるか？

完成した AI 製ソルバーは、SMT-LIB という世界的な基準テストで、Z3 や cvc5 といった「プロのソルバー」とほぼ同等の性能を出しました。
人間がコードを 1 行も書かないで、これだけの性能が出たのは驚異的です。

ただし、いくつかの課題も残りました。

• ジャギッド・インテリジェンス（ギザギザした知能）: 複雑なことは得意なのに、「A=A なら True だ」という極単純なことを最初に見落としていたりします。
• 証明の壁: 答えを出すのは得意ですが、その証明を完璧に書き上げるのはまだ人間の手助けが必要です。

結論：AI は「道具を作る職人」になれるか？

この実験は、**「AI は、人間が設計図を描かなくても、複雑な論理ツールをゼロから作れる」**ことを示しました。

ただし、AI は**「完璧な天才」ではなく「優秀だが、たまにミスをする見習い職人」**です。

• 人間は「何を作るか」の指示と、「テスト方法（フェージング）」の環境を用意する。
• AI は「どう作るか」を考え、失敗したら自分で直す。

この「人間と AI の共創」があれば、将来は人間がコードを書く必要なく、あらゆる専門的なソフトウェアが AI によって自動生成される日が来るかもしれません。

---

一言でまとめると：

「人間は『料理の味付け』と『味見の基準』だけ教え、AI が『包丁を握って』完璧な料理（SMT ソルバー）を作った。味はプロ級だが、盛り付け（証明）にはまだ人間のチェックが必要だ」という、AI 開発の新しい可能性を示す物語です。

技術概要

LLM2SMT: 人間によるコード記述ゼロでの SMT ソルバー構築に関する技術的概要

本論文「LLM2SMT: Building an SMT Solver with Zero Human-Written Code」は、大規模言語モデル（LLM）が自律的に高度な論理推論ツール（SMT ソルバー）を開発できるかという問いに対し、実証的なケーススタディを通じて回答を試みたものです。人間がコードを一行も書かずに、LLM のコーディングエージェントが完全な SMT ソルバーを構築し、既存のソルバーと競合する性能を示すことに成功しました。

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

1. 問題設定と背景

• 研究の動機: LLM がソフトウェアを記述できることは広く議論されていますが、LLM が「推論を行うソフトウェア（自動推論ツール）そのもの」を記述できるかは未探索の領域でした。
• 課題: 自動推論ツールは厳密な正しさが要求されます。LLM が基礎となる論理を十分に理解し、微細なバグ（例：ブール値と項の混同など）を含まずに信頼性の高いソルバーを生成できるかが問われました。
• 対象: 本稿では、DPLL(T) フレームワークの基盤となる「量化子なしの非解釈関数付き等式理論（QF_UF）」に焦点を当てました。

2. 手法と開発プロセス

研究は、Claude Code（Sonnet 4.6 モデル）を使用したコーディングエージェントによって実施されました。人間はコードの記述を行わず、最小限のレビューと評価のみを行いました。

2.1 開発の初期段階と課題

• 初期プロンプト: 研究者は「SMT ソルバーの実装（パーサー、SAT ソルバー、IPASIR-UP インターフェース、任意精度ライブラリ、CMake によるビルド、QF_UF 理論の congruence closure 実装）」という高レベルな指示を与えました。
• 初期の失敗: 初期の生成コードは、ブール論理結合子を扱えていなかったり、XOR を n 項演算として実装できていなかったりするなど、重大な欠陥を含んでいました。
• 修正プロセス: 研究者は具体的な仕様（SMT-LIB のコア理論仕様）や、特定の欠陥（XOR の実装、CaDiCaL の統合など）を指摘するプロンプトでエージェントを誘導しました。

2.2 技術的実装

• SAT ソルバー: 当初エージェントは独自の簡易 SAT ソルバーを作成しましたが、指示により CaDiCaL を IPASIR-UP インターフェース経由で統合しました。
• 理論ソルバー: Robert Nieuwenhuis と Albert Oliveras が提案した Congruence Closure アルゴリズム を実装しました。
• 言語と環境: C++20、ANTLR（パーサー用）、CMake（ビルド用）を使用。
• デバッグ支援: エージェント自身によるバグ修正を支援するため、以下の手法を適用しました。
  • Fuzzing: ランダムな論理式生成器の作成。
  • 差分テスト: 参照ソルバーとの比較スクリプトの作成。
  • これにより、LLM がバグを「手動」で特定するコストを削減し、トークン使用量を抑制しました。

2.3 前処理（Preprocessing）の工夫

• Diamond 問題への対応: SMT-LIB に含まれる「等式ダイヤモンド問題（$x_1 \neq x_{n+1}$ と、一連の等式の選言の組み合わせ）」は、DPLL(T) にとって指数関数的な探索を強いる難問です。
• 解決策: エージェントに「この問題に対する前処理手法を考案せよ」と指示したところ、エージェントは各分岐での等式の閉包（EUF-closure）を計算し、すべての分岐に共通する等式を抽出して新しい単位等式として追加する手法を自律的に開発しました。これにより、このクラスのベンチマークを瞬時に解決できるようになりました。

2.4 証明生成（Certification）

• 充足不能（UNSAT）の場合: 生成された証明を Lean（インタラクティブ定理証明器）形式で出力し、検証可能にしました。
• 実装戦略:
  • 理論補題（congruence closure から導かれるもの）は grind タックで検証。
  • 命題論理部分は bv_decide タックで検証。
  • 初期は 1 つの定理に全てを詰め込む試みは失敗（スケーラビリティの問題）したため、各理論補題を個別の定理とし、最終的に False を導く証明を構築する設計に変更しました。
• 課題: エージェントは「理論補題」と「最終証明」の区別や、Lean の証明レベルの複雑さを理解するのに苦戦し、人間による具体的な証明例の提示が必要となりました。

3. 結果と評価

SMT-LIB ベンチマーク（QF_UF 非増分）を用いて、Z3 や cvc5 と比較評価を行いました。

• 性能:
  • 解決したインスタンス数：LLM2SMT は 7,468 件（Z3: 7,500 件、cvc5: 7,494 件）。
  • 既存の成熟したソルバーとほぼ同等の性能を達成しました。
• 前処理と理論伝搬の影響:
  • 前処理（Preprocessing）を無効化すると性能が低下しました。
  • 意外なことに、理論伝搬（Theory Propagation）を無効化した方が、今回のベンチマークセットではわずかに高速でした（オーバーヘッドの方が効果を上回ったため）。
• 証明の検証:
  • Lean による証明検証はリソース制約（スタックオーバーフロー、タイムアウト）により多くの失敗がありましたが、誤った証明（誤って UNSAT と判定されたケース）は見つかりませんでした。

4. 主要な貢献

1. ゼロコードでのソルバー構築: 人間がコードを一切書かずに、LLM エージェントが DPLL(T) 型の SMT ソルバーをゼロから構築し、実用的な性能を達成した初のケーススタディ。
2. 自律的デバッグと改善: Fuzzing や差分テストなどの標準的な開発ツールを LLM に使用させることで、バグの特定と修正を効率的に行うプロセスの確立。
3. 高度な前処理技術の自律発見: 研究者が具体的なアルゴリズムを指示しなくても、LLM が「等式ダイヤモンド問題」を解決するための効率的な前処理手法を独自に考案・実装した点。
4. 証明生成の実証: 自動推論ツールの出力を、別の定理証明器（Lean）で検証可能な形式に変換するパイプラインの構築。

5. 意義と今後の展望

• 意義: LLM は、適切なスキャフォールディング（構造化された支援、具体的な失敗例の提示、リソース制限の明示）があれば、高度な論理ツールを開発できることを示しました。これは「LLM が推論ツールそのものを作れるか」という問いに対する「条件付きの Yes」です。
• 限界と課題:
  • 正しさの保証: 人間によるガイドなしでは、微妙なバグ（ブール値と項の混同など）が放置されるリスクがあります。
  • 証明生成の難易度: ソルバーのロジックだけでなく、証明チェッカー（Lean）の期待値を理解させるのは非常に困難でした。
  • ジャグド・インテリジェンス（Jagged Intelligence）: 高度なタスクをこなす一方で、単純なタスク（例：$t=t$ を true に簡約する）で失敗するなどの不安定さが観察されました。
• 将来の展望: より多くの理論のサポート、生成されたコードのより慎重な分析による改善提案、そして証明生成の自動化精度の向上が期待されます。

本論文は、LLM を単なるコード生成ツールとしてではなく、複雑なシステム設計と実装を担う「自律的なエンジニア」として活用する可能性を示唆する重要な一歩です。