arXiv:2606.16010cs.IRcs.AI2026-06

让大模型推理过程可执行、可审计,提升可解释性与可信度。

Theorem-Grounded Execution Ontologies for Interpretable Machine Reasoning

  • 将推理建模为可执行的状态转移过程,而非单纯生成文本序列。
  • 在数学推理任务中实现可验证、可复现的推理路径,支持错误定位。
  • 适合需要高可信度推理的领域,如数学证明、科学推演和AI安全验证。

大语言模型在数学、科学、编程和常识推理任务中表现优异,但其推理过程仍高度隐含,难以解释、验证、回放、调试及跨领域迁移。现有方法如思维链、树状思维、图状思维和工具增强推理虽暴露中间推理结果,但普遍缺乏明确的执行语义、形式化状态表示和可验证的推理结构。本文提出定理基执行本体(Theorem-Grounded Execution Ontologies, TGEO),将推理建模为可执行的状态转移过程。给定输入问题,TGEO识别相关定理族,绑定领域本体,发现语义对象,实例化状态与算子,构建谓词与契约,并合成可执行推理图。该图提供可解释、可回放、可审计的推理表示,每个状态转移、算子应用与验证步骤均显式表达。TGEO包含五个组件:(1) 定理基推理先验,(2) 可执行本体,(3) 算子驱动的状态转移,(4) 谓词与契约驱动的执行验证,(5) 架构审计与故障定位。我们在基于数学基准的定理密集型任务和精心设计的黄金执行套件上评估了TGEO,结果表明可执行推理表示在可解释性、可验证性和可复现性方面具有显著价值。

原文摘要 · Abstract (English)

Large language models have achieved impressive performance on reasoning tasks spanning mathematics, science, programming, and commonsense inference. Despite these advances, their reasoning processes remain largely latent, making them difficult to interpret, verify, replay, debug, and transfer across domains. Existing approaches such as chain-of-thought, tree-of-thoughts, graph-of-thoughts, and tool-augmented reasoning expose intermediate reasoning artifacts but typically lack explicit execution semantics, formal state representations, and verifiable reasoning structures. We introduce Theorem-Grounded Execution Ontologies (TGEO), a framework that models reasoning as an executable state-transition process rather than a sequence of generated tokens. Given an input problem, TGEO identifies relevant theorem families, binds the problem to a domain ontology, discovers semantic objects, instantiates states and operators, constructs predicates and contracts, and synthesizes an executable reasoning graph. The resulting graph provides an interpretable, replayable, and auditable representation of reasoning in which every state transition, operator application, and validation step is explicitly represented. TGEO integrates five architectural components: (1) theorem-grounded reasoning priors, (2) executable ontologies, (3) operator-mediated state transitions, (4) predicate and contract-based execution validation, and (5) architectural auditing and failure localization. We evaluate TGEO on theorem-intensive reasoning tasks derived from mathematical benchmark domains and a curated Golden Execution Suite. Our findings demonstrate the value of executable reasoning representations for interpretable, verifiable, and reproducible AI reasoning systems.

可解释推理形式化验证大模型本体建模

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。