PaperlayerView exact revision on arXiv

Source-linked AI summary

XLOG: A CUDA-Native Engine for Neurosymbolic Integration

Levi Dubrovin, Nikita Pospelov, Kirill Sabitov

arXiv:2609.27203v1cs.AI

TL;DR

Neurosymbolic integrations often place neural and symbolic computation on different processors, making repeated transfers a concern for large workloads. xlog combines neural predicates and multiple reasoning routes through a CUDA-native engine, with verified probabilistic compilation and measured results that vary by workload.

  • Problem

    Neurosymbolic systems often put neural computation on GPUs and symbolic backends on CPUs, so exchanging network outputs, symbolic results, or gradients can move data across PCIe.

    Source: §1 · p. 1

  • Method

    xlog treats networks as predicates and uses GPU knowledge compilation to turn probabilistic provenance into circuits for exact weighted model counting and backward gradients.

    Source: §5 · p. 8

  • Results

    Across workloads, xlog’s measured outcomes are mixed; weighting maritime clauses adds 0.0652 micro F1 over the crisp pool, and single-pass weights reproduce batch predictions exactly.

    Source: §8.4 · p. 18, §13 · p. 29

  • Takeaways & Limitations

    The measurements indicate xlog pays off on large, repeated symbolic workloads, including circuit reuse and skewed cyclic joins, while losing to a mature CPU compiler on small exact-inference programs.

    Source: §13 · p. 29

    On the leak-free, scene-family-grouped video corpus, too few initiation events support a cross-validated claim, and the committed clause does not transfer.

    Source: §12.1 · p. 29

Abstract

from arXiv · show

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.

1 Introduction

xlog addresses cross-processor data movement and fragmented neurosymbolic interfaces with a shared CUDA-native engine, while keeping the execution and gradient guarantees of its reasoning routes distinct. The introduction highlights measured gains in circuit reuse and skewed joins alongside benchmark-specific successes and limits.

Shared integration model

  • xlog treats networks as predicates and routes their outputs as weighted facts through probabilistic compilation, where exact query gradients can flow back to the network.Typed device-buffer interfaces also connect other supported reasoning routes, without claiming identical gradient semantics.Source: §1 · pp. 1–2

Contributions

  • 2.74× circuit caching speedup and a 27.96× geometric-mean WCOJ gain over xlog’s binary-join baseline are the introduction’s quantified system results.Circuit caching is measured on MNIST-addition training; the join gain is measured on skewed cyclic queries.Source: §1 · p. 2

External video benchmark

  • On CAVIAR, symbolic-credit training replaces the hand-set proximity predicate at unchanged held-out accuracy, but substituting the learned detector into Event-Calculus rule search fails.The passage distinguishes direct per-timestep target training from the separate Event-Calculus search setting.Source: §1 · p. 2

Maritime rule induction

  • Weighting maritime clauses raises micro F1 by 0.065 over crisp selection, and one chronological pass reproduces batch predictions exactly.The comparison uses the same gated clause pool; no comparison is claimed with the published maritime figure because its temporal grid differs.Source: §1 · p. 2

Reasoning beyond probability

  • The engine reuses its substrate for epistemic world views and well-founded semantics, including supported recursion through negation.The supported cases include finite programs and positive modal fixpoints.Source: §1 · p. 2

Target workloads

  • The target regime is large, repeated symbolic work; small MNIST-addition workloads demonstrate correctness and caching effects, while transfer costs are secondary and variable.At standard batch size, transfer is approximately 10% of a training step, and can be lost in run-to-run variation when only a few neural-to-symbolic handoffs occur.Source: §1 · p. 2

2 Integration Model and Architecture

xlog connects neural predicates to supported reasoning routes through typed device-buffer interfaces and a provider-owned CUDA runtime. Its architecture keeps data planes on the GPU while assigning orchestration and compilation to the host.

2.1 The integration model

  • A network is a predicate whose softmax may become weighted facts; exact query gradients flow through probabilistic knowledge compilation, while other routes do not claim the same gradient semantics.Facts, circuit values, and gradients remain device-resident at their data-plane handoffs.Source: §2.1 · p. 3

2.2 GPU residency model

  • The provider owns the runtime resources, and the certified resident recursive and Monte Carlo sampled cores record zero tracked transfers before returning one bounded terminal receipt.Exceeding byte or count capacities raises an error rather than silently spilling to a host executor.Source: §2.2 · p. 3

2.3 Crate architecture

  • The system’s tiers are strictly layered, with provider-owned CUDA resources and integrated compiler, runtime, and solver subsystems exposed through Python and a command-line interface.The crate hierarchy has no peer- or higher-tier dependencies.Source: §2.3 · p. 3

2.4 From program to GPU plan

  • Compilation parses programs, analyzes dependencies and SCCs, lowers into route-specific IRs, optimizes plans, and assembles GPU execution plans.Supported negated recursion uses GPU-backed well-founded semantics rather than the ordinary semi-naive schedule.Source: §2.4 · p. 3

2.5 Reasoning IRs and circuit format

  • RIR represents relational execution, PIR represents weighted provenance formulas, and EIR preserves modal operators; probabilistic compilation emits XGCF for device-resident circuit evaluation.SAT/MaxSAT and verification use a shared solver service rather than a fourth reasoning IR.Source: §2.5 · pp. 3–4

3 The xlog Language

The xlog language uses typed predicates and shared syntax for multiple reasoning paradigms, with backend-specific lowering preserving their semantics. Constructs that cannot be safely lowered within finite GPU-native execution are rejected rather than sent to a hidden CPU interpreter.

3.1 Design principles

  • xlog shares a syntactic core for deterministic rules, probabilistic facts, neural predicates, and SAT constraints, while dependency analysis and backend-specific lowering preserve route semantics.Unsupported shapes and unbounded terms are rejected before execution.Source: §3.1 · p. 4, §3 · p. 4

3.2 Type system

  • Predicate schemas use eight scalar types, can be declared or inferred, and are checked during compilation before kernel generation.String literals map to symbols through a global table; type mismatches in variables, constants, and arithmetic are rejected.Source: §3.2 · p. 5

3.3 Expressions, arithmetic, and user-defined functions

  • Rule bodies support arithmetic, comparisons, and user-defined functions, which inline into expression trees and share predicate-pushdown and expression optimization.Relational function calls can contribute zero, one, or many rows; nested expansion is depth-bounded, and unsupported conditional-branch calls are rejected.Source: §3.3 · p. 5

3.4 Modules and imports

  • Modules import whole files or selected names, and the resolver checks cycles and declarations before merging imported rules into the logical program.It performs bounded cross-module schema inference before full compiler type inference and route planning.Source: §3.4 · pp. 5–6

3.5 Aggregations and constraints

  • Aggregations lower to GroupBy kernels, are barred from recursive SCCs, and integrity constraints diagnose bodies that remain satisfiable at fixpoint.logsumexp supports probabilistic circuits with log-space numerical stability.Source: §3.5 · p. 6

3.6 Completeness over finite domains

  • Finite typed lists, selected statically resolvable meta-predicates, stratified negation, magic sets, and finite probabilistic aggregates extend the accepted language.Open-ended generators, dynamic database mutation, unrestricted call/N, and runtime-variable predicate names remain outside the contract.Source: §3.6 · p. 6

4 GPU-Native Symbolic Substrate

The symbolic substrate provides CUDA relational execution and device-resident relation storage, with an ordinary host-orchestrated executor and a certified resident route for eligible recursive plans. Join planning and runtime optimizations target intermediate blowup and repeated work.

4 GPU-Native Symbolic Substrate

  • Eligible recursive plans use a certified resident conditional graph with zero tracked transfers in its core, while ordinary Datalog execution remains host-orchestrated.The resident core records one launch and synchronization, then returns a pinned terminal receipt rather than tuple data.Source: §4 · p. 6

4.1 Semi-naive evaluation on GPU

  • Semi-naive evaluation reruns recursive rules over delta variants until no new tuples are produced, keeping unions, differences, and deduplication on-device.A self-join contributes a delta-rewritten variant for each recursive scan occurrence.Source: §4.1 · p. 6

4.2 Relational kernels

  • Bespoke CUDA relational kernels keep intermediate buffers on-device and make allocation, synchronization, and host staging explicit.Table 1 summarizes the core relational kernels.Source: §4.2 · p. 7, Table 1 · p. 7

4.3 Adaptive join planning

  • The planner pushes predicates using runtime statistics and uses deterministic greedy join ordering, with recognized triangle and four-cycle selectivity rewrites.General dynamic-programming join ordering is not active.Source: §4.3 · p. 7

4.4 Worst-case-optimal joins

  • WCOJ addresses potentially oversized binary-join intermediates on cyclic queries, promoting eligible rules while retaining binary plans for others.A skew classifier dispatches high-skew inputs to WCOJ and uniform or empty inputs to the binary-join chain; the kernel uses count, device prefix scan, and materialization.Source: §4.4 · p. 7

4.5 Runtime optimization

  • Runtime optimization reduces repeated work through safe subplan caching, telemetry-triggered plan re-optimization with equivalence checks and rollback, and persistent hash indices.The persistent index manager keys entries by relation generation, schema, and device, and uses deterministic LRU eviction.Source: §4.5 · p. 7

4.6 Reversible symbols

  • Strings are interned as dense u32 identifiers for GPU operations and resolved at output, while Arrow dictionary export preserves a compact representation without copying.The string table stays host-side because variable-length data is needed only at ingestion and output.Source: §4.6 · p. 8

5 Verified Knowledge Compilation

xlog compiles probabilistic programs into GPU-resident arithmetic circuits for exact weighted model counting and gradients, then certifies the final smoothed circuit before use. Circuit reuse and a resident Monte Carlo alternative extend this compilation path.

5.1 The compilation pipeline

  • xlog transforms a probabilistic program through provenance, CNF, and Decision-DNNF into an arithmetic circuit for exact weighted model counting and backward gradients.Intermediate data stays in device buffers while the host orchestrates compilation stages.Source: §5 · p. 8, §5.1 · p. 8

5.2 Verification: a machine-checked certificate

  • The final smoothed circuit is accepted only after an on-GPU solver proves it equivalent to its back-end formula; provenance extraction and CNF encoding remain trusted.A failed, incomplete, or budget-limited proof returns a typed error rather than allowing caching or evaluation.Source: §5.2 · p. 8, §5.1 · p. 8

5.3 Circuit caching

  • Because neural weight updates leave the Boolean formula unchanged, xlog caches the certified circuit by provenance structure and evidence configuration, then updates only weight buffers.Subsequent iterations use the cached circuit’s forward and backward kernels.Source: §5.3 · p. 9

5.4 Monte Carlo alternative

  • The approximate-inference alternative samples probabilistic facts on the GPU and evaluates each sampled world, using rejection sampling or evidence clamping when evidence atoms are Bernoulli facts.Its resident sampled core records zero tracked transfers and returns a bounded receipt; convergence or resource limits produce typed failures rather than host fallback.Source: §5.4 · p. 9

6 Neurosymbolic Integration

xlog treats neural networks as typed predicates connected to supported reasoning routes through device buffers. The integration supports cached differentiable training, zero-copy framework interoperability, trainable rule bodies, candidate selection, and complementary embedding and differentiable-ILP paths.

6.1 Neural predicates

  • A neural predicate’s softmax becomes weighted facts for probabilistic compilation, and circuit gradients return through DLPack to PyTorch autograd; predicates may also appear in rule bodies.Typed registry metadata lets downstream rule learners validate candidates against declared predicates rather than naming conventions.Source: §6.1 · p. 10

6.2 End-to-end training

  • 2.74× training speedup comes from compiling and verifying the circuit once, then reusing it for weight updates and level-parallel forward/backward kernels.Loss reduction across seeds confirms gradients flow through circuit evaluation and the logic program back to the CNN.Source: §6.2 · p. 10

6.3 Zero-copy interoperability

  • DLPack and Arrow expose device-resident tensors and relations to frameworks and columnar tools, while PyTorch autograd can consume circuit gradients without a custom autograd function.The training-iteration figure describes the circuit hot region as recording zero tracked data-plane transfers while host orchestration remains.Source: §6.3 · pp. 10–11, Figure 3 · p. 11

6.4 Trainable rule bodies

  • Trainable rule bodies combine neural atoms with hard symbolic join conditions, learned rule weights, and optional per-binding gates; gradients reach the network outputs and rule weights.By default, features are detached so gradients stop at their producer; an explicit candidate flag allows them to continue into the backbone.Source: §6.4 · p. 11

6.5 Engine-mode credit and candidate selection

  • Engine-mode credit scores enumerated candidates from witness semantics, then held-out folds and fit gates select by generalization rather than trained weight.The selector can prefer a uniquely supported relational candidate or abstain when the evidence cannot distinguish candidates.Source: §6.5 · p. 12

6.6 Term embeddings and differentiable ILP

  • Term embeddings provide trainable continuous representations of logical symbols, while differentiable ILP learns rule structure using sparse bitmasks and on-device credit assignment.Differentiable ILP is complementary to trainable rule bodies, but is a beta subsystem and is not exercised in the benchmark section.Source: §6.6 · pp. 12–13

7 Learning Event Rules from Perception

The section tests whether symbolic credit can train the perceptual predicate used in Event-Calculus rule induction. A learned proximity predicate replaces hand-set geometry under the direct per-timestep target, but the induced meeting rule does not transfer across scene families.

7.1 Protocol

  • The leak-free protocol folds by scene family because the distributed corpus contains duplicate events and source videos shared across its train and test files.The audit found 21 of 25 meeting transitions real, three duplicates, and one splice artifact.Source: §7.1 · p. 14

7.2 Results

  • 0.8276 versus 0.7905 mean held-out F1: the learned proximity predicate matches or exceeds hand-set geometry across the three direct per-timestep folds.It is trained through symbolic credit alone, without a distance label or perceptual target.Source: §7 · p. 13, §7.2 · p. 14
  • On the combined 26-segment corpus, ten-fold Event-Calculus cross-validation yields precision 0.6580, recall 0.8271, and F1 0.7329.The initiation clause is selected on all folds, while the termination theory is empty on all ten.Source: §7.2 · p. 14
  • The reported 0.7329 F1 is just below the published figures, but protocol differences prevent ranking the systems.Differences include fold structure, theory scope, body-length limits, and how reported settings were chosen.Source: §7.2 · p. 14
  • The second vocabulary iteration reaches precision 0.7357, recall 0.8260, and F1 0.7782, but its vocabulary was chosen after the first run's test-side failure was known.The added transition relations allow a termination theory on seven of ten folds; this result is not the pre-registered headline.Source: §7.2 · pp. 14–15
  • For the learned detector inside Event-Calculus initiation search, ten-fold results are precision 0.1250, recall 0.0005, and F1 0.0011; nine folds reject it for insufficient new coverage.The search scores coverage against sparse transition events.Source: §7.2 · p. 15
  • Under the leak-free split, both routes score meeting F1 0.0, and the induced clause covers none of the 489 positives outside the concentrated scene family.That family contains 1,323 of 1,812 meeting-positive frames; the clean corpus has only eleven observable meeting initiations and five moving ones.Source: §7.2 · p. 15

7.3 Discussion

  • The section's supported positive finding is that symbolic credit can learn a perceptual predicate that replaces hand-set geometry, while meeting rules fail to transfer across scene families.The authors also note that termination programs are not learned in the pre-registered run and the benchmark evidence is limited to one domain.Source: §7.3 · pp. 15–16

8 Rule Induction at Scale: Maritime Rendezvous

On a maritime rendezvous corpus, weighted clauses improve over crisp selection, and single-pass training reproduces batch predictions. The findings measure rule reconstruction on a sparse pair-time grid, not rendezvous detection in the wild.

8.1 Corpus and labels

  • The corpus converts public Brest AIS exports into pair-time rows, but its synthetic labels omit two gold-rule discriminators: minimum duration and vessel-pair exclusions.The labels reproduce a hand-crafted RTEC rule’s output, so alignment with the source streams establishes conversion fidelity, not label correctness.Source: §8.1 · p. 16

8.2 Protocol

  • Five-fold splits keep vessel pairs intact because positive rows concentrate heavily in a few pairs; candidate search and weighted runs use per-fold permutation-null gates.The top pair carries 33.4% of positive rows, motivating pair-level folds.Source: §8.2 · p. 17

8.3 Results

  • 0.6746 micro pointwise F1 for crisp base-vocabulary search, which commits both disjunctive branches of the gold body on every fold.No clause is accepted below its fold’s null gate.Source: §8.3 · p. 17
  • 0.7398 micro F1 (+0.0652 over crisp search) for base-vocabulary weighted clauses, although the weighted run wins only two of five folds.Its weakest fold is worse than crisp search’s.Source: §8.3 · p. 17
  • Before any cross-validated run, the widened-vocabulary ceiling probe achieved F1 0.9969 with no false negatives; duration eliminated at least 711 of 733 negative-pair false positives.Source: §8.3 · p. 17
  • Single-pass weight training reproduces batch predictions exactly, because all three regimes reduce to the same thresholded rule despite substantially different weights.The same predictions also hold in reverse chronological order.Source: §8.3 · p. 18

8.4 Discussion

  • 0.7435 interval-level F1 for weighted base clauses versus 0.6772 for crisp base clauses; both duration rows reach 0.9970.Table 5 reports these interval-level values alongside pointwise results.Source: Table 5 · p. 18
  • The results are rule-reconstruction figures, not a ranking against OLED or WOLED, a test of rendezvous detection in the wild, or evidence about GPU execution.Published work uses a dense temporal grid, unlike this sparse pair-level grid.Source: §8.4 · pp. 18–19

9 Epistemic and Other Reasoning Modes

xlog extends its shared CUDA substrate to epistemic world views, probabilistic aggregates, and well-founded semantics. The accepted execution routes reuse GPU-backed joins, circuits, and CDCL while retaining mode-specific semantics and limits.

9.1 Modal surface and the epistemic IR

  • The Epistemic IR preserves modal literals for execution planning, which selects Generate–Propagate–Test, a positive-cycle fixpoint, or GPU-backed WFS.The accepted surface includes finite nested modal chains, epistemic integrity constraints, coupled predicates, multi-arity modal predicates, and recursive epistemic execution.Source: §9.1 · p. 19

9.2 World-view semantics

  • A world view is a non-empty set of stable models: know requires a fact in every model, while possible requires it in at least one.Default FAEEL requires independent founded support; Gelfond-1991-style compatibility admits self-supporting tuples, while non-epistemic programs evaluate identically under both.Source: §9.2 · p. 19

9.3 Epistemic execution routes

  • Acyclic modal programs use a CUDA Generate–Propagate–Test schedule, while positive FAEEL cycles and supported Gelfond-1991 cycles use distinct fixpoint routes.Supported cycles through negation use GPU-backed WFS; recursive negation or aggregation inside a compatibility component is rejected, and unsupported hot-path constructs have no CPU fallback.Source: §9.3 · pp. 19–20

9.4 Probabilistic aggregates

  • Finite count, sum, min, max, and logsumexp queries are supported in exact and Monte Carlo inference, subject to a typed exact-domain cap.For small finite count domains, cardinality dynamic programming can replace naive world enumeration; a 217-outcome example is reduced to a few hundred lifted states with identical results.Source: §9.4 · p. 20

9.5 Well-founded semantics

  • For supported non-stratified programs, GPU-backed well-founded semantics assigns true, false, or undefined through an alternating fixpoint.In probabilistic programs, true atoms receive normal probability and gradient, while false and undefined atoms receive probability zero; unsupported cyclic shapes return a typed diagnostic.Source: §9.5 · p. 20

10 Evaluation

The evaluation combines subsystem ablations with controlled comparisons against external engines. Results show workload-dependent gains, while several comparisons are bounded by specific fixtures, fixed overheads, or CPU-quota effects.

10.1 Methodology

  • The evaluation uses hardware-specific subsystem ablations and controlled external comparisons, with cloud artifacts recording their device and CPU quota.Per-run measurement data is distributed for the head-to-head comparisons, overhead isolations, circuit-cache ablation, runtime-optimization ablations, and rule-induction runs.Source: §10.1 · p. 20, §10.4 · p. 22

10.2 WCOJ vs. the binary-join plan

  • The WCOJ ablation reports a 27.96× geometric-mean speedup over xlog’s binary-join plan on a skewed triangle join.The four fixture variants coincide at this scale, so their 26.6×–29.6× spread reflects run-to-run variation rather than robustness across distinct workloads.Source: §10.2 · p. 21

10.3 Circuit caching and training

  • The circuit-cache ablation compares recompiling each epoch with compiling once, isolating compilation amortization rather than a fixed speedup.Its 512-image protocol is deliberately under-trained, and the apparent speedup grows with epoch count toward the cold/warm ratio.Source: §10.3 · p. 21, Table 9 · p. 21

10.4 Head-to-head comparisons

  • On the 20k MNIST-addition protocol, xlog and Scallop reach held-out accuracies of 0.9561± 0.0008 and 0.9468 ± 0.0104, respectively.No per-epoch speed claim is made because Scallop’s epoch time varies non-monotonically with the pod’s CPU quota.Source: §10.4 · p. 22
  • On five probabilistic programs, xlog’s exact query probabilities match analytic answers to zero error, identical to ProbLog2, but ProbLog2 runs each query 45–100× faster.The comparison supports correctness-equivalent inference, not an exact-inference speed claim.Source: §10.4 · p. 22
  • The Soufflé-to-fused-xlog execution-time ratio rises from 0.88× at 150k edges, where Soufflé is faster, to 5.54× at 1.2M edges.Across the cases, xlog execution is nearly flat at 0.57–0.68 s while Soufflé grows from 0.51–3.77 s; fused device allocations are 85–1,033 MB versus 3,287–44,979 MB for enumerate-then-count.Source: §10.4 · p. 22

10.5 Event-Calculus rule induction

The Event-Calculus evaluation compares induced theories with published CAVIAR results and examines weaker or adaptive runs. It also measures verification and residency costs separately from ordinary GPU acceleration.

10.5 Event-Calculus rule induction

  • The pre-registered ten-fold CAVIAR result falls 0.0021 below the lowest published meeting F1, while the 0.7782 second-iteration result lies within the published span but is adaptive.The second-iteration result is not the row used for the pre-registered comparison.Source: §10.5 · p. 22
  • The direct-protocol reference theory scores far below the Event-Calculus row on the same ten folds, with recall dominated by a fold where the search abstains and misses 855 gold frames.The reported figure reflects the protocol’s pre-registered defaults and is not a ceiling for the direct protocol.Source: §10.5 · pp. 22, 24
  • For moving, widening the proximity threshold from 25 to 34 raises recall and lowers precision where the clause is selected, but a tie-fragile fold explains the lower canonical micro score.On the fold with 1,546 of 3,136 gold frames, the candidate margin is 0.0093 against a 0.01 tie floor, and the search abstains.Source: §10.5 · p. 24

10.6 Verification cost and residency benefit

  • On probabilistic reachability chains, GPU CDCL verification accounts for 98.8–99.4% of cold-compile time and grows with circuit size.D4 compilation remains between 1.2 and 11.7 ms at every measured point.Source: §10.6 · p. 24
  • At realistic training-batch scale, forced device-to-host-to-device transfers add an approximately 16% tax, distinct from and additive to GPU-compute and circuit-caching advantages.The forced per-buffer copy is an upper bound because a hybrid could coalesce transfers; large-state Datalog fixpoints are outside this isolation.Source: §10.6 · p. 24

10.7 Index reuse and the chain scorer

The section reports runtime-optimization ablations, capability coverage, and additional exact-inference and rule-union features. The measured benefits are workload-specific, and the capability table is qualitative rather than a performance comparison.

10.7 Index reuse and the chain scorer

  • 8.33× release and 7.72× debug index-reuse ratios accompany 5.58× and 7.20× chain-scorer ratios, with the latter partly reflecting a slower baseline.The chain scorer adds no host transfers relative to baseline; below its gate threshold, medians differ by 2.0% and ranges overlap. Both are single-fixture medians, and scorer coverage matches baseline.Source: §10.7 · pp. 24, 26, Table 14 · p. 26

10.8 Capability coverage across systems

  • Table 15 compares capabilities across representative systems, not performance; its entries indicate supported capability rather than maturity.The quantitative head-to-head comparisons with Scallop, ProbLog2, and Soufflé appear in Section 10.4.Source: §10.8 · p. 26

10.9 Log-evidence, rule unions, and exact constraint solving

  • Exact evaluation exposes log evidence and maps CNF variables to probabilistic facts, while same-head rule contributions now use one multiway union per iteration.The variable map is unavailable when no CNF encoding exists; long chain-shaped constraint components beyond enumeration capacity use memoized GPU dynamic programming for exact totals, while components wider than the configured limit are refused.Source: §10.9 · p. 26

11 Related Work

The related-work discussion places xlog among neurosymbolic, GPU logic, probabilistic inference, SAT, differentiable ILP, and logic-language systems. Its contribution is a typed language and shared CUDA services spanning capabilities with route-specific execution and differentiability contracts.

11.1 Neurosymbolic programming

  • xlog shares the GPU symbolic-data-plane premise with Lobster but adds exact knowledge compilation and epistemic reasoning, circuit-equivalence certification, and route-specific transfer accounting.The paper draws no head-to-head performance comparison with Lobster.Source: §11 · pp. 26–27, §11.1 · p. 27

11.2 GPU-accelerated Datalog and joins

  • GPU Datalog systems target deterministic reasoning, while xlog extends its CUDA relational substrate through weighted model counting and gradient computation over derived facts.The discussion also situates xlog’s cyclic and multiway worst-case-optimal join path among GPU join work.Source: §11.2 · p. 27

11.3 Probabilistic logic programming

  • xlog adopts compile-once/evaluate-many probabilistic inference with CUDA-backed provenance, encoding, compilation, equivalence verification, and forward/backward evaluation.The host orchestrates stages and reads bounded solver control state; circuit and gradient buffers share an address space with neural and deterministic data planes.Source: §11.3 · p. 27

11.4 GPU SAT

  • Unlike standalone GPU SAT systems, xlog uses GPU CDCL inside knowledge compilation to prove circuit–formula equivalence through two UNSAT proofs.The module provides certificates for the probabilistic and epistemic backends.Source: §11.4 · p. 28

11.5 Differentiable ILP

  • xlog’s differentiable-ILP subsystem replaces dense rule-space materialization with sparse GPU bitmasks and on-device scatter–gather credit assignment.The related-work passage describes dense materialization as scaling cubically in the number of constants.Source: §11.5 · p. 28

11.6 Logic programming languages

  • xlog adopts typed-predicate discipline while unifying typed Datalog, probabilistic facts, neural predicates, and epistemic operators in one language with CUDA-backed routes.The discussion contrasts this scope with Prolog, Mercury, Soufflé, and clingo.Source: §11.6 · p. 28

12 Limitations and Future Work

The paper identifies hardware, memory, capacity, evaluation, and maturity boundaries on xlog’s current scope. Future work targets out-of-core and multi-GPU execution, broader epistemic residency, and stream-based structure learning.

12.1 Current limitations

  • xlog requires a supported NVIDIA GPU and has no OpenCL, Metal, or ROCm backend.Its CUDA-specific primitives prevent users without supported NVIDIA hardware from running the system.Source: §12.1 · p. 28
  • On-device relations, indices, circuits, and sample arrays do not spill out of core; byte-budget, fixed-count, and iteration-limit exhaustion produce distinct typed failures.The respective outcomes are RESOURCE_EXHAUSTED, CAPACITY_EXCEEDED, and CONVERGENCE_FAILURE.Source: §12.1 · p. 28
  • Differentiable ILP and trainable rule bodies remain beta, with restricted search, schedule-sensitive convergence, and open standard-benchmark comparisons.The trainable-rule-body path is evaluated on a public benchmark, but its accuracy and training cost versus dedicated relational learners remain open.Source: §12.1 · p. 28
  • Epistemic coverage is still being broadened, and several modal, recursive, tuple-key, and negation forms remain fail-closed.Some supported epistemic routes are GPU-backed but host-orchestrated; the accepted surface and solver portfolio remain bounded.Source: §12.1 · p. 28
  • Head-to-head coverage is partial, and single-GPU comparisons do not establish a general system ranking.The MNIST epoch ratio varied with host conditions; the paper therefore reports accuracy but no timing for that comparison.Source: §12.1 · pp. 28–29
  • Leak-free grouped CAVIAR has too few initiation events for a cross-validated rule-induction claim; protocol-matched figures use a duplication-defect corpus.The maritime results are rule-reconstruction figures on synthetic labels, not detection figures; their single-pass result depends on the tested pool, corpus, and threshold.Source: §12.1 · p. 29

12.2 Future work

  • Future work proposes streaming out-of-core execution, multi-GPU partitioning, deeper epistemic residency, and structure learning on the stream.The paper also identifies broader non-finite tuple-key forms and semantic forms beyond the currently accepted epistemic surface.Source: §12.2 · p. 29

13 Conclusion

xlog brings deterministic, probabilistic, epistemic, and neural-symbolic reasoning into one typed CUDA-native engine, with route-specific execution boundaries. Its measured benefits are strongest on large or repeated symbolic workloads, while the paper does not claim universal superiority.

13 Conclusion

  • xlog unifies four reasoning modes in a typed language and provider-owned CUDA runtime, with exact probabilistic query gradients and GPU-checked circuit certificates.Ordinary relational and exact execution are host-orchestrated; eligible recursion and resident Monte Carlo cores record zero tracked transfers before a terminal receipt.Source: §13 · p. 29
  • The reported gains center on circuit reuse and skewed cyclic joins, while exact inference loses to a mature CPU compiler on small programs.The paper says these comparisons do not establish a general ranking, given limited engines, program classes, and young epistemic and rule-learning surfaces.Source: §13 · pp. 29–30
  • The proposed direction is out-of-core and multi-GPU execution, deeper epistemic residency, and structure learning on the stream.These directions address the memory ceiling and the remaining epistemic and rule-learning work identified by the paper.Source: §13 · p. 30

Related papers

Loading 2609.27203v1…