这篇是对论文 PrologMCP: A Standardized Prolog Tool Interface for LLM Agents 的学习笔记。
我读完后的第一感觉是：这篇论文不是在说“Prolog 又回来了”，而是在提醒我们一个很朴素的系统设计原则：
不要强迫大模型在所有事情上都扮演同一个角色。它擅长理解语言和改写表达，但不一定适合承担严格演绎推理的最后一步。
PrologMCP 做的事，就是把 Prolog 包成一个标准 MCP 工具，让 LLM Agent 可以把自然语言规则翻译成逻辑程序，再把真正的推理交给 Prolog 执行。
这听起来不复杂，但背后有一个很重要的方向：LLM 不必独自完成推理。它可以作为翻译器、编排器和修复器，把确定性任务交给更合适的系统。
1. 问题：LLM 会推理，但不保证会稳定演绎
现在的大模型确实能做很多推理题。给它事实、规则、问题，它可以写出很像样的思考过程，最后回答 true 或 false。
但演绎推理有一个麻烦点：它不是“差不多对”就行。
如果规则是：
如果 A 成立，则 B 成立
如果 B 成立，则 C 成立
A 成立
问 C 是否成立这个例子很简单，LLM 通常没问题。但当规则变多、链条变深、否定关系出现、多个谓词互相依赖时，语言模型的自然语言推理就容易变得不稳定。它可能漏掉一条规则，也可能在否定上犯错，还可能生成一个看似连贯但实际不严格的解释。
靠 reasoning model 增加思考 token 可以缓解，但不能从根本上保证正确。更长的推理轨迹也意味着更高延迟、更高成本，以及更多中间步骤出错的机会。
这正是 Prolog 这类符号系统擅长的地方。只要事实和规则形式化正确，求解器可以用确定性的机制去做查询。它不会因为今天语气不一样就换一个答案，也不会因为上下文太长就随手跳过某条规则。
所以 PrologMCP 的核心问题不是“LLM 和 Prolog 谁更聪明”，而是：
LLM 应该负责哪一段？
符号求解器应该负责哪一段？
两者之间的接口应该怎么标准化？2. 核心分工：模型做形式化，Prolog 做推理
PrologMCP 采用的是一个很清楚的 Formalizer 模式。
用户给出自然语言题目，里面包含事实、规则和问题。LLM 不直接回答，而是先把这些内容翻译成 Prolog 程序和查询。随后 Agent 把程序交给 PrologMCP，调用 Prolog 执行查询，再根据执行结果生成最终回答。
可以简化成这样：
自然语言题目
↓
LLM 翻译成 Prolog facts/rules/query
↓
PrologMCP 加载程序并运行查询
↓
返回 true/false、绑定变量、错误信息或 trace
↓
LLM 解释结果并回答用户这里最关键的变化，是 LLM 不再负责“在脑子里模拟证明过程”。它只需要把题目忠实翻译成形式语言。真正的证明、回溯、否定处理、查询求值由 Prolog 完成。
这个分工很有工程意义。
让 LLM 做翻译，是因为自然语言到形式语言本来就带有语义理解和表达选择，需要模型的语言能力。让 Prolog 做推理，是因为形式系统在确定性、可复现、可检查方面更强。
换句话说，PrologMCP 不是否定 LLM，而是把 LLM 放在更适合的位置上。
3. 为什么一定要做成 MCP
过去也有很多“LLM 调 Prolog”的实验。为什么这篇论文还要强调 PrologMCP？
因为真正要让 Agent 使用外部求解器，不能只靠一次性脚本。它需要标准化接口、会话状态、错误反馈、隔离机制和可检查的工具调用过程。
论文里的 PrologMCP 把 Prolog 暴露成一个 stateful MCP server。它提供的不只是“运行一段 Prolog 代码”这么简单，而是一组适合 Agent 循环使用的工具：
consult_text：把 Prolog 代码加载进当前会话。run_goal：执行查询目标。inspect_predicate：检查某个谓词的定义和状态。get_source：取回当前会话里的源代码。replace_predicate：替换某个谓词定义。list_messages：查看加载或执行过程中的诊断信息。run_tests：运行测试。trace_goal：查看目标执行轨迹。close_session：关闭会话。
这套接口解决了一个很实际的问题：LLM 第一次生成的 Prolog 程序未必完全正确。
如果程序有语法错误、谓词未定义、变量写错、递归不收敛，PrologMCP 会返回结构化错误信息。模型可以根据这些信息修复程序，而不是在一段混乱的 stderr 文本里猜。
更重要的是，PrologMCP 设计了按会话隔离的执行语义。每个任务有自己的 session，程序状态不会随便串到另一个任务里。这对 Agent 系统非常关键，因为外部工具一旦有状态，污染和泄漏就会很难排查。
所以 MCP 在这里的意义，不只是“让 LLM 能调用 Prolog”。它把 Prolog 变成了一个可被 Agent 稳定使用、可调试、可修复、可隔离的标准工具。
4. 实验结果说明了什么
论文在 PARARULE-Plus 上评测。这个基准包含自然语言形式的规则推理题，要求模型判断结论是否由事实和规则推出。
主实验里，Formalizer 路线表现非常强。论文报告，在 400 个样本上，Claude Sonnet 4.6 的 Standard baseline 已经很高，Reasoning 和 Formalizer 都达到 1.000；OpenAI 侧 GPT-4.1 Standard 只有 0.762，o4-mini Reasoning 达到 0.998，而 GPT-4.1 Formalizer 达到 1.000。
更有意思的是 targeted subset。论文专门构造了一批对 SLDNF 风格推理更容易造成干扰的样本。这个子集里，纯 reasoning 的表现会掉：Claude reasoning 到 0.95，o4-mini 到 0.94；Formalizer 路线基本保持在 1.00 或 0.99。
这说明一个很重要的点：在规则推理这类任务上，长思考不一定是最稳的路线。
如果任务本质上可以被形式化，那么与其让模型用自然语言一步一步推，不如让模型把问题翻译成可执行逻辑，然后让求解器算。模型的 token 用在翻译和修复上，而不是用在模拟求解器。
论文还报告了运行时间和 token 成本上的优势。在 targeted subset 中，Formalizer 比 reasoning 条件更快，OpenAI 侧 Formalizer 的 token 使用也明显低于 reasoning model。这很符合直觉：一旦形式化成功，符号求解器做推理通常比大模型长链思考更经济。
5. 这篇论文真正有启发的地方
我觉得 PrologMCP 最有价值的不是“Prolog 能赢某个 benchmark”，而是它清楚展示了一种 Agent 系统分工：
LLM：理解自然语言、生成形式表示、根据错误反馈修复表示
工具：执行确定性计算、返回结构化结果、提供可检查 trace
Agent：在两者之间编排、重试、验证、解释这和很多人默认的“让大模型自己想到底”不一样。
大模型很强，但它不是数据库，不是 SAT solver，不是类型检查器，不是定理证明器，也不是操作系统。很多系统问题如果强行塞进模型上下文里，模型确实能给答案，但答案的可靠性和成本未必好。
PrologMCP 的路线更像传统工程：能交给专门系统做的，就交给专门系统做。模型负责把人类语言和工具语言连接起来。
这个思路可以推广到很多方向：
- 规则推理交给 Prolog。
- 约束满足交给 SAT/SMT solver。
- 数值计算交给 Python、R 或数据库。
- 类型和接口一致性交给编译器。
- 权限和数据流策略交给 policy engine。
LLM 不需要替代这些系统。更好的形态是让它学会什么时候调用它们、如何表达问题、如何理解错误、如何把结果解释回人类语言。
6. 但 PrologMCP 没有解决所有问题
这篇论文也有明显边界。
第一，Formalizer 的前提是自然语言能被正确翻译成 Prolog。求解器只能保证“在给定形式化程序下”推理正确。如果模型把原题翻译错了，Prolog 会非常稳定地给出一个错误问题的正确答案。
所以系统真正的风险从“推理过程错”转移到了“形式化是否忠实”。这不是小问题。现实任务里的语言经常模糊、省略、带常识和上下文，远比 benchmark 里的规则题复杂。
第二，论文主要评测的是 PARARULE-Plus 这类合成或半合成的规则推理题。它能说明 PrologMCP 在这一类任务上有效，但还不能直接推出它在法律条文、企业规则、合规审计、业务流程判断里也同样稳定。
第三，安全隔离还不够完整。论文自己也提到，当前的 lexical sandbox 不是严格安全边界。只要让模型生成可执行逻辑程序，就必须认真处理资源限制、超时、文件访问、模块加载、递归爆炸和拒绝服务风险。
第四，它目前围绕 SWI-Prolog 构建。Prolog 很适合一部分逻辑推理，但不是所有形式化任务的最佳工具。不同问题可能需要 Datalog、ASP、SMT、SAT、Lean、Coq 或数据库规则引擎。
这些局限不削弱论文的方向，反而说明下一步应该怎么走：不是只做一个 Prolog wrapper，而是做一层 solver routing，让 Agent 根据任务类型选择合适的形式系统。
7. 我自己的 takeaway
PrologMCP 给我的最大提醒是：Agent 的能力边界，不应该由 LLM 单独定义。
如果一个任务需要严格演绎，就不要只问“哪个模型 reasoning 更强”。还应该问：
- 能不能把任务形式化？
- 有没有成熟求解器能做得更稳定？
- 模型是否只需要负责翻译和修复？
- 工具能否返回结构化错误，帮助模型迭代？
- 最终答案能否附带可检查 trace？
当这些问题的答案是肯定的，外部符号系统往往比单纯堆 reasoning token 更像工程解。
这也是我喜欢这篇论文的原因。它没有把 LLM 包装成全能智能，而是把它放进一个更合理的软件系统里。模型理解语言，Prolog 负责推理，MCP 负责把两者接成可交互、可调试、可隔离的工具协议。
未来的 Agent 系统很可能不是“一个大模型解决所有事”，而是一组能力清晰的系统协作：模型做语义接口，工具做确定性执行，运行时做权限和审计，最终由 Agent 把这些拼成用户能理解的结果。
PrologMCP 这篇论文正好给了一个很干净的样例：当问题适合形式化时，不要让大模型硬想。让它把问题说清楚，然后交给真正擅长推理的系统。