今天是2026年10月21日，星期三，北京，天气晴。
来回顾下本体相关进展。
一个是用于推理的Graph序列化形式对比，这个是个工程经验。
一个是open-ontologies这个项目，最近也受到关注，用来做本体的可信检查。可以把它想成一个本体界的CI检查：写本体像写代码，光写完不够，还要有语法检查（validate）、有lint（lint）、有测试（shacl约束）、有可复现的构建证明（certificate）。它不替代建模，它保证建的东西能被验证、被治理、被举证。
对于open-ontologies，先说一个结论，它最独特的证明携带能力，恰恰也是它最不普适的地方。对绝大多数只是要建个本体、跑个查询的人，这套独立复核是多余的，Protégé加rdflib就够了；它的价值只在一个特定场景里：当需要向审计、监管、合作方证明这个推理结论不是我拍的、是可验证的时，别的工具给不出这个保证，它能做些事情。
技术还是很有趣的，我们持续跟进，总会有所收获。
一、用于LLM推理的Graph序列化形式消融对比
这个工作把"图序列化"从静态prompt细节提升为"模型感知、任务感知的动态编排决策"，对做KG-groundedLLM系统的人有直接工程指导价值。
这其实就是序列化的问题，把知识图谱/本体序列化成文本喂给LLM，格式选择会带来几十个百分点的性能波动，所以，可以做个消融对比实验：
工作在《Graph Serializations for Reasoning LLMs:A Study Across Knowledge Extraction and Structural Reasoning》(https://arxiv.org/abs/2610.22734)，可以快速看几个点：
从实现方式上，评测15种格式（Turtle、JSON-LD、SHACL简化、Markdown表、Mermaid、DOT、邻接表、边列表、自然语言摘要等6个家族）×9种前沿LLM配置（gpt-5.4系列、o3、ClaudeSonnet4.6、Haiku、Grok4等），在两类任务上：基于本体的知识抽取（Text2KGBench，19个WebNLG本体）与结构图推理（GraphQA扩展）。
得到的结论是：知识抽取对格式相对不敏感（差异仅1.3–3.9%，收益主要来自模型能力）；结构推理对格式高度敏感（最难任务上格式差异最高28.4%，且推理能力越弱的模型越敏感）。没有任何单一格式在所有模型/任务上占优。据此提出"自适应选择器"：逐查询动态选格式，比最优固定格式提升，但是废资源。
实际上，最优格式高度依赖具体模型版本，结论会随模型更新快速失效。
二、本体验证引擎open-ontologies的一些思路
还是本体推理方向进展，锚定在可信阶段，看一个项目open-ontologies，地址在：https://github.com/fabio-rovai/open-ontologies
先做个定位，它不是一个画本体的工具，也不是reasoner推理工具，而是一个验证本体和数据、让结论可被复核的工具，管的是本体推理对不对、数据合不合规、推出来的结论可不可信。
对应到本体工程，它是本体工程里的验证与治理层，不是建模器、不是推理机、不是图数据库。打个比方：Protégé是画本体的CAD，HermiT/Pellet是算结论的计算器，GraphDB/Stardog是存本体的仓库，那open-ontologies是本体界的CI流水线，负责验证、治理、并把结论做成可被独立复核的东西。
所以，这块又可以看下与这些工具的区别，细分几点：
其一，结论可信，靠的是谁判的，不是谁算的。
这是最根本的分界点。HermiT、Pellet、Stardog这类推理机的结论，是引擎自己算出来的，信结论，等价于信这套引擎实现没有bug。open-ontologies把算和判拆开：Rust引擎负责算，一个用Lean4写的、健全性被机器证明过的检查器负责判，引擎算错了、证书被篡改了，检查器直接拒绝。源码里有10个以上的独立检查器（oo-horn、oo-refute、oo-shacl、oo-lrat等），全部coreLean、无Mathlib，把信任面压到最小。
其二，角色是治理层，不是建模/存储/推理
其他工具各自占一个角色：Protégé建模、rdflib/Jena给写代码的库、HermiT/Pellet推理、GraphDB/Stardog/TopBraid存储加推理加治理的整套平台。open-ontologies只做验证＋治理＋举证这一层，而且用的是Terraform风格的声明式生命周期（plan、apply、drift、enforce），把本体当成要被治理的资产而不是画完就放在那的文件。它不替代任何建模工具，它是在已有的建模和存储之上，加一道可验证、可追溯的治理层。
其三，信任面被显式列出来，而不是默认全信。
绝大多数工具不会告诉究竟在信什么。open-ontologies把它的信任计算基（TCB）枚举成30条可检查属性，逐条标明哪些已经被形式化证明、哪些仍是有界模型检查、哪些还是假设
1、为什么要单独验证？
涉及到可信问题的话，核心矛盾就在于：推理结果被信任，是因为"引擎"被信任。
一个本体推理器（reasoner）的工作，是从"断言的三元组"（assertedgraph）出发，用规则推导出"蕴含的三元组"（entailedtriples）。问题在于：这些规则是人写的代码，人会写错。
可以看个例子：
2026年9月13日，发现两条规则是unsound（不健全）的：cls-svf1从某个类的"限制超类"反向推出成员关系（这正是那条公理的逆命题），并把对象位置上的类IRI当作该类的实例。这两条规则从"扩展profile"写出之日起就存在，不是被测试发现的，而是逐条问"什么语义条件能让这条规则sound"，发现答不上来。
这个例子点出了本质：测试套件只能抓住"有人想到过的bug"。真正缺的，是一个"不依赖引擎开发人想到这个bug"的检查，所以，问题就变成了如何让这个变得更为健壮。
2、具体怎么做？
open-ontologies的核心主张是：对生产本体的每一次变更，都能在"不信任引擎、不信任作者、不信任生成本体的模型"的前提下，被任何人独立复核，也就是，把"推理结果可信"这个问题，从"信任reasoner的作者"转译成"信任一个更小、可读、且被机器检查过的验证器"。
在实现上，写了一堆本体和数据，这个工具做三点判断：这本体逻辑对不对、这批数据合不合的约束、推出来的结论凭什么让人信，这就对应到工具上就是三件事：验证（查一致性）、治理（跑约束出违规清单）、举证（出可独立复核的证书），然后是把算和判做成两个独立进程，中间用一份证书文件当接口，最后用Rust的类型系统保证certified这个词只能靠挣、不能靠写。
第1步：引擎算结论，顺带把怎么算的记下来（不可信侧）
本体（Turtle）先进Oxigraph三元组存储。reason--profile owl-dl --certificate DIR启动推理：rdfs/owl-rl/owl-rl-ext走前向链，owl-dl走SHIQ tableaux。关键不在算，而在算的同时把每一步推导写成证书：每推出一个三元组，就记录结论是什么、用了哪条规则、读了哪些前提。落到磁盘是两个文件：asserted.tsv（输入断言）和derivations.tsv（推导，每行一步）。如果推理发现矛盾，还会多写一个refutation.tsv。
第2步：证书文件当接口。derivations.tsv就是Rust侧和Lean侧之间的合同。Rust只管写，Lean只管读，两边不共享任何代码、不共享任何内存，只有这份文件在中间。
第3步：Lean检查器逐条重放（可信侧）。lakeexeoo-horn check RAD跑起来的是一个用Lean4写的检查器，coreLean、无Mathlib、几百行。它不重新推理，只逐条重放证书：验证每条记录的前提确实在断言集里、规则确实合法。它的健全性是一条机器证明过的定理OOCert.certificate_sound。退出码是硬判词：0全过、1拒绝、2输入不可读。这跟很多形式化验证项目的区别在于：检查器不搜索、只检查，因为找结论贵、验证结论便宜。
3、怎么用？
怎么用，看下几个场景来讲，看两个常用场景：
场景1：验AI生成的本体自不自洽。
输入：一个LLM生成的本体文件。
处理：validate（语法与OWL一致性）加reason--profileowl-dl（推理，检查会不会推出矛盾）。
输出：consistent/inconsistent。一旦有矛盾，reason--certificate还会额外吐出一份refutation.tsv（反证证书），告诉矛盾具体卡在哪几条公理上。这是当前LLM生成本体场景最稀缺的能力：模型能产出海量本体，但没人知道哪些自相矛盾。
场景2：数据治理与合规核验（最典型的用法）
输入：本体加实例加约束，三样一起喂。仓库investment-fund-ontology案例里，约束ifo-shapes.ttl有一条很直白的规则：
处理：shacl ifo-shapes.ttl。
输出：一份违规清单，每条带严重级别和原因。真实结果是37个findings，其中有报价但无可解析交易场所这一类被形状自己标成Warning而非Violation，因为它是需要拍板的治理缺口，不是记录本身错了。注意这个细微处：约束里怎么写，输出就怎么判，工具不替下结论。
三、关于我们
老刘说NLP技术社区，自2022年建立以来，以公正、客观的角度，围绕知识图谱本体论+RAG知识库+Agent智能体三个方向做深入跟进，加入方式在：https://mp.weixin.qq.com/s/_sEWHeV20sN1JcwGJU9tJw