Large Language Model for OWL Proofs

TL;DR

This paper investigates the ability of Large Language Models to generate faithful, human-readable proofs for OWL ontologies, highlighting their strengths and limitations in complex reasoning scenarios.

Contribution

The study develops an automated dataset and evaluation framework for proof generation in OWL reasoning, providing new insights into LLM capabilities and challenges.

Findings

Some models perform well on simple cases but struggle with complexity.

Logical complexity impacts performance more than representation format.

Input noise and incompleteness significantly reduce LLM effectiveness.

Abstract

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.