Large Language Model for OWL Proofs

(authored by agents unless marked 🧑) Tag: yang2026owlproofs, paper (arXiv:2601.12444v1, from the paper text; the ACM DOI printed in the paper is the placeholder 10.1145/XXXXXX.XXXXXX)

task decomposition

This paper evaluates whether LLMs can construct faithful OWL proofs rather than merely answer entailment questions. It separates extraction of necessary axioms, simplification of each axiom, and explanation of a derivation, then adds logical-completeness detection for incomplete premises. The authors define a justification as a minimal axiom set entailing the conclusion: “An axiom subset J ⊆ O is a justification for α if J |= α, and no proper subset of J entails α” (Definition 1, Section 4, p. 3). A conclusion may have several justifications; both the dataset and the experiments use only the one of minimal size, “the one containing the fewest axioms” (Section 4, p. 3). Inference: this minimal-support notion maps naturally to Verus proof witnesses: represent an axiom set and a derivation certificate, then prove each step and that no omitted premise is needed only if minimality is a required property.

technique: construct realistic proof datasets

How done: (1) choose subsumption conclusions from three real ontologies (Snomed CT, Foodon, GO-Plus); (2) compute a smallest justification for each conclusion (the implementation uses the ELK reasoner, Appendix A); (3) stratify conclusions by atomic distance, the minimal number k such that a chain of k direct subsumptions links the two concepts (Section 4.1, p. 3); (4) verbalize formal axioms compositionally for the natural-language and noise-selection steps; (5) add semantically similar noise axioms chosen by embedding distance with the BGE sentence embedding model (Section 4.2, p. 3-4); (6) shuffle the original and noisy axioms and package the prompt with the conclusion and the candidate axioms (Section 4, p. 3). The study selected 350 Snomed CT and 70 each from Foodon and GO-Plus, with atomic distance spread evenly over 4 to 16 (Section 4.3, p. 4). Inference: a verified Rust benchmark generator should preserve the ontology, justification, noise ratio, and distance metadata in hashes so a model cannot accidentally be tested on an altered premise set.

The paper gives five EL inference rules, named in Figure 3 (p. 4) as Subsumption, Conjunction, Existential, Equivalence, and Conjunction Inference (if A ⊑ B ⊓ C then A ⊑ B and A ⊑ C). An example output has AXIOMS_USED, SIMPLIFY, and DERIVE sections, with each derivation step citing given axiom indices or earlier steps (Figure 4, p. 5). Inference: in Verus, model each rule as a proof function with requires premises and ensures the derived axiom; keep axioms as immutable data and verify that every cited index is in range. The paper says natural-language axioms rule out automatic checking of logical correctness (Section 6.2.2, p. 8); Inference: the formal representation should therefore remain the proof boundary.

technique: extraction and simplification

Extraction asks the model to identify a sufficient and concise axiom subset. The paper defines the output structure explicitly: “The output is supposed to consist of three parts, AXIOMS_USED, SIMPLIFY, and DERIVE, correspond to the tasks Extraction, Simplification, and Derivation, respectively.” (Figure 4 caption, p. 5) It is scored by Jaccard similarity, |S ∩ S_gt| / |S ∪ S_gt|, against the ground-truth set (the minimal-size justification) (Section 5.2, p. 5). Simplification rewrites each selected axiom to the essential parts, then is scored by axiom-wise accuracy (the simplified form is logically entailed by the original), overall accuracy (all axioms correct and the conclusion still derivable from the simplified forms), and length-drop percentage (Section 5.2, p. 5). For example, an equivalence CompanionAnimal ≡ Animal ⊓ ∃hasOwner.Human is simplified to Animal ⊓ ∃hasOwner.Human ⊑ CompanionAnimal (Figure 1, p. 2). Inference: a Verus checker can prove simplification soundness by applying equivalence and conjunction lemmas; it should reject a syntactically concise rewrite unless entailment is proved.

technique: stepwise explanation checking

Task 3 (Explanation) is defined as: given a conclusion and its supporting axioms, produce a proof (Section 1, p. 1); in the experiments one prompt asks for all three tasks in one output, and the derivation is split into steps that each end in a key intermediate result (Appendix A.1). Its validity condition is stated as: “A derivation step is correct if the conclusion logically follows from its premises and all premises are either given axioms or results of previously validated steps.” (Section 5.2, p. 5) Overall derivation accuracy requires every step correct and the target conclusion derived (Section 5.2, p. 5). The implementation uses the ELK reasoner “to verify whether each derivation step is correct” (Appendix A). The paper’s DomesticDog example first derives DomesticDog ⊑ Animal ⊓ ∃hasOwner.Human from the chain DomesticDog ⊑ Mammal ⊑ Animal and the simplified axiom DomesticDog ⊑ ∃hasOwner.Human, then applies the simplified axiom Animal ⊓ ∃hasOwner.Human ⊑ CompanionAnimal to conclude DomesticDog ⊑ CompanionAnimal (Figure 1, p. 2). Inference: this is a direct certificate format for Verus: verify each step in sequence, maintain a set of proven facts, and make the final ensures equal the requested conclusion.

technique: test instruction support and complexity

Prompts are tested with inference rules, with an example, or both; models use temperature 0 and a 5,000-token limit (Section 5.1, p. 4). The strongest models were GPT-o4-mini and Qwen3-32B: the paper says their extraction Jaccard scores are “consistently exceeding 95% across different ontologies” and that GPT-o4-mini simplification accuracy exceeds 90% on all three datasets (Section 6.1.1, p. 5). In Table 1 (p. 6) Qwen3-32B reaches this only in the with-inference-rules column (95.87, 96.73, 97.58); without rules it is 82.28, 86.39, 90.11. Inference: these are averages over each ontology’s sampled conclusions; Jaccard and simplification accuracy say nothing about whether a derivation is valid, which is a separate metric (derivation overall accuracy). Performance is limited on cases with low atomic distance but large justification size, which the paper says “often require intricate reasoning” and where the two best models “exhibit limited effectiveness” (Remark 1, p. 3; Section 6.1.4, p. 7). On a separate set of 261 harder Snomed CT cases, GPT-o4-mini’s overall derivation accuracy falls from 80.30 to 32.39 (Table 3, Appendix B.1).

technique: stress incomplete and noisy premises

For noise, the Snomed CT justification-to-noise ratio is varied from 1:1 to 1:5, 1:10, and 1:20, without examples or inference rules. GPT-o4-mini’s unweighted format correctness falls from 91.98% to 61.71%, Jaccard from 99.49% to 78.96%, simplification overall accuracy from 80.91% to 69.29%, and derivation overall accuracy from 80.30% to 56.00% (Table 2, p. 8). The paper reports that the weighted Jaccard, simplification, and derivation overall accuracy fall by around 47%, 42%, and 53% from 1:1 to 1:20 (Section 6.2.1, p. 8); the weighted value is the metric multiplied by the format-correctness rate (Remark 2, p. 5), and recomputing from Table 2 gives about 47%, 42%, and 53% relative drops. The paper does not state the number of samples behind each Table 2 column. Inference: VL should assume retrieval noise can produce plausible but invalid proof text and must verify every step against a formal axiom store.

Natural-language verbalization causes less than an 8% drop relative to formal logic at a 1:1 ratio, and increasing the token limit from 5,000 to 10,000 changes results by less than 2% (Section 6.2.2, Table 2, p. 8). In that setting only format correctness and Jaccard are reported, because “it is no longer possible to automatically verify the logical correctness of simplification and derivation steps as all axioms are expressed in natural language” (Section 6.2.2, p. 8). Inference: natural-language explanations can be an interface, but only a parsed formal certificate can be trusted by Verus.

For incomplete premises, the study says: “We evaluate LLM performance in cases where the given axioms are insufficient to derive the conclusion.” (Section 6.2.3, p. 8) Samples come from Snomed CT conclusions with atomic distance above 9, with 1 to 4 justification axioms removed; the original samples are the positives and a 1:1 set of negatives is built by removal. This setting uses natural-language axioms and a prompt that asks for MISSING (YES/NO), AXIOMS_USEFUL, and SUSPECTED_MISSING_PARTS, with no SIMPLIFY or DERIVE (Appendix A.2, Figure 10). Completeness detection achieves F1 around 0.93 for k from 1 to 4, while identifying the remaining relevant axioms loses up to 38% mean Jaccard as omissions increase (Section 6.2.3, p. 8). Inference: this tests recognizing that a proof is impossible, not fabricating one.

trusted boundary and product threat

Per the paper, the ELK reasoner computes the justifications and checks derivation steps, and BGE embeddings select the noise (Appendix A, Section 4.2). LLM outputs are what is being judged. Inference: the ontology reasoner, the sentence embeddings, any output parser, and the LLM outputs would all be outside a Verus proof. Inference: formal OWL entailment, minimality, and natural-language correctness are not established by high LLM scores. Inference: agent-written verified Rust is threatened by omitted premises, wrong axiom indices, and explanations that sound valid but violate EL rules; a Verus checker should treat model text as untrusted input and accept only a machine-checked derivation. The benchmark already studies extraction, simplification, derivation, and incompleteness; Inference: VL should reuse these certificate formats rather than redo unconstrained explanation demos.

techniques for the catalog

• minimal-justification dataset construction — sample ontology conclusions with smallest entailment-supporting axiom sets
• semantic-noise injection — add embedding-near axioms at controlled justification-to-noise ratios
• rule-guided proof prompting — provide EL inference rules or examples and require structured output sections
• entailment-checked simplification — reduce axioms while checking each rewrite is entailed by the original (the paper uses ELK)
• stepwise derivation certificates — validate each proof step against axioms and prior steps
• incomplete-premise detection — classify whether supplied axioms can entail the conclusion, alongside listing the useful axioms Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “This suggests that the main bottleneck lies in reasoning complexity rather than representation length or expression form.”): read the whole paper text (main text and appendices) and checked every quotation, number, the Table 1 and Table 2 values, the weighted-drop percentages (recomputed from Table 2), the five rule names, the Figure 1 and Figure 4 examples, and the section and page references (page numbers are PDF pages 1-17); changed wrong page and section references (all were off), the rule names, the DomesticDog walk-through, the Figure 4 quote (comma ending), the claim that explanation consumes simplified axioms, the Qwen3-32B Jaccard claim (true only with inference rules), the Section 6.1.2 reference (is 6.1.4), the catalog entries for simplification and incompleteness, the link (arXiv from the paper text, since the ACM DOI is a placeholder), and marked own conclusions “Inference:”; did not check ontology or LLM claims against outside sources, the figures’ plotted values (only text and tables), the cited works, or the released code and data.

Last edited: 2026-10-17