Reasoning Benchmarks: LUBM, OWL2Bench, ORE

📍 Where we are: Part V · Reasoners in Practice — Chapter 17. Datalog and DL Engines sorted the production engines — RDFox saturating rules, HermiT and Konclude searching for models — into two families and showed they compute the same fixpoint for the tractable logics; that chapter ended on a question it could not answer, which engine should you actually use, and how would you know? This chapter builds the instrument that answers it.

Two reasoners can both be correct and still differ by orders of magnitude in speed; two can both be fast and quietly disagree on the answer. "It felt quick on my ontology" tells you nothing about either gap — it is an anecdote, not a measurement, because the ontology, the hardware, and the task were never pinned down and nothing about the claim reruns. What replaces the anecdote is a benchmark: a fixed dataset and a fixed task that every reasoner runs under identical rules, so that "faster" and "more accurate" stop being boasts and become numbers anyone can reproduce. This chapter surveys the three benchmarks that shaped ontology reasoning — LUBM, OWL2Bench, and ORE — and shows that all three, stripped to their core, measure the same two things the companion measures on one tiny ontology: correctness and speed.

The simple version

Imagine a school sports day where every runner runs the same measured track, timed by the same stopwatch, on the same afternoon. Without the shared track, "I'm faster" is just a claim; with it, everyone reads their time off one board. A reasoning benchmark is that measured track for reasoners: the same ontology, the same question, the same clock. It turns arguments about which engine is better into a leaderboard you can check — and, just as importantly, rerun tomorrow to see whether the winner still wins.

What this chapter covers

• Why benchmarks exist — reasoners differ by orders of magnitude and cover different profiles, so only shared datasets and fixed tasks can compare them; testimonials cannot.
• LUBM — the Lehigh University Benchmark: a generator that mints university-domain data at any scale behind fourteen fixed queries, the classic scalability test, and a scaled-up cousin of our academic world.
• OWL2Bench — a profile-aware benchmark that stress-tests each OWL 2 profile (EL, QL, RL, DL), so a reasoner is judged on exactly what it claims to support.
• ORE — the OWL Reasoner Evaluation competition: classification, consistency, and satisfiability over a corpus of real ontologies, ranked by correctness and time.
• The two metrics, decoded — correctness (does the output match a trusted gold standard?) and performance (wall-clock, memory, scaling), and why correctness is the harder one because it needs a reference.
• The companion as a one-ontology benchmark — our correctness metric is the exact agreement of classify() with HermiT: 8 subsumptions, 2 unsatisfiable concepts, agreement confirmed.

Why benchmarks: testimonials do not compare reasoners

The engines of the previous chapter are not interchangeable. On the same input they span orders of magnitude in speed; they occupy different OWL 2 profiles — the standardized sub-languages of the Web Ontology Language, each trading expressive power for a better worst-case cost; and they are tuned for different questions. An EL-specialised classifier finishes a biomedical terminology in seconds where a full-DL (Description Logic) reasoner may labour for minutes, and a query engine over a database-scale ABox is built for a task a classifier never faces. Comparing such tools by testimonial is hopeless: the ontologies differ, the hardware differs, the task is left vague, and nothing reruns to settle the argument.

A benchmark removes every one of those degrees of freedom. It fixes three things — (i) a dataset, an ontology given outright or generated reproducibly from a seed; (ii) a task, defined precisely enough to have a single right answer, such as classification, consistency checking, or query answering; and (iii) a protocol, spelling out how to time the run and what counts as correct. Fix that triple and the two properties that actually matter become measurable on equal footing:

$$\text{benchmark} \;=\; (\text{dataset},\ \text{task},\ \text{protocol}) \;\longmapsto\; \big(\underbrace{\text{correctness}}_{\text{is the answer right?}},\ \underbrace{\text{performance}}_{\text{how costly?}}\big).$$

Each benchmark below is a different choice of that triple, aimed at a different weakness of the naive comparison, but all three land on the same output pair. We take them in the order the field built them.

LUBM: scale the data, fix the queries

The Lehigh University Benchmark (LUBM) is the original scalability test for OWL knowledge-base systems [1]. Its heart is a data generator: given a target number of universities and a random seed, it deterministically mints a synthetic university world — departments, full and assistant professors, graduate and undergraduate students, courses, publications, and the advising, teaching, and member-of relations among them. Turn the dial from one university to a thousand and the same schema produces a proportionally larger ABox (the ground assertions), so a single knob sweeps the dataset from a small instance up to one with well over a hundred million assertions, with the schema — the Univ-Bench ontology — held fixed the whole way.

The task is query answering. LUBM ships fourteen fixed queries over that ontology, chosen so that answering them requires genuine inference — following the subclass hierarchy, chasing the advises and member-of relations, applying transitivity — rather than a plain table lookup. Here the generator emits only the ABox, not an answer key; the gold standard comes for free from a different source. Because the data is synthetic and the Univ-Bench semantics are fixed, the correct answer set for each query is known by construction — computable exactly, without an oracle, from the deterministic data and the fixed ontology. That free gold standard is an unusual luxury, and — as ORE will show — one that vanishes the moment the ontologies are real rather than generated.

The kinship to our running example is not decoration; it is the same world, scaled. Our ontology's chain Professor ⊑ Researcher ⊑ Person, its advises role, and its role chain advises ∘ advises ⊑ grandAdvisor are a hand-sized version of LUBM's professor/student hierarchy and advisor relation. Where the companion has 13 individuals — running python3 ontology.py prints 10 named concepts, 6 roles, 14 TBox axioms; ABox: 13 concept assertions, 18 role assertions over 13 individuals. — LUBM has the identical shape wound out to millions of edges. That is exactly what makes LUBM a scalability test rather than a reasoning test: the inference each query needs is easy, the volume is the challenge, and the metric is how the time and memory curves bend as the ABox grows.

OWL2Bench: judged on the profile you claim

LUBM predates OWL 2 and exercises one modelling style. OWL2Bench was built to fix a narrower unfairness: a reasoner should be tested on the profile it actually implements, not on constructors it never promised to handle [2]. OWL 2 defines three tractable profiles plus the full description logic, and each was designed for a different job:

• OWL 2 EL — built on the EL family (the logic of our completion algorithm); classification stays polynomial, so it scales to terminologies with hundreds of thousands of classes such as SNOMED CT and the Gene Ontology.
• OWL 2 QL — built on DL-Lite; tuned for query answering over large ABoxes by rewriting queries into ordinary database queries.
• OWL 2 RL — a rule-language fragment; reasoning runs as forward-chaining rules, the Datalog style of the previous chapter.
• OWL 2 DL — the full expressive logic, decidable but with a punishing worst-case cost.

OWL2Bench supplies a TBox exercising the constructors of each profile, together with a scalable ABox generator (in the LUBM spirit) and a set of SPARQL queries, so a reasoner can be measured on both TBox reasoning (classification, consistency) and ABox reasoning (query answering) within the profile it claims. An EL reasoner is scored on the EL workload it is built for and is neither penalised on constructs outside its remit nor allowed to hide a missing feature. The three benchmarks divide the labour cleanly:

Benchmark	What it stresses	Primary metric
LUBM	scalable ABox query answering over one fixed university TBox	load time + query response time; answer soundness and completeness
OWL2Bench	profile-specific reasoning (EL, QL, RL, DL), TBox and ABox, at scale	reasoning time + query time, reported per profile
ORE	classification, consistency, satisfiability over real ontologies	correctness (vs a reference) + wall-clock time

ORE: a competition over real ontologies

Synthetic data is repeatable but tame; it rarely contains the awkward, hand-authored modelling that trips a real reasoner. The OWL Reasoner Evaluation (ORE) competition closed that gap by running reasoners head-to-head over a corpus of real-world ontologies gathered from the community, and reporting the outcome as a ranked competition [3]. ORE fixed three standard reasoning tasks, each with a crisp answer:

• Classification — compute the full subsumption hierarchy: every entailed $A \sqsubseteq B$ among named concepts.
• Consistency — decide whether the ontology has a model at all, or whether its axioms contradict each other outright.
• Satisfiability — decide, for a given class, whether it can have any instance, or is forced empty ($C \sqsubseteq \bot$) like our TenuredStudent.

Reasoners competed within profile tracks (DL, EL, RL), so each was matched against peers on comparable inputs, and were ranked by how many problems they solved correctly within a time limit and how quickly. Named engines — Konclude, HermiT, ELK, FaCT++, Pellet, JFact — met on one corpus under one clock, and the leaderboard, not a testimonial, decided the standings.

The hard part ORE had to solve is exactly the one LUBM sidestepped: real ontologies do not come with an answer key. No oracle already knows the true classification of an arbitrary ontology pulled off the web. ORE's pragmatic fix is a majority vote — when reasoners disagree on a problem, the answer returned by most of them is taken as the reference, and the disagreements are flagged for human inspection. It is an imperfect gold standard, but a reproducible one, and it makes correctness scorable at a scale no manual key could reach.

The two metrics decoded: correctness and performance

Strip away what separates the three benchmarks and the same two axes remain.

Performance is the easy axis to define and the loud one to report. It is wall-clock time to finish the task, peak memory, and — the axis LUBM was built for — how those quantities scale with input size. Write $t(n)$ for the time on an ABox of $n$ assertions: a reasoner that scales well keeps $t(n)$ near-linear, while worst-case DL reasoning can climb exponentially, which is precisely why the tractable profiles exist. Performance is easy to measure because a stopwatch needs no oracle — but a fast wrong answer is worthless, which is why speed is never reported alone.

Correctness is the subtle axis, because it presupposes something to be correct against: a gold standard. For a set-valued task like classification, correctness is exact agreement between the reasoner's output set $O$ and the reference set $G$. Introduce the symmetric difference $O \oplus G$ — the entries on which the two sets disagree, present in one but not the other — and correctness is simply

$$\text{correct} \quad\Longleftrightarrow\quad O \oplus G = \varnothing,$$

the empty symmetric difference. For query answering, correctness is usually reported as two ratios borrowed from precision and recall: completeness (did it return all the true answers?) and soundness (were all the answers it returned actually true?),

$$\text{completeness} = \frac{\lvert A_{\text{returned}} \cap A_{\text{correct}}\rvert}{\lvert A_{\text{correct}}\rvert}, \qquad \text{soundness} = \frac{\lvert A_{\text{returned}} \cap A_{\text{correct}}\rvert}{\lvert A_{\text{returned}}\rvert},$$

which reach 1 together exactly when the returned set equals the correct set. The whole difficulty of correctness — and the whole reason ORE needs a majority vote while LUBM does not — is that $G$, the right answer, has to come from somewhere trustworthy before either formula means anything.

The companion as a benchmark in miniature

The companion runs exactly this correctness measurement, on one ontology, with a trusted reference standing in for the gold standard. The module reasoners.py rebuilds the academic world with owlready2, drives HermiT — a complete OWL 2 DL reasoner, hence a strict superset of EL and the strongest available oracle — through sync_reasoner (reasoners.py line 99), and reads its classification back among the named concepts so it is directly comparable to the from-scratch result (reasoner_classification, reasoners.py lines 94–113). It then compares HermiT's output against classify(), entry for entry. The comparison is the empty-symmetric-difference test written in Python (reasoners.py lines 145–151):

    subs_agree = r_subs == el_subs
    unsat_agree = r_unsat == el_unsat
    print(f"\n  subsumptions agree : {subs_agree}")
    print(f"  unsatisfiable agree: {unsat_agree}")

    assert subs_agree, ("subsumption mismatch", r_subs ^ el_subs)
    assert unsat_agree, ("unsat mismatch", r_unsat ^ el_unsat)

Read the two axes off the code. Each == is the test $O = G$ — once on the subsumption set, once on the unsatisfiable-class set — and the ^ in each assertion message is Python's symmetric-difference operator $O \oplus G$, so a failure would print precisely the entries that diverged. It never does. The committed output of python3 reasoners.py is a clean agreement on both counts:

Reasoner (HermiT via owlready2) vs. from-scratch EL completion
  from-scratch subsumptions : 8
  HermiT subsumptions       : 8
  from-scratch unsatisfiable: ['TenuredStudent', 'TenuredStudentAdvisor']
  HermiT unsatisfiable      : ['TenuredStudent', 'TenuredStudentAdvisor']

  subsumptions agree : True
  unsatisfiable agree: True

  AGREEMENT CONFIRMED — the from-scratch reasoner matches HermiT.

Map this onto the benchmark vocabulary and it is a benchmark in miniature. The dataset is one 14-axiom ontology; the task is ORE's classification track plus a satisfiability check — the two unsatisfiable concepts TenuredStudent and TenuredStudentAdvisor are classify()'s satisfiability verdicts; the gold standard is HermiT rather than a majority vote, the same move ORE makes when it treats a trusted reasoner's output as the reference; and the correctness score is a perfect $O \oplus G = \varnothing$ on both the 8 subsumptions and the 2 unsatisfiable classes. What this one-ontology, two-reasoner benchmark does not stress is the performance axis — 14 axioms say nothing about scaling — though even here the cost side is faintly visible: classify() reaches its fixpoint in 3 rounds, the polynomial climb that lets EL scale to real terminologies. Correctness certified here, speed deferred to the profile that owns it: the same split every serious benchmark reports.

Three benchmarks, three datasets, one scoreboard: LUBM scales the data, OWL2Bench gates by profile, ORE ranks over real ontologies — and every lane resolves to the same two columns, correctness and time, the pair the companion checks in miniature against HermiT. Original diagram by the authors, created with AI assistance.

The unsolved part

Every benchmark on this page scores plain entailment: does $A \sqsubseteq B$ follow, is the ontology consistent, is the class satisfiable — crisp facts, timed and tallied. That is exactly what makes them reproducible, and exactly what makes them blind to everything a fact carries besides its truth. Real knowledge is annotated. A derived subsumption has a provenance — which axioms, from which source, had to hold for it to follow. An asserted fact has a confidence — a curator's 0.9, a learned model's soft score. A relationship has a time — true during a degree, false after graduation. None of LUBM, OWL2Bench, or ORE measures any of this, because their gold standards are Boolean: a reasoner that returns the right answer for the wrong reasons, or that cannot say how sure it is, or that ignores when a fact held, still earns a perfect mark. The benchmarks honestly certify that an engine reasons correctly over knowledge stripped of its metadata — a faithful measurement of a deliberately narrowed task. Whether we can even define a gold standard for provenance-aware, confidence-aware, or time-aware entailment, let alone build a benchmark that scores it, is open — and it is exactly where the crisp yes-or-no of Part V gives way to the annotated reasoning of Part VI.

Why it matters

Benchmarks are how a field keeps itself honest, and honesty about the symbolic half is precisely what the neuro-symbolic program needs. When a later volume's neural or differentiable reasoner ranks subsumptions by plausibility, the question that decides whether it is any good is correct against what? — and the answer is a benchmark's gold standard: the exact classification a sound-and-complete reasoner produces, timed so you know what the approximation cost. The two axes recur unchanged for a soft reasoner, but with a twist. A neural model, unlike HermiT, will rarely score $O \oplus G = \varnothing$, so the interesting measurement stops being exact agreement and becomes how far it drifts (its precision and recall against $G$) and how fast it runs. You cannot report that drift without the exact answer to subtract from, and the exact answer is what the companion's HermiT cross-check — and the benchmarks it miniaturises — exist to supply. A benchmark is the specification the learning half is measured against; without one, a fluent wrong answer is indistinguishable from a right one.

Key terms

• Benchmark — a fixed (dataset, task, protocol) triple that reduces reasoner comparison to two reproducible numbers: correctness and performance.
• LUBM (Lehigh University Benchmark) — a generator that mints university-domain ABoxes at any scale behind fourteen fixed queries; the classic scalability test, and a scaled-up cousin of the academic world.
• OWL2Bench — a profile-aware benchmark with a TBox and ABox for each OWL 2 profile (EL, QL, RL, DL), so a reasoner is judged only on what it claims to support.
• ORE (OWL Reasoner Evaluation) — a competition scoring reasoners on classification, consistency, and satisfiability over a corpus of real ontologies, ranked by correctness and time.
• Correctness — exact agreement with a gold standard, $O \oplus G = \varnothing$ for set-valued tasks, or soundness and completeness (precision and recall) for query answering.
• Performance — wall-clock time, peak memory, and how they scale with input size $n$; easy to measure because it needs no oracle.
• Gold standard — the trusted reference answer correctness is scored against; known by construction for LUBM's synthetic data, approximated by ORE's majority vote, and played by HermiT in the companion.
• Symmetric difference $\oplus$ — the entries on which two answer sets disagree; empty exactly when the reasoner is correct.

Where this leads

The benchmarks certify entailment stripped bare — right or wrong, fast or slow — and in doing so make vivid everything they leave out: why a fact holds, how sure we are of it, when it is true. The next chapter, Provenance Semirings, picks up the first of those three. It shows how to run the very same fixpoint reasoning while carrying, alongside each derived fact, an algebraic record of the axioms that produced it — so that reach(p3, p1) comes back not just True but tagged with the polynomial t + r·s naming the two derivations behind it. Reasoning stops being a bare yes and becomes an annotated yes, and the crisp world of Part V opens onto the richer one of Part VI.