--- title: "如何验证 Open Ontologies 的推导证书？" canonical: https://wavect.io/zh/blog/open-ontologies-proof-verification/ language: zh description: "如何验证 Open Ontologies 的推导证书？用可复现图谱测试区分伪造证明被拒与检查器故障，核对语义变更和 RAG 切片结论，再确定智能体使用结果前的审批条件。" image: "https://wavect.io/img/blog/headers/header_open-ontologies-proof-verification.png" author: ["Kevin Riedl"] published: "2026-11-03" updated: "2026-11-03" reviewed: "2026-11-03" --- # 如何验证 Open Ontologies 的推导证书？ [**返回**](/zh/blog/overview/) [![Kevin Riedl](/img/team/kevin.webp)](/zh/team/kevin-riedl/) [Kevin Riedl](/zh/team/kevin-riedl/) https://linkedin.com/in/wsdt 12 分钟 阅读 · 2026年11月3日 最近审核 2026年11月3日 [**下一篇**](/zh/blog/graph-engineering-ai-agents/) 要点速览 验证 Open Ontologies 推导证书时，要核对断言、规则范围和独立检查器的完整输出。我们的单行变更产生新推论，伪造结论被拒绝；原始证书却因运行时错误未能确认通过。RAG 切片返回成功也可能仍未核验。独立验证完成前，应保留待审状态。 只增加一个三元组，我们的 Open Ontologies 测试就多出三项推论，结构风险却仍显示为 `low`。随后的一次检索检查正常退出，报告明确标注：结论尚未经过独立核验。 **验证 Open Ontologies 的推导证书，需要保留原始断言和规则范围，用独立检查器读取断言文件与推导文件，再结合结构化结果和进程退出码判断是否通过。**只批准已通过检查的具体图谱与结论。未经核验的结果和检查器故障都应保持待审状态。 [Open Ontologies](https://github.com/fabio-rovai/open-ontologies/blob/c7fd75f9491253c56e4d4f408ceac179de343e48/README.md) 是一个开源引擎，可规划本体变更，并为受支持的推理生成证书。项目所说的 Terraform 类比，指的是规划、审查与应用变更的流程。如果你还在判断智能体是否需要知识图谱，先看我们的 [智能体图谱架构选择指南](/zh/blog/graph-engineering-ai-agents/) 。 **测试与资料核查日期：2026年11月3日。**我们使用了2026年10月23日发布的 [v2.1.0](https://github.com/fabio-rovai/open-ontologies/releases/tag/v2.1.0) Linux 文件，并核对了校验和。源码链接固定到较晚的11月2日提交 `c7fd75f`。原始证书的检查器在我们的环境中发生运行时错误，独立验证是否通过仍**未获确认**。这套样例测试功能行为，不提供性能基准。 ## Open Ontologies 的证明能确认什么？ **检查器接受一份 Open Ontologies 推导证书，意味着其中的结论可以在受支持的形式语义下，从所提供的断言推出。**文档是否获批、准确或有效，仍需各自的证据。即使前提有误，检查器也可能确认其后续推导有效，却无法发现前提与现实不符。 项目的 [验证架构说明](https://github.com/fabio-rovai/open-ontologies/blob/c7fd75f9491253c56e4d4f408ceac179de343e48/docs/assurance-architecture.md) 将两个问题分开处理：结论能否成立，以及引擎究竟使用了哪张图谱。 | 问题 | 应检查的证据 | 适用边界 | | --- | --- | --- | | 推导是否成立？ | 独立检查器对断言文件和推导文件的检查结果 | 结论以这些断言和受支持的规则为条件 | | 这是本次要使用的图谱吗？ | 图谱版本、断言摘要与选定的图谱范围 | 有效证明也可能针对错误的快照 | | 断言是否可靠？ | 来源证据、抽取审核与责任人 | 形式推导不会核实现实世界 | | 智能体可以使用结果吗？ | 应用策略与访问权限检查 | 类名本身不授予任何权限 | 我们的 [LLM-as-a-Verifier 分析](/zh/blog/llm-as-a-verifier/) 介绍如何用模型学习到的分数对输出排序。Open Ontologies 检查的是一条明确推导是否符合规则。 ## 如何检查 Open Ontologies 的推导证书？ **先生成证书，再运行 `oo-cert`，让它读取 `asserted.tsv` 和 `derivations.tsv`。**保留标准输出、标准错误和退出码。只有检查器正常完成，并返回文档规定的成功结果，才能确认通过。 [证书指南](https://github.com/fabio-rovai/open-ontologies/blob/c7fd75f9491253c56e4d4f408ceac179de343e48/docs/lean-certificates.md) 说明，独立的 Lean 检查器会重新检查记录中的推导步骤。文档规定的成功结果包括退出码 `0`、`ok: true` 和定理名 `OOCert.certificate_sound`。若某一步被拒绝，报告应指出对应的规则、结论和前提。 下载我们的 [Open Ontologies 证书测试样例与运行记录](/downloads/open-ontologies-proof-verification-fixture.zip) ，解压后进入该目录。以下命令假设经过校验的引擎和检查器已位于 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: . @prefix rdfs: . ex:note42 a ex:ProjectNote . ex:ProjectNote rdfs:subClassOf ex:Document . ex:Retrievable a rdfs:Class . ``` 提议的变更新增一个三元组： ``` ex:Document rdfs:subClassOf ex:Retrievable . ``` [保守性检查文档](https://github.com/fabio-rovai/open-ontologies/blob/c7fd75f9491253c56e4d4f408ceac179de343e48/docs/modules-and-conservativity.md) 说明，这里比较的是指定有限规则表下的结果，不能据此推断所有逻辑体系中的保守性。我们的 `owl-rl` 计划报告一次插入，结构影响范围为零个三元组，`risk_score: low`，并给出 `not_conservative_under_rule_table`。 | 三元组简写 | 出现原因 | | --- | --- | | Document 是 Retrievable 的子类 | 新增的断言本身 | | ProjectNote 是 Retrievable 的子类 | 沿子类关系链得到的新推导 | | note42 的类型是 Retrievable | 利用该分类得到的新推导 | 这里的**三项新增推论，包含一条断言和两条新推导**。推理证书中则有三条推导，因为它还记录了 `note42 type Document`，这条结论在初始图谱中就已成立。 项目的 [公开演示](https://github.com/fabio-rovai/open-ontologies/blob/c7fd75f9491253c56e4d4f408ceac179de343e48/README.md) 报告在 0.04 秒内发现 901 项新推论，另一次证书演示核验了 259 条推导，并拒绝一个伪造结果。我们没有复现这些数量或耗时。本次小样例也表明，推论总数可能包含新增断言本身。 我们的批处理进程还出现了另一种差异：进程退出码为 `0`，嵌套的保守性报告却包含 `exit_code: 1`。这项语义变化可能正是预期效果。审批任务需要读取报告并记录决定，只检查进程退出状态会漏掉这项发现。 ## 缩小 RAG 上下文后，还能保留同一个结论吗？ **Open Ontologies 可以检查选定的图谱切片，是否仍能在指定规则配置下支持正向的具体事实三元组（不含变量）。**待检查的主张由你提供。它不会自动抽取并核验生成答案中的每句话，保留一定比例的邻近三元组也无法说明所需前提仍然存在。 本例的目标是 `note42 type Retrievable`。完整切片保留推导所需的三个三元组，省略独立的类声明。截断切片则删除 `ProjectNote subClassOf Document`。两者都是提议后图谱的子集。 [切片推论保留检查指南](https://github.com/fabio-rovai/open-ontologies/blob/c7fd75f9491253c56e4d4f408ceac179de343e48/docs/projection-entailment.md) 分别命名了已核验、直接存在于断言中和未经核验的结果： | 运行条件 | 逐目标结果 | 进程退出码 | 对审批的含义 | | --- | --- | --- | --- | | 完整切片，未配置检查器 | `preserved_unchecked` | 0 | 引擎能够推出目标，但缺少独立验证 | | 截断切片，未配置检查器 | `lost_under_profile_unchecked` | 1 | 所选规则配置已无法从切片推出目标 | | 完整切片，强制要求检查器 | `certificate_rejected`、`STOP_THE_LINE` | 2 | 暂缓，并查看检查器的原始错误 | 第三行的报告包含同一个运行时错误：`failed to locate application`。外层工具标记为拒绝，不能说明某条规则已被证伪。在这个环境中，我们没有获得 `preserved_checked`。 切片丢失推论的判定也有边界：它是引擎在受支持规则范围内给出的否定结果，不能证明所有本体逻辑下都无法推出该结论。如果工作流要求独立证明，我们会暂缓采用未经核验的正向结果，补回丢失的前提，并排查检查器故障，再允许智能体依赖该主张。 推论保留检查也不负责授权。用户是否有权检索这些事实，应参考我们的 [RAG 访问权限指南](/zh/blog/rag-permissions-sharepoint-confluence-drive/) 。 ## 审批记录应该包含哪些内容？ **Open Ontologies 的审批记录应写明图谱版本、所选断言、规则配置、语义变化和检查器的完整结果。**如果涉及检索切片，还要记录逐目标判定。这是我们建议的应用策略，不代表引擎会自动批准业务变更。 | 记录项 | 验收问题 | | --- | --- | | 引擎与检查器身份 | 运行的是哪些发布文件或构建产物？哈希是否与审查过的版本一致？ | | 图谱版本与断言字节内容 | 证书是否对应本次获批的准确输入？ | | 选定范围与规则配置 | 使用了哪些图谱和规则？是否拒绝了相关语法结构或检查目标？ | | 语义变更报告 | 审核者是否确认了报告中的推论，并处理无法判定的结果，而不是仅凭结构风险标签放行？ | | 检查器的标准输出、标准错误与退出码 | 指定检查器是否输出了成功验证的结果？ | | 切片、明确目标与逐项判定 | 每条必需的派生主张是否都有应用要求的证据？ | [可信计算基文档](https://github.com/fabio-rovai/open-ontologies/blob/c7fd75f9491253c56e4d4f408ceac179de343e48/docs/trusted-computing-base.md) 解释，检查器读取的是证书文件，并不知道应用本来打算使用什么状态。它不检查 `scope.tsv`，调用方必须审核图谱选择。断言摘要绑定字节内容，不能说明这些内容在现实中是否真实、是否仍然有效，或是否有权使用。 本次实验的审批结论仍是**暂缓，等待独立验证**。伪造证书被拒绝提供了有用证据，却不能替代对实际要使用的原始证书进行成功检查。接入智能体前，先在部署主机上重复执行应当通过和应当拒绝的两组对照测试。 ## 如何把 Open Ontologies 接入 Claude Code？ **将 Open Ontologies 注册为本地 stdio MCP 服务，并指定可执行文件和存储目录的绝对路径。**项目默认使用内存存储，重启进程后不会保留已加载的图谱，请明确选择是否持久化。MCP 连接正常，也不能说明独立证明检查器已经安装。 固定提交中的 [存储与嵌入配置](https://github.com/fabio-rovai/open-ontologies/blob/c7fd75f9491253c56e4d4f408ceac179de343e48/src/config.rs) 定义了默认内存模式和持久化模式。依据当前 [Claude Code MCP 文档](https://code.claude.com/docs/en/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 产品与智能体开发服务](/zh/services/artificial-intelligence/) 。先确定待核验的主张和审批条件，再扩展图谱。 ## 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。项目的 [快速入门指南](https://github.com/fabio-rovai/open-ontologies/blob/c7fd75f9491253c56e4d4f408ceac179de343e48/docs/quickstart.md) 记录了嵌入初始化中的模型下载步骤。判断数据是否全程留在本地前，应检查构建版本、提供方与客户端的数据流向。 ### derivations.tsv 会列出所有可能的论证依据吗？ 不会。证书指南说明，每个新增推导三元组记录一条推导步骤，采用最先找到的推导路径。同一结论可能还有其他有效论证，文件并不会穷举这些路径。若要回答完整论证或来源追溯问题，应独立评估项目对应机制的保证，不能由某份证书是否通过检查来推断。 模型与基础设施 ## 接下来读什么 模型选择、推理经济性、本地部署、压缩与服务架构。 [从这里开始**在欧盟自托管 LLM：开放权重模型何时才真正划算**](/zh/blog/self-hosting-llms-eu-cost/) - [Cue 轮次检测：电话号码采集、基准测试与局限](/zh/blog/cue-turn-detection-phone-numbers/) - [Google SAM 现名 Agent Mesh：跨机器调用 MCP 工具](/zh/blog/google-sam-agent-mesh-mcp-tools/) - [EdgeQuake：用 PostgreSQL GraphRAG 构建 MCP 智能体记忆](/zh/blog/edgequake-postgresql-graphrag-mcp-agent-memory/) - [BitNet CPU 推理：2B4T 的实际内存需求与 100B 说法](/zh/blog/bitnet-cpu-llm-ram-requirements/) - [SuperPenguin：按 PR、客户和功能核算 AI 成本](/zh/blog/superpenguin-ai-roi-cost-per-pr-customer/) [下一篇文章**Cue 轮次检测：电话号码采集、基准测试与局限**](/zh/blog/cue-turn-detection-phone-numbers/) [**返回**](/zh/blog/overview/) [![Kevin Riedl](/img/team/kevin.webp)](/zh/team/kevin-riedl/) [Kevin Riedl](/zh/team/kevin-riedl/) https://linkedin.com/in/wsdt 12 分钟 阅读 · 2026年11月3日 最近审核 2026年11月3日 [**下一篇**](/zh/blog/graph-engineering-ai-agents/)