基于本体的神经符号语言到逻辑自动翻译

这份论文要回答的是一个很具体的问题：当生成式人工智能在美国国防部（Department of Defense）这类环境里越来越普遍，人们要怎样对 AI 生成的信息做验证、接地（ground）和推理。作者的切入点是先把自然语言形式化——材料里说得很直接，形式化之后计算机才能做推理和推断。眼下把自然语言翻成形式语言的主流做法依赖大语言模型（LLM），但训练 LLM 学会这种翻译需要海量数据，这就是卡住的地方。值得现在看的原因在于，它没有去要更多人工标注，而是转向合成数据，并把整条流程绑在一个已有本体上。

研究的目标语言是 Standard Upper Ontology Knowledge Interchange Format（SUO-KIF），要求术语锚定在 Suggested Upper Merged Ontology（SUMO）里；源语言是英语。做法是用数百万条合成生成的英文句子及其等价逻辑公式来微调模型。整套策略围绕四个方向展开：公式语法、本体接地、句子连贯性和形态准确性。换句话说，翻译质量被拆成了几个可以分别处理的工程问题，而不是笼统地追求“翻得像”。

在公式语法和本体接地这两项上，材料给出的具体手段是一种新的 tokenization 技术，作者称它提高了 SUMO 接地术语的占比与语法正确的比例。数据质量一侧则靠高精度过滤器，用来提升数据集的语义质量、减少不连贯的句子。这两件事指向同一个思路：合成数据的规模本身不是难点，噪声才是，所以要在生成端和过滤端同时下手。

形态准确性这一块，作者分析的是如何从 LLM 中高效抽取正确的词形变化（inflection）和词性归类（categorization）。这些信息被用于生成更流畅、语法更正确的英文句子——源句子本身不通，配套的逻辑公式也很难有意义。论文把这些贡献合在一起表述：它们推进了 LLM 在本体接地推理上的使用，使高风险环境下的自然语言自动分析与形式验证更可靠。

这意味着什么？把英语到逻辑的翻译与本体绑定，带来的不只是句子更通顺，而是生成的每条逻辑公式里的术语都能追溯到 SUMO 的概念上，形式验证才有明确的对象可验。对实践而言，合成数据加高精度过滤是一条绕开大规模人工标注的路径；就主题词里列出的自动定理证明（ATP）这类下游用途看，数据供给方式的变化可能和模型结构的变化同样关键。需要说明的是，这是基于摘要层面信息的解读，材料本身只讲了方向，没有给出量化收益。

做神经符号 AI、本体工程、auto-formalization、LLM 数据合成的人，以及需要在高风险场景里核查 AI 输出的人，都能从中拿到东西：一套可复用的配方——目标形式语言选 SUO-KIF、术语锚在 SUMO、用合成句—公式对做微调、在语法／接地／连贯／形态四个维度上分别设卡。边界也要讲清楚：可见材料只到摘要与元数据层面，“数百万”是唯一给出的规模量级，没有基线对比、没有精确率数字，也没有交代合成数据的具体生成流程；此外导师信息在材料内部并不一致——正文题页写的是 R A. Pease，而编辑导读列出的是 Xie, Geoffrey G. 与 Kolsch, Mathias N.，引用前应回到原文核对。原文可通过 https://hdl.handle.net/10945/75984 获取。

AUTOMATED NEURO-SYMBOLIC LANGUAGE TO LOGIC TRANSLATION GROUNDED IN AN ONTOLOGY Title AUTOMATED NEURO-SYMBOLIC LANGUAGE TO LOGIC TRANSLATION GROUNDED IN AN ONTOLOGY Item Type Thesis Authors Thompson, Richard B. URI https://hdl.handle.net/10945/75984 Publisher Monterey, CA; Naval Postgraduate School Date Issued 2026-06 Rights This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States. Download date 2026-11-04 22:58:06 Link to Item https://hdl.handle.net/10945/75984 Downloaded from NPS Archive: Calhoun NAVAL POSTGRADUATE SCHOOL MONTEREY, CALIFORNIA DISSERTATION AUTOMATED NEURO-SYMBOLIC LANGUAGE TO LOGIC TRANSLATION GROUNDED IN AN ONTOLOGY by Richard B. Thompson June 2026 Dissertation Supervisor: R A. Pease Distribution Statement A.