用大模型生成符合逻辑的本体推理证明，揭示其在复杂情况下的表现瓶颈。
Large Language Model for OWL Proofs
- 构建自动化数据与评估框架，分三步完成完整推理证明
- 复杂逻辑是影响模型表现的主要因素，而非表达形式
- 输入数据噪声和不完整会显著降低模型性能，适合做可解释性研究
近年来，大语言模型（LLMs）在演绎推理等任务上的能力受到广泛关注。然而，其生成忠实、可读的推理证明（即结论成立的原因说明）的能力仍鲜有研究。本文聚焦于广泛用于表示和推理复杂知识的OWL本体，通过开发自动化数据构建与评估框架，系统评估了三个连续推理任务：提取、简化与解释，以及一个额外的前提出理完备性评估任务。在多个主流推理型大模型上进行的实验发现：（1）部分模型整体表现良好，但在复杂案例中仍有局限；（2）逻辑复杂度是影响模型性能的主导因素，而非形式化语言与自然语言的表达方式；（3）输入数据中的噪声与不完整性会显著削弱模型表现。这些结果凸显了大模型在严谨逻辑解释方面的潜力，也暴露了其在复杂或不完善条件下支持鲁棒推理的差距。代码与数据已开源于 https://github.com/HuiYang1997/LLMOwlR。
原文摘要 · Abstract (English)
The ability of Large Language Models (LLMs) to perform reasoning tasks such as deduction has been widely investigated in recent years. Yet, their capacity to generate proofs-faithful, human-readable explanations of why conclusions follow-remains largely under explored. In this work, we study proof generation in the context of OWL ontologies, which are widely adopted for representing and reasoning over complex knowledge, by developing an automated dataset construction and evaluation framework. Our evaluation encompassing three sequential tasks for complete proving: Extraction, Simplification, and Explanation, as well as an additional task of assessing Logic Completeness of the premise. Through extensive experiments on widely used reasoning LLMs, we achieve important findings including: (1) Some models achieve overall strong results but remain limited on complex cases; (2) Logical complexity, rather than representation format (formal logic language versus natural language), is the dominant factor shaping LLM performance; and (3) Noise and incompleteness in input data substantially diminish LLMs' performance. Together, these results underscore both the promise of LLMs for explanation with rigorous logics and the gap of supporting resilient reasoning under complex or imperfect conditions. Code and data are available at https://github.com/HuiYang1997/LLMOwlR.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。