Ontology-Grounded, Reasoner-Verified Benchmarks for Evaluating LLM Reasoning in Scientific AI

# Ontology-Grounded, Reasoner-Verified Benchmarks for Evaluating LLM Reasoning in Scientific AI
Source: [https://arxiv.org/html/2610.00682](https://arxiv.org/html/2610.00682)
\\workshoptitle

AIDaR: AI Data Readiness for Scientific Discovery

Nishtha N\. VaidyaStephan GrimmAffiliation:Siemens AGThomas HubauerAffiliation:Siemens AGThomas A\. RunklerAffiliation:Siemens AGAffiliation:Technical University of MunichEmail:nishtha\.vaidya@tum\.de

###### Abstract

Large language models \(LLMs\) increasingly underpin scientific AI applications that reason over structured knowledge, from biomedical question answering and clinical decision support to materials informatics\. However, their logical reasoning often falls short, producing factual inaccuracies unacceptable in these settings\. Reliable evaluation remains challenging: manual dataset construction scales poorly, and LLM\-based generation risks embedding the very flaws it aims to measure\. High\-quality benchmarks must therefore ground both correct and incorrect labelled examples in explicit background knowledge, formally verifiable by a standard reasoner\. We propose a pipeline that automatically generates ontology\-grounded multiple\-choice question \(MCQ\) benchmarks from any sufficiently axiomatised OWL 2 ontology, with correct answers grounded in the ontology by design\. Incorrect answers, called distractors, are generated by perturbing the right\-hand\-side class expressions of class definition axioms, and their incorrectness with respect to the ontology’s axioms is formally verified by an OWL reasoner via entailment checks\. We evaluate the pipeline on three ontologies: Pizza \(small, academic\), PMDco \(complex, materials science\), and DOID \(large, biomedical\)\. The results validate three claims\. First, the pipeline is productive and grounded: we use it to generate 112, 2,491, and 15,216 MCQs respectively, each anchored to a class definition axiom\. Second, distractors span four semantic categories from class unsatisfiability to weakened subsumptions, enabling diagnostic evaluation of specific reasoning failures\. Third, items meet natural language quality standards: mean LLM judge scores of 4\.02, 4\.36, and 3\.36 out of 5 confirm fluency, and correct\-answer\-to\-distractor similarity above 0\.8 shows that wrong options cannot be dismissed on surface form alone\. Six LLMs \(frontier, open\-source, reasoning, and non\-reasoning\) evaluated zero\-shot achieve 41\.1–76\.8% accuracy, well above the 25% random\-guessing baseline, indicating the benchmarks are challenging and discriminative\. This work is a step towards more reliable benchmarks for assessing logical reasoning in next generation scientific AI applications\.

## 1Introduction

Large language models \(LLMs\) perform well on natural language \(NL\) tasks but fail on logical reasoning over domain knowledge\([Liu et al\., 2025](https://arxiv.org/html/2610.00682#bib.bib11)\), producing factual inaccuracies unacceptable for scientific applications such as biomedical knowledge retrieval, clinical decision support, and materials informatics\. This holds even when models are augmented with prompt engineering\([Vaidya et al\., 2025](https://arxiv.org/html/2610.00682#bib.bib26)\), retrieval\-augmented generation\([Toro et al\., 2024](https://arxiv.org/html/2610.00682#bib.bib24)\), or multi\-step reasoning pipelines\([Singh et al\., 2025](https://arxiv.org/html/2610.00682#bib.bib23)\)\. Structured domain ontologies, widely used across biomedicine, materials science, and other scientific fields, encode the formal knowledge underpinning scientific discovery workflows such as entity classification and data annotation, making correct LLM reasoning over these ontologies a prerequisite for reliable scientific AI\.

Benchmarking LLM logical reasoning over domain ontologies requires datasets that: 1\) ground entries in explicit background knowledge, and 2\) express statements in formal logic verifiable by a reasoner\. Such datasets serve multiple communities: scientific AI developers evaluating model fitness for scientific reasoning tasks; model builders extracting training signals to penalise specific reasoning errors; domain scientists validating LLM outputs against their knowledge base without formal logic expertise; and neuro\-symbolic researchers evaluating hybrid architectures\([Vsevolodovna and Monti, 2025](https://arxiv.org/html/2610.00682#bib.bib27)\)\. Manual benchmark construction requires expert verification of logical soundness, which is labour\-intensive and does not scale\. LLM\-based auto\-generation risks embedding the same reasoning flaws the benchmark aims to measure, since LLMs are prone to hallucinations\.

We propose a pipeline that automatically generates multiple\-choice question \(MCQ\) benchmarks from any sufficiently axiomatised Web Ontology Language \(OWL 2\) ontology\. Each MCQ has precisely one answer that is correct with respect to the ontology’s axioms, and distractors verified as incorrect against those same axioms by a reasoner\. Each pair is provided in two complementary forms: an NL verbalisation and the underlying symbolic representation\. The correct answers are derived from ontology class definition axioms, verbalizing their concept expression structure\. Distractors are generated by perturbing the right\-hand\-side class expressions of these axioms and their incorrectness is formally verified by an OWL reasoner via entailment checks\. Distractors span four semantic categories, from class unsatisfiability to weakened subsumptions, enabling diagnostic evaluation of specific reasoning failures\. We evaluate the pipeline on three ontologies: Pizza \(academic\)\([Horridge et al\., 2009](https://arxiv.org/html/2610.00682#bib.bib9)\), PMDco \(materials science\)\([Schilling et al\., 2026](https://arxiv.org/html/2610.00682#bib.bib21)\), and the Disease Ontology \(DOID, biomedical\)\([Schriml et al\., 2022](https://arxiv.org/html/2610.00682#bib.bib22)\)\. The pipeline is domain\-agnostic: applied to any sufficiently axiomatised OWL 2 ontology, it produces a benchmark grounded in that domain’s scientific knowledge\. Named domain concepts are retained by design, reflecting the target deployment context: scientific AI systems reason over specific ontologies where domain concepts are named, and a benchmark that strips them would not reflect this setting\. This work offers a significant step towards developing more reliable and accurate benchmarks for assessing the logical reasoning capabilities of next\-generation scientific AI systems\. The paper is organised as follows: Section 2 reviews the related work\. Section 3 presents the proposed pipeline\. Section 4 and Section 5 report the experiments and the conclusions\.

## 2Related Works

Existing benchmarks fail at least one of three requirements: grounding in domain ontologies, formal verification of both correct answers and distractors, and scalable automated construction\. OntoLAMA\([He et al\., 2023](https://arxiv.org/html/2610.00682#bib.bib8)\)probes subsumption entailment as a binary classification task, deriving positive samples with a symbolic reasoner\. Its negative samples rely on assumed disjointness theory but are not formally verified in practice\. LLM\-ORBench\([Loesch et al\., 2026](https://arxiv.org/html/2610.00682#bib.bib12)\)grounds true/false and open\-ended questions in ontology\-derived triples verified by a reasoner\. It does not specify how false examples are constructed, leaving distractor type undefined\. OntoURL\([Zhang et al\., 2025](https://arxiv.org/html/2610.00682#bib.bib30)\)broadens coverage to 57,303 MCQs and applies a reasoner to derive inferred relations\. Its distractors are drawn from structurally related entities such as ancestors and siblings, without formal verification of their incorrectness\. It uses named classes as distractors, reducing the task to named entity recall\. MALLS\([Yang et al\., 2024](https://arxiv.org/html/2610.00682#bib.bib29)\)generates NL–first\-order logic \(FOL\) pairs via LLM; its authors acknowledge these as silver\-label data requiring gold\-standard benchmarks for reliable evaluation\. FOLIO\([Han et al\., 2024](https://arxiv.org/html/2610.00682#bib.bib5)\)provides formally grounded, verifier\-checked natural language reasoning examples\. However, its 1,435 examples required approximately 980 expert annotation hours, and it targets general FOL over Wikipedia rather than structured domain knowledge\.

## 3A Method for Generating MCQs from Ontology Class Definition Axioms

We present a four\-stage pipeline to automatically generate an MCQ benchmark from any sufficiently axiomatised OWL 2 ontology\. The high\-level workflow \(Figure[1](https://arxiv.org/html/2610.00682#S3.F1), top\) proceeds as follows:

Stage 1\(Axiom extraction and perturbation\):Class definition axioms are selected from the ontology to ground MCQ generation\. Each axiom is perturbed to generate concept distractors\.

Stage 2\(Verbalisation and smoothing\):The description logic \(DL\) expressions for both axioms and distractors are verbalised into fluent NL\.

Stage 3\(Distractor ranking and selection\):Not all distractors are equally challenging, so they are ranked to identify the top\-kkhardest\-to\-reject distractors\.

![Refer to caption](https://arxiv.org/html/2610.00682v1/IMAGE3-WORKFLOW.png)Figure 1:Four\-stage pipeline for generating ontology\-grounded multiple\-choice questions\. Stages proceed left to right and the bottom row illustrates each stage with an example from PMDco\.Stage 4\(MCQ assembly and quality filtering\):A question stem \(the instruction that precedes the options and defines what is being evaluated\) is generated for each record\. Options are shuffled and assembled into a complete MCQ; each is scored by an LLM judge and only high\-quality items are retained\.

The MCQ format makes evaluation objective and reproducible: exactly one correct answer, no additional annotation, and difficulty controllable through distractor design\. Existing ontology\-based benchmarks share this format but use named classes as distractors; our pipeline instead generates complex class expressions, shifting the challenge from named entity recall to ontological reasoning\. The following subsections describe each stage, illustrated by a running example from PMDco \(Figure[1](https://arxiv.org/html/2610.00682#S3.F1), bottom row\)\.

### 3\.1Generating Concept Distractors by Perturbation

We consider class definition axioms of the formA⊑CA\\sqsubseteq C, whereAAis a named OWL class andCCis a complex class expression\. We assume access to the inferred class hierarchy of named classes in𝒪\\mathcal\{O\}:ℋ=\{A1⊑A2:𝒪⊧A1⊑A2,A1,A2∈σ\(𝒪\)\}\\mathcal\{H\}=\\\{A\_\{1\}\\sqsubseteq A\_\{2\}:\\mathcal\{O\}\\models A\_\{1\}\\sqsubseteq A\_\{2\},\\ A\_\{1\},A\_\{2\}\\in\\sigma\(\\mathcal\{O\}\)\\\}\.

For example, consider the class definition axiom from the PMDco materials ontology:

GrainBoundary⊑=2memberOf\.\(Crystal⊓∃hasRelationalQuality\.AngleOfMisalignment\)\\textit\{GrainBoundary\}\\sqsubseteq\\ \{=\}2\\,\\textit\{memberOf\}\.\(\\textit\{Crystal\}\\ \\sqcap\\ \\exists\\textit\{hasRelationalQuality\}\.\\textit\{AngleOfMisalignment\}\)\(1\)This axiom defines a grain boundary as a class with exactly two members, each a crystal bearing some angle of misalignment as a relational quality\.ℋ\\mathcal\{H\}provides, for example, that every alloy crystal is also a crystal \(AlloyCrystal⊑Crystal\\textit\{AlloyCrystal\}\\sqsubseteq\\textit\{Crystal\}\)\.

We generate distractor candidates for a class definition axiomA⊑CA\\sqsubseteq Cby applying perturbation operators toCC\.

###### Definition 1\(Concept Distractor and Perturbation Operator\)\.

A*concept distractor*forCCis a concept expressionC′C^\{\\prime\}in the vocabulary of𝒪\\mathcal\{O\}withC≢C′C\\not\\equiv C^\{\\prime\}\. A*perturbation operator*π\\pimapsCCto a finite setπ⁡\(C\)=\{C1′,C2′,…\}\\pi\(C\)=\\\{C^\{\\prime\}\_\{1\},C^\{\\prime\}\_\{2\},\\ldots\\\}, where eachCi′C^\{\\prime\}\_\{i\}is expressed in the vocabulary of𝒪\\mathcal\{O\}\. We writeC\[p←v′\]C\[p\\leftarrow v^\{\\prime\}\]for replacing the valuevvat positionppwithv′v^\{\\prime\}\(single\-position substitution\), andC\[v↞v′\]C\[v\\twoheadleftarrow v^\{\\prime\}\]for replacing all occurrences ofvvinCC\(global substitution\)\.

For example, the concept expression in Eq\.[2](https://arxiv.org/html/2610.00682#S3.E2)is a concept distractor for the right\-hand side of Eq\.[1](https://arxiv.org/html/2610.00682#S3.E1): it uses only vocabulary of𝒪\\mathcal\{O\}but requires*some*crystal member rather than*exactly two*\.

∃memberOf\.\(Crystal⊓∃hasRelationalQuality\.AngleOfMisalignment\)\\exists\\,\\textit\{memberOf\}\.\(\\textit\{Crystal\}\\sqcap\\exists\\,\\textit\{hasRelationalQuality\}\.\\textit\{AngleOfMisalignment\}\)\(2\)
Each operatorπ\\pitargets a positionppinCC, which may be a named class, role, cardinality bound, restriction kind \(existential, universal, exact, min, or max\), or Boolean constructor, and draws a replacementv′v^\{\\prime\}from an operator\-specific source set𝒮π​\(p,C\)\\mathcal\{S\}\_\{\\pi\}\(p,C\), yieldingCi′=C\[p←v′\]C^\{\\prime\}\_\{i\}=C\[p\\leftarrow v^\{\\prime\}\]orC\[v↞v′\]C\[v\\twoheadleftarrow v^\{\\prime\}\]\. Each operator is characterised by its target type, source set𝒮π\\mathcal\{S\}\_\{\\pi\}, an optional guard condition onCCorpp, and an optional output cap that bounds\|π⁡\(C\)\|\|\\pi\(C\)\|; Table[1](https://arxiv.org/html/2610.00682#S3.T1)summarises all operators\.

Consider operatorπQ1\\pi\_\{Q\_\{1\}\}applied to Eq\.[1](https://arxiv.org/html/2610.00682#S3.E1)\. The target positionppis the exact cardinality constructor=2\{=\}2in=2​memberOf\{=\}2\\;\\textit\{memberOf\}; the source set𝒮πQ1=\{∃\}\\mathcal\{S\}\_\{\\pi\_\{Q\_\{1\}\}\}=\\\{\\exists\\\}, so the replacementv′v^\{\\prime\}is the existential constructor∃\\exists\. The substitutionC\[p←v′\]C\[p\\leftarrow v^\{\\prime\}\]yields Eq\.[2](https://arxiv.org/html/2610.00682#S3.E2), leaving the rest of the expression unchanged\.

Table 1:Formal Perturbation Operatorsπ\\pi\.We illustrate each operator on Eq\.[1](https://arxiv.org/html/2610.00682#S3.E1)\.

Filler substitution \(πF1\\pi\_\{F\_\{1\}\}–πF4\\pi\_\{F\_\{4\}\}\)\.OperatorsπF1\\pi\_\{F\_\{1\}\}throughπF4\\pi\_\{F\_\{4\}\}each target a named atomic classBBappearing as a filler inCCand replace it globally with a class drawn from a position\-specific source set inℋ\\mathcal\{H\}\. For example,πF3\\pi\_\{F\_\{3\}\}targets the fillerCrystaland replaces it with each of its direct children inℋ\\mathcal\{H\}\. Sinceℋ\\mathcal\{H\}containsAlloyCrystal⊑Crystal\\textit\{AlloyCrystal\}\\sqsubseteq\\textit\{Crystal\}, a candidate produced byπF3\\pi\_\{F\_\{3\}\}is

=2memberOf\.\(AlloyCrystal⊓∃hasRelationalQuality\.AngleOfMisalignment\)\{=\}2\\;\\textit\{memberOf\}\.\(\\textit\{AlloyCrystal\}\\;\\sqcap\\;\\exists\\,\\textit\{hasRelationalQuality\}\.\\textit\{AngleOfMisalignment\}\)\(3\)Only the filler is modified; the restriction kind, role, and remaining conjunct are unchanged\.πF1\\pi\_\{F\_\{1\}\}replacesBBwith the siblings ofBBand their descendants\.πF2\\pi\_\{F\_\{2\}\}replacesBBwith each of its ancestors inℋ\\mathcal\{H\}\. By contrast,πF4\\pi\_\{F\_\{4\}\}replacesBBwith a class from the disjointness index𝒟⁡\[B\]\\mathcal\{D\}\[B\], the set of classes disjoint withBBin𝒪\\mathcal\{O\}\.

πF1\\pi\_\{F\_\{1\}\}andπF4\\pi\_\{F\_\{4\}\}include a guard that skips anyCCcontaining a universal restriction∀r\.E\\forall r\.E\. In such expressions, replacing the filler with a sibling or disjoint class produces a candidate rejectable from the expression structure alone, without ontology knowledge; such distractors do not test the target reasoning skill and are excluded\. To keep the candidate pool tractable for large\|ℋ\|\|\\mathcal\{H\}\|, the operators apply output caps: descendants to depthNNforπF1\\pi\_\{F\_\{1\}\}, up toPPdirect children forπF3\\pi\_\{F\_\{3\}\}, and up toMMdisjoint classes forπF4\\pi\_\{F\_\{4\}\}\.

Cardinality bound modification \(πS1\\pi\_\{S\_\{1\}\}\)\.OperatorπS1\\pi\_\{S\_\{1\}\}targets the cardinality boundnnin a top\-level restriction⋈nr\.E\{\\bowtie\}\_\{n\}\\,r\.E, where⋈∈\{=,≥,≤\}\{\\bowtie\}\\in\\\{=,\\geq,\\leq\\\}is the restriction kind,rra role, andEEa concept expression\. It produces up to two candidates by replacingnnwithn\+1n\+1andn−1n\-1\. Applied to the top\-level restriction=2​memberOf\{=\}2\\;\\textit\{memberOf\}inCC,πS1\\pi\_\{S\_\{1\}\}produces

C1′≡=3memberOf\.\(Crystal⊓∃hasRelationalQuality\.AngleOfMisalignment\)C^\{\\prime\}\_\{1\}\\equiv\{=\}3\\;\\textit\{memberOf\}\.\(\\textit\{Crystal\}\\;\\sqcap\\;\\exists\\,\\textit\{hasRelationalQuality\}\.\\textit\{AngleOfMisalignment\}\)\(4\)C2′≡=1memberOf\.\(Crystal⊓∃hasRelationalQuality\.AngleOfMisalignment\)C^\{\\prime\}\_\{2\}\\equiv\{=\}1\\;\\textit\{memberOf\}\.\(\\textit\{Crystal\}\\;\\sqcap\\;\\exists\\,\\textit\{hasRelationalQuality\}\.\\textit\{AngleOfMisalignment\}\)\(5\)Both candidates are semantically distinct fromCC, since exact cardinality restrictions with different bounds are mutually inconsistent; then−1n\-1variant is skipped whenn=0n=0to avoid a negative bound\.

Restriction kind replacement \(πQ1\\pi\_\{Q\_\{1\}\}–πQ3\\pi\_\{Q\_\{3\}\}\)\.OperatorsπQ1\\pi\_\{Q\_\{1\}\}throughπQ3\\pi\_\{Q\_\{3\}\}each target the restriction kind at the top\-level restriction, leaving the role and filler unchanged\.πQ1\\pi\_\{Q\_\{1\}\}applies when the top\-level restriction is an exact cardinality=n​r\.E\{=\}n\\,r\.Eand replaces it with the existential∃r\.E\\exists r\.E, dropping the cardinality bound\. Applied toCC,πQ1\\pi\_\{Q\_\{1\}\}produces the single candidate in Eq\.[2](https://arxiv.org/html/2610.00682#S3.E2)\.πQ2\\pi\_\{Q\_\{2\}\}applies analogously when the top\-level restriction is a minimum cardinality≥n​r\.E\{\\geq\}\\,n\\,r\.E, again replacing it with∃r\.E\\exists r\.E\.πQ3\\pi\_\{Q\_\{3\}\}operates in the reverse direction: when the top\-level restriction is already existential∃r\.E\\exists r\.E, it replaces it with the exact restriction=1​r\.E\{=\}1\\,r\.E, introducing a cardinality constraint where none existed\. Since OWL 2 forbids cardinality restrictions on transitive properties,πQ3\\pi\_\{Q\_\{3\}\}skips existential restrictions whose role is transitive\.

Each candidateC′C^\{\\prime\}produced by a perturbation operator stands in a specific logical relationship to the original axiomA⊑CA\\sqsubseteq Cunder𝒪\\mathcal\{O\}\. This relationship determines what kind of reasoning is required to rejectC′C^\{\\prime\}as a wrong answer\. We formalise this as a semantic category

###### Definition 2\.

\[Semantic Category of Candidate Distractors\] Let𝒪\\mathcal\{O\}be an ontology,A⊑CA\\sqsubseteq Ca class definition axiom, andC′C^\{\\prime\}a concept expression obtained by applying a perturbation operator onCC\. The*semantic category*ofC′C^\{\\prime\}with respect to𝒪\\mathcal\{O\}andA⊑CA\\sqsubseteq Cis

category​\(C′\)=\{contradictionif𝒪⊧̸A⊑C′and𝒪⊧A⊓C′⊑⊥non\-entailed\-satisfiableif𝒪⊧̸A⊑C′and𝒪⊧̸A⊓C′⊑⊥weakeningif​𝒪⊧A⊑C′​and​𝒪⊧C⊑C′​and​𝒪⊧̸C′⊑Cincomparableif​𝒪⊧A⊑C′​and​𝒪⊧̸C⊑C′​and​𝒪⊧̸C′⊑Cstrengtheningif​𝒪⊧A⊑C′​and​𝒪⊧̸C⊑C′​and​𝒪⊧C′⊑Cequivalentif​𝒪⊧A⊑C′​and​𝒪⊧C⊑C′​and​𝒪⊧C′⊑C\\displaystyle\\text\{category\}\(C^\{\\prime\}\)=\\begin\{cases\}\\textit\{contradiction\}&\\text\{if \}\\mathcal\{O\}\\not\\models A\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\models A\\sqcap C^\{\\prime\}\\sqsubseteq\\bot\\\\\[4\.0pt\] \\textit\{non\-entailed\-satisfiable\}&\\text\{if \}\\mathcal\{O\}\\not\\models A\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\not\\models A\\sqcap C^\{\\prime\}\\sqsubseteq\\bot\\\\\[4\.0pt\] \\textit\{weakening\}&\\text\{if \}\\mathcal\{O\}\\models A\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\models C\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\not\\models C^\{\\prime\}\\sqsubseteq C\\\\\[4\.0pt\] \\textit\{incomparable\}&\\text\{if \}\\mathcal\{O\}\\models A\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\not\\models C\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\not\\models C^\{\\prime\}\\sqsubseteq C\\\\\[4\.0pt\] \\textit\{strengthening\}&\\text\{if \}\\mathcal\{O\}\\models A\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\not\\models C\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\models C^\{\\prime\}\\sqsubseteq C\\\\\[4\.0pt\] \\textit\{equivalent\}&\\text\{if \}\\mathcal\{O\}\\models A\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\models C\\sqsubseteq C^\{\\prime\}\\text\{ and \}\\mathcal\{O\}\\models C^\{\\prime\}\\sqsubseteq C\\end\{cases\}

The category labels*contradiction*,*weakening*, and*strengthening*, and the entailment checks used to assign them, are borrowed from ontology repair research\([Troquard et al\., 2018](https://arxiv.org/html/2610.00682#bib.bib25);[Colucci et al\., 2003](https://arxiv.org/html/2610.00682#bib.bib2)\), which characterises how a repair candidate relates to an inconsistent axiom\. We extend the taxonomy with*non\-entailed\-satisfiable*and*incomparable*, which complete the case analysis of the entailment check outcomes and have no counterpart in repair settings\.

A distractorC′C^\{\\prime\}is a*contradiction*ifAAandC′C^\{\\prime\}are disjoint under𝒪\\mathcal\{O\}, makingA⊓C′A\\sqcap C^\{\\prime\}unsatisfiable\. OperatorπS1\\pi\_\{S\_\{1\}\}produces such candidates: replacing the exact cardinality bound22with11\(Eq\.[5](https://arxiv.org/html/2610.00682#S3.E5)\) means no individual can simultaneously satisfy both the original and the perturbed definition\. By contrast, a distractorC′C^\{\\prime\}is a*weakening*ifC′C^\{\\prime\}is strictly more general thanCC\. OperatorπQ1\\pi\_\{Q\_\{1\}\}produces such candidates: replacing the exact cardinality restriction with an existential \(Eq\.[2](https://arxiv.org/html/2610.00682#S3.E2)\) yields a definition that admits a broader range of individuals\. Not all distractors, however, stand in a clear\-cut entailment or disjointness relationship withCC\. A distractorC′C^\{\\prime\}is*non\-entailed\-satisfiable*if𝒪\\mathcal\{O\}neither entailsA⊑C′A\\sqsubseteq C^\{\\prime\}nor derives a contradiction betweenAAandC′C^\{\\prime\}: the perturbed expression is consistent with𝒪\\mathcal\{O\}but does not hold forAA\. This typically arises from sibling or child substitutions \(πF1\\pi\_\{F\_\{1\}\},πF3\\pi\_\{F\_\{3\}\}\) involving classes without disjointness axioms: replacingCrystalwith a child class \(Eq\.[3](https://arxiv.org/html/2610.00682#S3.E3)\) is consistent since no disjointness axiom excludes it, but the ontology does not entail that every grain boundary has exactly two alloy crystal members\. A distractorC′C^\{\\prime\}is*incomparable*if𝒪\\mathcal\{O\}entailsA⊑C′A\\sqsubseteq C^\{\\prime\}butCCandC′C^\{\\prime\}are not related by subsumption in either direction, describing unrelated aspects ofAA\. For example, if𝒪\\mathcal\{O\}also entailsGrainBoundary⊑∃partOf\.Polycrystal\\textit\{GrainBoundary\}\\sqsubseteq\\exists\\textit\{partOf\}\.\\textit\{Polycrystal\}, thenC′=∃partOf\.PolycrystalC^\{\\prime\}=\\exists\\textit\{partOf\}\.\\textit\{Polycrystal\}is incomparable withCC\. A*strengthening*makesC′C^\{\\prime\}strictly more specific thanCC: for example, adding∃partOf\.Polycrystal\\exists\\textit\{partOf\}\.\\textit\{Polycrystal\}as a conjunct yieldsC′=C⊓∃partOf\.PolycrystalC^\{\\prime\}=C\\sqcap\\exists\\textit\{partOf\}\.\\textit\{Polycrystal\}, which is subsumed byCCbut does not subsume it\. The most subtle case is*equivalence*:C′C^\{\\prime\}andCCsubsume each other under𝒪\\mathcal\{O\}, makingC′C^\{\\prime\}semantically indistinguishable from the correct answer\.

Each operator in Table[1](https://arxiv.org/html/2610.00682#S3.T1)is applied toCC, and each resulting candidate is evaluated against𝒪\\mathcal\{O\}using an OWL reasoner to determine its semantic category \(Definition 3\)\. This requires four reasoner checks per candidate:𝒪⊧A⊑C′\\mathcal\{O\}\\models A\\sqsubseteq C^\{\\prime\}\(entailment\),𝒪⊧A⊓C′⊑⊥\\mathcal\{O\}\\models A\\sqcap C^\{\\prime\}\\sqsubseteq\\bot\(satisfiability\), and𝒪⊧C⊑C′\\mathcal\{O\}\\models C\\sqsubseteq C^\{\\prime\}and𝒪⊧C′⊑C\\mathcal\{O\}\\models C^\{\\prime\}\\sqsubseteq C\(subsumption in both directions\)\. Candidates classified asequivalentorstrengtheningare also correct answers and are discarded; the remaining candidates, in the four valid categories, form the distractor pool for the axiom\.111Operators that guarantee a fixed semantic category would remove the need for post\-hoc reasoning checks but must account for ontology entailments and may still not yield sufficient candidates; we leave this to future work\.

### 3\.2Verbalisation of Concept Expressions

Both the correct expression and the distractors must be presented as readable text, so they are verbalised into NL as MCQ options\. Verbalisation begins withDeepOnto\([He et al\., 2023](https://arxiv.org/html/2610.00682#bib.bib8)\), the established rule\-based ontology verbaliser, which recursively applies fixed linguistic patterns to each constructor in the expression, producing deterministic output\. However,DeepOntocovers only the𝒜​ℒ​𝒞\\mathcal\{ALC\}fragment of OWL 2, so constructs such asowl:hasSelfand nominal sets may receive incomplete or unnatural verbalisations\. Each verbalisation is thereforesmoothedusing an LLM with a fixed prompt template that receives both theDeepOntoverbalisation and the underlying DL expression; the LLM rewrites for fluency and grammatical completeness, with the logical content anchored by the expression rather than generated freely\.222The LLM judge’s option\-faithfulness dimension \(Section[3\.4](https://arxiv.org/html/2610.00682#S3.SS4)\) provides a quality signal for the smoothed verbalisations\.For example, the distractor from Eq\.[2](https://arxiv.org/html/2610.00682#S3.E2)is first verbalised as*“something that member of crystal that has some relational quality angle of misalignment”*and then smoothed to*“something that has some member that is a crystal that has some angle of misalignment as a relational quality”*\.

### 3\.3Metrics

We measure syntactic complexity by the*operator count*𝚘𝚌⁡\(C\)\\mathtt\{oc\}\(C\): the number of occurrences of the keywordssome,only,and,or,not,min,max, andexactlyin the Manchester Syntax rendering ofCC\.𝚘𝚌⁡\(C\)\\mathtt\{oc\}\(C\)is computable from the expression string alone and is used to rank axioms by complexity and to match distractors structurally to the correct expression \(Section[3\.4](https://arxiv.org/html/2610.00682#S3.SS4)\)\. All operators in Table[1](https://arxiv.org/html/2610.00682#S3.T1)preserve the operator count by design: each substitutes a value at a fixed structural position without adding or removing a constructor, so every distractor has the same syntactic complexity as the correct expression \(𝚘𝚌⁡\(C′\)=𝚘𝚌⁡\(C\)\\mathtt\{oc\}\(C^\{\\prime\}\)=\\mathtt\{oc\}\(C\)\) and cannot be eliminated by comparing structure alone\.333𝚘𝚌⁡\(C\)\\mathtt\{oc\}\(C\)is a syntactic approximation of formal concept complexity measures such as description\-tree complexity\([Distel et al\., 2014](https://arxiv.org/html/2610.00682#bib.bib4)\), which are unsuitable here as they cover only EL rather than the full𝒮​ℛ​𝒪​ℐ​𝒬\\mathcal\{SROIQ\}expressivity of OWL 2\.

Concept expressions that differ minimally in NL are harder for LLMs to distinguish\([He et al\., 2025](https://arxiv.org/html/2610.00682#bib.bib7)\)and require formal reasoning, so we define a similarity metric over their verbalisations, used for distractor ranking and class selection \(Section[3\.4](https://arxiv.org/html/2610.00682#S3.SS4)\):

𝚜𝚒𝚖⁡\(C,C′\)=𝐞​\(𝚜𝚖𝚘𝚘𝚝𝚑⁡\(C\)\)⊤​𝐞​\(𝚜𝚖𝚘𝚘𝚝𝚑⁡\(C′\)\)‖𝐞⁡\(𝚜𝚖𝚘𝚘𝚝𝚑⁡\(C\)\)‖​‖𝐞⁡\(𝚜𝚖𝚘𝚘𝚝𝚑⁡\(C′\)\)‖\\mathtt\{sim\}\(C,C^\{\\prime\}\)\\;=\\;\\frac\{\\mathbf\{e\}\(\\mathtt\{smooth\}\(C\)\)^\{\\top\}\\,\\mathbf\{e\}\(\\mathtt\{smooth\}\(C^\{\\prime\}\)\)\}\{\\\|\\mathbf\{e\}\(\\mathtt\{smooth\}\(C\)\)\\\|\\;\\\|\\mathbf\{e\}\(\\mathtt\{smooth\}\(C^\{\\prime\}\)\)\\\|\}\(6\)where𝐞⁡\(⋅\)\\mathbf\{e\}\(\\cdot\)denotes the text\-embedding function and𝚜𝚖𝚘𝚘𝚝𝚑⁡\(C\)\\mathtt\{smooth\}\(C\)the smoothed natural\-language verbalisation ofCCfrom Stage 2\. For example, for the grain boundary axiom, the three highest\-ranked distractors are the child crystal swaps \(𝚜𝚒𝚖=0\.976\\mathtt\{sim\}=0\.976,0\.9660\.966,0\.9540\.954\), while the cardinality contradiction \(𝚜𝚒𝚖=0\.909\\mathtt\{sim\}=0\.909\) and the existential weakening \(𝚜𝚒𝚖=0\.856\\mathtt\{sim\}=0\.856\) rank lower\.

### 3\.4Overall Pipeline

Stage 1 produces two outputs from𝒪\\mathcal\{O\}: a set𝒢\\mathcal\{G\}of class\-indexed axiom groups each sorted by descending𝚘𝚌⁡\(C\)\\mathtt\{oc\}\(C\), and a named\-class hierarchy indexℋ\\mathcal\{H\}built from inferredsubClassOftriples\. Two filters are applied:MinDepthexcludes axioms whereCCis a single named class \(trivially answerable\), andPrimitivesexcludes axioms whose fillers are entirely upper ontology classes too generic for domain\-specific evaluation\. The remaining axioms form the working\-set, which is extended with inferred axioms: a reasoner propagates the complex expressions of each entailed superclass toAAasA⊑CA\\sqsubseteq C, with duplicate\(A,C\)\(A,C\)pairs removed\.MaxClassesPerAxiomcaps the number of classes sharing the sameCCfrom a common ancestor, preventing a single popular ancestor expression from dominating the benchmark; when exceeded, a greedy max\-min selection retains the most label\-diverse subset, measured by Eq\.[6](https://arxiv.org/html/2610.00682#S3.E6)over class labels fromℋ\\mathcal\{H\}\.

Distractor candidates are generated for each axiom in the working\-set, producing𝒲𝑓𝑜𝑟𝑚𝑎𝑙=\{\(A,C,𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟​\_​𝑝𝑜𝑜𝑙,𝚘𝚌⁡\(C\)\)\}\\mathcal\{W\}\_\{\\mathit\{formal\}\}=\\\{\(A,\\,C,\\,\\mathit\{distractor\\\_pool\},\\,\\mathtt\{oc\}\(C\)\)\\\}, where𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟​\_​𝑝𝑜𝑜𝑙=\{\(C′,𝑐𝑎𝑡𝑒𝑔𝑜𝑟𝑦⁡\(C′\)\)\}\\mathit\{distractor\\\_pool\}=\\\{\(C^\{\\prime\},\\,\\mathit\{category\}\(C^\{\\prime\}\)\)\\\}\. The disjoint index𝒟\\mathcal\{D\}is built by scanning𝒪\\mathcal\{O\}for disjointness axioms and expanding each entry to descendants viaℋ\\mathcal\{H\}\. Operators are applied to each axiom in descending𝚘𝚌⁡\(C\)\\mathtt\{oc\}\(C\)order; when a class exceedsMaxAxiomsPerClass, only its most complex axioms are retained, ensuring representative coverage\. An axiom is included in𝒲𝑓𝑜𝑟𝑚𝑎𝑙\\mathcal\{W\}\_\{\\mathit\{formal\}\}only if its distractor pool contains at leastMinDistrvalid candidates; axioms below this threshold cannot yield complete MCQs\.

In Stage 2, every concept expression in𝒲𝑓𝑜𝑟𝑚𝑎𝑙\\mathcal\{W\}\_\{\\mathit\{formal\}\}is verbalised as described in Section[3\.2](https://arxiv.org/html/2610.00682#S3.SS2)\.

In Stage 3, each record is assigned its top\-TopKdistractors, ranked first byCategoryRank, prioritising categories that require more precise formal reasoning \(contradiction, weakening\), then by descending𝚜𝚒𝚖⁡\(C,C′\)\\mathtt\{sim\}\(C,C^\{\\prime\}\)\(Eq\.[6](https://arxiv.org/html/2610.00682#S3.E6)\) within each category\. Category rank thus controls the reasoning\-type composition, while similarity maximises NL difficulty\. For the grain boundary axiom \(TopK=3\), the selected distractors are the cardinality contradiction \(𝚜𝚒𝚖=0\.909\\mathtt\{sim\}=0\.909\), the existential weakening \(𝚜𝚒𝚖=0\.856\\mathtt\{sim\}=0\.856\), and a child\-filler non\-entailed\-satisfiable candidate \(𝚜𝚒𝚖=0\.976\\mathtt\{sim\}=0\.976\); the last ranks third despite its higher similarity because category rank takes precedence\.

In Stage 4, each record is assembled into a complete MCQ and subjected to quality filtering, producing𝒲m​c​q\\mathcal\{W\}\_\{mcq\}\. Two stem variants are generated: a*template stem*that fills a fixed pattern with the class label \(e\.g\., “Which of the following best describes grain boundary?”\) and, since fixed templates cannot produce domain\-contextualised prose, a*scenario stem*generated by an LLM from the class label and domain description\. To prevent the stem wording from hinting at the correct answer, the LLM prompt includes a blocklist of non\-stopword content tokens extracted from the smoothed verbalisations ofCCand allC′C^\{\\prime\}, forbidden in the stem\. For the grain boundary record, the domain description is “materials engineering” and the blocklist is \[exactly, member, crystal, angle, misalignment, relational, quality, alloy, each\], producing the scenario stem: “When evaluating the microstructure of a polycrystalline metal, which of the following best describes a grain boundary?”\. The four options are assembled by randomly shuffling the correct answer and the top\-TopKdistractors, giving a random\-guessing baseline of100TopK\+1\\frac\{100\}\{\\textsc\{TopK\}\+1\}% \(25% whenTopK=3\\textsc\{TopK\}=3\)\. The complete assembled MCQ for the grain boundary record is shown in Fig\.[1](https://arxiv.org/html/2610.00682#S3.F1)\. Correctness with respect to the ontology’s axiom set, and structural diversity, are guaranteed by design, but the NL quality of the assembled MCQ requires a separate check: following work showing that LLM judges are effective for filtering large MCQ benchmarks\([Hashemi et al\., 2024](https://arxiv.org/html/2610.00682#bib.bib6)\), an LLM judge scores each item on three dimensions \(integer 1–5\): option faithfulness, stem clarity, and domain relevance\. The judge prompt is a fixed template that includes the MCQ together with the DL expressions of the class definition axiom and the distractor expressions\. Records whose mean score meets or exceedsQualityThreshare retained in𝒲m​c​q\\mathcal\{W\}\_\{mcq\}\. The pipeline pseudocode is provided in the Appendix\.

## 4Experiments

Experiments validate three claims: 1\) the pipeline produces MCQs grounded in the input ontology, provided it is sufficiently axiomatised; 2\) the distractors are formally incorrect with respect to the ontology and test distinct forms of logical reasoning; 3\) the MCQs meet the natural language quality standard required for a meaningful benchmark\.

Setup\.We consider three ontologies with contrasting scale and axiomatisation depth: 1\) Pizza \(85 classes, 77 disjointness declarations, 159 working\-set axioms,𝚘𝚌≤2\\mathtt\{oc\}\\leq 2, mean 1\.28\); 2\) PMDco \(1,071 classes, 15 disjointness declarations, 2,727 working\-set axioms,𝚘𝚌⁡\(C\)\\mathtt\{oc\}\(C\)up to 6, mean 1\.55, 299 axioms with𝚘𝚌⁡\(C\)≥3\\mathtt\{oc\}\(C\)\\geq 3\); and 3\) DOID \(9,969 classes, 26 disjointness declarations, 19,010 working\-set axioms,𝚘𝚌⁡\(C\)\\mathtt\{oc\}\(C\)up to 17, mean 1\.14, 679 axioms with𝚘𝚌⁡\(C\)≥3\\mathtt\{oc\}\(C\)\\geq 3\)\.

The pipeline usesTopK=3\\textsc\{TopK\}\{=\}3,MinDistr=3\\textsc\{MinDistr\}\{=\}3,QualityThresh=3\.0\\textsc\{QualityThresh\}\{=\}3\.0, andSeed=42\\textsc\{Seed\}\{=\}42; distractors are ranked byCategoryRank=\[contradiction≻weakening≻non\_entailed\_satisfiable≻incomparable\]\\textsc\{CategoryRank\}=\[\\textit\{contradiction\}\\succ\\textit\{weakening\}\\succ\\textit\{non\\\_entailed\\\_satisfiable\}\\succ\\textit\{incomparable\}\]\. HermiT 1\.3\.8 accessed via Owlready2\([Lamy, 2017](https://arxiv.org/html/2610.00682#bib.bib10)\)is used as the reasoner\. Stage 2 smoothing and Stage 4 stem generation use GPT\-4\.1\([OpenAI, 2025](https://arxiv.org/html/2610.00682#bib.bib17)\), Stage 4 quality judging uses GPT\-5\.4\([OpenAI, 2026a](https://arxiv.org/html/2610.00682#bib.bib18)\), and Stage 3 similarity uses text\-embedding\-3\-small\([OpenAI, 2024b](https://arxiv.org/html/2610.00682#bib.bib16)\)\. Full implementation details including operator caps and prompts are provided in the Appendix\.

Pipeline Productivity\.With this configuration, Pizza yields 112 MCQs; PMDco 2,491; and DOID 15,216 \(Table[3](https://arxiv.org/html/2610.00682#S4.T3)\)\. Example MCQs are in Fig\.[2](https://arxiv.org/html/2610.00682#S4.F2)\(Pizza and DOID\) and Fig\.[1](https://arxiv.org/html/2610.00682#S3.F1)\(PMDco\), each showing the question, correct answer, DL grounding, and HermiT\-verified distractor category\. Every MCQ is grounded in an ontology axiom, validating Claim 1\.

Formal Quality\.Every correct answer is a class definition axiom; every distractor is HermiT\-verified incorrect before entering the pool\. All four distractor categories are present in all three ontologies\. Pizza’s 77 disjointness declarations produce a high contradiction rate \(43\.5 %\); PMDco’s sparse disjointness shifts the distribution toward non\-entailed\-satisfiable \(61\.4 %\) and weakening \(36\.8 %\)\. DOID’s 26 disjointness declarations similarly suppress contradiction \(1\.9 %\), with the distribution splitting between weakening \(52\.3 %\) and non\-entailed\-satisfiable \(45\.7 %\), reflecting its predominantly existential restriction axioms\. The distractor category distribution thus mirrors each ontology’s original axiomatisation rather than a distribution imposed by the pipeline\. These results validate Claim 2\.

![Refer to caption](https://arxiv.org/html/2610.00682v1/example_mcq.png)Figure 2:Example of MCQ generated using the proposed pipeline from Pizza \(left\) and DOID\.Table 2:Pipeline results across three ontologies: Pizza, PMDCo, and DOID\.
Table 3:LLM accuracy \(%\)\.∘open†reason∙frontier; random baseline: 25%

NL Quality\.Mean distractor similarity \(Eq\.[6](https://arxiv.org/html/2610.00682#S3.E6)\) is 0\.922 \(Pizza\), 0\.810 \(PMDco\), and 0\.906 \(DOID\): distractors cannot be rejected on surface form alone\. Mean LLM judge score is 4\.02 \(Pizza\), 4\.36 \(PMDco\), and 3\.36 \(DOID\) out of 5, all above the scale midpoint\. Lower Pizza scores reflect its simpler axiom structure, which yields less domain\-specific stems; lower DOID scores reflect verbalisations that read unlike clinical prose, penalising domain relevance \(2\.27\) despite near\-perfect option faithfulness \(4\.80\)\. These results validate Claim 3\.

As a preliminary check, a domain expert independently scored 20 PMDco items\. Expert mean \(3\.33\) and LLM judge mean \(4\.0\) both exceed the scale midpoint, with a mean absolute difference of 1\.33, indicating that both raters rate quality similarly at the aggregate level and supporting the LLM judge as a practical quality filter; a larger human study with formal inter\-rater agreement \(e\.g\. Cohen’sκ\\kappa\) may be investigated in future work\.

Six LLMs \(frontier, open\-source, reasoning and non\-reasoning\) evaluated zero\-shot \(Table[3](https://arxiv.org/html/2610.00682#S4.T3)\) achieve 41\.1–76\.8% accuracy, well above the 25% random\-guessing baseline, confirming that the benchmarks are challenging and discriminative \(LLM details in Appendix, Table[5](https://arxiv.org/html/2610.00682#Ax1.T5)\)\.

## 5Conclusions

Validating LLM reasoning over structured domain knowledge remains an open challenge for reliable scientific AI: manual benchmark construction does not scale, and LLM\-generated benchmarks cannot be trusted to be logically sound\. This paper closes that gap with a pipeline that automatically turns any sufficiently axiomatised OWL 2 ontology into an MCQ benchmark, with every correct answer grounded in a class definition axiom and every distractor formally verified as incorrect by an OWL reasoner\. Applying the pipeline to three structurally contrasting ontologies \(Pizza, PMDco, and DOID\), we generated benchmarks of 112, 2,491, and 15,216 items with no manual annotation\. Practitioners building scientific AI systems can point the pipeline at their own domain ontology to obtain a diagnostic benchmark that reveals not just whether but where and how model reasoning breaks down, and to extract fine\-tuning signal or neuro\-symbolic supervision from the description logic formalisation and reasoner\-verified labels\. Future work includes extending the distractor operators, strengthening the DeepOnto verbalisation templates, and quantifying the effect of verbalisation and smoothing on benchmark quality\. The most promising direction is extending benchmark generation to derived axioms \(logical consequences entailed by the ontology but not explicitly asserted\), which probe deeper reasoning and better isolate reasoning ability from prior knowledge of public ontologies\. Initial experiments on Pizza, reusingπF2\\pi\_\{F\_\{2\}\}\(ancestor filler substitution\) to derive entailed axioms, already yield 191 additional MCQs\.

## References

- Arp et al\. \[2015\]Robert Arp, Barry Smith, and Andrew D Spear\.*Building Ontologies with Basic Formal Ontology*\.MIT Press, 2015\.
- Colucci et al\. \[2003\]Simona Colucci, T\. D\. Noia, Eugenio Di Sciascio, Francesco Maria Donini, and Marina Mongiello\.Concept Abduction and Contraction in Description Logics\.*Description Logics*, 2003\.URL[https://api\.semanticscholar\.org/CorpusID:38022677](https://api.semanticscholar.org/CorpusID:38022677)\.
- DeepSeek \[2025\]DeepSeek\.DeepSeek\-R1\-Distill\-Qwen\-32B\.[https://huggingface\.co/deepseek\-ai/DeepSeek\-R1\-Distill\-Qwen\-32B](https://huggingface.co/deepseek-ai/DeepSeek-R1-Distill-Qwen-32B), 2025\.
- Distel et al\. \[2014\]Felix Distel, I Bloch, and J Atif\.Concept Dissimilarity Based on Tree Edit Distance and Morphological Dilation\.In*21st European Conference on Artificial Intelligence \(ECAI\)*, 2014\.
- Han et al\. \[2024\]Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, Lucy Sun, Alexander Wardle\-Solano, Hannah Szabó, Ekaterina Zubova, Matthew Burtell, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, Ansong Ni, Linyong Nan, Jungo Kasai, Tao Yu, Rui Zhang, Alexander Fabbri, Wojciech Maciej Kryscinski, Semih Yavuz, Ye Liu, Xi Victoria Lin, Shafiq Joty, Yingbo Zhou, Caiming Xiong, Rex Ying, Arman Cohan, and Dragomir Radev\.FOLIO: Natural Language Reasoning With First\-Order Logic\.In Yaser Al\-Onaizan, Mohit Bansal, and Yun\-Nung Chen, editors,*Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing*, pages 22017–22031, Miami, Florida, USA, nov 2024\. Association for Computational Linguistics\.doi:10\.18653/v1/2024\.emnlp\-main\.1229\.URL[https://aclanthology\.org/2024\.emnlp\-main\.1229/](https://aclanthology.org/2024.emnlp-main.1229/)\.
- Hashemi et al\. \[2024\]Helia Hashemi, Jason Eisner, Corby Rosset, Benjamin Van Durme, and Chris Kedzie\.LLM\-Rubric: A Multidimensional, Calibrated Approach to Automated Evaluation of Natural Language Texts\.In*Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\)*, pages 13806–13834, 2024\.
- He et al\. \[2025\]Linyang He, Ercong Nie, Sukru Samet Dindar, Arsalan Firoozi, Adrian Florea, Van Nguyen, Corentin Puffay, Riki Shimizu, Haotian Ye, Jonathan Brennan, Helmut Schmid, Hinrich Schütze, and Nima Mesgarani\.XCOMPS: A Multilingual Benchmark of Conceptual Minimal Pairs\.In Michael Hahn, Priya Rani, Ritesh Kumar, Andreas Shcherbakov, Alexey Sorokin, Oleg Serikov, Ryan Cotterell, and Ekaterina Vylomova, editors,*Proceedings of the 7th Workshop on Research in Computational Linguistic Typology and Multilingual NLP*, pages 75–81, Vienna, Austria, August 2025\. Association for Computational Linguistics\.ISBN 979\-8\-89176\-281\-7\.doi:10\.18653/v1/2025\.sigtyp\-1\.9\.URL[https://aclanthology\.org/2025\.sigtyp\-1\.9/](https://aclanthology.org/2025.sigtyp-1.9/)\.
- He et al\. \[2023\]Yuan He, Jiaoyan Chen, Ernesto Jimenez\-Ruiz, Hang Dong, and Ian Horrocks\.Language Model Analysis for Ontology Subsumption Inference\.In*Findings of the Association for Computational Linguistics: ACL 2023*, pages 3439–3453, 2023\.
- Horridge et al\. \[2009\]Matthew Horridge, Simon Jupp, Georgina Moulton, Alan Rector, Robert Stevens, and Chris Wroe\.A Practical Guide to Building OWL Ontologies Using Protégé 4 and CO\-ODE Tools Edition 1\.3\.*The university of Manchester*, 107, 2009\.
- Lamy \[2017\]Jean\-Baptiste Lamy\.Owlready: Ontology\-oriented Programming in Python with Automatic Classification and High Level Constructs for Biomedical Ontologies\.*Artificial Intelligence in Medicine*, 80:11–28, 2017\.
- Liu et al\. \[2025\]Hanmeng Liu, Zhizhang Fu, Mengru Ding, Ruoxi Ning, Chaoli Zhang, Xiaozhang Liu, and Yue Zhang\.Logical Reasoning in Large Language Models: A Survey\.*arXiv preprint arXiv:2502\.09100*, 2025\.
- Loesch et al\. \[2026\]Julie Loesch, Rishabh Jakhar, Raghava Mutharaju, Michel Dumontier, and Remzi Celebi\.LLM\-ORBench: Designing a Benchmark Dataset for Complex Ontology\-Based Reasoning Tasks in Large Language Models, 2026\.URL[https://openreview\.net/forum?id=11ZzyjZEcc](https://openreview.net/forum?id=11ZzyjZEcc)\.
- Microsoft \[2025\]Microsoft\.Azure OpenAI REST API Reference\.[https://learn\.microsoft\.com/rest/api/azureopenai/](https://learn.microsoft.com/rest/api/azureopenai/), 2025\.API version 2025\-01\-01\-preview\.
- Mistral \[2025\]Mistral\.Ministral\-3\-14B\-Instruct\-2512\.[https://huggingface\.co/mistralai/Ministral\-3\-14B\-Instruct\-2512](https://huggingface.co/mistralai/Ministral-3-14B-Instruct-2512), 2025\.
- OpenAI \[2024a\]OpenAI\.Hello GPT\-4o\.[https://openai\.com/index/hello\-gpt\-4o/](https://openai.com/index/hello-gpt-4o/), 2024a\.
- OpenAI \[2024b\]OpenAI\.text\-embedding\-3\-small, 2024b\.URL[https://platform\.openai\.com/docs/models/text\-embedding\-3\-small](https://platform.openai.com/docs/models/text-embedding-3-small)\.OpenAI API model documentation\.
- OpenAI \[2025\]OpenAI\.Introducing GPT\-4\.1 in the API\.[https://openai\.com/index/gpt\-4\-1/](https://openai.com/index/gpt-4-1/), 2025\.
- OpenAI \[2026a\]OpenAI\.Introducing GPT\-5 for Developers\.[https://openai\.com/index/introducing\-gpt\-5\-for\-developers/](https://openai.com/index/introducing-gpt-5-for-developers/), 2026a\.
- OpenAI \[2026b\]OpenAI\.GPT\-5\.6\.[https://openai\.com/index/gpt\-5\-6/](https://openai.com/index/gpt-5-6/), 2026b\.
- Qwen \[2026\]Qwen\.Qwen3\.8\-27B\.[https://huggingface\.co/Qwen/Qwen3\.8\-27B](https://huggingface.co/Qwen/Qwen3.8-27B), 2026\.
- Schilling et al\. \[2026\]Markus Schilling, Philipp von Hartrott, Jörg Waitelonis, Thomas Hanke, Henk Birkholz, Hossein Beygi Nasrabadi, Khashayar Razghandi, Kamilla Zaripova, Felix Thonagel, Fabian Neuhaus, Martin Glauer, Lars Vogt, Harald Sack, Lutz Mädler, Bernd Bayerlein, and Chris Eberl\.Semantic Modeling in Materials Science and Engineering With Platform MaterialDigital Core Ontology 3\.0\.*Advanced Engineering Materials*, 2026\.
- Schriml et al\. \[2022\]Lynn M Schriml, James B Munro, Mike Schor, Dustin Olley, Carrie McCracken, Victor Felix, J Allen Baron, Rebecca Jackson, Susan M Bello, Cynthia Bearer, et al\.The Human Disease Ontology 2022 Update\.*Nucleic acids research*, 50\(D1\):D1255–D1261, 2022\.
- Singh et al\. \[2025\]Aditi Singh, Abul Ehtesham, Saket Kumar, Tala Talaei Khoei, and Athanasios V Vasilakos\.Agentic Retrieval\-augmented Generation: A Survey on Agentic RAG\.*arXiv preprint arXiv:2501\.09136*, 2025\.
- Toro et al\. \[2024\]Sabrina Toro, Anna V Anagnostopoulos, Susan M Bello, Kai Blumberg, Rhiannon Cameron, Leigh Carmody, Alexander D Diehl, Damion M Dooley, William D Duncan, Petra Fey, et al\.Dynamic retrieval augmented generation of ontologies using artificial intelligence \(DRAGON\-AI\)\.*Journal of Biomedical Semantics*, 15\(1\):19, 2024\.
- Troquard et al\. \[2018\]Nicolas Troquard, Roberto Confalonieri, Pietro Galliani, Rafael Penaloza, Daniele Porello, and Oliver Kutz\.Repairing Ontologies via Axiom Weakening\.In*Proceedings of the AAAI Conference on Artificial Intelligence*, volume 32, 2018\.
- Vaidya et al\. \[2025\]Nishtha N\. Vaidya, Thomas A\. Runkler, Thomas Hubauer, Veronika Haderlein\-Hoegberg, and Maja Milicic Brandt\.Conceptual In\-Context Learning and Chain of Concepts: Solving Complex Conceptual Problems Using Large Language Models\.In*2025 IEEE Symposium on Computational Intelligence in Natural Language Processing and Social Media \(CI\-NLPSoMe\)*, pages 1–7, 2025\.doi:10\.1109/CI\-NLPSoMe64976\.2025\.10970773\.
- Vsevolodovna and Monti \[2025\]Ruslan Idelfonso Magana Vsevolodovna and Marco Monti\.Enhancing Large Language Models Through Neuro\-symbolic Integration and Ontological Reasoning\.*arXiv preprint arXiv:2504\.07640*, 2025\.
- Wolf et al\. \[2020\]Thomas Wolf, Lysandre Debut, Victor Sanh, Julien Chaumond, Clement Delangue, Anthony Moi, Pierric Cistac, Tim Rault, Remi Louf, Morgan Funtowicz, Joe Davison, Sam Shleifer, Patrick von Platen, Clara Ma, Yacine Jernite, Julien Plu, Canwen Xu, Teven Le Scao, Sylvain Gugger, Mariama Drame, Quentin Lhoest, and Alexander Rush\.Transformers: State\-of\-the\-art natural language processing\.In*Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing: System Demonstrations*, pages 38–45\. Association for Computational Linguistics, 2020\.URL[https://aclanthology\.org/2020\.emnlp\-demos\.6](https://aclanthology.org/2020.emnlp-demos.6)\.
- Yang et al\. \[2024\]Yu’an Yang, Siheng Xiong, Ali Payani, Ehsan Shareghi, and Faramarz Fekri\.Harnessing the Power of Large Language Models for Natural Language to First\-Order Logic Translation\.In*Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\)*, pages 6942–6959, 2024\.
- Zhang et al\. \[2025\]Xiao Zhang, Huiyuan Lai, Qianru Meng, and Johan Bos\.OntoURL: A Benchmark for Evaluating Large Language Models on Symbolic Ontological Understanding, Reasoning and Learning\.*arXiv preprint arXiv:2505\.11031*, 2025\.

## Appendix

### LLM Usage Disclosure

LLMs are core components of the presented pipeline and the subjects of its evaluation; the models, roles, parameters, and prompt templates are described in Section 4 and this appendix\. An LLM assistant was additionally used only for writing, editing, or formatting purposes and did not impact the core methodology, scientific rigorousness, or originality of the research\.

### Full Pipeline Implementation Details

MaxClassesPerAxiom=3\\textsc\{MaxClassesPerAxiom\}\{=\}3,MaxAxiomsPerClass=3\\textsc\{MaxAxiomsPerClass\}\{=\}3; operatorπF\\pi\_\{F\}capsN=2N\{=\}2,P=4P\{=\}4,M=6M\{=\}6\(Table[1](https://arxiv.org/html/2610.00682#S3.T1)\); seeded shuffle \(Seed=42\\textsc\{Seed\}\{=\}42\) applied when multiple candidates share the same similarity score\. BFO\[[Arp et al\., 2015](https://arxiv.org/html/2610.00682#bib.bib1)\]classes are used as primitives for PMDco; none for Pizza\. The reasoner is HermiT 1\.3\.8 \(build 1\.3\.8\.1099\) via Owlready2 0\.50\[[Lamy, 2017](https://arxiv.org/html/2610.00682#bib.bib10)\], with a 180\-second timeout per call; axioms exceeding this limit are skipped\. Stage 2 smoothing uses GPT\-4\.1\[[OpenAI, 2025](https://arxiv.org/html/2610.00682#bib.bib17)\]\(temperature=0=0, max tokens=150=150\)\. Stage 3 similarity uses text\-embedding\-3\-small\[[OpenAI, 2024b](https://arxiv.org/html/2610.00682#bib.bib16)\]\(1536 dimensions\)\. Stage 4 stem generation uses GPT\-4\.1 \(temperature=0\.7=0\.7, max tokens=120=120\); quality judging uses GPT\-5\.4\[[OpenAI, 2026a](https://arxiv.org/html/2610.00682#bib.bib18)\]\(temperature=0=0, max tokens=200=200\)\. All models were selected based on availability during the period this research was conducted\. All GPT LLMs and text embedding models are accessed via Azure OpenAI\[[Microsoft, 2025](https://arxiv.org/html/2610.00682#bib.bib13)\]with all other parameters set to their defaults as per the Azure OpenAI API\.

### Overall Pipeline Algorithm

The overall pipeline with four stages is detailed in Algorithm[1](https://arxiv.org/html/2610.00682#alg1)\.

Algorithm 1Ontology\-grounded MCQ Benchmark Generation \(Overview\)1:\[User Inputs\] Ontology

𝒪\\mathcal\{O\}, domain description

DD
2:\[Parameters\]MinDepth: minimum operator count

𝚘𝚌⁡\(C\)\\mathtt\{oc\}\(C\),MaxClassesPerAxiom: max classes

AAretained per shared \(ancestor,

CC\) group,MaxAxiomsPerClass: max axioms perturbed per class

AA,MinDistr: minimum distractors required to retain an axiom,TopK: number of distractors selected per axiom for the MCQ,QualityThresh: minimum mean judge score to include a MCQ in the benchmark,Seed: random seed for template assignment and option shuffling,CategoryRank: distractor category preference order,

𝑃𝑟𝑖𝑚𝑖𝑡𝑖𝑣𝑒𝑠\\mathit\{Primitives\}: set of upper\-level ontology classes used to filter axioms,Templates: set of stem templates,SmoothPrompt: prompt template for smoothing,StemPrompt: prompt template for stem scenario generation,JudgePrompt: prompt template for MCQ quality scoring

3:\[API calls/ Tools\]DeepOnto: rules\-based verbaliser,Embed: text embedding model,LLM: LLM used for smoothing, stem generation, and judging

4:

𝒲m​c​q\\mathcal\{W\}\_\{mcq\}: quality\-filtered MCQ benchmark

5:// Stage 1: Formal Record Generation

6:

\(𝒢,ℋ\)←SelectAxioms​\(𝒪,MinDepth,MaxClassesPerAxiom,𝑃𝑟𝑖𝑚𝑖𝑡𝑖𝑣𝑒𝑠\)\(\\mathcal\{G\},\\;\\mathcal\{H\}\)\\leftarrow\\textsc\{SelectAxioms\}\(\\mathcal\{O\},\\ \\textsc\{MinDepth\},\\ \\textsc\{MaxClassesPerAxiom\},\\ \\mathit\{Primitives\}\)
7:

𝒲f​o​r​m​a​l←PerturbAndClassify​\(𝒪,𝒢,ℋ,MaxAxiomsPerClass,MinDistr\)\\mathcal\{W\}\_\{formal\}\\leftarrow\\textsc\{PerturbAndClassify\}\(\\mathcal\{O\},\\,\\mathcal\{G\},\\,\\mathcal\{H\},\\,\\textsc\{MaxAxiomsPerClass\},\\,\\textsc\{MinDistr\}\)⊳\\trianglerightrefer Operator Table[1](https://arxiv.org/html/2610.00682#S3.T1)

8:// Stage 2: Verbalisation & Smoothing

9:for all

\(A,C,𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟\_𝑝𝑜𝑜𝑙,⋅\)∈𝒲f​o​r​m​a​l\(A,\\,C,\\,\\mathit\{distractor\\\_pool\},\\,\\cdot\)\\in\\mathcal\{W\}\_\{formal\}do

10:for all

e∈\{C\}∪\{C′∣\(C′,⋅\)∈𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟​\_​𝑝𝑜𝑜𝑙\}e\\in\\\{C\\\}\\cup\\\{C^\{\\prime\}\\mid\(C^\{\\prime\},\\cdot\)\\in\\mathit\{distractor\\\_pool\}\\\}do

11:Verbalise

eew\.r\.t\.

𝒪\\mathcal\{O\}viaDeepOnto; smooth via

LLM​\(SmoothPrompt\)\\textsc\{LLM\}\(\\textsc\{SmoothPrompt\}\); store as

smooth⁡\(e\)\\mathrm\{smooth\}\(e\)
12:endfor

13:endfor

14:// Stage 3: Distractor Ranking

15:for all

\(A,C,𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟\_𝑝𝑜𝑜𝑙,⋅\)∈𝒲f​o​r​m​a​l\(A,\\,C,\\,\\mathit\{distractor\\\_pool\},\\,\\cdot\)\\in\\mathcal\{W\}\_\{formal\}do

16:for all

\(C′,⋅\)∈𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟​\_​𝑝𝑜𝑜𝑙\(C^\{\\prime\},\\,\\cdot\)\\in\\mathit\{distractor\\\_pool\}do

17:

sim⁡\(C,C′\)\\mathrm\{sim\}\(C,C^\{\\prime\}\)⊳\\trianglerightEq\.[6](https://arxiv.org/html/2610.00682#S3.E6)

18:endfor

19:Sort

𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟​\_​𝑝𝑜𝑜𝑙\\mathit\{distractor\\\_pool\}by

CategoryRank​\(𝑐𝑎𝑡𝑒𝑔𝑜𝑟𝑦\)\\textsc\{CategoryRank\}\(\\mathit\{category\}\), then by

sim⁡\(C,C′\)↓\\mathrm\{sim\}\(C,C^\{\\prime\}\)\\downarrowwithin each category

20:

𝑡𝑜𝑝​\_​k←\\mathit\{top\\\_k\}\\leftarrowtopTopKcandidates from sorted pool⊳\\triangleright↓\\downarrow: descending order

21:endfor

22:// Stage 4: MCQ Assembly & Quality Filtering

23:

𝒲m​c​q←∅\\mathcal\{W\}\_\{mcq\}\\leftarrow\\emptyset
24:for all

\(A,C,𝑡𝑜𝑝\_k,⋅\)∈𝒲f​o​r​m​a​l\(A,\\,C,\\,\\mathit\{top\\\_k\},\\,\\cdot\)\\in\\mathcal\{W\}\_\{formal\}do

25:

𝑠𝑡𝑒𝑚T←\\mathit\{stem\}\_\{T\}\\leftarrowtemplate for

label⁡\(A,ℋ\)\\mathrm\{label\}\(A,\\mathcal\{H\}\)fromTemplatesusingSeed

26:

𝑠𝑡𝑒𝑚S←LLM​\(StemPrompt​\(label⁡\(A,ℋ\),D,blocklist⁡\(C,𝑡𝑜𝑝​\_​k\)\)\)\\mathit\{stem\}\_\{S\}\\leftarrow\\textsc\{LLM\}\\bigl\(\\textsc\{StemPrompt\}\(\\mathrm\{label\}\(A,\\mathcal\{H\}\),\\,D,\\,\\mathrm\{blocklist\}\(C,\\,\\mathit\{top\\\_k\}\)\)\\bigr\)⊳\\trianglerightblocklist: content words ofsmooth⁡\(C\)\\mathrm\{smooth\}\(C\)and allsmooth⁡\(C′\)\\mathrm\{smooth\}\(C^\{\\prime\}\), forbidden in stem

27:

\(𝑜𝑝𝑡𝑠,𝑎𝑛𝑠\)←shuffle⁡\(\{C\}∪𝑡𝑜𝑝​\_​k,Seed\)\(\\mathit\{opts\},\\,\\mathit\{ans\}\)\\leftarrow\\mathrm\{shuffle\}\\bigl\(\\\{C\\\}\\cup\\mathit\{top\\\_k\},\\;\\textsc\{Seed\}\\bigr\)
28:

𝑠𝑐𝑜𝑟𝑒𝑠←LLM​\(JudgePrompt​\(𝑠𝑡𝑒𝑚S,𝑜𝑝𝑡𝑠,𝑎𝑛𝑠,A,C,C′\)\)\\mathit\{scores\}\\leftarrow\\textsc\{LLM\}\\bigl\(\\textsc\{JudgePrompt\}\(\\mathit\{stem\}\_\{S\},\\,\\mathit\{opts\},\\,\\mathit\{ans\},A,C,C^\{\\prime\}\)\\bigr\)
29:if

mean⁡\(𝑠𝑐𝑜𝑟𝑒𝑠\)≥QualityThresh\\mathrm\{mean\}\(\\mathit\{scores\}\)\\geq\\textsc\{QualityThresh\}then

30:

𝒲m​c​q←𝒲m​c​q∪\{\(A,C,𝑡𝑜𝑝​\_​k,𝑠𝑡𝑒𝑚T,𝑠𝑡𝑒𝑚S,𝑜𝑝𝑡𝑠,𝑎𝑛𝑠\)\}\\mathcal\{W\}\_\{mcq\}\\leftarrow\\mathcal\{W\}\_\{mcq\}\\cup\\\{\(A,\\,C,\\,\\mathit\{top\\\_k\},\\,\\mathit\{stem\}\_\{T\},\\,\\mathit\{stem\}\_\{S\},\\,\\mathit\{opts\},\\,\\mathit\{ans\}\)\\\}
31:endif

32:endfor

33:return

𝒲m​c​q\\mathcal\{W\}\_\{mcq\}

### Concept Distractor Generation Algorithm

The distractor generation algorithm of Stage 1 \(Section[3\.1](https://arxiv.org/html/2610.00682#S3.SS1)\) is provided in Algorithm[2](https://arxiv.org/html/2610.00682#alg2)\.

Algorithm 2PerturbAndClassify: Concept Distractor Generation1:

𝒪\\mathcal\{O\},

𝒢\\mathcal\{G\},

ℋ\\mathcal\{H\},MaxAxiomsPerClass,MinDistr

2:\[Tool\]HermiT: OWL reasoner

3:

𝒲f​o​r​m​a​l=\{\(A,C,𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟​\_​𝑝𝑜𝑜𝑙,𝚘𝚌⁡\(C\)\)\}\\mathcal\{W\}\_\{formal\}=\\\{\(A,\\,C,\\,\\mathit\{distractor\\\_pool\},\\,\\mathtt\{oc\}\(C\)\)\\\}
4:

𝒟\\mathcal\{D\}: disjoint index \(owl:disjointWith \+ owl:AllDisjointClasses, expanded to descendants\); operatorsπ∈\{πF1,πF2,πF3,πF4,πS1,πQ1,πQ2,πQ3\}\\pi\\in\\\{\\pi\_\{F\_\{1\}\},\\pi\_\{F\_\{2\}\},\\pi\_\{F\_\{3\}\},\\pi\_\{F\_\{4\}\},\\pi\_\{S\_\{1\}\},\\pi\_\{Q\_\{1\}\},\\pi\_\{Q\_\{2\}\},\\pi\_\{Q\_\{3\}\}\\\}: see Table[1](https://arxiv.org/html/2610.00682#S3.T1);𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑑\\mathit\{produced\}: axioms accepted so far for classAA

5:

𝒟←build​\_​disjoint​\_​index​\(𝒪,ℋ\)\\mathcal\{D\}\\leftarrow\\mathrm\{build\\\_disjoint\\\_index\}\(\\mathcal\{O\},\\,\\mathcal\{H\}\)
6:

𝒲f​o​r​m​a​l←∅\\mathcal\{W\}\_\{formal\}\\leftarrow\\emptyset
7:for all

\(A,\[\(C1,𝚘𝚌⁡\(C1\)\),\(C2,𝚘𝚌⁡\(C2\)\),…\]\)∈𝒢\(A,\\,\[\(C\_\{1\},\\mathtt\{oc\}\(C\_\{1\}\)\),\(C\_\{2\},\\mathtt\{oc\}\(C\_\{2\}\)\),\\ldots\]\)\\in\\mathcal\{G\}do

8:

𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑑←0\\mathit\{produced\}\\leftarrow 0
9:for all

CiC\_\{i\}in order of

𝚘𝚌↓,\\mathtt\{oc\}\\\!\\downarrow,while

𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑑<MaxAxiomsPerClass\\mathit\{produced\}<\\textsc\{MaxAxiomsPerClass\}do

10:// Generate candidates

11:

𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝑠←\{\(C′,π\)∣π∈operators,C′∈π\(Ci\),C′≠Ci\}\\mathit\{candidates\}\\leftarrow\\\{\(C^\{\\prime\},\\pi\)\\mid\\pi\\in\\text\{operators\},\\ C^\{\\prime\}\\in\\pi\(C\_\{i\}\),\\ C^\{\\prime\}\\neq C\_\{i\}\\\}⊳\\trianglerightduplicates removed

12:// Phase 1: entailment \+ satisfiability \(batched HermiT call\)

13:for all

C′∈𝑐𝑎𝑛𝑑𝑖𝑑𝑎𝑡𝑒𝑠C^\{\\prime\}\\in\\mathit\{candidates\}do

14:

c1←\[𝒪⊧A⊑C′\]c\_\{1\}\\leftarrow\[\\mathcal\{O\}\\models A\\sqsubseteq C^\{\\prime\}\];

𝑠𝑎𝑡←\[𝒪⊧A⊓C′⊑⊥\]\\mathit\{sat\}\\leftarrow\[\\mathcal\{O\}\\models A\\sqcap C^\{\\prime\}\\sqsubseteq\\bot\]
15:endfor

16:// Phase 2: subsumption betweenCiC\_\{i\}andC′C^\{\\prime\}\(batched,c1=⊤c\_\{1\}\{=\}\\toponly\)

17:for all

C′C^\{\\prime\}with

c1=⊤c\_\{1\}\{=\}\\topdo

18:

c2←\[𝒪⊧Ci⊑C′\]c\_\{2\}\\leftarrow\[\\mathcal\{O\}\\models C\_\{i\}\\sqsubseteq C^\{\\prime\}\];

c3←\[𝒪⊧C′⊑Ci\]c\_\{3\}\\leftarrow\[\\mathcal\{O\}\\models C^\{\\prime\}\\sqsubseteq C\_\{i\}\]
19:endfor

20:// Classify and filter

21:

𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟\_𝑝𝑜𝑜𝑙←\{\(C′,𝑐𝑎𝑡𝑒𝑔𝑜𝑟𝑦\(C′\)\)∣\\mathit\{distractor\\\_pool\}\\leftarrow\\\{\\,\(C^\{\\prime\},\\,\\mathit\{category\}\(C^\{\\prime\}\)\)\\mid⊳\\trianglerightrefer Definition[2](https://arxiv.org/html/2610.00682#Thmdefinition2)

22:

¬c1∧𝑠𝑎𝑡⇒contradiction\\neg c\_\{1\}\\wedge\\mathit\{sat\}\\ \\Rightarrow\\ \\textit\{contradiction\}
23:

¬c1∧¬𝑠𝑎𝑡⇒non\_entailed\_satisfiable\\neg c\_\{1\}\\wedge\\neg\\mathit\{sat\}\\ \\Rightarrow\\ \\textit\{non\\\_entailed\\\_satisfiable\}
24:

c1∧c2∧¬c3⇒weakeningc\_\{1\}\\wedge c\_\{2\}\\wedge\\neg c\_\{3\}\\ \\Rightarrow\\ \\textit\{weakening\}
25:

c1∧¬c2∧¬c3⇒incomparable\}c\_\{1\}\\wedge\\neg c\_\{2\}\\wedge\\neg c\_\{3\}\\ \\Rightarrow\\ \\textit\{incomparable\}\\,\\\}⊳\\trianglerightequivalent/strengthening discarded

26:if

\|𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟​\_​𝑝𝑜𝑜𝑙\|≥MinDistr\|\\mathit\{distractor\\\_pool\}\|\\geq\\textsc\{MinDistr\}then

27:

𝒲f​o​r​m​a​l←𝒲f​o​r​m​a​l∪\{\(A,Ci,𝑑𝑖𝑠𝑡𝑟𝑎𝑐𝑡𝑜𝑟​\_​𝑝𝑜𝑜𝑙,𝚘𝚌⁡\(Ci\)\)\}\\mathcal\{W\}\_\{formal\}\\leftarrow\\mathcal\{W\}\_\{formal\}\\cup\\\{\(A,\\,C\_\{i\},\\,\\mathit\{distractor\\\_pool\},\\,\\mathtt\{oc\}\(C\_\{i\}\)\)\\\}
28:

𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑑←𝑝𝑟𝑜𝑑𝑢𝑐𝑒𝑑\+1\\mathit\{produced\}\\leftarrow\\mathit\{produced\}\+1
29:endif

30:endfor

31:endfor

32:return

𝒲f​o​r​m​a​l\\mathcal\{W\}\_\{formal\}

### Smoothing Prompt \(Stage 2\)

The following template implements the Stage 2 smoothing described in Section[3\.2](https://arxiv.org/html/2610.00682#S3.SS2)\.

System message

Youareanaturallanguageeditorforontologyclassdescriptions\.

Youwillreceivetwoinputs:

RAW:aphraseproducedbyarule\-basedverbaliser\(maycontain

artifactsoranerrorstring\)

EXPR:alabel\-substitutedDescriptionLogicexpressiongiving

theexactlogicalmeaning

Yourtask:writeasinglefluent,grammaticalEnglishsentence

thataccuratelycapturesthemeaninginEXPR\.Thesentencewill

beusedasanansweroptioninamultiple\-choicequestion\.

Rules:

\-KeepallconceptandpropertynamesexactlyastheyappearinEXPR\.

\-Conjuncts"C1⊓\\sqcapC2⊓\\sqcap\.\.\."\-\>joinwith"and";

disjuncts"C1⊔\\sqcupC2⊔\\sqcup\.\.\."\-\>joinwith"or"\.

\-"∃\\existsr\.C"\-\>"hasrsomeC"orthemostnaturalequivalent\.

\-"∀\\forallr\.C"\-\>"hasronlyC"\.

\-"\>=nr\.C"\-\>"hasatleastnrC"\.

\-"<=nr\.C"\-\>"hasatmostnrC"\.

\-"=nr\.C"\-\>"hasexactlynrC"\.

\-"¬\\negC"\-\>"isnotaC"\.

\-"∃\\existsr\{v\}"\-\>"whoserisv"\.

\-"∃\\existsr\.Self"\-\>"thatritself"\.

\-"⊤\\top"\-\>"anything";"⊥\\bot"\-\>"nothing"\.

\-IfRAWcontainsforeign\-languagelabelsorlabelsnotpresentin

EXPR,ignoreRAWanduseEXPRalone\.

\-IfRAWisa"\[verbalisationerror:\.\.\.\]"string,ignoreitand

useEXPRalone\.

\-Startthesentencewith"somethingthat"andendwithouttrailing

punctuation\.

\-OutputONLYtherewrittensentence\-\-noexplanation,nolabel,

noquotes\.

\-\-\-Example1:foreign\-languagelabelsinRAW\-\-ignoreRAW\-\-\-

RAW:EtwasdaseineTierOderPflanze

EXPR:∃\\existshaspart\.animal⊔\\sqcup∃\\existshaspart\.plant

\-\>somethingthathassomeanimalorplantasapart

\-\-\-Example2:chainedrelativeclauses\-\-flattenwith"and"\-\-\-

RAW:somethingthathasoutputdocumentthatisaboutlegalentity

thathasroledefendantrole

EXPR:∃\\existshasoutput\.document⊓\\sqcap∃\\existsisabout\.legalentity

⊓\\sqcap∃\\existshasrole\.defendantrole

\-\>somethingthatproducessomedocumentaboutalegalentity

thathasadefendantrole

\-\-\-Example3:verbalisationerror\-\-ignoreRAW,useEXPR\-\-\-

RAW:\[verbalisationerror:memberof\-\-ObjectExactCardinality\(

2<hasRole\>\)\]

EXPR:=2hasmember\.structuralunit

\-\>somethingthathasexactly2structuralunitsasmembers

User message

RewritethefollowingintoafluentEnglishsentence:

RAW:<deepontoverbalisationorerrorstring\>

EXPR:<label\-substitutedDLexpression\>

### Stem Generation Prompt \(Stage 4\)

The following template generates the Stage 4 scenario stem \(Section[3\.4](https://arxiv.org/html/2610.00682#S3.SS4)\)\.

System message

Youwritemultiple\-choicequestionstemsforprofessionalknowledge

assessments\.

Writeasasubject\-matterexpertauthoringanexam\-\-notasa

knowledgeengineer\.

Neverusemeta\-languagesuchas:ontology,ontological,

formalization,formalconstraint,taxonomy,classificationscheme,

orknowledgebase\.WriteonlyinplainprofessionalEnglish\.

User message

Concept:<classlabel\>

Domain:<domainstring\>

Definition:<SKOSdefinition,ifavailable\>

Writeasingleconcisequestionstem\(onesentence,max30words\)

that:

\-Names"<classlabel\>"asthesubjectinarealistic<domain\>

professionalcontext\(e\.g\.classifyingamaterial,evaluatinga

sample,designingaprocess,preparingadish\)

\-Endswith"whichofthefollowing\.\.\."or"whichofthefollowing

best\.\.\."

\-Usesdomain\-professionallanguage\-\-nometa\-languageabout

ontologies,definitions,orformalizations

\-DoesNOTmentionanyoftheseterms\(theyappearintheanswer

optionsandwouldhintattheanswer\):<blocklist\>

\-Doesnotdescribeorhintatthecorrectconstraint

OutputONLYthestem\-\-noexplanation,noquotes,nolabel\.

### Judge Prompt \(Stage 4\)

The following template implements the Stage 4 LLM judge \(Section[3\.4](https://arxiv.org/html/2610.00682#S3.SS4)\)\.

System message

Youarearigorousexaminerreviewingmultiple\-choicequestionsfor

aprofessionalknowledgeassessment\.Scoreeachquestiononthethree

dimensionsprovided\.

OutputonlyvalidJSON\-\-nomarkdownfences,noexplanation\.

User message

Domain:<domainstring\>

Class:<classlabel\>

Questionstem\(scenario\):

<stem\_scenario\>

Options:

A\)<optiontext\>

B\)<optiontext\>

C\)<optiontext\>

D\)<optiontext\>

Correctanswer:<letter\>

Correctoptiontext:<smoothedNLofcorrectexpression\>

CorrectDLexpression:<DLstring\>

Wrongoptions:

<letter\>\)<optiontext\>\[failure\_type:<type\>\]

\.\.\.

Scoringrubric\(applytoeachdimension\):

5\-\-Excellent:fullymeetsthecriterionwithnoissues

4\-\-Good:meetsthecriterionwithminorissues

3\-\-Acceptable:partiallymeetsthecriterion,noticeableissues

2\-\-Poor:failstomeetthecriterioninasignificantway

1\-\-Unacceptable:completelyfailsthecriterion

Dimensionrubrics:

option\_faithfulness:

5\-\-NLtextofcorrectoptioncaptureseveryconstraintinthe

DLexpressionexactly,noomissions,noadditions,

noambiguity

4\-\-Minorwordingimprecisionbutmeaningfullypreserved

3\-\-Oneconstraintisweakened,generalised,orslightly

misleading

2\-\-Akeyconstraintismissingorincorrectlystated

1\-\-NLtextdoesnotreflecttheDLexpressionatall

stem\_clarity:

5\-\-Stemisaclear,naturalprofessionalquestion;nohintof

theanswer;domain\-appropriatephrasingthroughout

4\-\-Clearandappropriatewithminorphrasingissues

3\-\-Understandablebutawkwardorslightlyambiguous

2\-\-Ambiguous,misleading,orcontainsasubtlehinttoward

theanswer

1\-\-Confusing,domain\-inappropriate,ordirectlyhintsat

theanswer

relevance:

5\-\-Adomainexpertwouldfindthisquestionmeaningful,

appropriatelychallenging,anddirectlyrelevantto

professionalpractice

4\-\-Relevantandmeaningfulwithminorreservations

3\-\-Somewhatrelevantbuttooeasy,tooobscure,orcontrived

2\-\-Marginallyrelevant;mostdomainexpertswouldfindit

trivialorodd

1\-\-Notrelevanttothedomainorincomprehensibletoa

professional

ScorethequestiononallthreedimensionsandoutputONLYvalidJSON:

\{

"option\_faithfulness":<1\-5\>,

"stem\_clarity":<1\-5\>,

"relevance":<1\-5\>,

"notes":"<onesentenceonmainqualityissue,or’none’\>"

\}

### Benchmark Schema

The complete schema of each benchmark record is illustrated in Table[4](https://arxiv.org/html/2610.00682#Ax1.T4)\.

Table 4:Complete Benchmark Record SchemaFieldTypeDescriptionClass identityclass\_iristringOntology IRI of subject classclass\_labelstringrdfs:label of classinferredboolTrue if axiom inherited via HermiTaxiom complexityinteger𝚘𝚌\\mathtt\{oc\}\(Section[3\.3](https://arxiv.org/html/2610.00682#S3.SS3)\)Correct expressioncorrect\_expressionstringOwlready2 string ofCCcorrect\.dldictRecursive JSON encoding ofCCcorrect\.smoothstringFluent English option stringDistractor pool \(per distractor entry\)distractors\[i\]\.failure\_typeenumcontradiction\|\|weakening\|\|incomparable\|\|non\_entailed\_satisfiabledistractors\[i\]\.similarityfloatsimilarity as per Eq\.[6](https://arxiv.org/html/2610.00682#S3.E6)to correct optiondistractors\[i\]\.rankintRank as per Stage 3distractors\[i\]\.dldictC′C^\{\\prime\}in JSON encodingdistractors\[i\]\.smoothstringFluent English option stringdistractor\_pool\_sizeintTotal candidates before filterTop\-kkdistractors \(selected for MCQ\)top\_klistTopk=3k\{=\}3distractorsQuestion stemsstem\_templatestringTemplate stem, seeded by class IRIstem\_scenariostringLLM domain scenario stemMCQ optionsoptionsdict\{A,B,C,D\}→\\rightarrowoption string; reproducible seeded shufflecorrect\_answerA–DLetter of correct optionQuality scoresquality\_meanfloat 1–5Mean of three dimension scoresquality\_flagboolTrueif mean≥3\.0\\geq 3\.0quality\_notesstringOne\-sentence judge summary
### LLM Evaluation Setup

We evaluate six models spanning proprietary and open\-source, reasoning and non\-reasoning varieties, as detailed in Table[5](https://arxiv.org/html/2610.00682#Ax1.T5)\. Proprietary models \(GPT\-4o\[[OpenAI, 2024a](https://arxiv.org/html/2610.00682#bib.bib15)\], GPT\-5\.4\[[OpenAI, 2026a](https://arxiv.org/html/2610.00682#bib.bib18)\], GPT\-5\.6\-sol\[[OpenAI, 2026b](https://arxiv.org/html/2610.00682#bib.bib19)\]\) are accessed via the Azure OpenAI API\[[Microsoft, 2025](https://arxiv.org/html/2610.00682#bib.bib13)\]with all parameters set to their defaults except temperature \(0\) and maximum output tokens \(4,096\)\. Open\-source models \(Ministral\-3\-14B\[[Mistral, 2025](https://arxiv.org/html/2610.00682#bib.bib14)\], Qwen\-3\.8\-27B\[[Qwen, 2026](https://arxiv.org/html/2610.00682#bib.bib20)\], DeepSeek\-R1\[[DeepSeek, 2025](https://arxiv.org/html/2610.00682#bib.bib3)\]\) are loaded locally via HuggingFace Transformers\[[Wolf et al\., 2020](https://arxiv.org/html/2610.00682#bib.bib28)\]and served with the same inference settings\. Qwen\-3\.8\-27B is evaluated in two configurations:thinking off\(standard generation, non\-reasoning\) andthinking on\(extended chain\-of\-thought enabled via the model’s native thinking flag\), allowing direct comparison of the effect of the reasoning mode on the same base model\.

Table 5:LLMs used for zero\-shot MCQ evaluation\. Prop\. = proprietary \(Azure OpenAI\); Open = open\-source \(HuggingFace\); HF = HuggingFace; R = reasoning mode enabled; NR = non\-reasoning\.All models are evaluated zero\-shot with temperature 0, a maximum of 4,096 output tokens, a domain\-specific system prompt, and no chain\-of\-thought, ensuring purely direct letter prediction\.

All models are prompted with the following zero\-shot template:

System message

Youarea\[domainexpert\]\.Answerthemultiple\-choicequestion

belowbyreplyingwithONLYthesingleletterofthecorrect

option\(A,B,C,orD\)\.Donotaddanyexplanation\.

User message

<stem\_scenario\>

A\.<option\_A\>

B\.<option\_B\>

C\.<option\_C\>

D\.<option\_D\>

Answer\(A/B/C/D\):

The \[Domain expert\] phrase varies per ontology to provide the domain specific instructions of the task:an expert in food science and Italian cuisine\(Pizza\),an expert in process metallurgy and materials science\(PMDco\),a medical expert in human disease and clinical medicine\(DOID\)\.