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

Nishtha N. Vaidya; Stephan Grimm; Thomas Hubauer; Thomas A. Runkler

cs.AISep 30, 2026

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

Authors: Nishtha N. Vaidya, Stephan Grimm, Thomas Hubauer, Thomas A. Runkler

Organizations: Siemens AG · Technical University of Munich

Abstract

Large language models (LLMs) increasingly underpin scientific AI applications that reason over structured knowledge, from biomedical question answering 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 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. Distractors are generated by perturbing the right-hand-side class expressions of class definition axioms, and their incorrectness 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), generating 112, 2,491, and 15,216 MCQs respectively. Distractors span four semantic categories from class unsatisfiability to weakened subsumptions, enabling diagnostic evaluation of specific reasoning failures. 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 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 scientific AI.

Figures & tables

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.

Op	Transformation $C^{\prime}_{i}$	Source Set $\mathcal{S}_{\pi}(p,C)$	Guard / Cap
$\pi_{F_{1}}$	Per distinct filler $B$ at position $p$ : $C[B\twoheadleftarrow v^{\prime}]$ for each $v^{\prime}\in\mathcal{S}_{\pi}(p,C)$	Siblings of $B$ and their descendants to depth $N$ in $\mathcal{H}$	Skip if $C$ contains $\forall$ ; depth cap $=N$
$\pi_{F_{2}}$	Per distinct filler $B$ at position $p$ : $C[B\twoheadleftarrow v^{\prime}]$ for each $v^{\prime}\in\mathcal{S}_{\pi}(p,C)$	All ancestors of $B$ in $\mathcal{H}$ ; all levels	None
$\pi_{F_{3}}$	Per distinct filler $B$ at position $p$ : $C[B\twoheadleftarrow v^{\prime}]$ for each $v^{\prime}\in\mathcal{S}_{\pi}(p,C)$	Direct children of $B$ in $\mathcal{H}$	Cap $=P$ children per filler
$\pi_{F_{4}}$	Per distinct filler $B$ at position $p$ : $C[B\twoheadleftarrow v^{\prime}]$ for each $v^{\prime}\in\mathcal{S}_{\pi}(p,C)$	Classes disjoint with $B$ in $\mathcal{H}:\mathcal{D}[B]$	Skip if $C$ contains $\forall$ ; cap $=M$ per filler
$\pi_{S_{1}}$	$p$ = cardinality bound $n$ in top-level ${\bowtie}_{n}\,r.E$ : $C[p\leftarrow n+1]$ and $C[p\leftarrow n-1]$	$\mathcal{S}_{\pi}(p,C)=\{n-1,\,n+1\}$ ; omit $n-1$ if $n-1<0$	Top-level kind $\in\{\text{exact},\,\text{min},\,\text{max}\}$
$\pi_{Q_{1}}$	$p$ = restriction kind in top-level ${=}_{n}\,r.E$ : $C[p\leftarrow\exists]$ , dropping $n$	$\mathcal{S}_{\pi}(p,C)=\{\exists\}$	Top-level must be exact

Table 1: Formal Perturbation Operators

\pi

Figure 2: Example of MCQ generated using the proposed pipeline from Pizza (left) and DOID.

Table 4

Appendix figures & tables2 assets

Supplementary material from the paper’s appendix.

Appendix

Field	Type	Description
Class identity
class_iri	string	Ontology IRI of subject class
class_label	string	rdfs:label of class
inferred	bool	True if axiom inherited via HermiT
axiom complexity	integer	$\mathtt{oc}$ (Section 3.3 )
Correct expression

Appendix

Table 4: Complete Benchmark Record Schema

Model label (Table 3 )	Model / HF ID	Access	Mode
GPT-5.6-sol	gpt-5.6-sol (Azure OpenAI)	Prop.	R
GPT-5.4	gpt-5.4 (Azure OpenAI)	Prop.	NR
GPT-4o	gpt-4o (Azure OpenAI)	Prop.	NR
Ministral-3-14B	mistralai/Ministral-3-14B-Instruct-2512 (HF)	Open	NR
Qwen-3.8-27B	Qwen/Qwen3.8-27B thinking off (HF)	Open	NR
Qwen-3.8-27B	Qwen/Qwen3.8-27B thinking on (HF)	Open	R

Appendix

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.

Explore similar work

Jun 11, 2026cs.AI

SciR: A Controllable Benchmark for Scientific Reasoning in LLMs

Three paradigmatic forms of inference recur across scientific reasoning: deduction, induction, and causal abduction. Reliably evaluating LLMs on these in scientific settings is currently out of reach: scientific benchmarks built on human annotations are costly and lack mechanistic ground truth, while synthetic logical-reasoning benchmarks do not resemble real scientific documents. We introduce SciR, a benchmark that combines multi-paradigm reasoning with controllable scientific rendering, anchored on three paradigmatic scientific problems. Tasks are generated from formal objects (deduction tree, inductive rule hypothesis, causal graph) to guarantee verifiable answers, then rendered into multi-document scientific discourse via per-track domain-tuned genres. The construction lets us independently vary two difficulty axes: how hard it is to extract the key information needed for inference, and how hard the principled inference itself is. We test six models. Both axes hurt every model, and their effects compound. The rendering even hurts neurosymbolic pipelines, which hand inference to a verified solver. The two axes yield a per-model extraction-vs-inference profile: for instance, reasoning models like deepseek-r1 mostly surpass non-reasoning instruct models on the inference axis. To our knowledge, SciR is the first multi-paradigm scientific-reasoning benchmark with parametric control on both extraction and inference difficulty.

Pierre Beckmann, Marco Valentino, Andre Freitas

Idiap Research Institute, Switzerland · EPFL, Switzerland · School of Computer Science, University of Sheffield, UK +2

Reasoning Benchmark Scientific Discovery Large Language Model Benchmarks

Ask PDF

May 19, 2026cs.CL

LLMEval-Logic: A Solver-Verified Chinese Benchmark for Logical Reasoning of LLMs with Adversarial Hardening

Evaluating large language models (LLMs) on natural-language logical reasoning is essential because rule-governed tasks require conclusions to follow strictly from stated premises. Many existing logical-reasoning benchmarks are generated by templating natural-language items from sampled formulas, provide only coarse or unaudited formal annotations, and are now quickly saturated by frontier reasoning models. We present LLMEval-Logic, a Chinese logical reasoning benchmark built from realistic situational scenarios. Its pipeline forward-authors and expert-audits natural-language items together with their reference formalizations, verifies annotated answers with Z3, constructs expert rubrics for natural-to-formal grading, and hardens selected items through a closed-loop adversarial workflow. The benchmark is released in two paired subsets: a 246-item Base subset shipped with 1,400 expert-developed rubric atoms, and a 190-item Hard subset with 938 multi-step sub-questions over closed model spaces. Evaluating 14 frontier LLMs on LLMEval-Logic reveals substantial gaps in current models: the best model reaches only 37.5% Hard Item Accuracy, and even with reference symbols the highest joint Z3+Rubric formalization score among evaluated models reaches only 60.16%. Our benchmark is publicly available at https://github.com/llmeval/LLMEval-Logic.

Ming Zhang, Qiyuan Peng, Yinxi Wei +13

Institute of Trustworthy Embodied Artificial Intelligence, Fudan University · 2Hunyuan Team, Tencent · School of Philosophy, Fudan University

Reasoning Benchmark Reasoning Skills

Ask PDF

Jun 22, 2026cs.AI

HOLMES: Evaluating Higher-Order Logical Reasoning in LLMs

Logical reasoning is essential for reliable AI, yet existing benchmarks are largely first-order-logic-centric, focusing on object-level deduction over fixed predicates. This misses many realistic scenarios where models must reason over rules, predicates, functions, constraints, and decision procedures themselves. We introduce HOLMES (Higher-Order Logic Meets real-world Explainable Symbolic reasoning), the first real-world benchmark for higher-order symbolic reasoning in LLMs, containing 1379 instances. Built on higher-order logic, HOLMES pairs natural-language problems with HOL formalizations, ground-truth answers, verifiable reasoning traces, and fine-grained controllable reasoning factors across law and finance. Experiments show that current LLMs still struggle on HOLMES, with an average accuracy of only 50.64% and the best model reaching 59.54%. Our analyses further reveal that high final-answer accuracy can mask shortcut reasoning in conflict-resolution settings, while performance drops sharply under scope-conditioned and compositional reasoning. These findings identify higher-order symbolic reasoning as a key bottleneck for building reliable and verifiable LLMs. The project code and dataset are publicly available at https://github.com/wuyucheng2002/HOLMES.

Yucheng Wu, Jundong Xu, Mingzhen Ju +4

State Key Laboratory of Multimedia Information Processing, Peking University · School of Computer Science, Peking University · School of Computing, National University of Singapore +3

Reasoning Skills

Ask PDF