Verifying Datalog Reasoning with Lean

Datalog is a simple and elegant rule language that is at the heart of many approaches to logic programming, knowledge representation, and data analysis [1, 13]. Syntactically, Datalog rules are universally quantified, function-free predicate logic implications, such as the following two recursive rules defining transitivity (written from right to left and without the implicit universal quantifiers, as is customary in logic programming):

The main reasoning task then is to compute all logical consequences of such programs over a given set of facts (e.g., for edge), which can equivalently be seen as first-order entailment or second-order model checking [1].¹¹1The views do differ for other reasoning tasks, notably program entailment (a.k.a. query containment), which is decidable for first-order rules but undecidable for second-order programs. Deciding such consequences is P-complete with respect to the set of input facts, making Datalog interesting for data-intensive applications.

Datalog is well supported in practice. Modern rule engines such as clingo [18], Nemo [21], RDFox [30], Soufflé [22], and VLog [34] can easily compute millions of Datalog consequences on commodity hardware. Tools like Datomic (https://www.datomic.com/) and Google’s Logica (https://logica.dev/) are database-oriented and leverage the robustness of existing data management infrastructure. In each case, practical tools include many additional features and language extensions and rely on intricate optimizations to achieve the necessary performance.

Unfortunately, the complexity of real-world systems unavoidably leads to errors that may compromise correctness. Mature systems like the above counteract this with extensive testing, code quality analysis, and public issue trackers, but complete freedom of bugs is rare and volatile in such ever-evolving systems [25, 26, 37]. Stronger correctness guarantees are given by certified Datalog systems, but the few prototypes that exist cannot scale to the input sizes of optimized systems yet [6], or even restrict to a subset of Datalog [7].

In this paper, we address this challenge by developing a certificate checker for Datalog, written and verified in Lean 4[29]. Instead of replacing optimized systems, such checkers validate certificates that prove the correctness of individual results. Successful uses of this approach (a.k.a. the de Bruijn criterion [5]) exist in various fields [20, 4, 17, 35, 8], but we are not aware of any solution for Datalog. This is surprising since the logical semantics of Datalog leads to structured proofs that are suitable certificates. Indeed, systems like Nemo and Soufflé include tracing features that can produce such proof trees for their derivations.

Our main concerns are correctness and performance. For correctness, we formalize the semantics of Datalog in two ways – least models and proofs – and prove their equivalence. We then formalize a checker that builds upon the proof-theoretic semantics to validate given proofs. This also requires us to formalize Datalog syntax, unification, and model theory.

Towards practical performance, we allow the checker to ingest JSON-formatted inputs that encode Datalog rules and (sets of) proofs in an implementation-independent exchange format. For proofs, we consider a traditional encoding in the form of proof trees and a redundancy-avoiding encoding as proof graphs that can be exponentially more succinct. We evaluate the feasibility and performance of our approach using synthetic and real Datalog tasks and proofs generated by the Datalog engine Nemo.

This paper hyperlinks most Lean-symbols to their formal definitions in our repository. Some proofs are abbreviated in the code blocks by _, but are available in the linked code. All proofs in this paper reflect the ideas of the formal Lean proofs in natural language.

We begin by formalizing Datalog and two definitions of its semantics, which we then show to be equivalent. Datalog programs are based on a Signature that provides sets of constants, variables, and relation symbols, where each relation has an arity $\ge 0$:

If not stated otherwise, we use a fixed Signature$\tau$. A Termis a constant or a variable; our formalization uses distinct constructors for each case so that constants and variables are disjoint. Further restrictions are not required in our work.

An Atomis an expression of the form $p(t_1,\mathrm{\dots },t_n)$, where $t_1,\mathrm{\dots },t_n$ are terms and $p$ is a relation of arity $n$. A Rulehas the form $H\leftarrow B_1\wedge \mathrm{\cdots }\wedge B_n$, where the head $H$ is an Atom, and the body $B_1\wedge \mathrm{\cdots }\wedge B_n$ is a conjunction of Atoms (represented as a list in Lean). A Programis a finite set of rules. A GroundAtom(or fact) is an Atomwithout variables and a Databaseis a finite set of facts. A KnowledgeBaseis a pair of a Programand a Database.

The semantics of Datalog is given by defining the set of all facts that are logical consequences of a knowledge base. A (possibly infinite) set of facts is an Interpretation, which can indeed be seen as a first-order Herbrand interpretation, interpreting constant symbols by themselves (a. k. a.unique name assumption). Several equivalent definitions for the semantics of Datalog exist, e.g., based on least models, proof trees, and fixed-point operators [1]. We formalize the first two – model-theoretic and proof-theoretic – semantics, and validate their correctness by proving the equivalence of these distinct definitions.

Both semantics consider GroundRules, i.e., rules that contain only GroundAtoms, obtained from rules by mapping variables to constants. Such a mapping $g$ is a Grounding, and its application to a rule is formalized as applyRule. For a Program$P$, the groundProgram$\mathrm{𝑔𝑟𝑜𝑢𝑛𝑑}(P)$ is the set of all ground rules $r$ obtained from some $r^{\prime }\in P$ by some grounding $g$:

An interpretation $I$ satisfies a ground rule $r$ if, whenever $I$ contains all body atoms of $r$, $I$ also contains the head of $r$. $I$ satisfies a Program$P$ if $I$ satisfies all rules $r\in \mathrm{𝑔𝑟𝑜𝑢𝑛𝑑}(P)$. Finally, $I$ modelsa knowledge base $⟨P,D⟩$ if $I$ satisfies $P$ and $D\subseteq I$. The modelTheoreticSemanticsfor $⟨P,D⟩$ is the least model of $⟨P,D⟩$:

The proofTheoreticSemanticsof a knowledge base $⟨P,D⟩$ is the set of all facts that have a ProofTreevalid in $P$ and $D$. Listing 1 shows our formalization: a directed node-labeled tree $𝒯$ of ground atoms is a ProofTreeSkeletonand it is valid in $P$ and $D$ for a ground atom $a$ if (1) the root of $𝒯$ is labeled by $a$ and (2) for all nodes $t$ (including the root) either (2a) $t$ is a leaf and the label of $t$ occurs in $D$, or (2b) if $s_1,\mathrm{\dots },s_k$ are the children of $t$ in $𝒯$, then there is a rule $r\in \mathrm{𝑔𝑟𝑜𝑢𝑛𝑑}(P)$ such that the head of $r$ is $t$ and the body atoms of $r$ are $s_1,\mathrm{\dots },s_k$. A ProofTreeis then a valid proof tree skeleton. We can now define:

In modelAndProofTreeSemanticsEquivalent, we formally verify the equivalence of the semantics. The proof uses the fact that the modelTheoreticSemanticsyields the least model together with the subsequent lemmas.

In this section, we describe our implementation for a checker of proof tree validity. In contrast to the general formalizations in Section 2, this leads to an effective approach for verifying the soundness of individual conclusions, which can be applied on proof trees that are provided by existing Datalog implementations.

We implement a computable function checkValiditywhose result coincides with the (uncomputable) ProofTreeSkeleton.isValid, shown in checkValidityOkIffIsValid.

Trees are a traditional representation of proofs in logic programming, and many practical tools provide tracing features in terms of tree structures. However, this is far from optimal, as the following example illustrates.

We therefore propose the use of directed acyclic graphs to allow more efficient encodings of certificates. The special case of proof trees is still supported, but optimized outputs are possible if a tool supports them. Lean has graph-theoretic primitives and theorems in its mathlib, but their formalization was not sufficient for our purposes. First, mathlib currently considers undirected graphs and has only very limited results on directed graphs which is crucial to model our problem. Second, its graph model uses an adjacency matrix approach, but we expect the proof graphs to be sparse and therefore expect an adjacency list. Instead, we design two new graph encodings – referred to as unordered and ordered –, which we implement using HashMap and Array, respectively. Both encodings resemble adjacency lists in the sense that each atom is directly associated with all atoms that are used for its derivation.

Both approaches require that the graph is acyclic in order to capture a valid derivation, but differ in the way of achieving this requirement. The ordered approach requires a topological sorting of the graph already as the input and therefore allows faster checking and a more compact representation. The output of reasoners does however not reflect this input format and is instead often just a list of edges. These can easily be verified using the unordered graph approach which computes the topological sorting.

Besides verifying soundness, we also want to provide basic functionality to check if the atoms included in the input form a (first-order) model of the input program. In this section we require rules to be safe (isSafe), i.e. all variables in the head also occur in the body.

In principle, the implementation is straightforward: collect all atoms from the tree/ graph into an interpretation $i$ and check for all possible rule body instantiations if their head is also present. To improve performance over a brute force approach, we introduce PartialGroundRules that allow us to keep track which body atoms we have instantiated while applying the same variable mapping on all other atoms. Any rule can be transformed into a partial ground rule and vice versa so that we may reuse terminology from rules.

Additionally, this structure allows stopping the procedure early. We call a partial ground rule $r$ active in $i$, if all atoms in the grounded body are in $i$. If not active, then $r$ is satisfied for any remaining variable assignment and we can stop early (satisfied_of_not_active).

We use this in a recursive exploration using checkPGR(see Listing 5). If the ungrounded body is empty, then we simply check if the head, which due to the safety assumption must also be a ground atom, is in $i$. If the ungrounded body is not empty, we take the first element and check for all possible substitutions between this element and ground atoms in $i$. In order to be consistent we apply this substitution to the whole partial ground rule (except for the grounded body which is not affected by it). On all these new partial ground rules we again call checkPGR. In order to check the whole program, we call this procedure for every rule which at the start is always active. This returns the correct result (checkPGRIsOkIffRuleIsSatisfied) for any active rule and the newly created rules in the procedure preserve activeness.

Apart from using the activeness of the partial ground rules, the other main idea of the proof is that we can transform groundings that instantiate the first atom of the ungrounded body into a substitution from substitutionsForAtomand a grounding and vice versa. Note that this is only a first version for a completeness check for datalog reasoning not yet implementing optimizations that would be necessary for large models.

In this section, we evaluate the practicality of our Lean implementation on synthetic and real-world examples. Moreover, we compare the different encodings of datalog proofs in practice. To obtain Datalog consequences and proofs, we use the Datalog reasoning engine Nemo [21], which has a tracing feature that returns proof graphs in a custom JSON format.²²2The Nemo version used was https://github.com/knowsys/nemo/releases/tag/v0.7.1 Transformations of Nemo’s output into our various formats are realized by Python scripts. On top of the implementation described in the previous sections, we created a parsing infrastructure for a JSON-based input format in Mainand Parsing.

Database facts are not part of our JSON representation. Instead, we interpret nodes in proof trees or graphs as database facts if they do not have any predecessors. For production use, an explicit representation of the assumed facts would be preferable, resulting in more robust certificates, but this is not important for our (performance) evaluation. A full validation might also have to encompass that facts and rules are correctly read from the input sources (e.g., CSV files), which is beyond the scope of the certification-based approach.

We illustrate the usage of our tool with the following toy example showing both a valid and an invalid proof tree/graph. The example also reflects the experimental setup.

We consider four scenarios – (1a), (1b), (2), and (3) – which include realistic synthetic and real-world applications of Datalog. Moreover, we consider individual certification of single facts and joint certification of many facts. The latter case is implemented for proof trees by checking a collection of trees, and for proof graphs by checking a single graph that includes all conclusions that are to be certified.

1. (1)

   We consider the rules of Example 12 with facts of the form $\mathrm{𝖾𝖽𝗀𝖾}(0,1),\mathrm{\dots },\mathrm{𝖾𝖽𝗀𝖾}(n-1,n)$ for some number $n$. For (1a), we set $n=1000$ and check the conclusion $\mathrm{𝗍𝗋𝖺𝗇𝗌}(0,1000)$ (tcBenchSingleFact); for (1b), we set $n=100$ and check all 5050 conclusions for $\mathrm{𝗍𝗋𝖺𝗇𝗌}$ (tcBenchAllFacts). Transitivity is a frequent type of (sub-)task in Datalog reasoning, but chains of length 1000 are very long even for large datasets, since transitivity is mostly used on hierarchies that are relatively shallow.

2. (2)

   We consider the rules of Example 3 with an edge-chain of length $n=20$, and we check the conclusion $\mathrm{𝗍𝗋𝖺𝗇𝗌}(0,20)$ (tcBenchExponential). This scenario emphasizes the possibly exponential advantage of proof graphs over trees.

3. (3)

   We consider the real-world task of reasoning in the OWL EL profile of the W3C Web Ontology Language, which is possible in Datalog by translating reasoning calculi to rules [12]. We use the derivation rules by Kazakov et al. [23], and the medical ontology GALEN that was also used in the evaluation of their work. The rules and pre-processed input ontology³³3https://github.com/knowsys/nemo-examples/tree/main/examples/owl-el/from-preprocessed-csv yield more than 1.8 million facts. We randomly select 1000 conclusions from the output predicate mainSubClassOf that represents the output of the EL reasoning task (elReasoning).

All experiments were performed on a mid-range laptop (Intel Core i5 gen8, 16GB RAM, NixOS Linux). Table 1 reports the results including Nemo reasoning times without tracing. The other columns give the proof file sizes and total validation time for the scenarios representing proofs as trees (T), unordered graphs (G), or ordered graphs (O). Times are overall wall-clock times of the prototype checker averaged over 5 runs, and sizes refer to compact (not pretty-printed) JSON. For example, while Nemo reasons in (1b) for less than 0.1 seconds, the proof trees amount to 53MB of JSON taking 2.7 seconds to validate.

Overall, even the check based on unordered graphs is very fast in all cases and the tree-based implementation achieves similar performance in cases (1a) and (3). The overall fast times for (3) reflect the fact that proofs in real-world applications are rarely very deep, even in cases where millions of consequences are derived. The advantages of graphs are seen when considering many overlapping proofs (1b) and, as expected, for rules that realize the exponential worst-case penalty of using proof trees (2). The ordered graph approach outperforms the others in all scenarios regarding both time and memory.

We still find that both tree-based and graph-based validations are fit for practical use. While graphs are theoretically and empirically superior, the choice may also be governed by the native tracing output of a tool (which is graph-like in Nemo, but tree-like, e.g., in Soufflé). While the ordered graph would always be the best option, it also requires some additional effort to output the trace in the right order. But when all inferences have indeed been done properly by the reasoning engine, this should not be too much of a challenge.

The de Bruijn criterion [5] requires that the software tools (e.g., logical reasoners) provide certificates together with their output and the tool checking the validity based on output and certificate (e.g., our Lean-based validator) are independent entities. Besides certificate-based verifiers [4, 20], a similar criterion has been coined as certifying algorithms in software engineering [28]. One approach there is to transpile certificate checker code written in the C programming language to an interactive theorem prover. Alkassar et al. [2] use a transpilation to Isabelle to verify the certificate checker in this sense. Thereby, one has to additionally trust the transpilation while our work implements the checker directly in Lean. Baader et al. [3] generate certificates for consequences of the description logic $ℰℒ$, computed by an existing $ℰℒ$-reasoner. The validation of the generated proof certificates is done by the LSFC checker⁴⁴4https://github.com/CVC4/LFSC. In contrast to this approach, we have provided the correctness of our proof validator (w.r.t.the Datalog semantics) ourselves and, therefore, do not rely on third-party developments like the LSFC checker. Our approach partly generalizes the work of Baader et al.in that the $ℰℒ$-reasoning calculus can be expressed in Datalog [24], making our proof validator also available to $ℰℒ$ reasoning.

Another approach to building trust in automated reasoning engines is to implement the reasoner itself (i.e., not a certificate checker) in Lean. For instance, Benzaken et al. [6] and Dumbravă [15] proposed a certified Datalog engine written in Rocq. Later on, a similar approach was implemented for a subset of Datalog, which Bonifati et al. [7] call Regular Datalog, for (knowledge) graph view maintenance. The Rocq implementations formalize the model-theoretic semantics up to basic definitions for rule satisfaction and modelhood, but fully integrate the fixed-point semantics for proving correctness. Whitehead [36] also formalizes the fixed point semantics of Datalog and its extension Binder, a security logic, in Rocq to extract a monitoring framework for access control policies. An Isabelle/HOL formalization of the model-theoretic semantics of stratified Datalog – an non-monotone extension of Datalog – is provided by Schlichtkrull et al. [32] to verify program analysis algorithms, which are themselves written in Datalog. In contrast, our work fully formalizes the model-theoretic semantics as well as the proof-theoretic semantics, neglecting the fixed point semantics. Thereby, we aim at independence of our implementation from the reasoners in use (i.e., ultimately satisfying the de Bruijn criterion). This independence additionally preserves the original reasoners’ efficiency.

A rather data-driven approach has been coined as data provenance [9, 19], providing explanations in different formats (formalized as expressions of certain semirings). Such explanations are often based on the (finite) input database. Notably, usual provenance explanations for Datalog reasoning results are obtained from analyzing all (i.e., infinitely many) proof trees [16] or a careful selection thereof [10]. Thus, our work provides the necessary ingredients to obtain a fully formalized theory of data provenance for Datalog. While provenance solutions, specialized for particular reasoners [31], exist, our certificate-based framework is independent of the reasoner in use, as long as it provides proof trees (i.e., certificates) for their derivations.

We propose a certificate-based approach to the verification of Datalog reasoning, built on the proof-theoretic semantics of Datalog. The certificate checker is formalized and implemented in Lean, validating proof trees of Datalog conclusions, as provided by Datalog tools such as Nemo [21] or Soufflé [22]. Our evaluation shows that the exponentially more succinct proof graphs can accelerate the validation of complex derivations or multiple conclusions.

In practical applications, Datalog is often extended with further features, which should be covered in future works. Relevant extensions include: (1) negation in rule bodies, stratified or under a general semantics for normal logic programs; (2) existential quantification in rule heads [11]; (3) datatypes and aggregate functions; and (4) function terms and complex values, such as tuples or sets [1, 27]. Function terms, complex values, and existential quantifiers are closest to our work, since they admit similar proof structures. With negation and aggregates, proofs must refer to all facts of a certain shape, e.g., to show that a conclusion was not derived, which can lead to larger proofs and more checks. Stratified negation has already been integrated in certified reasoners [6, 7], but certificate checkers for stratified Datalog do not yet exist. Datatypes in turn present their own challenges, but their validation could be based on existing support for some datatypes in Lean.

Within a Datalog toolchain, our tool builds trust in these database systems with the ability to exemplarily verify derivations. In principle, one could automatically check the proof trees for each derivation. In many applications this might not be viable if there is a large number of facts and is likely also not necessary once we can be sure enough that the system indeed works as intended after enough exemplary checks. However, for critical applications, one could directly generate certificates, i.e. proof trees/graphs, for each derived fact and autmatically check their correctness with our tool. When debugging a Datalog program or even the system itself, our certified checker can act as a companion to explainability tools by checking that the given explanation in form of a proof tree/graph is valid in the first place, which enhances user trust into the explanation and the result of the Datalog system. Another line of research is to directly verify the Datalog reasoner itself but, as mentioned in the introduction, this is challenging since today’s Datalog systems are highly sophisticated and optimized pieces of software. Reimplementing the systems in e.g. Lean most likely cannot compete with implementations directly done in C(++) or Rust in terms of performance. However, it might be possible (with significant effort) to maintain both implementations (the formally verified one and the fast one) and verify with enough tests that their components behave the same on all inputs. Automatic transpilations could also come in handy here.