この論文は、大規模言語モデル（LLM）だけを使って自動定理証明系の一部であるSMTソルバーを作れるかを試したケーススタディです。SMT（充足可能性修正理論）は論理式の満足性を調べる技術です。研究者らは人間が書いたコードを一切使わずに、DPLL(T)スタイルという一般的な設計のSMTソルバーを構築しました。対象とした理論は「量化子なしの解釈されない関数の等式」（QF_UF）で、等式の扱いに必要な手法を実装しています。成果物はSMT-LIBベンチマークで競争力のある性能を示し、正しさの検査にも合格しました。コードは公開リポジトリとして入手できます。 (arXiv:2603.06931v2, 10 Mar 2026)

実際にやったことは次の通りです。LLMエージェント（ClaudeCode上のSonnet 4.6）に指示して、C++20で動くソルバー一式を生成させました。具体的には、Nieuwenhuis–Oliverasの「高速同値閉包（congruence closure）」アルゴリズムを実装し、前処理モジュールやSATソルバーとの接続（CaDiCaLをIPASIR‑UP経由で利用）を組み込みました。入力の解析にはANTLRのSMT-LIB文法を使うよう指示しています。満たされない（unsat）場合は、Leanという定理証明支援系向けの証明を出力する機能も試験的に実装しました。

なぜ重要か。第一に、この仕事はLLMが「推論するソフトウェア」を自動生成できる可能性を示します。通常は専門家が長時間かけて書くような、理論的に繊細なソフトウェアをLLMが短期間で組み上げられることを示した点が新しいです。実用面では、等式推論（QF_UF）は多くのSMTアプリケーションの基盤です。さらに、生成されたソルバーは既存ベンチマークで競争力があり、SATで見つかったモデルを別のリファレンスソルバーで検査するなどの検証手順も組み込まれています。

ただし重要な制約と不確実性があります。最初から完全に正しい実装が出たわけではありません。開発中にブール結合子の扱いが欠けていたり、排他的論理和（xor）がn項として実装されていなかったり、LLMが独自の簡易SATソルバーを書いてしまうなどの問題が生じました。これらは追加の指示や修正プロンプトで直しています。デバッグにはファジング（乱数式の生成）や差分テストを自動生成させて用いましたが、やはり人間の監督や補助は一部で必要でした。証明出力についても制限があり、「すべての不満足例で完全な証明を自動生成する」のは現状のLLMには難しいと著者は述べています。Leanへの証明出力では、大量の前提を扱う際のパース問題や、自動化戦略の工夫が必要でした。

まとめると、この研究はLLMを用いて実際に動くSMTソルバーを「ゼロ人間コード」で構築できることを示す実証例です。同時に、細かな論理的取り扱いや大規模な検証を確実にするためには追加の工夫や人間の介入がまだ必要であることも示しています。成果物と実験の詳細は論文と付属のGitHubリポジトリで公開されています。