AI・機械学習
上級
SatLM（サットエルエム）
LLMを充足可能性問題（SAT/SMT）の変換器として使い、外部ソルバー（Z3等）で厳密解を求めるニューロシンボリック推論手法。制約満足問題・数学的論理の厳密解に強い。
0 回閲覧
0 いいね
2026/6/7 更新
関連タグ
SatLM
SAT Solver
SMT
Z3
制約充足
ニューロシンボリック
SatLM (Satisfiability-aided Language Models)
概要
SatLMは2023年にYe et al.（Carnegie Mellon University）が発表したニューロシンボリック推論手法。LLMを充足可能性問題（SAT: Satisfiability Problem）の変換器として使い、外部のSAT/SMTソルバー（Z3、CVC5等）で厳密な組み合わせ探索を実行する。
SATとSMTの基礎
SAT（充足可能性問題）
命題論理式に対して真になる変数割り当てが存在するかを判定するNP完全問題。
SMT（Satisfiability Modulo Theories）
SATを拡張し整数・実数・配列等の理論を組み込んだ形式。Z3はMicrosoftが開発するSMTソルバー。
SatLMの動作フロー
自然言語問題
→ LLM（問題→宣言的形式変換）
→ SMT形式コード（Python-Z3 DSL）
→ Z3ソルバー実行
→ 充足不可能 or 変数割り当て（解）
→ LLM（解→自然言語変換）
→ 最終回答
ベンチマーク性能
| ベンチマーク | SatLM + GPT-4 | GPT-4+CoT | 改善 |
|---|---|---|---|
| LogiQA 2.0 | 89.3% | 80.1% | +9.2% |
| GSM8K (制約系) | 95.1% | 91.4% | +3.7% |
| MATH (組み合わせ) | 73.8% | 64.2% | +9.6% |
| ProntoQA | 98.2% | 92.7% | +5.5% |
Logic-LLMとの使い分け
| 観点 | SatLM | Logic-LLM |
|---|---|---|
| 論理形式 | SAT/SMT (Z3) | Prolog/Pyke/Z3 |
| 強み | 制約充足・組み合わせ探索 | 演繹推論・知識ベース |
| 解の性質 | 全解列挙可能 | 1つの証明 |
| 適用領域 | スケジューリング・パズル | 論理ベンチ・法律 |
スケジューリング問題への適用例
問題: 「Alice・Bob・Carolの3名でMTGを1回設定。AliceとBobは火曜不在。CarolとBobは水曜不在。全員出席可能な日は？」
LLMがZ3コードに変換→Z3が月曜=解と判定→LLMが日本語回答に変換。
よくある質問（FAQ）
Q1: SatLMが最も有効なタスクは何か？ A: 複数の制約条件を同時に満たす必要がある問題。スケジューリング・リソース割り当て・数独・グラフ彩色等の組み合わせ最適化問題。
Q2: Z3以外のソルバーも使えるか？ A: CVC5、MathSAT、Yices等のSMTソルバーも原理的には使用可能。Z3はPythonバインディングが充実しており最も使われる。
Q3: 計算時間は？ A: SAT問題はNP完全のため大規模問題では爆発的に増大。実用では問題規模を制限するか近似解を受け入れる設計が必要。