面向 OWL 证明的大语言模型

大语言模型（LLM）执行演绎等推理任务的能力近年已被广泛研究。然而，它们生成证明——对结论为何成立给出忠实、人类可读解释——的能力在很大程度上仍未被探索。本工作研究 OWL 本体语境下的证明生成，OWL 本体被广泛用于表示复杂知识并在其上推理，我们为此开发自动化数据集构建与评估框架。我们的评估涵盖面向完整证明的三个先后任务——抽取（Extraction）、简化（Simplification）与解释（Explanation），以及评估前提逻辑完备性的附加任务。通过对广泛使用的推理 LLM 的大量实验，我们得到重要发现：(1) 一些模型总体成绩强劲，但在复杂案例上仍然受限；(2) 逻辑复杂度而非表示格式（形式逻辑语言与自然语言之别）是塑造 LLM 性能的主导因素；(3) 输入数据中的噪声与不完整会大幅削弱 LLM 性能。这些结果共同凸显了 LLM 在严谨逻辑解释上的前景，以及在复杂或不完美条件下支持韧性推理方面的差距。代码与数据可在 https://github.com/HuiYang1997/LLMOwlR 获取。