MCP Server Logical Solver

MCP Server Logical Solver

大規模言語モデル（LLM）と形式的な定理証明機能を組み合わせた、強力な論理推論システムです。このプロジェクトでは、MCP-Logic サーバーを活用して、自動推論と論理検証を行います。

概要

このシステムは、次の機能を提供するように設計されています。

• 自然言語と一階述語論理（FOL）形式の両方で論理問題を処理します
• Prover9/Mace4 による自動定理証明を利用します
• LLM ベースの分析によって、構造化された推論を行います
• XOR 変換を含む複雑な論理演算を処理します
• 論理的な結論について詳細な説明を生成します

FOL の入力要件

一階述語論理（FOL）の入力は、Prover9 の構文要件に厳密に従う必要があります。

1. 論理演算子：

   • 全称量化子：∀（all に変換）
   • 存在量化子：∃（exists に変換）
   • 論理積：∧（& に変換）
   • 論理和：∨（| に変換）
   • 含意：→（-> に変換）
   • 同値：↔（<-> に変換）
   • 否定：¬（- に変換）
   • XOR 演算：⊕（同値な形式に自動変換）

2. 形式のガイドライン：

   • 前提と結論は、整形式の論理式である必要があります
   • 変数と述語は、Prover9 の命名規則に従う必要があります
   • XOR 式は、否定と同値を使って同値な形式に自動変換されます

例：

# Original FOL with Unicode
∀x (P(x) ∧ Q(x)) → (R(x) ⊕ S(x))

# Translated for Prover9
all x ((P(x) & Q(x)) -> -(R(x) <-> S(x)))

主なコンポーネント

1. 論理ソルバー（main.py）

• 2 段階のパイプラインで論理問題を処理します。
  • 第 1 段階：Prover9 と連携した LLM による詳細な論理分析
  • 第 2 段階：推論プロセスの構造化された要約
• 複数の論理問題のバッチ処理に対応します
• 前提、結論、説明を含む包括的な出力を提供します

2. テンプレート（template.py）

• LOGICAL_SOLVER_TEMPLATE：LLM による論理問題の解決をガイドします
  • 自然言語と FOL の分析を組み合わせます
  • 形式検証のために Prover9 と連携します
  • 構造化された推論のガイドラインを提供します
• LOGICAL_SUMMARIZER_TEMPLATE：一貫した出力形式を確保します
  • JSON 形式のレスポンスを生成します
  • 説明、回答、ツール使用に関する情報を含みます

3. パーサー（parser.py）

• FOL 論理式の変換を処理します
• XOR 演算の処理に特化しています
• Prover9 の構文との互換性を確保します

4. Prover9 の出力解釈

このシステムは、Prover9 の定理証明結果を次のように解釈します。

• THEOREM PROVED：Prover9 が、前提から結論が論理的に導かれることを形式的に証明したことを示します。この場合、システムは「True」を返します。

• SEARCH FAILED：Prover9 が証明を見つけられなかったことを示します。この結果は、次のいずれかを意味する可能性があるため、さらなる分析が必要です。

  • 「False」：前提が結論と明らかに矛盾する場合、または結論を裏付けない場合
  • 「Uncertain」：前提だけでは結論の真偽を判断できない場合

SEARCH FAILED が発生した場合、システムは LLM ベースの分析を使って「False」と「Uncertain」を区別します。

前提条件

このプロジェクトをセットアップする前に、次の作業が必要です。

1. MCP-Logic サーバーをセットアップします。

   git clone https://github.com/angrysky56/mcp-logic
   cd mcp-logic
   

2. MCP-Logic のセットアップ手順に従います。

   • Windows の場合：

     windows-setup-mcp-logic.bat
     

   • Linux の場合：

     chmod +x linux-setup-script.sh
     ./linux-setup-script.sh
     

3. MCP-Logic サーバーを起動します。

   • Windows の場合：

     run-mcp-logic.bat
     

   • Linux の場合：

     ./run-mcp-logic.sh
     

インストール

1. このリポジトリをクローンします。

   git clone [your-repository-url]
   cd mcp-server-logical-solver
   

2. 依存関係をインストールします。

   pip install -r requirements.txt
   

設定

1. 環境変数（.env）

ルートディレクトリに .env ファイルを作成し、次の設定を記述します。

# Model Configuration
MODEL_PROVIDER=openai  # Options: openai, anthropic, gemini, ollama
MODEL_NAME=gpt-4  # Specify your model name
API_KEY=your_api_key_here  # Required for OpenAI/Anthropic/Gemini

# Optional Settings
DEBUG=False  # Enable debug mode

2. MCP 設定（mcp_config.json）

ルートディレクトリで、ファイル名を mcp_config_example.json から mcp_config.json に変更します：

{
  "mcpServers": {
    "mcp-logic": {
      "command": "uv",
      "args": [
        "--directory", 
        "/path/to/mcp-logic/src/mcp_logic",
        "run", 
        "mcp_logic", 
        "--prover-path", 
        "/path/to/mcp-logic/ladr/bin"
      ]
    }
  }
}

--prover-path と --directory の値を、MCP-Logic をクローンした場所に合わせて変更してください。

プロジェクトの実行

1. 基本的な使い方（単一の問題）

python test.py

これにより、サンプルの問題が処理され、出力が output.json に保存されます。

2. バッチ処理

python main.py input.json output.json

各項目の説明：

• input.json：論理問題を含む入力ファイルのパス
• output.json：結果の保存先となるパス

入力 JSON 形式：

[
  {
    "premises": "Natural language premises...",
    "premises-FOL": "First order logic premises...",
    "conclusion": "Natural language conclusion...",
    "conclusion-FOL": "First order logic conclusion...",
    "label": "True/False/Uncertain"  // Optional ground truth
  }
]

出力形式

システムは、以下の形式で構造化された出力を生成します。tool_use は、ツール呼び出しが成功したかどうかを示します：

{
    "premises": "Original natural language premises",
    "premises-FOL": "Processed FOL premises",
    "conclusion": "Natural language conclusion",
    "conclusion-FOL": "FOL conclusion",
    "answer": "True/False/Uncertain",
    "explanation": "Detailed reasoning process",
    "tool_use": "True/False"
}

トラブルシューティング

1. MCP サーバーの接続に関する問題

   • MCP-Logic サーバーが実行中であることを確認します
   • mcp_config.json のポート設定を確認します
   • ファイアウォールによって接続がブロックされていないことを確認します

2. モデル API に関する問題

   • .env ファイルの API キーを確認します
   • API クレジットが十分にあることを確認します
   • 選択したモデルをアカウントで利用できることを確認します

3. 入力形式に関する問題

   • 入力 JSON の形式を検証します
   • FOL の文が正しい形式で記述されていることを確認します
   • 論理記号に適切な Unicode 文字が使われていることを確認します