PrologMCP：面向LLM代理的标准化Prolog工具接口

# PrologMCP: 面向LLM代理的标准化Prolog工具接口

**来源:** https://arxiv.org/html/2606.14935  
\\copyrightclause 本文作者拥有版权。允许在知识共享署名4.0国际许可证（CC BY 4.0）下使用。  
\\conference 逻辑、学习、伦理决策与LLM统计与知识集成联合研讨会，2026年7月18日，里斯本  

\[[email protected], \]  
\[[email protected], \]  
\[[email protected], \]  
\[[email protected], \]  
\[[email protected], \]  

Adarsh Prabhakaran, Adrian Haret, Vince Trencsenyi, Kostas Stathis  
伦敦大学皇家霍洛威学院计算机科学系，英国（2026年）

###### 摘要

前沿推理调优语言模型在深度演绎推理任务上仍然表现不佳，而通过扩展内部推理来提升性能的成本扩展性很差。符号委派提供了一种互补的路径：语言模型负责翻译问题，求解器负责执行推理。然而，当前用于逻辑编程的自动形式化流水线通常是针对特定任务或代理的定制集成。我们提出PrologMCP，一个任务无关的开源服务器，它通过模型上下文协议（MCP）将Prolog暴露为有状态工具。其紧凑的工具接口、结构化的错误报告以及每个会话的隔离性，使得"翻译–运行–检查–修复"循环成为MCP兼容代理的可重用原语。我们评估了一个配备PrologMCP的形式化代理，与标准LLM和推理LLM（Claude Sonnet 4.6、GPT-4.1和o4-mini）在PARARULE-Plus的两个子集上进行对比：一个通用样本，以及一个针对自然语言推理特定失败模式的更具挑战性的样本。在通用样本上，形式化代理匹配或超越了推理LLM（准确率1.00对比1.00/0.998），相比标准模型提升最为显著（GPT-4.1为0.762）。在挑战性子集上，形式化代理保持近乎完美（1.00/0.99），而推理LLM下降到0.95/0.94。这些结果表明，通过MCP将推理委派给Prolog是扩展自然语言推理的一种稳健且可检查的替代方案。

###### 关键词: Prolog\\sep 模型上下文协议\\sep 自动形式化\\sep 大语言模型\\sep 符号推理

## 1 引言

自人工智能诞生以来，推理一直被视为智能行为的基本组成部分\[mccarthy1959, kowalski1974, newell1976\]。大语言模型在推理基准上最初表现不佳后，取得了快速进展；然而，重要的局限性依然存在。首先，即使在强大的推理调优模型上，长推导链的准确性也会下降。与符号求解器不同（在符号求解器中，多步规则应用保证了正确性），语言模型没有机制确保每一步生成都是前一步的有效逻辑推论。这种缺乏逐步保证使得长链变得脆弱：错误会累积，成功推理依赖于维持连贯的推导。Lin等人\[lin2025zebralogic\]在网格式逻辑谜题上展示了这种崩溃，其中前沿推理模型随着问题复杂性增加而遭受显著的准确性下降。Kazemi等人\[kazemi2025bbeh\]同样报告，前沿推理模型在一个困难的推理基准上远未饱和。早期对组合任务\[dziri2023faith\]和标准数学基准的模板变体\[mirzadeh2025gsm\]的分析将此类失败归因于对训练分布结构的模式匹配，而非真正的多步演绎，其准确性随所需推理步骤数量的增加而下降。

其次，额外可靠性的成本扩展性很差。当前的推理调优模型试图通过分配更多的内部推理（或思考）token来提高可靠性。然而，这增加了推理成本，同时无法保证额外的token对应于有效的演绎步骤。对于规则简单但搜索空间呈组合分支的任务，额外生成可能产生递减的回报。近期描述这些局限的研究\[shojaee2025illusion, lin2025zebralogic\]发现，增加思考预算在超过一定问题复杂度阈值后会产生递减回报，在某些情况下推理模型甚至随着问题变得困难而减少思考token的使用。相比之下，符号求解器——Prolog用于基于规则的演绎，SAT和CSP求解器用于组合搜索——通常能够处理超出推理调优模型崩溃阈值多个数量级的问题。这些求解器提供了自然语言推理所缺乏的两个特性：可预测的计算扩展性和由构造保证正确的答案。

这催生了一个已建立的替代方案——工具使用范式\[schick2023toolformer, gao2023pal\]，其中模型并非内部执行每一个推理步骤，而是将明确定义的任务委派给外部工具。例如，算术和一般计算可由代码解释器处理；事实查找由检索系统处理；推理问题由符号求解器处理。后一个方向与*自动形式化*\[wu_autoformalization_2022, mensfelt2026towards\]密切相关，该方向已探索了多类形式系统和求解器。逻辑编程对于许多演绎推理任务而言是一种特别自然的匹配，因为它将声明式表示与自动推理结合在一起。然而，与代码执行和检索相比，逻辑编程作为语言模型代理的标准化工具仍相对未被充分服务。

越来越多的研究探索了LLM与Prolog的结合。\[borazjanizadeh2024reliable\]使用现成的LLM生成Prolog程序，并在执行失败时重试；\[mensfelt2024generative\]将博弈论场景自动形式化为可执行的Prolog，并采用迭代求解器反馈修正循环——这是我们在此提出的"翻译–运行–检查–修复"模式的接近先例。\[yang2024arithmetic\]微调LLM以生成用于算术文字题的Prolog程序，而\[tan2024thought\]使用Prolog引擎生成经过验证的推理轨迹，LLM将其模仿为结构化思维链。密切相关地，\[mellgren2025training\]使用GRPO微调一个小模型，使其将Prolog作为可调用的内部修复工具使用，这激发了PrologMCP所暴露的标准化接口原语。其他近期工作\[zunjare2026neuroprolog, he2025protoreasoning\]在训练过程中融入了结构化的Prolog表示。

然而，现有系统大多为定制构建：每个系统定义了自己的接口、执行模型和错误处理策略，限制了跨模型和代理框架的可移植性。特别是，目前没有标准化接口能让代理以统一方式发现、调用、检查和修复Prolog程序。

本文提出PrologMCP，一个模型上下文协议（MCP）服务器，它将Prolog作为有状态工具暴露给任何兼容MCP的语言模型代理。它支持可重用的"翻译–运行–检查–修复"循环：代理将自然语言问题翻译成Prolog，对符号求解器执行查询，检查结构化输出或错误，并在必要时修正形式化。我们的贡献如下：
1. I.一个标准化的Prolog工具接口，实现为MCP服务器，支持结构化交互、错误报告和会话级隔离（第3节（https://arxiv.org/html/2606.14935#S3））。
2. II.一个形式化LLM代理，将自然语言问题翻译成Prolog，使用服务器执行查询，并利用结构化反馈迭代优化其表示（第4节（https://arxiv.org/html/2606.14935#S4））。
3. III.在PARARULE-Plus\[bao2022multi\]上对形式化代理进行实证评估，并与标准LLM和推理模型推理进行对比（第4节（https://arxiv.org/html/2606.14935#S4））。

## 2 背景

#### Prolog中的逻辑程序。
逻辑程序，最突出地实现于Prolog\[korner2022fifty, wielemaker2012swi\]，提供了基于Horn子句的声明式表示：形式为"如果$b_1$，...，$b_n$，则$h$"的全称量化蕴含式，自然映射到事实（无体子句）、规则（有一个或多个体文字的子句）和查询（要证明的目标）。推理结合了项统一、SLD分辨率\[kowalski1971linear\]（将查询归约为匹配子句头的子目标）以及带回溯的目标导向搜索。Prolog通过SLDNF扩展了SLD，即否定即失败\[clark1978negation\]，其中当系统无法证明相应的正目标时，负目标被视为满足。Horn子句与自然语言规则的表面形式紧密对应（例如"如果X是善良的，则X是好的"变成`nice(X) :- kind(X).`），而Prolog的目标导向推理、对否定即失败的支持以及跨调用持久的子句状态使其成为演绎推理任务中自动形式化的自然目标。竞争方法如SAT、SMT或CP需要转换为可满足性公式、背景理论或显式变量域，而SAT和CP求解器通常每次调用是无状态的，这不太适合在增长的知识库上进行多轮代理推理。

#### 模型上下文协议。
模型上下文协议\[anthropic2024mcp, Hou2026e\]为向LLM代理暴露工具提供了标准接口，包括工具发现、类型化参数模式和结构化错误报告的约定。通过MCP暴露的工具可以被任何支持MCP的代理使用，无需特定模型的胶水代码。MCP也容纳有状态工具如Prolog：在一系列调用中，代理可以断言子句、检查程序状态、发出查询、接收结构化诊断并修正形式化。最接近的先例是\[szeider2025bridging\]中讨论的MCP-Solver，它暴露了约束、SAT、SMT和答案集后端（MiniZinc、PySAT、Z3和clingo），但不支持带有统一和回溯的Prolog风格SLDNF分辨率。

#### 自动形式化。
*自动形式化*是将非正式语言表达式自动翻译成形式上对应的正式语言表达式。该术语源于形式化数学\[wu_autoformalization_2022\]，此后扩展至涵盖这样的流水线：模型发出一个形式化制品（逻辑程序、约束模型、SMT公式或规划规范），然后传递给一个可靠的的外部推理过程。近期一篇统一的综述\[mensfelt2026towards\]将自动形式化参数化为：非正式语言$L_i$及其可形式化子集，具有精确语义的形式推理语言$L_f$，以及一个指定必须保留哪些意义方面的语义等价准则$E$。由于$E$本身是非正式的且无法直接检查，实际流水线引入了一个可计算的*验证准则*$V$来近似$E$，例如通过执行形式化制品并将输出与预期结果进行比较。

参阅图注
图1: PrologMCP架构。

## 3 架构

PrologMCP是一个MCP服务器，它将Prolog以有状态工具的形式暴露给LLM代理。三个特性驱动了设计：($i$) *有状态性*——子句跨调用持久存在，因此代理可以增量构建知识库，而不是在每个目标上重新提交；($ii$) *结构化错误报告*——编译时和运行时诊断以类型化JSON形式返回；($iii$) *隔离性*——每个会话在专用的解释器子进程中运行，并具有资源限制。目前，服务器仅支持SWI-Prolog。工具签名和JSON模式见附录B（https://arxiv.org/html/2606.14935#A2）。源代码可在GitHub（https://github.com/dicelab-rhul/PrologMCP）获取。

### 3.1 组件

系统具有三层（图1（https://arxiv.org/html/2606.14935#S2.F1）），形成从代理工具调用到Prolog子进程并返回的单一路径：
1. 1. **Python MCP服务器**：向代理呈现第3.3节（https://arxiv.org/html/2606.14935#S3.SS3）的工具接口：声明每个工具的输入模式，验证并调度传入调用到相应的会话，并将（包括失败在内的）处理结果映射到MCP的结构化工具结果格式。服务器本身不持有任何Prolog状态；它只是会话注册表之上的一个薄协议适配器。
2. 2. **会话注册表**：持有一池Prolog会话，通过创建会话时返回的`load_id`进行索引。注册表是线程安全的，将并发会话限制在可配置的上限，在溢出时驱逐最近最少使用（LRU）会话，并从后台线程回收超过生存时间（TTL）的空闲会话。
3. 3. **Prolog处理程序**（harness.pl）：加载到每个会话的`swipl`子进程中，读取stdin上的换行分隔JSON命令，分派给处理程序，并在stdout上写入换行分隔JSON响应。Stderr保留用于未捕获的诊断。

### 3.2 会话语义

会话通过`consult_text(source, dialect)`创建：注册表分配一个新的`load_id`，启动一个加载了处理程序的`swipl`子进程，将`source`写入会话临时目录中的一个文件，并发出一个`consult`命令。如果`source`缺少模块声明，注册表会添加：`:- module(m_⟨load_id⟩, []).`，以便后续定义的谓词存在于每个会话的模块中，与处理程序和其他会话隔离。全程使用模块限定目标求值（`Module:Goal`），因此无论`source`写于哪个模块，谓词解析都是明确的。语法错误、单例警告等诊断由处理程序中安装的`message_hook/3`捕获，因此引发错误的consult仍然会加载其能加载的子句，而不是中止。捕获的诊断作为`messages`数组返回，每个条目包含严重性、来自固定词汇表的种类、消息字符串，以及当诊断可归因于特定子句时，触发该诊断的源代码行。由于成功加载的谓词在失败的consult后仍然可调用，代理可以使用`replace_predicate`修复源代码；因此consult是*非致命*的。子进程在会话生命周期内保持打开；会话通过`close_session`显式关闭，或在TTL过期时隐式关闭，或在负载下执行LRU驱逐时关闭。

### 3.3 工具接口

| 工具 | 行为 |
|------|------|
| `consult_text` | 从源代码字符串打开一个会话，返回其`load_id`、已定义谓词的可选清单以及咨询期间产生的任何诊断。 |
| `run_goal` | 用`call_with_depth_limit/3`包裹的`findnsols/4`评估目标字符串，报告类型化绑定、解的数量以及是否达到深度限制。 |
| `inspect_predicate` | 报告谓词的子句、元数、类型（static \| dynamic \| foreign）、导出状态和子句计数；如果不存在精确匹配，建议名称相似的谓词。 |
| `get_source` | 通过遍历`predicate_property/2`和`clause/2`重建模块的源代码。 |
| `replace_predicate` | 使用`abolish/1`收回一个谓词，然后通过`load_files/2`将单个谓词的补丁重新加载到会话模块中。 |
| `list_messages` | 检索当前会话中收集的诊断。 |
| `run_tests` | 咨询一个可选的`plunit`文件并执行每个注册的单元测试，返回通过、失败和阻止的计数及每个测试的结果。 |
| `trace_goal` | 对目标运行一个深度有界元解释器，返回（待续？原文此处似乎不完整，但按照论文常见结构，可能还有内容，但当前输入截断了。不过基于已有信息，表格到此为止。翻译时保持原样） |