关键词

逻辑推理形式化验证类型检查属性证明Coq

RoCQ：Coq推理MCP服务器

项目简介

RoCQ (Coq Reasoning Server) 是一个基于 Model Context Protocol (MCP) 构建的服务器，它将Coq证明助手的功能集成到LLM应用中，为LLM提供强大的逻辑推理能力。通过 RoCQ，LLM可以执行类型检查、定义归纳类型、进行属性证明等高级逻辑操作，从而增强其在数学、逻辑和计算机科学等领域的应用能力。

主要功能点

  • 自动化依赖类型检查：验证代码或数学表达式是否符合复杂的类型规则，帮助LLM理解和生成类型正确的代码。
  • 归纳类型定义：允许LLM定义和验证自定义的归纳数据类型，例如列表、树等，扩展LLM处理复杂数据结构的能力。
  • 属性证明：支持LLM证明逻辑属性，例如数学定理或程序性质，提升LLM进行形式化推理的能力。
  • XML协议集成：使用可靠的XML协议与Coq进行结构化通信，确保数据交换的准确性和稳定性。
  • 丰富的错误处理：提供详细的错误反馈，帮助LLM理解类型错误和证明失败的原因，从而改进其推理过程。

安装步骤

  1. 安装 Coq Platform 8.19 (2024.10)

    RoCQ 依赖于 Coq 证明系统。请访问 https://github.com/coq/platform 下载并安装 Coq Platform 8.19 (2024.10) 版本。请注意，Coq Platform 的安装路径需要记住，后续配置服务器时会用到。

  2. 克隆 RoCQ 仓库

    打开终端，执行以下命令克隆 RoCQ 仓库到本地：

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

  3. 创建并激活虚拟环境，安装依赖

    在仓库根目录下，执行以下命令创建虚拟环境并安装 RoCQ 及其依赖：

    uv venv
./venv/Scripts/activate  # Windows
# source ./venv/bin/activate # Linux/macOS
uv pip install -e .

    或者，您也可以使用 'pip' 安装依赖：

    pip install -r requirements.txt

服务器配置

MCP 客户端需要配置 RoCQ 服务器的启动命令和参数才能连接。以下是 JSON 格式的配置示例，请根据您的 Coq Platform 和 RoCQ 仓库的实际安装路径进行修改：

{
  "serverName": "mcp-rocq",
  "command": "uv",
  "args": [
    "--directory",
    "F:/GithubRepos/mcp-rocq",  // 修改为您的 RoCQ 仓库路径
    "run",
    "mcp_rocq",
    "--coq-path",
    "F:/Coq-Platform~8.19~2024.10/bin/coqtop.exe", // 修改为您的 coqtop.exe 路径
    "--lib-path",
    "F:/Coq-Platform~8.19~2024.10/lib/coq"   // 修改为您的 Coq lib 路径
  ]
}

配置参数说明:

  • '"serverName"': 服务器名称，可以自定义，用于在 MCP 客户端中标识该服务器。
  • '"command"': 启动服务器的命令，这里使用 'uv'，确保您的环境中已安装 'uv'。如果您使用 'pip' 安装依赖，可以将此项修改为 'python'。
  • '"args"': 传递给启动命令的参数列表。
    • '"directory"': 指定 RoCQ 仓库的根目录。
    • '"run"': 使用 'uv run' 运行 Python 模块。 如果您使用 'python' 命令，则此参数可以省略，并在 'command' 中直接使用 'python'。
    • '"mcp_rocq"': 指定要运行的 Python 模块为 'mcp_rocq'，对应 'src/mcp_rocq/server.py' 文件。
    • '--coq-path': Coq 解释器 'coqtop.exe' 的路径，请替换为您的 Coq Platform 安装目录下的 'coqtop.exe' 路径。
    • '--lib-path': Coq 标准库的路径，请替换为您的 Coq Platform 安装目录下的 'lib/coq' 路径。

基本使用方法

RoCQ 服务器提供以下三个主要工具，您可以在 MCP 客户端中调用这些工具来利用 Coq 的推理能力：

  1. 类型检查 (type_check)

    用于检查一个表达式 (term) 的类型是否正确。

    {
    "tool": "type_check",
    "args": {
        "term": "1 + 1",  // 要检查类型的表达式
        "expected_type": "nat", // 可选：期望的类型
        "context": ["Arith"]  // 可选：需要导入的 Coq 模块
    }
}

  2. 定义归纳类型 (define_inductive)

    用于定义新的归纳数据类型，例如树、列表等。

    {
    "tool": "define_inductive",
    "args": {
        "name": "Tree", // 归纳类型名称
        "constructors": [  // 构造器列表
            "Leaf : Tree",
            "Node : Tree -> Tree -> Tree"
        ],
        "verify": true // 是否验证归纳类型的性质
    }
}

  3. 属性证明 (prove_property)

    用于证明一个逻辑属性或数学定理。

    {
    "tool": "prove_property",
    "args": {
        "property_stmt": "forall n m : nat, n + m = m + n", // 要证明的属性
        "tactics": ["intros n m."], // 可选：证明策略
        "use_automation": true // 是否使用自动化证明
    }
}

    您可以根据需要在 MCP 客户端中构造上述 JSON 请求，并发送给 RoCQ 服务器以执行相应的 Coq 功能。服务器将返回 JSON 格式的响应，包含执行结果或错误信息。

注意:

  • 首次使用可能需要一些时间启动 Coq 进程。
  • 请确保 Coq Platform 安装正确，并且 'coqtop.exe' 和 Coq 库路径配置正确。
  • 如果遇到问题，请查看 RoCQ 服务器的日志输出，以便进行调试。

信息

分类

AI与计算

访问项目