Machine Learning That Carries Its Own Proof: New Framework Keeps AI Reasoning Auditable

Artificial intelligence systems that blend neural networks with symbolic logic have long promised the best of both worlds: the pattern recognition of machine learning and the rigor of formal reasoning. In practice, however, most neuro-symbolic systems quietly assume that the knowledge base they reason over is fixed. In the real world, ontologies—the formal catalogs of concepts and relationships that anchor knowledge graphs, biomedical databases, and the semantic web—change constantly. When an ontology is updated, rules that were valid yesterday may conflict with the schema of today, and the predictions of a learned model can silently drift out of compliance. A new framework called Delta Semantics, published in Knowledge and Information Systems by Rahul Kumar Singh, Ashok Kumar, and Rajat Kumar, tackles precisely this gap by treating ontology versioning, proof validation, and uncertainty calibration as first-class citizens of the reasoning pipeline.

The core idea behind Delta Semantics is a typed ontology, written as Delta-t, that is explicitly versioned over time. Rather than a static schema, the system maintains a temporal sequence of ontology states, each with its own type constraints and logical rules. Candidate inference rules are synthesized through two complementary mechanisms the authors call Path-to-Rule and Prompt-to-Rule. Path-to-Rule mines logical rules from paths observed in a knowledge graph, in the tradition of rule-learning systems such as AMIE+, while Prompt-to-Rule elicits candidate rules through language-model-driven prompting. This dual strategy allows the framework to combine bottom-up statistical regularities with top-down hypotheses, giving the system a broad pool of candidate rules to draw from when reasoning tasks demand multi-step inference.

What distinguishes the framework is its inference loop, structured as propose–verify–repair. A learned model first proposes predictions, whether link predictions in a knowledge graph, answers to multi-hop questions, or relationships in a visual scene graph. A symbolic checker then verifies each candidate against the current ontology version, rejecting any output that violates type constraints or logical rules. Predictions that survive receive a checker-validated proof certificate—a machine-checkable record of why the answer is consistent with the ontology. Predictions that fail are routed to a repair stage that attempts to fix the violation, for example by substituting a type-consistent alternative. The result is an auditable output stream in which every accepted answer can, in principle, be traced back to a chain of verified logical justifications.

Complementing the proof machinery, Delta Semantics draws on conformal prediction, a statistical framework that produces set-valued outputs with calibrated coverage guarantees. Instead of committing to a single answer, the model can return a calibrated set of candidate answers, each backed by a certificate. This reflects a broader movement in machine learning toward honest uncertainty quantification: rather than reporting a point prediction whose reliability is unknown, the system reports a set whose statistical coverage is controlled. In safety-critical applications—medical knowledge bases, legal reasoning, financial compliance—the combination of proof certificates and calibrated sets offers two independent layers of assurance, one logical and one statistical.

The empirical evaluation spans three demanding benchmarks that exercise different facets of the framework. FB15k-237, a canonical knowledge graph completion dataset, tests link prediction under ontology change. HotpotQA, a multi-hop question answering dataset, tests whether the framework can produce explainable, provably supported answers to compositional questions. Visual Genome tests scene-graph reasoning, where predicted object relationships must comply with the type system of the scene ontology. Across all three, the central reported quantity is not raw leaderboard accuracy but proof-pass rate and ontology-violation rate—measures of how consistently the system’s outputs survive formal scrutiny.

The FB15k-237 experiments illuminate the cost of ontology change and the value of adaptation. When 10,000 entailed edges were enabled at a new ontology version, Hits@10 remained flat at 0.1400 across the pre-adaptation versions on 20,466 test queries, but Mean Reciprocal Rank degraded from 0.1064 to 0.0921. This is a subtle but important failure mode: the system still retrieved the right answers somewhere in its ranked lists, but the logical update pushed correct entities further down. A brief post-update adaptation step recovered 64.3 percent of the lost MRR, raising it to 0.1013, while every Hits metric improved—Hits@1 from 0.0650 to 0.0739, Hits@3 from 0.0980 to 0.1070, and Hits@10 from 0.1400 to 0.1404. Proof-pass rate climbed from 95.6 to 97.1 percent and the ontology-violation rate fell from 0.11 to 0.03 percent. The lesson is sobering and useful in equal measure: adaptation recovers much of the degradation, but not all of it.

On HotpotQA, exact match scores increased modestly from 58.6 to 59.8, but the more striking numbers concern provenance. Mapped support—a measure of whether the supporting evidence is properly aligned with the answer—reached 0.8274, and 92.6 percent of accepted predictions received checker-validated proof certificates. In other words, nearly every answer the system accepted came with a formal record of why it is consistent with the ontology. This is precisely the kind of verifiable explainability that pure neural systems struggle to provide and that regulatory environments increasingly demand.

The Visual Genome results are arguably the most dramatic. Mean recall at 50 rose from 6.8 to 8.9 and mean recall at 100 from 7.9 to 10.2—substantial relative gains in a task notorious for biased predictions that favor frequent relationship types. More telling, type compliance jumped from 82.4 to 96.7 percent, with a proof-pass rate of 94.6 percent. Scene-graph generation is a domain where learned models routinely hallucinate physically or logically impossible object relationships; the checker-verify-repair loop appears to prune those violations at scale while improving recall, suggesting that logical constraints are not merely a brake on neural predictions but can actively sharpen them.

The authors are careful to position the contribution. Results for classic knowledge graph embedding methods such as TransE, ComplEx, and RotatE are reported only as protocol-matched reference points; the central contribution concerns proof-carrying inference and controlled adaptation to ontology updates rather than leaderboard-oriented link prediction. This framing matters, because the deeper question the paper addresses is architectural: how should a reasoning system behave when the logical substrate beneath it shifts? The proposed answer—version the ontology, certify every accepted output, calibrate the answer sets, and adapt after each update—points toward knowledge systems that degrade gracefully and expose their own correctness criteria rather than hiding them inside opaque weights.

The implications extend well beyond benchmark datasets. Knowledge graphs power search engines, recommendation systems, drug discovery pipelines, and enterprise data integration, and virtually all of them evolve continuously as contributors add entities, refine hierarchies, or correct errors. A framework that can absorb those changes, quantify its uncertainty, and attach machine-checkable proofs to its outputs offers a template for what auditable AI might look like in production. The recovery results also carry a practical warning: logical updates will always impose some rank degradation on learned models, and no adaptation step studied here eliminated it entirely. Teams deploying neuro-symbolic systems should therefore budget for post-update retraining and monitor proof-pass rates as a live health metric. Delta Semantics may not be the last word on dynamic ontological reasoning, but it makes a compelling case that the future of trustworthy AI lies in systems that can show their work—version by version, proof by proof.

Subject of Research: A neuro-symbolic framework for reasoning over versioned ontologies with proof-carrying machine learning

Article Title: (\Delta )Semantics: a neuro-symbolic framework for dynamic ontological reasoning with proof-carrying machine learning

Article References: (\Delta )Semantics: a neuro-symbolic framework for dynamic ontological reasoning with proof-carrying machine learning. (n.d.). https://doi.org/10.1007/s10115-026-02897-w

Image Credits: AI Generated

DOI: 10.1007/s10115-026-02897-w

Keywords: neuro-symbolic AI, ontologies, proof-carrying inference, conformal prediction, knowledge graphs, ontology versioning, HotpotQA, FB15k-237, Visual Genome, scene graph generation, explainable AI, Knowledge and Information Systems