MCP-Solver： 言語モデルと制約プログラミングシステムの統合 Integrating Language Models with Constraint Programming Systems
S Szeider著・31 Dec 2024・TU Wien
Code
mcp-solver
szeider • Updated Apr 16, 2025
MCP Document
Blog
Overview
WHAT（これは何？）
- モデルコンテキストプロトコル（MCP）のプロトタイプ実装であるMCP Solverを提案し、LLMと制約システム（制約条件に基づいて最適解を探索するシステム）間の体系的な統合の可能性を実証した
- MCP Solverは、制約プログラミング言語と対話するために、モデルの送信、パラメータ管理、ソリューションの検索、およびインタラクティブな改良のためのツールを提供する
WHY（提案手法の価値は？）
- LLMと制約ソルバー間をMCPベースで統合する形式的仕様を提供した
- この統合アプローチの実用的な実現可能性を実証
- 自然言語で記述された仕様をLLMが形式的な制約モデルに変換し、これらのモデルを検証し、解を確認するための正確なインターフェースを提供
- LLMの推論の限界を、制約ソルバーのもつ形式的な保証によって補完する目的
- 検証機能を備えたアイテムベースの編集アプローチにより、システムは各修正ステップで制約モデルの一貫性を確保し、構造化された反復的な改良を可能にする
WHERE（技術のキモはどこ？）
MCP Solverは、MCPに準拠した柔軟なアーキテクチャを提供する
LLMと制約ソルバーを組み合わせる従来のアプローチは、特定の用途に特化した固定的な連携が多かった
- 固定的な連携（従来システム）
- 用途が限定
- 特定の問題やタスクに合わせて設計されている
- システム変更が困難
- LLMと制約ソルバー間の連携方法が固定されている
- パイプライン型
- LLMの出力が直接制約ソルバーに入力されるなど、一方向のデータフローが多い、あるいは、限定的な双方向インタラクションにとどまる
- MCP Solver
- 汎用的
- 様々な制約プログラミングのパラダイム（充足問題、最適化問題、パラメータ探索など）に対応できる
- 反復的なインタラクション
- 制約ソルバーの解に基づいてLLMが制約やモデルを修正したり、ユーザのフィードバックを反映することが可能
- 標準化されたインターフェース
- MCPに準拠したツールインターフェース
- 動的な問題の対応
MCP Solverの設計
主要コンポーネント
- Claude Desktopアプリ
- MCPクライアント
- MCP Solver
- MCPサーバー
- 検証とエラー処理を備えたMCPのリクエスト-レスポンスプロトコルを実装
- MiniZinc
- 制約を解決するバックエンド
- デフォルトソルバーとしてChuffedを採用
- MiniZincと互換性のある全てのソルバーをサポート
- ClaudeのようなLLMが自然言語を通じて制約モデルと対話し、サーバーはこれらの対話を管理し、Python APIを使用してMiniZinc操作に変換する
- LLMは、反復的な改良をサポートする制約モデリングアシスタントとして機能する
- その後、MiniZincはこれらのモデルを制約ソルバーで処理可能なFlatZinc仕様にコンパイルする
ツール
- アイテムベースのモデル管理アプローチ
- get model: 番号付きアイテムで現在のモデルを表示
- add item: 特定のインデックスに新しいアイテムを追加
- delete item: インデックスのアイテムを削除
- replace item: インデックスのアイテムを置換
- clear model: モデルをリセット
- solve model: Chuffedソルバーで実行
- get solution: 配列インデックスを使用してソリューション変数の値を取得
- get solve time: 実行時間を取得
- get memo: 知識ベースにアクセス
- edit memo: 知識ベースを更新
- 行ベースでなくアイテムベースの編集アプローチ
- モデルの変更は、制約モデルのコードを1行ずつ修正するのではなく、意味のある単位（アイテム）に分割し、アイテムベースで追加、削除、置換などの操作を行う
- モデルの変更は、検証が成功した場合にのみ適用され、現在のモデルが常に有効な状態を維持することを保証する
- 各変更が提案されると、Python MiniZincの検証チェーン（構文解析、型チェック、インスタンス化の検証）が起動する
- 行ベースの編集で発生する可能性のある不整合を排除
- 現在のモデルは番号付きアイテムとして一貫して追跡される
- LLMはソルバーのフィードバックに基づいて制約を反復的に追加し、目的関数を修正し、パラメータ宣言を調整してモデルを改良することができる
- LLMが的確な改良を行えるように、検証システムは詳細な診断情報を提供し、正確なエラー報告を可能にする
- 継続的な検証
- 編集中の継続的な検証により、LLMはモデルの整合性を保ちながら自由にモデリングアプローチを探索する
- セッションの状態維持
- システムは、現在のモデル、ソリューションキャッシュ、パフォーマンス統計を含むソルバーセッションの状態を維持
- ソルバープロセスの終了処理において、非同期コンテキストマネージャーを通じて適切なリソースのクリーンアップを実装
- モデルの更新、解決操作、ソリューションの取得を調整
- メモシステム
- メモシステムが、セッション間でソリューションの知見を維持し、過去のモデリング経験からの知識を蓄積する
- 定期的にレビューとキュレーションが可能な、解決とモデリングの知見からなる成長型の知識ベースを維持
- LLMは成功したモデリング戦略と複雑な問題の解決策を自動的に記録する
- get memoとedit memoツールで、行ベースの編集インターフェースを通じてこの知識ベースへアクセス可能
代表的なテスト例
- ユーザーが入力した複雑な論理条件をLLMが論理式に変換する
Focus
MCP Solverのシステムアーキテクチャ
Keyword
モデルコンテキストプロトコル（MCP）
- LLMを外部システムに接続する方法を標準化する共通の仕様またはプロトコル
- Anthropicが2024年11月26日に公開
- 非形式的な自然言語処理と形式的な計算システム間の体系的な相互作用のための共通プロトコル
- 現在のMCP関連サービス
- MCPサーバー例
- MCP採用企業
- BlockやApollo
- MCP統合プラットフォーム
- Zed、Replit、Codeium、Sourcegraph
制約プログラミング constraint programming
- 問題を制約として記述し、ソルバーを用いてその制約を満たす解を探索する手法
- 制約プログラミング言語の例：MiniZinc
- 問題の解決策は、制約モデルとして定義される
制約モデル constraint mod
- 問題の変数とそれらの間の制約条件を形式的に記述した数理モデルのこと
- MiniZincのような制約モデリング言語で表現される
- 変数、制約、および目的関数で構成される
制約ソルバー constraint solver
- 制約モデルで定義された、制約を満たす解を探索するアルゴリズム
- 制約充足問題（解が存在するかどうかを判定する問題）や最適化問題（最適な解を求める問題）のソルバーが存在する
MCP-Solver
- MCPプロトコルを実装したサーバー（MCPサーバー）の一種
- 形式的推論を行うシステム（制約モデル、制約ソルバー含む）とLLMを統合する
- 以下のオープンソース
- ‣
RelatedWork
PRoC3S
- ロボット工学における長期的な問題解決にLLMと制約充足（Constraint Satisfaction）を組み合わせたシステム
- LLMはロボットの行動計画の草案を作成し、制約充足ソルバーがその計画が現実世界で実行可能かどうかを検証し、必要に応じて修正するという連携作業を行う
- LLMが生成したパラメータ化されたスキルシーケンスが制約充足問題として定式化され、継続的に検証される
- MCPは、このプロセスをさらに柔軟にし、LLM と制約ソルバー間の連携を標準化できる可能性を持つ
- MCPを使用することで、LLM は制約ソルバーにアクセスし、制約モデルを動的に編集し、結果を解釈して行動計画を改善する