Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Large Language Model for OWL Proofs

Hui Yang, Jiaoyan Chen, Uli Sattler

TL;DR

We address proving with Large Language Models over OWL ontologies, formulating Extraction, Simplification, and Explanation tasks within the EL fragment and introducing a dataset-building framework based on justifications. The study systematically evaluates diverse LLMs (including GPT-o4-mini, Qwen3-32B, and Magistral variants) under standard and complex conditions, analyzing effects of inference rules, examples, noisy data, natural-language inputs, and incomplete premises. Key findings show that while large models achieve strong performance overall, complex derivations, input noise, and missing premises substantially degrade reasoning; the dominant factor is logical complexity rather than representation form. The results highlight both the potential and limitations of LLMs for rigorous logical explanation and suggest directions for resilient, explainable knowledge retrieval and generation in ontology reasoning.

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.

Large Language Model for OWL Proofs

TL;DR

We address proving with Large Language Models over OWL ontologies, formulating Extraction, Simplification, and Explanation tasks within the EL fragment and introducing a dataset-building framework based on justifications. The study systematically evaluates diverse LLMs (including GPT-o4-mini, Qwen3-32B, and Magistral variants) under standard and complex conditions, analyzing effects of inference rules, examples, noisy data, natural-language inputs, and incomplete premises. Key findings show that while large models achieve strong performance overall, complex derivations, input noise, and missing premises substantially degrade reasoning; the dominant factor is logical complexity rather than representation form. The results highlight both the potential and limitations of LLMs for rigorous logical explanation and suggest directions for resilient, explainable knowledge retrieval and generation in ontology reasoning.

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.
Paper Structure (34 sections, 2 equations, 21 figures, 3 tables)

This paper contains 34 sections, 2 equations, 21 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. LLM Evaluation on Logical Reasoning
  4. LLMs on Ontologies.
  5. Preliminaries
  6. Dataset Construction
  7. Selecting Conclusions
  8. Selecting Noisy Axioms
  9. Constructed Dataset
  10. Evaluation Methods and Settings
  11. Methods
  12. Metrics
  13. Evaluation Results
  14. Standard Setting
  15. Performance of Different Evaluation Methods
  16. ...and 19 more sections

Figures (21)

  • Figure 1: LLMs for proof construction and presentation with Web ontologies
  • Figure 2: Distribution of the selected conclusions (subsumptions).
  • Figure 3: Inference Rules (for $\mathcal{EL}$-ontologies)
  • Figure 4: An example of the given input and desired output. The output is supposed to consist of three parts, AXIOMS_USED, SIMPLIFY, and DERIVE, correspond to the tasks Extraction, Simplification, and Derivation, respectively.
  • Figure 5: Comparison (weighted) of Qwen3-32B and GPT-o4-mini with/without Inference Rules (IR).
  • ...and 16 more figures

Theorems & Definitions (4)

  • Example 1
  • Definition 1: Justification
  • Remark 1
  • Remark 2