如何验证 Open Ontologies 的推导证书？

12 分钟阅读 · 2026年11月3日
最近审核 2026年11月3日

只增加一个三元组，我们的 Open Ontologies 测试就多出三项推论，结构风险却仍显示为 low。随后的一次检索检查正常退出，报告明确标注：结论尚未经过独立核验。

验证 Open Ontologies 的推导证书，需要保留原始断言和规则范围，用独立检查器读取断言文件与推导文件，再结合结构化结果和进程退出码判断是否通过。只批准已通过检查的具体图谱与结论。未经核验的结果和检查器故障都应保持待审状态。

Open Ontologies 是一个开源引擎，可规划本体变更，并为受支持的推理生成证书。项目所说的 Terraform 类比，指的是规划、审查与应用变更的流程。如果你还在判断智能体是否需要知识图谱，先看我们的智能体图谱架构选择指南。

测试与资料核查日期：2026年11月3日。我们使用了2026年10月23日发布的 v2.1.0 Linux 文件，并核对了校验和。源码链接固定到较晚的11月2日提交 c7fd75f。原始证书的检查器在我们的环境中发生运行时错误，独立验证是否通过仍未获确认。这套样例测试功能行为，不提供性能基准。

Open Ontologies 的证明能确认什么？

检查器接受一份 Open Ontologies 推导证书，意味着其中的结论可以在受支持的形式语义下，从所提供的断言推出。文档是否获批、准确或有效，仍需各自的证据。即使前提有误，检查器也可能确认其后续推导有效，却无法发现前提与现实不符。

项目的验证架构说明将两个问题分开处理：结论能否成立，以及引擎究竟使用了哪张图谱。

不同审核问题需要不同证据
问题	应检查的证据	适用边界
推导是否成立？	独立检查器对断言文件和推导文件的检查结果	结论以这些断言和受支持的规则为条件
这是本次要使用的图谱吗？	图谱版本、断言摘要与选定的图谱范围	有效证明也可能针对错误的快照
断言是否可靠？	来源证据、抽取审核与责任人	形式推导不会核实现实世界
智能体可以使用结果吗？	应用策略与访问权限检查	类名本身不授予任何权限

我们的 LLM-as-a-Verifier 分析介绍如何用模型学习到的分数对输出排序。Open Ontologies 检查的是一条明确推导是否符合规则。

如何检查 Open Ontologies 的推导证书？

先生成证书，再运行 oo-cert，让它读取 asserted.tsv 和 derivations.tsv。保留标准输出、标准错误和退出码。只有检查器正常完成，并返回文档规定的成功结果，才能确认通过。

证书指南说明，独立的 Lean 检查器会重新检查记录中的推导步骤。文档规定的成功结果包括退出码 0、ok: true 和定理名 OOCert.certificate_sound。若某一步被拒绝，报告应指出对应的规则、结论和前提。

下载我们的 Open Ontologies 证书测试样例与运行记录，解压后进入该目录。以下命令假设经过校验的引擎和检查器已位于 PATH 中。下载包提供样例源码与证据采集脚本，可执行文件需自行准备。

open-ontologies --no-connect --data-dir ./review-store batch - <<'OO'
load proposed.ttl
reason --profile rdfs --certificate ./certificate
OO

oo-cert ./certificate/asserted.tsv ./certificate/derivations.tsv

批处理让加载和推理发生在同一进程中。提议后的图谱有四条断言，rdfs 推理生成了三条推导记录。随后，我们只修改一个结论，声称 note42 属于 ApprovedForProduction，保留其原有前提。

原创样例中独立检查器的实际输出
输入	实际结果	审核决定
未经修改的生成证书	退出码 1，标准输出为空，标准错误为 `failed to locate application`	暂缓。检查器未输出独立验证成功的结果
修改结论，保留原有前提	退出码 1，JSON 包含 `ok: false`、`first_rejected: 2` 和规则 `rdfs9`	拒绝被修改的推导。具体规则检查未通过

两个进程的退出码都是 1，但只有第二次输出了结构化的规则拒绝结果。索引从零开始，first_rejected: 2 指的是第三条推导记录。第一次运行在定位程序时失败。这两种故障不同；伪造样例被拒绝，不能替代原始证书成功通过验证。

计划显示低风险，为什么还要审查语义变化？

Open Ontologies 分别报告结构风险和语义后果。即使变更没有增加命名类，已有规则也可能推出新的分类。决定是否接受变更前，要查看 conservativity 部分及其影响到的结论。

我们的初始图谱包含以下三条断言。其中声明 Retrievable 是一个类，是为了让这个名称已经存在于原有词汇集合中：

@prefix ex: <https://example.com/knowledge/> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .

ex:note42 a ex:ProjectNote .
ex:ProjectNote rdfs:subClassOf ex:Document .
ex:Retrievable a rdfs:Class .

提议的变更新增一个三元组：

ex:Document rdfs:subClassOf ex:Retrievable .

保守性检查文档说明，这里比较的是指定有限规则表下的结果，不能据此推断所有逻辑体系中的保守性。我们的 owl-rl 计划报告一次插入，结构影响范围为零个三元组，risk_score: low，并给出 not_conservative_under_rule_table。

本次计划新增的三项推论
三元组简写	出现原因
Document 是 Retrievable 的子类	新增的断言本身
ProjectNote 是 Retrievable 的子类	沿子类关系链得到的新推导
note42 的类型是 Retrievable	利用该分类得到的新推导

这里的三项新增推论，包含一条断言和两条新推导。推理证书中则有三条推导，因为它还记录了 note42 type Document，这条结论在初始图谱中就已成立。

项目的公开演示报告在 0.04 秒内发现 901 项新推论，另一次证书演示核验了 259 条推导，并拒绝一个伪造结果。我们没有复现这些数量或耗时。本次小样例也表明，推论总数可能包含新增断言本身。

我们的批处理进程还出现了另一种差异：进程退出码为 0，嵌套的保守性报告却包含 exit_code: 1。这项语义变化可能正是预期效果。审批任务需要读取报告并记录决定，只检查进程退出状态会漏掉这项发现。

缩小 RAG 上下文后，还能保留同一个结论吗？

Open Ontologies 可以检查选定的图谱切片，是否仍能在指定规则配置下支持正向的具体事实三元组（不含变量）。待检查的主张由你提供。它不会自动抽取并核验生成答案中的每句话，保留一定比例的邻近三元组也无法说明所需前提仍然存在。

本例的目标是 note42 type Retrievable。完整切片保留推导所需的三个三元组，省略独立的类声明。截断切片则删除 ProjectNote subClassOf Document。两者都是提议后图谱的子集。

切片推论保留检查指南分别命名了已核验、直接存在于断言中和未经核验的结果：

对一个明确目标执行 RAG 检查的实际结果
运行条件	逐目标结果	进程退出码	对审批的含义
完整切片，未配置检查器	`preserved_unchecked`	0	引擎能够推出目标，但缺少独立验证
截断切片，未配置检查器	`lost_under_profile_unchecked`	1	所选规则配置已无法从切片推出目标
完整切片，强制要求检查器	`certificate_rejected`、`STOP_THE_LINE`	2	暂缓，并查看检查器的原始错误

第三行的报告包含同一个运行时错误：failed to locate application。外层工具标记为拒绝，不能说明某条规则已被证伪。在这个环境中，我们没有获得 preserved_checked。

切片丢失推论的判定也有边界：它是引擎在受支持规则范围内给出的否定结果，不能证明所有本体逻辑下都无法推出该结论。如果工作流要求独立证明，我们会暂缓采用未经核验的正向结果，补回丢失的前提，并排查检查器故障，再允许智能体依赖该主张。

推论保留检查也不负责授权。用户是否有权检索这些事实，应参考我们的 RAG 访问权限指南。

审批记录应该包含哪些内容？

Open Ontologies 的审批记录应写明图谱版本、所选断言、规则配置、语义变化和检查器的完整结果。如果涉及检索切片，还要记录逐目标判定。这是我们建议的应用策略，不代表引擎会自动批准业务变更。

智能体使用变更后的图谱前，建议保留的证据
记录项	验收问题
引擎与检查器身份	运行的是哪些发布文件或构建产物？哈希是否与审查过的版本一致？
图谱版本与断言字节内容	证书是否对应本次获批的准确输入？
选定范围与规则配置	使用了哪些图谱和规则？是否拒绝了相关语法结构或检查目标？
语义变更报告	审核者是否确认了报告中的推论，并处理无法判定的结果，而不是仅凭结构风险标签放行？
检查器的标准输出、标准错误与退出码	指定检查器是否输出了成功验证的结果？
切片、明确目标与逐项判定	每条必需的派生主张是否都有应用要求的证据？

可信计算基文档解释，检查器读取的是证书文件，并不知道应用本来打算使用什么状态。它不检查 scope.tsv，调用方必须审核图谱选择。断言摘要绑定字节内容，不能说明这些内容在现实中是否真实、是否仍然有效，或是否有权使用。

本次实验的审批结论仍是暂缓，等待独立验证。伪造证书被拒绝提供了有用证据，却不能替代对实际要使用的原始证书进行成功检查。接入智能体前，先在部署主机上重复执行应当通过和应当拒绝的两组对照测试。

如何把 Open Ontologies 接入 Claude Code？

将 Open Ontologies 注册为本地 stdio MCP 服务，并指定可执行文件和存储目录的绝对路径。项目默认使用内存存储，重启进程后不会保留已加载的图谱，请明确选择是否持久化。MCP 连接正常，也不能说明独立证明检查器已经安装。

固定提交中的存储与嵌入配置定义了默认内存模式和持久化模式。依据当前 Claude Code MCP 文档，可用以下命令注册本地服务：

claude mcp add \
  --env OPEN_ONTOLOGIES_STORAGE_MODE=persistent \
  --transport stdio open-ontologies -- \
  /absolute/path/open-ontologies \
  --data-dir /absolute/path/oo-store serve

替换两个绝对路径，单独配置并验证检查器，再通过 /mcp 查看连接状态。我们核对了文档中的命令结构，没有运行真实的 Claude Code 会话，也没有逐一测试所有 MCP 客户端。--data-dir 是命令行参数，不是环境变量。

安排部署时间时，要包含两个可执行文件的准备工作，以及在部署主机上完成一次成功的证明检查。本次测试无法支持“一分钟完成已验证配置”的承诺。

什么情况下值得试用 Open Ontologies？

当智能体依赖明确、可审查的断言与规则，且推导结果会影响后续行为时，我们会考虑评估 Open Ontologies。先选一条有实际影响的主张、一次本体变更和一条刻意破坏的推导。确认部署环境中的独立检查器能接受原始证书，并按预期拒绝错误推导后，再扩大范围。

如果你需要把这层推理能力接入应用，可以参考我们的 AI 产品与智能体开发服务。先确定待核验的主张和审批条件，再扩展图谱。

Open Ontologies 证明核验常见问题

Open Ontologies 是 Terraform Provider 吗？

项目借用 Terraform 来描述规划、审查、应用和回滚本体变更的流程，这个类比并不表示它兼容 Terraform Provider 或 HCL。应把 Open Ontologies 作为独立的推理与变更管理工具评估。设计集成方案前，先核对实际命令与证据格式，避免把类比当成接口兼容承诺。

Open Ontologies 能消除所有智能体幻觉吗？

不能。推导检查器覆盖的是：在受支持规则下，从所提供断言推出的指定形式化结论。智能体仍可能抽取错误断言、遗漏必需的检查目标、误述结果，或提出无关主张。应用需要把已核验的三元组与对外发布的陈述对应起来，并保留支撑断言的来源证据。

同一种推导证书也能核验 OWL DL 推理吗？

文档中的 reason --certificate 路径支持 rdfs、owl-rl 和 owl-rl-ext；owl-dl 会拒绝这个参数。项目还有其他验证机制，需要分别评估其适用范围。某个受支持规则片段内的检查通过，不能据此声称所有 OWL 特性或引擎的每一种回答都已获得证明。

证明能说明自定义 Horn 规则本身正确吗？

自定义规则的 Horn 证书，证明的是结论相对于所提供规则与断言成立；规则本身仍是前提假设。应完整保留 entailed_under_supplied_rules 这类判定，并审查规则表及其摘要。若把结果缩写成“已证明”，就会隐藏审核者必须看到的假设。

MCP 在本地运行，是否意味着所有数据都留在设备上？

本地推理无法单独保证整个 AI 工作流都在本地。工具结果会返回 MCP 客户端，而客户端使用的模型可能运行在远端。固定提交中的配置还支持兼容 OpenAI 的嵌入 API。项目的快速入门指南记录了嵌入初始化中的模型下载步骤。判断数据是否全程留在本地前，应检查构建版本、提供方与客户端的数据流向。

derivations.tsv 会列出所有可能的论证依据吗？

不会。证书指南说明，每个新增推导三元组记录一条推导步骤，采用最先找到的推导路径。同一结论可能还有其他有效论证，文件并不会穷举这些路径。若要回答完整论证或来源追溯问题，应独立评估项目对应机制的保证，不能由某份证书是否通过检查来推断。