XLOG: A CUDA-Native Engine for Neurosymbolic Integration

Levi Dubrovin; Nikita Pospelov; Kirill Sabitov

cs.AISep 23, 2026

XLOG: A CUDA-Native Engine for Neurosymbolic Integration

Authors: Levi Dubrovin, Nikita Pospelov, Kirill Sabitov

Organizations: Brainyblaze Dynamics Inc.

Abstract

xlog is a CUDA-native logic programming engine integrating neural perception with deterministic Datalog, probabilistic inference, and epistemic world views through a typed frontend and provider-owned CUDA runtime. Its reasoning modes share device data planes, but their execution boundaries differ: ordinary Datalog and exact inference are host-orchestrated, while certified resident recursive and Monte Carlo sampled cores record zero tracked host-device transfers before a bounded terminal receipt. The probabilistic path supports end-to-end gradients through GPU knowledge compilation from provenance to CNF to Decision-DNNF, exact weighted model counting, and backward gradients. A final smoothed circuit is certified against its source formula before caching or evaluation. Circuit caching yields a 2.74x MNIST-addition training speedup; a worst-case-optimal join subsystem yields a 27.96x geometric-mean gain over xlog's binary-join baseline. MNIST-addition accuracy matches Scallop's (0.9561 versus 0.9468), but no per-epoch speed claim is made because baseline epoch time varies with CPU quota. In five hub-skewed triangle-counting cases, the Souffle-to-fused-xlog execution-time ratio rises from 0.88x at 150k edges, where Souffle is faster, to 5.54x at 1.2M; fused peak device allocations are 85-1,033 MB versus 3,287-44,979 MB for the materializing arm. Exact inference is correctness-equivalent to but slower than ProbLog2. On a public video benchmark, a proximity predicate trained only through symbolic credit replaces hand-set geometry at unchanged held-out accuracy; within Event-Calculus rule search it fails ten-fold cross-validation and does not transfer on a leak-free split. On a maritime corpus, weighted clauses beat crisp selection by 0.065 F1, with the result reproduced by one chronological training pass.

Figures & tables

Panel of Figure 1 — Figure 1: xlog crate hierarchy. Each tier depends only on lower tiers; the shaded device plane marks GPU-resident runtime data planes, while the host provides orchestration, I/O, compilation, and bounded control reads.

Kernel	Purpose
join	Hash join with linked-list collision chains and FNV-1a composite hashing over raw key bytes, so all scalar types share one path; count $\to$ scan $\to$ materialize variants for inner and left-outer joins.
sort	Stable 4-bit radix sort (8 passes over 32-bit keys): per-pass histogram, prefix sum, scatter.
filter	Comparison operators for column-vs-constant and column-vs-column, with stream compaction via prefix sum.
groupby	Sorted-input grouped aggregation: boundary detection, then per-group Count/Sum/Min/Max/LogSumExp reduction.
dedup	Sort-based deduplication and set difference with type-aware equality, including IEEE 754 float handling.
set_ops	Union (concat + sort + dedup) and set difference via sorted-array binary search.

Table 1: Core relational CUDA kernels.

Panel of Figure 2 — Figure 2: Verified knowledge-compilation pipeline. The data plane uses CUDA kernels and device-resident state under host orchestration. The final smoothed circuit $C$ reaches evaluation only through the equivalence gate (✓): an on-GPU CDCL solver proves $\varphi\wedge\lnot C$ and $C\wedge\lnot\varphi$ both unsatisfiable; the host observes bounded status and error scalars, and any failed or incomplete proof returns a typed error.

Panel of Figure 3 — Figure 3: One neurosymbolic training iteration. Neural tensors, circuit values, and gradient buffers occupy one CUDA device (shaded plane); the measured circuit hot region records zero tracked data-plane transfers. The host still orchestrates stages and observes bounded control state. The final smoothed circuit is compiled and certified once (✓, Figure 2 ), then reused across iterations, and gradients re-enter PyTorch’s autograd graph zero-copy through DLPack.

Judgement	What it judges	Path
Six always-run gates	the rule derives every training positive and no training negative, passes the novel-fact audit, loses no protected fact, meets a held-out F1 threshold, and names only relations with typed schemas	dILP
Two held-out gates	the same rule on the supplied held-out positives and negatives	dILP
Ambiguity scan	which other candidates also explain the data; reported, never decisive	dILP
Permutation-null fit threshold	whether a candidate generalizes better than shuffled labels do on its own fold	arbiter

Table 2: What judges what, on which path: the promotion pipeline of differentiable ILP or the holdout arbiter of Section 6.5 . Convergence and supplied held-out examples are preconditions, not gates: without them the pipeline returns for manual review before any row below runs.

Windowed folds, direct target (mean of 3 folds)
Run	P	R	F1
precomputed close	—	—	0.7905
learned close_nn	—	—	0.8276
Distributed corpus, 10-fold CV, EC + inertia
pre-registered	0.6580	0.8271	0.7329
+ termination relations	0.7357	0.8260	0.7782

Table 3: Runs reported in this section. Micro F1 over pooled per-fold counts, except the windowed rows, which are fold means. The + termination relations row is the second, adaptive vocabulary iteration. The clean-protocol zeros are scored predictions, not empty theories, except the moving Event-Calculus row, whose initiation theory is empty on every fold; the census behind them is in the text. Published figures for the same benchmark are tabulated separately in Section 10 .

Quantity	Value
Rows (vessel pair $\times$ timestamp)	$454{,}858$
Vessel pairs	$806$
carrying a rendezVous interval	$302$
negatives, by fixed stride	$504$
Gold intervals	$3{,}548$
Positive rows	$3{,}579$

Table 4: The pair-time corpus, as the converter leaves it. The negative pairs are drawn by fixed stride from the

2{,}014

pairs that come within proximity but carry no interval.

Base vocabulary (11 relations; declared ceiling ${\approx}0.66$ )
Run	P	R	F1	F1, fold median
crisp search	0.5109	0.9925	0.6746	0.6596
weighted, batch	0.8715	0.6426	0.7398	0.6928
weighted, forward pass	0.8715	0.6426	0.7398	0.6928
weighted, reverse pass	0.8715	0.6426	0.7398	0.6928
Duration vocabulary ( $+$ sustained_240 ; ceiling $0.9969$ )

Table 5: Maritime rendezVous : five-fold cross-validation over whole vessel pairs, seed 7. P, R and F1 are pointwise micro-averages over pooled per-fold counts; the last column is the median of the five per-fold values. The three base-vocabulary weighted rows are identical row by row, though their weights are not: fold 0’s top body carries

\sigma(w)=0.6476

in batch,

0.5880

in the forward pass and

0.8398

in the reverse, and the

L_{\infty}

distance between the logit vectors of any two regimes is

1.06

–

2.95

. Interval-level F1: 0.6772 (crisp, base; 3,545 of the 3,548 gold intervals matched), 0.7435 (weighted, base), 0.9970 (both duration rows). No published figure appears here ( Section 8.4 ).

Base vocabulary	f0	f1	f2	f3	f4
crisp search	0.9933	0.4690	0.6685	0.5699	0.6596
weighted, all three	0.9346	0.4237	0.8000	0.6928	0.5342
Pooled counts	tp / fp / fn
ceiling probe, base	3,579 / 3,689 / 0
crisp search	3,552 / 3,400 / 27
weighted, all three	2,300 / 339 / 1,279

Table 6: Per-fold F1 on the base vocabulary and the pooled counts behind Table 5 . The three weighted regimes share a row because their predictions are identical. The probe rows evaluate the gold rule’s definitional body directly; the duration probe’s

22

residual false positives are what its

0.9969

ceiling reflects.

Setting	Value
Sample size	10–100 runs (benchmark-dependent)
Warm-up	3 iterations (PTX JIT, memory-pool init)
Significance level	0.10
Noise threshold	0.05 (ignore ${<}5\%$ variance)
Seeding	Deterministic LCG

Table 7: Benchmark harness settings.

Item	Value
Query	three-way triangle join, one multiway join
Key generation	four fixture variants, coinciding size parameters
Input	three relations of $65{,}536$ rows each
Output	${\approx}4.19$ M triples
Warm-up	$20$ windows
Reported time	mean of $10$ timing windows

Table 8: Triangle-join fixture and timing protocol for the WCOJ ablation.

Figure 4: WCOJ vs. binary-join speedup on the four key-generation variants of the triangle fixture ( Table 8 ). Single-system ablation; the dashed line is the geometric mean.

Metric	Value	Notes
First epoch (cold)	$71.7$ s	D4 compile + CDCL verify
Steady-state epoch (warm)	$0.25$ s	cached forward/backward path
Total training (5 epochs)	$72.6$ s
Per-query cost (steady state)	$0.97$ ms	forward + backward; steady epoch over 256 pairs, cold epoch excluded
Ablation, uncached arm	$242.9$ s	mean training time, recompiling every epoch
Ablation, cached arm	$88.9$ s	mean training time, compiling once

Table 9: MNIST-addition training summary. The timing rows come from a 512-image, 5-epoch training run at batch size 64; the ablation rows come from a separate experiment (512 images, 3 epochs, 3 seeds), whose speedup is the mean of its three per-seed ratios, not the ratio of its means.

Mode / task	Baseline	xlog	Baseline	Ratio
Neural: MNIST addition; 20 000 training images, 5 epochs, 3 seeds, held-out on the 10k test set	Scallop	acc $0.9561\pm 0.0008$	acc $0.9468\pm 0.0104$	accuracy parity; no timing claim
Probabilistic: exact inference on five small programs	ProbLog2	$0$ error; per query flat at $0.79$ – $0.87$ s	$0$ error; per query $0.0085$ – $0.0186$ s	$45$ – $100\times$ slower
Deterministic: triangle counting on hub-skewed graphs of $3.65$ M to $17.84$ M triangles	Soufflé (standalone compiled mode, 26 jobs)	counts match at every size; $0.57$ – $0.68$ s, nearly flat in the input; peak device allocations $85$ – $1{,}033$ MB	$0.51$ – $3.77$ s, growing with the input; one-time per-case compilation recorded separately	Soufflé/xlog: $0.88\times\to\mathbf{5.54\times}$

Table 10: Head-to-head comparisons: one external engine per reasoning mode, matched programs, data, metrics and seeds, on cloud GPU pods. The correctness and all-arm completeness gates pass for every comparison.

System	P	R	F1	Source
Hand-crafted rules	$0.644$	$0.855$	$0.735$	OLED [ 21 ] Tab. 1(b), EC_crisp ; the same value appears in WOLED [ 22 ] Tab. 2
OLED	$0.678$	$0.953$	$0.792$	OLED [ 21 ] Tab. 1(b), whole dataset
OLED, as re-run by other authors	—	—	$0.782$	WOLED [ 22 ] Tab. 2
This work, EC ${}+{}$ inertia, pre-registered	$0.6580$	$0.8271$	$0.7329$	10-fold CV by video segment, all gates re-derived per fold ( Section 7 )
WOLED-ASP	—	—	$0.887$	WOLED [ 22 ] Tab. 2

Table 11: Frame-level holdsAt F1 for the meeting fluent on the distributed CAVIAR corpus, micro-averaged over pooled counts. Rows are ordered alphabetically by system name, not by F1: the five protocol deltas printed beneath the table do not all act in the same direction. Dashes are figures the cited table does not report.

Run	Corpus	P	R	F1	tp / fp / fn
meeting , Event-Calculus route, pre-registered	distributed	$0.6580$	$0.8271$	$0.7329$	$1516$ / $788$ / $317$
meeting , direct-protocol reference, same folds	distributed	$0.6864$	$0.1266$	$0.2137$	$232$ / $106$ / $1{,}601$
meeting , Event-Calculus route with learned close_nn	distributed	$0.1250$	$0.0005$	$0.0011$	$1$ / $7$ / $1{,}832$
meeting , Event-Calculus route	clean	—	—	$0.0$	$0$ / $120$ / $1812$
meeting , direct route	clean	—	—	$0.0$	$0$ / $106$ / $1812$
moving , Event-Calculus route, no initiation clause on any fold	clean	—	—	—	$0$ / $0$ / $3136$

Table 12: Frame-level holdsAt scores for every rule-induction run of Section 7 , micro F1 over pooled per-fold counts. The distributed corpus is the dump shipped with the published Event-Calculus learners and carries the duplication defect measured in Section 7 ; the clean corpus is its deduplicated, scene-family-grouped form. Dashes are quantities the run does not report separately.

Verification cost
Setting	Measured
chain $n{=}5$	CDCL verify $531$ ms
chain $n{=}40$	CDCL verify $2{,}633$ ms
Residency benefit
per handoff	round-trip of roughly $61$ – $176\,{\mu}$ s
$32$ handoffs/step	$9.2\%$ of the step

Table 13: Design-cost isolations. Verification splits the cold compile on probabilistic reachability chains of length

n

. Residency forces a device

\to

host

\to

device round-trip at the neural–symbolic boundary, swept over

2

512

handoffs per step on the batched addition path.

Fixture	Baseline median $\to$ optimized median
Persistent index reuse: repeated-session semi-join, eight left rows probing eight million right rows	$15.78$ ms $\to$ $1.89$ ms, a $8.33\times$ gain over $9$ timed runs after $12$ warm-up runs
Shared-memory chain scorer: chain-hot body search, $768$ candidate rows against a gate threshold of $256$	$52.42$ ms ( $52.41$ – $52.97$ ) $\to$ $7.28$ ms ( $7.28$ – $7.29$ ), a $7.20\times$ gain over $12$ timed runs after $3$ warm-up runs

Table 14: Runtime-optimization ablations, each a median over the timed runs of one synthetic fixture.

Dimension	DeepProbLog	Scallop	Lobster	GPUlog	xlog
Symbolic execution	CPU (Prolog)	CPU (Datalog)	GPU (Datalog)	GPU (Datalog)	GPU (semi-naive)
Probabilistic inference	Exact (CPU)	Provenance (CPU)	Provenance (GPU)	None	Exact d-DNNF + MC (GPU)
Circuit verification	None	None	None	—	On-GPU CDCL
Neural integration	Prolog bridge	Differentiable	Differentiable (GPU)	None	Zero-copy, fused
Zero-copy ML interop	No	Partial	Partial	No	Yes
Rule structure induction	No	No	No	No	Yes (beta): trainable bodies, dILP

Table 15: Capability comparison across neurosymbolic and GPU logic systems.

Neuro-Symbolic Reasoning

Neuro-symbolic reasoning combines learned neural models with explicit logic, rules, knowledge structures, or executable tools to solve structured tasks.

See all 275 papers

DeepSWIP: Quotient-WMC Counterfactuals for Neural Probabilistic Logic Programs
Jun 18, 2026Saimun Habib, Vaishak Belle, Fengxiang HeProbabilistic Logic Structural Causal Models
University of Edinburgh
DeepLog: A Software Framework for Modular Neurosymbolic AI
May 11, 2026Robin Manhaeve, Stefano Colamonaco, Vincent Derkinderen +4Neuro-Symbolic AI Neurosymbolic Learning
Department of Computer Science and Leuven.AI KU Leuven, Belgium
Efficient Counterfactual Reasoning in ProbLog via Single World Intervention Programs
Mar 20, 2026Saimun Habib, Vaishak Belle, Fengxiang HeCounterfactual Reasoning Probabilistic Programming
University of Edinburgh, Edinburgh, United Kingdom · The MITRE Corporation, McLean, Virgina, USA

Jun 18, 2026J/K move · Enter open · S save

DeepSWIP: Quotient-WMC Counterfactuals for Neural Probabilistic Logic Programs

Saimun Habib, Vaishak Belle, Fengxiang He

University of Edinburgh

Probabilistic Logic Structural Causal Models Neuro-Symbolic Reasoning Probabilistic Programming Counterfactual Reasoning

Open paper AskPDF arXiv

Neurosymbolic systems such as DeepProbLog combine neural perception with probabilistic logic, but standard inference is associational. Counterfactual reasoning additionally requires a causal semantics for interventions and evidence. We introduce DeepSWIP, a single-world counterfactual semantics for DeepProbLog programs. Using neural materialization, we reduce fixed-context neural predicates to ordinary ProbLog choices, apply Single World Intervention Programs (SWIPs), and compute counterfactuals by weighted model counting (WMC) over a single transformed program. Under finite grounding and unique-supported-model assumptions, DeepSWIP is exact relative to the learned materialized FCM. The standard quotient-WMC form of ProbLog conditionals identifies active neural probabilities and explains intervention cleaning, calibration sensitivity, and rare-evidence instability. Experiments on MPI3D confirm the transformation against a DeepTwin construction against 12,000 queries, as predicted and a 2.14

\times

inference speedup from avoiding the Twin's endogenous duplication. A SUMO HOV experiment shows that neural calibration degradation biases plug-in estimates, while a correctly scoped randomized-policy AIPW estimator removes most first-order bias for population mean and ATE estimands. Code is at https://github.com/saibib/deep_SWIP.

Abstract

Neuro-Symbolic Reasoning

Explore similar work

DeepSWIP: Quotient-WMC Counterfactuals for Neural Probabilistic Logic Programs

DeepLog: A Software Framework for Modular Neurosymbolic AI

Efficient Counterfactual Reasoning in ProbLog via Single World Intervention Programs