Zenn
🌊

LLM × Constraint Solvingを融合するMCP-Solver入門

2025/04/14に公開
OSS
paper
Model Context Protocol
LLM
VLM
tech

MCP-Solver: Bridging the Gap Between LLMs and Formal Reasoning

ソフトウェアエンジニアとして、Claude3.7 sonnet、GPT-4.5、Llamaといった大規模言語モデル（LLMs）の可能性を探っている方は多いと思います。LLMsは膨大な自然言語やコードの学習を通じて、テキストの理解・生成、コードの下書き、要約といった作業には非常に優れています。一方で、厳密な論理的推論、数学的精度、複雑な制約充足などを要するタスクにおいては、LLMsがときに不正確な推測や“幻覚（hallucinate）”を起こしたり、もっともらしいが誤った回答を生成してしまうことも経験があるかもしれません。こうした形式的論理推論が苦手という点は、すでに数多くの研究で指摘されています。

今回紹介する論文では、この問題に対処するために開発されたMCP-Solverというシステムを取り上げます。これは、LLMの自然言語処理能力と、既存のシンボリックソルバー（論理・制約解決ツール）の確かな計算能力とを連携させる「ブリッジ」的存在です。イメージとしては、LLMアシスタントに対して、論理や制約を厳密に処理してくれる専用の“計算機”を与えるようなものです。本記事はStefan Szeiderの論文「MCP-Solver: Integrating Language Models with Constraint Programming Systems」に基づき、その仕組みや応用例、エンジニアにとってどのように役立つかを解説します。

The Core Problem: LLMs and the Rigors of Logic

LLMsは膨大なテキストやコードを学習し、次にくる単語を予測する確率的アプローチに優れています。そのため、文章生成や感情分析といったタスクには非常に強力です。しかし、決定論的かつ論理的に一貫した推論を必要とするタスクには本質的に苦手さが残ります。

たとえば次のような課題を考えてみてください:

  • Scheduling: たくさんの相互依存する制約（従業員シフト、リソース割当など）を考慮して複雑なスケジュールを最適化する。
  • Verification: あるコードやシステム構成が特定の性質を満たしていることを厳密に証明する。
  • Configuration: 一連の複雑なルールに従って有効なシステム設定を見つける。
  • Optimization: 多数の候補から、定義した目的関数に照らして最適な解を見つける（たとえばTraveling Salesperson Problemなど）。

これらは多くの場合、constraint satisfaction problems (CSP)やsatisfiability problems (SAT)、あるいは**satisfiability modulo theories (SMT)**に分類されます。こうした問題を解決するために、何十年もかけて開発・最適化されてきたシンボリックソルバー（Symbolic Solvers）を使えば、多くの場合効率よく信頼性の高い解を得ることが可能です。ソルバーは形式モデルを扱い、論理ルールに基づいて、解の存在を証明したり最適解を見つけることができます。

他方、LLMsだけでは以下のような問題が起こりがちです:

  • 自然言語で書かれた微妙な制約を誤読する
  • ルール違反の解を生成してしまう
  • 解空間（solution space）の探索を体系的に行うことが苦手
  • 最適性や正しさを保証するのが難しい

要するに、自然言語による問題記述の理解という強みを活かしつつ、実際の解の導出はシンボリックソルバーに任せたいというニーズがあるわけです。これをどう実現するかが大きな課題でした。

Proposed Solution/Algorithm: The MCP-Solver Architecture

MCP-Solverは、まさにこの課題に応えるために考案されたシステムです。Model Context Protocol (MCP) というオープンソース標準を用いて、LLMと外部ツール・データソースを統合します。MCPは既にOpenAI、Anthropic、Replit、Sourcegraphなど複数の企業で採用が進んでいるプロトコルです。

1. The Model Context Protocol (MCP)

MCPのコアは、状態を持つサーバ・クライアント型通信プロトコルです。

  • MCP Server: データや計算能力（今回の場合はMCP-Solver）を提供するサーバ。明確に定義されたtools（関数やAPIエンドポイントのようなもの）を公開する。
  • MCP Client: 一般的にはLLMを利用するアプリケーション（例: AIチャットボットやエージェント）。サーバに接続し、必要なtoolを呼び出して情報や処理を取得する。
  • Interaction: クライアントが構造化された入力を伴うtool callを行い、サーバが構造化された出力を返すという形のやり取り。セッションごとに状態が維持されるため、複数回のインタラクションを通じて段階的に大きなモデルを組み立てることができる（例: スケジューリング問題の制約を少しずつ追加していく）。

多くの最新LLMは、この種の「道具としての外部ツールを呼び出す」形態に対応するように訓練されているため、MCPは自然な統合方法として注目されています。

2. The MCP-Solver Implementation

MCP-SolverはMCPサーバとして動作し、LLMクライアントと様々なシンボリックソルバーの間を取り持ちます。論文では以下の3つのバックエンドをサポートする実装が紹介されています:

  • MiniZinc:
    • 制約プログラミング向けの高水準モデリング言語。グローバル制約や最適化をサポート。
    • スケジューリング、リソース割り当て、組合せ最適化などに適用可能。
  • PySAT:
    • PythonでBoolean Satisfiability (SAT)ソルバー（Glucose, Cadicalなど）を扱うためのツールキット。
    • 命題論理式をtrue/falseで満たす割り当ての存在を判定する問題を解く。検証やプランニング、パズル系にも有効。
  • Python Z3:
    • Microsoft Research製のZ3 SMTソルバーをPythonから利用するためのバインディング。
    • SATの枠組みに加え、整数・実数演算、ビットベクトル、配列、量化子などリッチな理論を扱える。プログラム解析や検証、複雑なデータ型を含む問題に強い。

3. Core Interaction: Item-Based Editing and Tools

LLM側が一度にソルバモデル全体を生成するのではなく、アイテム単位でモデルを構築していくアプローチがMCP-Solverの特徴です。モデル（MiniZincコードやPySAT/Z3用のPythonコード）を少しずつ追加・修正する形で組み立てます。ここで、モデルを構成する小さな完結したパーツを「item」と呼びます（変数宣言、制約、Pythonの関数定義など）。

MCP-Solverは以下のような“ツール”をLLMクライアントに公開しています:

  • clear_model: 現在のモデルをリセットして白紙に戻す
  • add_item(index, content): 指定した行番号（index）にアイテム（コード文字列）を追加する
  • replace_item(index, content): 指定した行番号のアイテムを新しい内容で置き換える
  • delete_item(index): 指定した行番号のアイテムを削除する
  • get_model: 現在のモデル内容をアイテムごとに番号付きで取得する
  • solve_model(timeout): バックエンドソルバーに現在のモデルを渡し、指定タイムアウトで解を求める

さらに、サーバ側ではクライアント（LLM）用のinstruction promptsを提供しており、これをLLMに読み込ませることで、ツールの使い方や推奨されるインタラクション手法を学習させられます。

4. Incremental Validation: Ensuring Consistency

  • Validation Succeeds: 新しいモデルの状態が確定
  • Validation Fails: モデルは変更されず、エラーがLLMクライアントに返される

この反復的なバリデーションにより、以下が実現されます:

  • Model Consistency: モデルは常に文法的・論理的（静的にチェックできる範囲で）に正しい状態を保つ
  • Immediate Feedback: もし提案した変更がエラーを引き起こせば、LLMはすぐに修正を試みることができる

バックエンドごとにバリデーションの内容は異なります:

  • MiniZinc Mode:
    • 文法パース（セミコロン漏れなどの基本的なエラー検出）
    • 型チェック（宣言した型に合わない式の排除）
    • インクリメンタルな整合性検証（既存モデルとの整合性確認）
  • Python Modes (PySAT & Z3):
    • Pythonの**Abstract Syntax Tree (AST)**を利用した静的解析
    • 構文チェック: Python組み込みのパーサを用いて、行と列を含むエラーロケーションを取得
    • 安全性解析: import文や関数呼び出し、セキュリティリスクとなりうる操作を調査（後述のSecurity参照）
    • Dictionary Misuse Detection: モデル化でよく用いられるdictionary変数の上書きミスを専用のAST解析で検出
    • Function Call Verification: ソルバー固有の呼び出しパターンの検証（例: solve()や解の取得ロジックなどが正しく書かれているか）
    • エラーメッセージは行番号と共に詳しく返され、修正案まで含む場合もある

5. Security Considerations

Pythonモード（PySAT/Z3）は実行時にPythonコードを生成・実行するため、セキュリティ対策が重要です。MCP-Solverでは次のような対策を施しています:

  • Process Isolation: ソルバー実行はメインのMCP-Solverサーバとは別プロセス（multiprocessing）内で行う。これにより、生成コードがサーバ本体のメモリ空間に直接アクセスするのを防ぐ。
  • Restricted Environment: Python実行環境は必要最小限のビルトインと標準ライブラリのみを許可。ファイルシステムやネットワークなど危険な操作にはアクセスできないようにする。
  • Timeouts: solve_model呼び出し時には必ずタイムアウトを指定し、無限ループなどによるリソースの占有を防ぐ。

6. Execution and Solution Processing

solve_modelが呼ばれたときの流れは以下の通りです:

  1. MCP-Solverは、隔離環境内でバックエンドソルバーを起動
  2. ソルバーが終了するかタイムアウトになるまで待機（論文では同期的に待つ設計だが、将来的には非同期対応も検討）
  3. 解が見つかった（あるいはunsatisfiableやタイムアウト）場合、結果を標準化フォーマットにまとめて返す

標準化された解の辞書には、以下のようなフィールドが含まれます:

  • status: 文字列（"sat", "unsat", "timeout", "error"など）
  • satisfiable: 真偽値
  • values: 解が存在する場合は変数名→割り当て値の辞書
  • objective: 最適化問題での目的関数値
  • solve_time: ソルバーの計算時間
  • success: 処理全体が重大エラーなく完了したかどうか
  • message: ヒューマンリーダブルなステータス説明

PySATやZ3では、内部のexport_solution関数がソルバー固有の結果（論理変数のtrue/false、Z3のビットベクトルなど）をこの標準化フォーマットへ変換します。エラー時にはソルバー固有の詳細やバリデーションメタデータが含まれる構造化されたフィードバックを返します。

Key Results: Demonstrating Capabilities

論文では、大規模な性能比較ベンチマークではなく、MCP-Solverの柔軟性や堅牢性、インタラクションのパターンを示す事例紹介に重点が置かれています（付録の対話ログなど）。

1. Showcase Problem Examples

  • MiniZinc - Traveling Salesperson (TSP):
    付録では、Claude Sonnet 3.5（Claude Desktop経由）のLLMがMCP-Solver（MiniZincモード）をどのように使うかが紹介されています。
    • ユーザがTSPの問題説明や距離行列を提示
    • LLMがclear_modelし、add_itemを複数回呼んでMiniZincモデルを段階的に生成
      • グローバル制約のinclude、nの定義、dist配列宣言、tour変数配列宣言、alldifferent制約、始点都市の制約（tour[1] = 1）、total_distanceの目的関数、solve minimizeステートメントなど
    • solve_modelを呼ぶ
    • MCP-Solverが標準化ソリューションを返す（status: passed, satisfiable: True, 目的関数値, 最適経路など）
    • LLMがその解を自然言語で要約し、ユーザに最適ルートと総距離を報告
  • PySAT - 6 Queens and 5 Knights:
    6x6ボード上にピースを置くパズルで、女王（Queen）同士はナイト（Knight）が間にいる場合以外はお互いに脅威にならない、ナイトは女王や他のナイトを脅かさない…など多層的な制約を持つ問題。
    • LLMがclear_model→複数のadd_item
    • Pythonヘルパー関数（create_var）を定義し、マスごとのqueen_at[(r,c)], knight_at[(r,c)]といった変数を生成
    • PySATの制約生成用ヘルパー（exactly_k）で女王6つ、ナイト5つを置くCardinality制約を追加
    • are_aligned, positions_betweenなどの関数でクイーン同士の攻撃や間にナイトがいるかを判定
    • “ナイトが間にいないとクイーン同士は攻撃しあわない”、“ナイト対クイーンの脅威がない”、“ナイト同士の脅威がない”などの制約を追加
    • 最後にソルバー実行（Glucose3()）と解の取得ロジックを加える。export_solutionで結果をまとめる。
    • solve_model呼び出し→解が返される
    • LLMがそれを読み取り、ボード配置を提示し、制約を満たしていることを確認
  • Z3 - Processor Parity Verification:
    簡易化された8ビットプロセッサで特定の命令列（LOAD, XOR, AND, STORE, COND ORなど）を実行したあと、レジスタR3が常にR0のパリティビットを保持しているかどうかを検証する問題。
    • LLMがZ3のビットベクトル理論を使うコードをadd_itemで追加
    • BitVecでレジスタを表し、Arrayでメモリを表す、execute_instructions関数でZ3演算子（Select, Extract, ^, &など）を使って命令をシミュレート
    • calculate_parity関数でR0のパリティ計算（ビット単位のXORを畳み込む）
    • verify_property関数でプロセッサを初期化→命令実行→期待パリティを算出→R3の下位ビットと比較→property_holdsが常にtrueかどうかをNot(property_holds)でアサート
    • solver.check()で解があればプロパティはfalse（反例あり）、unsatならプロパティはtrue。結果はexport_solutionで返る。
    • solve_modelを呼ぶ→MCP-Solverがstatus: successとproperty_verified: Falseを返す
    • LLMは「パリティが常に保持されるわけではない」と解釈し、Z3が見つけた具体的な反例（R0やメモリの初期値）をユーザに提示

これらの例から、段階的にモデルを組み立て、各ソルバー機能を使い、自然言語と形式的モデルが往復翻訳される流れを確認できます。

2. Lightweight Test Client & Autonomous Use

論文には、MCP-Solverを自動エージェントで使う軽量クライアントの例も掲載されています。ここでは:

  • ReAct Agent: “Reason and Act”スタイルのプロンプトを使うLLMエージェント。問題文を受け取り、必要なときにMCP-Solverのツールを呼び出す。
  • Reviewer Agent: 別のLLMエージェントで、ReAct Agent＋MCP-Solverが出した最終解を検証する。元の問題制約に沿っているかを判定し、結果はcorrect・incorrect・unknownを返す。
  • Self-Correction: ReAct Agentは自分の出した解を再検証するよう促される。論文によれば、エージェントが自力で解の欠陥を見つけ、モデルを修正（MCP-Solverツール呼び出しのやり直し）するケースも多い。Reviewer Agentがさらに検証を行うことで、二重のチェック体制になる。

これにより、単なるチャットボット統合を超えて、自律エージェントが形式的推論を外部委譲するシナリオが示されています。

Practical Implications & Limitations

エンジニア目線で見ると、MCP-Solverは以下のような利点・用途が考えられます。

Implications & Use Cases

  1. Enhanced AI Assistants: 既存のAIチャットボット（ClaudeやChatGPT with MCPなど）やカスタムアプリとMCP-Solverを統合することで、複雑な計画・スケジューリング・構成管理などを自然言語で説明し、LLMがモデルを生成してソルバーで厳密解を得る、といったことが可能になる。
  2. Interactive Modeling & Debugging: 段階的なモデル編集と即時バリデーションにより、制約モデルの開発・デバッグが対話的に行いやすくなる。ユーザはモデルの進化をリアルタイムで追い、エラーフィードバックを元に自然言語で修正指示を出すことができる。
  3. Educational Tool: MiniZincやPySAT CNF、Z3 SMTといったモデリング手法を学ぶ上で、自然言語で制約を記述→形式モデルに変換→ソルバー実行、という一連の流れを観察できるため、教育用途にも有用。
  4. Backend for Autonomous Agents: 複数エージェントで構成されたシステムの一部としてMCP-Solverを組み込み、厳密な論理推論タスクをオフロードさせることで、LLM単独よりも信頼性の高い意思決定が可能になる。
  5. Democratizing Formal Methods: 高度なシンボリックソルバーを、自然言語I/Oを介して扱えるようにすることで、形式手法の専門知識がなくとも強力な解決能力にアクセスできるようになる。

Limitations & Considerations

  1. Synchronous Solving: 現状、solve_model呼び出しはソルバーが終了・タイムアウトするまでブロックする。非常に重い問題には不向きで、今後の改善予定あり。
  2. LLM Capability: MCP-Solverの実力は、最終的にツールを使うLLMのプロンプト理解・モデル生成能力に依存する。LLMが正しい制約定義を学習していない場合は誤ったモデルを作りがち。
  3. Complexity Management: アイテム単位アプローチとはいえ、大規模モデルをチャットベースで扱うのは煩雑になる可能性がある。論文でも、大規模問題向けには複数エージェントや高度なオーケストレーションが必要だと示唆している。
  4. Backend Selection: 現状は1セッションで1バックエンド（MiniZincかPySATかZ3）を使う設計。複数のソルバーを並行利用すると、LLMのトークン消費が増え複雑化するため。将来的に動的バックエンド選択の検討がありうる。
  5. Validation Overhead: 追加・修正のたびにバリデーションが走るため、速度面のオーバーヘッドは多少ある。
  6. Security: LLMが生成したコードを実行する以上、常にセキュリティリスクが付きまとう。MCP-Solverではプロセス分離や制限付き環境を導入しているが、運用には注意が必要。
  7. Removed Legacy Feature: かつては“memo”という永続的ナレッジベース機能があったが、現在はコアのソルバー統合に注力するため削除されている。

Conclusion

MCP-Solverは、LLMが苦手とする論理推論・制約解決の部分を、長年蓄積のあるシンボリックソルバーの厳密性と結びつけることで、LLMの弱点を補完する興味深いアプローチです。**Model Context Protocol (MCP)**を介してソルバーを呼び出す設計により、段階的・検証付きのモデル編集が実現され、自然言語による大まかな記述と形式的な解決手法とのギャップが大きく縮まります。

論文中で扱われているMiniZinc（制約プログラミング）、PySAT（SAT）、Z3（SMT）の3つのパラダイムは、最適化やプランニングから検証に至る広範なソフトウェアエンジニアリング分野をカバーしています。まだ開発途上ではありますが、特にMCPを用いた**反復的な精緻化（iterative refinement）**の概念は、自然言語モデルと形式手法を組み合わせたより強力なAIシステムの方向性を示唆しています。今後、MaxSAT/MUS、非同期ソルビング、追加バックエンドや実データハンドリングなどがサポートされることで、さらに幅広い問題領域での応用が見込まれます。

Discussion