内容
# rocq-mcp-evolve —— 一种为 Rocq 进化的 MCP 服务器，由 LLM 驱动的设计搜索
[](https://github.com/LLM4Rocq/rocq-mcp-evolve/actions/workflows/ci.yml)
[](https://llm4rocq.github.io/rocq-mcp-evolve/)
一种**经验设计的、中立策略的 MCP 工具层**，允许 LLM 代理驱动 Rocq（Coq）证明器 —— *以及* 受控实验，以产生它。从一个故意朴素的控制（一个工具 = 一个完整的 `rocq compile`）开始，我们分析了一个弱代理哪里会失败，并迭代接口，每次一个可衡量的变化，以对抗每个存储桶的基准；每个设计决策都得到了数字的支持，每个证明只有通过反作弊正确性门槛才被接受。该层是一个独立的 OCaml 项目，链接到进程中安装的 Rocq 9.1.1 库 —— **无需修改 Rocq 源代码** —— 并且是一个服务器，既可以是弱模型，也可以是强模型，通过预注册的跨策略最佳-最差情况标准选择。
**从这里开始**： [`STATUS.md`](STATUS.md) （2 分钟状态）·
[`docs/REPORT.md`](docs/REPORT.md) （所有结果）·
[`docs/DESIGN.md`](docs/DESIGN.md) （每个决策的理由）。
## 主要结果
所有三个目标，按难度分类（简单 / 中等 / 困难），dev60。
**$/solve** = 平均每次尝试的成本 ÷ pass@1（预期解决每个证明的支出，包括失败）；**wall** = 平均每次尝试的秒数。SOTA =
[rocq-mcp](https://github.com/LLM4Rocq/rocq-mcp)，在相同的环境、问题、门槛和策略下测量（仅在我们的设计冻结后首次接触；“公平” = 在审计发现原始集成竞赛服务器启动后重新运行，通过即时握手代理）。
| 接口 | 策略 | pass@1 | $ / solve | wall 秒 |
| --- | --- | --- | --- | --- |
| 朴素整个文件（控制） | haiku | .44 / .25 / .30 | .18 / .44 / .49 | 90 / 122 / 157 |
| rocq-mcp（SOTA，公平） | haiku | .68 / .35 / .33 | .08 / .22 / .31 | 65 / 76 / 97 |
| **`universal`**（推荐） | haiku | **.66 / .58 / .40** | .10 / .16 / .23 | 59 / 71 / 74 |
| 朴素整个文件 | sonnet | .93 / .95 / .80 | .09 / .15 / .18 | 61 / 77 / 112 |
| rocq-mcp（SOTA，公平） | sonnet | .95 / .93 / .80 | .11 / .19 / .26 | 50 / 64 / 105 |
| **`universal`** | sonnet | **.95 / 1.00 / .85** | **.07 / .09 / .13** | **36 / 42 / 85** |
| 朴素整个文件 | fable | .95 / 1.00 / .95 | .09 / .19 / .35 | 51 / 40 / 73 （1 次重复） |
| **`universal`** | fable | **.95 / 1.00 / 1.00** | .14 / .16 / .29 | 49 / 41 / 57 （1 次重复） |
| `frozen` —— **保留** miniF2F 测试 | haiku | .52 / .13 / .04 | — | 单次登录运行 |
读取：`universal` 在 **所有三个策略层** 中都是最佳或并列最佳；在 sonnet 上，它同时是最准确 *和* 最便宜的每个已解决证明的工具，测量公平 SOTA 比较：接近 sonnet 的准确性对齐，rocq-mcp 在 haiku 上领先容易；rocq-mcp-evolve 在弱策略中等/困难方面领先，并且在 sonnet 上每个已解决证明的成本约为一半。
**阶梯（弱策略）：** 基线 `.44/.25/.30` → 获胜者 `.70/.525/.425`
（4 次重复）通过 6 次保留 + 4 次回滚的测量变化，**-45% 成本，-55% 壁垒**；
每次交互的证明延迟 **266 毫秒 → ~1 毫秒**（持久的进程内会话 + O（1）快照回滚 vs 完整重新编译）。可扩展性：在 N=8 个代理时，约 80% 的并行效率，≈6× 已解决证明/小时 vs 控制。
> **设计规律，从 10 次消融：** *最大化模型每次转换的证明基础信息，零边际转换成本。* 所有将信息推入现有转换（尝试，提示，自动关闭，是否意味着-什么，预加载）的内容都赢了；所有花费转换或丢失上下文以获取信息的内容（拉取搜索工具，紧凑渲染，3 代理中继）都失败了。
诚实笔记：haiku universal hard 为 .400±.14，4 次重复，.075 低于 haiku 专用配置（其一个非领先单元格）；
sonnet 中等 `1.00` 为 2/2 次重复；保留的行是单个冻结配置运行（无测试问题影响任何决策）；
强策略附件为 1-2 次重复。
## 工具 —— 一个中立策略的 MCP 服务器（`rocq`）
代理通过 stdio 与 `rocq-mcp-evolve` 进行 MCP 通信。整个证明和增量样式都在 **一个** 服务器中都是首选的。所有工具和增强功能默认开启（使用 `ROCQ_ENABLE_TOOLS` 修剪，禁用功能使用 `ROCQ_<FEATURE>=0`）。
| 工具 | 功能 |
| --- | --- |
| `build{file}` | 在一次调用中诊断整个文件：每个顶级块都会执行；失败的证明在会话中被 `Admitted`，因此依赖项仍然会检查 —— 您一次可以得到 **所有** 损坏的证明，然后通过 `open` 修复每个证明。纯粹用于诊断。 |
| `open{file, theorem?}` | 在运行时打开一个 `.v` 文件并启动（或重启）一个会话：目标是命名定理的语句（其旧证明/`Admitted` 被忽略，并且任何 **较早** 的损坏证明自动被 `Admitted`，因此每个定理都是可达的 —— 修复任何顺序的孔）或文件的末尾开放目标。项目加载路径从文件位置自动发现。 |
| `check{script}` | 在一次调用中提交一个 **完整的** 证明（`Proof. … Qed.`）。成功时，完成；失败时，保留有效前缀，您将位于带有实时目标的失败句子处 —— 修复或重新提交。 |
| `step{text}` | 增量执行一个或多个句子；每个成功永久提交，第一个失败报告结构化错误，并将状态留在最后一个成功处。查询（`Search`/`Check`）也会在这里运行。 |
| `try{candidates}` | 从当前状态 **推测性** 测试最多 8 个候选脚本；完全成功时，提交第一个候选（k 个想法，一个回合）。 |
| `auto_close{}` | 对当前目标运行标准终结者投资组合（lia/lra/nra/nia/ring/…）；如果一个终结者成功，则提交一个终结者。便宜 —— 自由调用。 |
| `rollback{count}` | 撤销上一次提交的句子（O（1）状态交换），并显示您返回的目标。 |
| `state{}` | 重新渲染所有开放目标和已提交的证明； |
跨越剪切增强（零额外回合，所有默认开启；禁用 = 0）：
- **错误提示** （`ROCQ_HINTS`）—— 将 Lean-isms 和常见错误重写为 Rocq 形式，内联到错误有效载荷中。
- **是否意味着-什么** （`ROCQ_SUGGEST`）—— 将近似的现有引理名称附加到未知引用错误中。
- **提示合成** （`ROCQ_AUTO2`）—— `auto_close` 机械地断言辅助事实（例如，从目标子项 `0 <= (t)²`）并重试非线性终结者。
- **示例检索** （`ROCQ_EXEMPLARS=1`，按需）—— 将 `k` 个最语句相似的 **已证明** 引理（及其证明）推入第一个响应。测得在测试的策略下中立（弱策略可能会被它分散注意力），因此默认关闭；检索质量本身经过验证且无泄漏。
- **挂起安全** —— 每个句子都在检查点超时 **和** 分配触发的中断（memprof-limits，coq-lsp 机制）下运行，因此即使 `vm_compute`/`native_compute` 分歧也返回结构化 **TIMEOUT** 而不是冻结会话（`ROCQ_FORK_PROBE=1` 为零状态风险上下文添加了一个 fork-isolated 腰带）。
- **策略预加载** （`ROCQ_PRELOAD`）—— 加载 Lia/Lra/Psatz 之后语句，因此标准终结者始终存在。在 **mathcomp** 文件中，它还会预加载 `zify`/`algebra-tactics`，给予 `by lia`/`by ring`/`by lra` 在布尔反射和 ssralg 目标上的实际权力（`ROCQ_MC_TACTICS=0` 禁用）。桥梁需要可选的 opam 包 `coq-mathcomp-zify` 和 `coq-mathcomp-algebra-tactics` —— 仍然 `coq-` 上游命名；这些两个卫星尚未遵循 mathcomp 核心重命名为 `rocq-mathcomp-*`。（`ROCQ_ENV_V2=1` 另外 **拒绝** 证明中的 `Require` —— 一个基准反作弊策略，正常使用时关闭。）
## 安装和尝试（2 分钟）
```sh
opam pin add rocq-mcp-evolve https://github.com/LLM4Rocq/rocq-mcp-evolve.git
```
将 `rocq-mcp-evolve` 二进制文件安装到您的 opam 开关（会自动拉取 `rocq-runtime` 9.1+）。然后在任何 MCP 客户端配置（Claude Code，`claude` CLI 或任何 MCP 说话的客户端）中添加一个块：
```json
{ "mcpServers": { "rocq": { "command": "rocq-mcp-evolve" } } }
```
就是这样 —— 没有任何配置。然后让您的代理完成一个证明：它调用 `open{file}`（可选 `theorem:<name>` 目标一个 `Admitted` 或文件中的任何特定语句），使用其他工具完成证明，并在完成后接收完成的脚本以插入您的文件中。一个会话可以打开同一个项目中的多个证明 —— 导入前缀是 **重放记忆化** 的，因此即使是 mathcomp-heavy 导入也只需支付一次每个会话，而不是每个打开（重新打开：~0.4 秒）。
其他一切都是自动的：
- **项目加载路径自动发现** —— 服务器从任务文件一路向上遍历到您的 `_CoqProject`/`_RocqProject` （解析为 `-Q/-R/-I`）或 `dune-project` （`coq.theory` 条款，映射到 `_build/default` 镜像）。首先构建您的项目；不需要其他设置。可以使用 `ROCQ_INIT_ARGS` （换行分隔的 rocq 参数）进行覆盖，如果需要的话。
- **标准策略模块** （Lia/Lra/Psatz）预加载（禁用：`ROCQ_PRELOAD=0`）。
- **所有工具默认开启**：`open`，`build`（整个文件诊断），`check`（完整证明），`step`，`try`，`auto_close`（投资组合 + 提示合成），`rollback`，`state` —— 带有错误提示和近似建议。使用 `ROCQ_ENABLE_TOOLS=step,state,...` 修剪工具，使用 `ROCQ_HINTS=0`/`ROCQ_SUGGEST=0`/`ROCQ_AUTO2=0` 禁用功能，使用 `ROCQ_EXEMPLARS=1` 选择项目示例检索。
- 完成后，响应带有 **完成的证明脚本** （从实际执行的脚本组装 —— 代理将其插入您的文件中）；还会将一个独立的 `candidate.v` 文件写入 `ROCQ_WORKDIR`/temp。
- `ROCQ_TASK_FILE` （可选）预设启动时一个文件 —— 由基准测试框架使用；交互式使用永远不需要它。
无需任何 MCP 客户端的快速烟雾测试：
```sh
printf '%s\n%s\n%s\n' \
'{"jsonrpc":"2.0","id":1,"method":"initialize","params":{}}' \
'{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"open","arguments":{"file":"/path/to/your/File.v","theorem":"my_admitted_lemma"}}}' \
'{"jsonrpc":"2.0","id":3,"method":"tools/call","params":{"name":"auto_close","arguments":{}}}' \
| rocq-mcp-evolve
```
对于多代理在一个证明上的工作，`rocq-mcp-evolve-daemon` + `rocq-mcp-evolve-shim` 一起安装（参见 docs/DESIGN.md，证明内的并行性）。
*开发/重现实验？* `repro/setup.sh` 从头构建固定的环境，`dune build` 在树中工作；Python `harness/` **仅用于运行基准测试实验**，从未需要使用该工具。
## 测试
`dune runtest` —— 集成级，无模拟；每个测试用例都会启动一个真正的二进制文件，并断言其行为（每个测试用例都会引用它所回归的事件；预算 ≤ ~4 分钟）。
**109 个断言**，涵盖四个套件（A：57 · B：35 · C：10 · D：7）。
架构： [`test/ARCHITECTURE.md`](test/ARCHITECTURE.md)。
- **`test_session.ml`** （A，57）—— 会话服务器核心合约：提交-好-前缀，自动 Qed 握手，try/auto_close 语义，回滚，env-v2 拒绝，错误提示 + 是否意味着什么，完整证明 `check`，项目加载路径，整个文件 `build` 诊断（admit-and-continue），运行时 `open`（包括 Admitted-targeting 和 A36 reach-any-theorem），前缀重放记忆化安全重开，以及示例检索（包括防泄漏）—— 加上失败-atlas 回归（自动 Qed，死工具清除，搜索翻转）。
- **`test_daemon.ml`** （B，35）—— 共享证明的多代理守护进程：两代理分支/合并，不聚焦代理安全，和 **merge-renumbering** 回归（一个审查修复程序，会破坏 >2 目标的合并）。
- **`test_perf.ml`** （C，10）—— 可扩展性/延迟边界（慷慨，CI 稳定）：初始化 < 15 秒，步骤 p50 < 250 毫秒，无死锁，8 个并发客户端下 O（1）-ish 50 句子回滚。
- **`test_gate.py`** （D，7）—— 正确性门槛健全性：合法接受，禁止令牌，前缀篡改，新编译，和 **注释/字符串 desync** 漏洞 `(* "(*" *) Admitted.` （一个测量-审查关键发现）。
## 仓库地图
```
src/mcp_core/ MCP stdio 服务器框架 + 子进程实用程序
src/baseline_server/ 朴素控制：一个 `check` 工具 = 完整的 rocq 编译
src/session_server/ 迭代接口（本自述服务器）
src/psession/ 共享证明守护进程（k 个代理，一个实时证明）+ MCP shim
harness/ 评估运行程序，正确性门控，团队组织者，报告，
分析师，监视器，仪表板，绘图，扫描，项目参数
configs/ 每个实验条件一个 JSON （+ FROZEN.md）
data/manifests/ 分层问题清单（dev60/dev150/hard70/…）
docs/ 报告，设计原理，假设，失败地图，任务
repro/ 固定的包清单 + 一条命令环境重建
test/ dune 驱动的集成套件（A–D 上述）
```
文档： [`docs/REPORT.md`](docs/REPORT.md) ·
[`STATUS.md`](STATUS.md) · [`docs/DESIGN.md`](docs/DESIGN.md) ·
[`docs/FAILURE_ATLAS.md`](docs/FAILURE_ATLAS.md) ·
[`docs/ASSUMPTIONS.md`](docs/ASSUMPTIONS.md) （自主决策日志 A1–A37） ·
[`docs/TASK.md`](docs/TASK.md) （原始简报）。
## 重现实验
```sh
./repro/setup.sh /path/for/new/switch # 开关 → 固定依赖 → 构建 → 自我测试
python3 harness/run_eval.py --config baseline --manifest smoke5 --reps 1
python3 harness/report.py <run_id> [--compare baseline_dev60] # 每个数字都来自这里
python3 harness/dashboard.py --watch # live view: logs/dashboard.html
```
数据集作为此存储库的兄弟节点（`rocq-workbook/`，`miniF2F-rocq/`）；策略端点是身份验证的固定 `claude` CLI。 保留的分割线受到保护——代码拒绝读取 `miniF2F-rocq/test` 除非设置了 `FINAL_UNLOCK` + `ROCQ_FINAL_EVAL=1`；单个解锁（2026-07-03 13:57:42）记录在 `configs/FROZEN.md` 中；重现保留运行需要故意重建 `FINAL_UNLOCK` 哨兵。
## 如何引用
```bibtex
@software{rocqmcpevolve2026,
author = {{LLM4Rocq}},
title = {rocq-mcp-evolve: {AI}-native {MCP} server for {Rocq}},
year = {2026},
url = {https://github.com/LLM4Rocq/rocq-mcp-evolve}
}
```
