DPNL: A DPLL-based Algorithm for Probabilistic Neurosymbolic Learning

• Inference may require aggregating many assignments that produce a target output, and this can be hard even when evaluating the symbolic function on one assignment is inexpensive.The number of relevant assignments can grow rapidly with the number of intermediate variables.Source: §1 · p. 1
• Existing exact PNL approaches construct query provenance before inference, but that construction can become a bottleneck when reasoning paths proliferate.Approximate methods trade exact inference for scalability, motivating inference that avoids complete provenance while controlling approximation error.Source: §1 · p. 1
• DPNL lazily explores partial assignments and dynamically resolves regions that can already be determined to succeed or fail, yielding exact inference when exploration finishes.It avoids constructing complete logical provenance before inference.Source: §1 · p. 2
• ApproxDPNL can stop exploration early while tracking unresolved probability mass to maintain certified lower and upper bounds on the exact output probability.This provides controlled approximation guarantees.Source: §1 · p. 2
• The oracle interface separates inference from the symbolic component’s representation, and experiments show oracle-guided reasoning extends the range of tractable PNL instances.The framework supports executable programs, solver-backed specifications, and domain-specific oracles, with conditions for soundness and termination.Source: §1 · p. 2

• A PNL problem combines a neural component with symbolic reasoning to learn intermediate predictions from supervision on the final symbolic output.The intermediate predictions need not have direct labels.Source: §2 · p. 2
• For each input, the neural component predicts distributions over finite-domain variables, and the symbolic component deterministically maps their joint assignment to an output.The variables are assumed mutually independent, so the output probability is a sum of products of their predicted probabilities.Source: §2 · p. 2
• Because the symbolic function is deterministic and independent of neural parameters, the output probability is differentiable and supports end-to-end learning without intermediate-variable labels.Source: §2 · p. 2
• The assignment set may be exponentially large, making explicit enumeration of assignments that contribute to the output intractable.The inference objective is to compute the output probability exactly or approximate it with certified bounds without materializing all satisfying assignments.Source: §2 · p. 2

3 DPNL: Oracle-Guided Inference

• DPNL explores assignment-space regions lazily, asking an oracle whether each region can be accepted, rejected, or needs further exploration.The split-or-prune procedure follows a DPLL-style recursive search and abstracts away the symbolic component’s representation.Source: §3 · p. 2

3.1 Search Regions and Oracle Interface

• A valuation represents a region through its total refinements; a valid oracle’s definitive answers must be sound and it must decide total valuations.Completeness can improve pruning, but DPNL requires validity rather than completeness for correctness.Source: §3.1 · p. 3

3.2 Exact Inference with DPNL

• For any valid oracle, DPNL terminates and returns the exact output probability, exploring regions further only when the oracle cannot decide them.This avoids materializing full query provenance before inference.Source: §3.2 · p. 3

3.3 Approximate Inference with ApproxDPNL

• ApproxDPNL maintains certified lower and upper bounds whose gap equals unresolved probability mass, allowing early stopping while preserving a guaranteed interval.Stopping when the interval width is at most 2ϵ makes its midpoint an additive ϵ-approximation; when low > 0, a multiplicative guarantee is also available.Source: §3.3 · pp. 3–4

3.4 Designing and Combining Oracles

• Oracles may use direct program execution, solvers, or domain knowledge; stronger pruning trades off against the cost of oracle calls.Valid oracles can be queried in sequence, placing inexpensive checks before stronger, more costly reasoning.Source: §3.4 · p. 4

4 Experimental Evaluation

• The evaluation asks how DPNL compares with exact probabilistic reasoning systems, how it performs against exact and approximate PNL systems, and how ApproxDPNL’s parameters trade accuracy against runtime.The reported sequence covers symbolic reasoning, neurosymbolic benchmarks, and approximation-parameter analysis.Source: §4 · p. 4

4.1 Symbolic reasoning (Q1)

• On MNIST-N-SUM, DPNL solves instances for N ≥7 where ProbLog times out; on graph reachability, DPNL completes N ≥ 7 with logic and combined oracles, though ProbLog is faster up to N = 5.The logic oracle scales better than the basic oracle on MNIST-N-SUM, despite being slower on small instances.Source: §4.1 · p. 5, Figure 1 · p. 5, Figure 2 · p. 5

4.2 Application to neurosymbolic AI (Q2)

• The neurosymbolic evaluation covers MNIST-N-SUM, Visual Sudoku, and Leaf classification, with Table 1 summarizing task difficulty and the DPNL inference modes evaluated.Difficulty is characterized by symbolic search-space size.Source: §4.2 · p. 5, Table 1 · p. 5

Leaf Classification

• DPNL with exact reasoning achieves the highest mean Leaf accuracy (0.808) and is faster than the other exact methods.It takes 10:15, compared with 55:34 for Scallop with k = 120 and 1:02:28 for DeepProbLog; DeepProbLog’s accuracy is 0.43.Source: Leaf Classification · p. 6, Table 2 · p. 6

MNIST-N-Sum

• At N = 4, exact DPNL reaches average accuracy 0.83, while anytime DPNL matches exact inference within one point at every N and cuts per-sample symbolic time by 5 to 23×.At N = 4, A-NeSI also finishes, with its best explain variant reaching 0.66.Source: MNIST-N-Sum · p. 6

Visual Sudoku

• At N = 9, anytime DPNL reaches 0.757, the highest accuracy of all methods, while exact inference times out.At N = 4, exact DPNL reaches 0.912 without classifier pretraining, slightly above the best baselines in the same setting.Source: Visual Sudoku · pp. 6–7

4.3 Analysis of the ϵ and Anytime Timeout Parameters (Q3)

• On MNIST-N-SUM, runtime grows roughly linearly with anytime timeout while accuracy jumps from zero to a plateau; for ϵ-approximation, runtime drops as ϵ grows, but accuracy eventually collapses.The accuracy break point decreases with task size; on Visual Sudoku N = 4, accuracy rises to 0.815 at t = 0.07 s and saturates between 0.877 and 0.903 from t = 0.08 s to 0.5 s as runtime grows from 5 to 16 min.Source: §4.3 · p. 7, Table 5 · p. 7

5.1 Symbolic AI

• DPNL’s recursive search follows DPLL, and partial-valuation oracles draw inspiration from decision-DNNF compilation.Approximation techniques also draw on anytime and error-guaranteed weighted model counting.Source: §5.1 · p. 8

5.2 Neurosymbolic AI

• Neurosymbolic approaches vary in how they combine neural and symbolic components, including relaxed logic, semantic-loss penalties, and probabilistic soft logic.The section focuses on PNL methods that combine predictions over intermediate variables through a symbolic function.Source: §5.2 · p. 8
• DPNL lazily searches assignment-space regions instead of materializing complete query provenance, unlike exact methods such as DeepProbLog [Manhaeve et al., 2018].The section frames this as a different inference procedure, not a change to the PNL problem.Source: §5.2 · p. 8
• ApproxDPNL bounds output-probability error directly, unlike proof-limited methods whose error depends on the probability mass of discarded proofs.Scallop’s k limits retained proofs, while ApproxDPNL returns certified bounds and can stop at any point.Source: §5.2 · p. 8
• Surrogate and sampling approaches avoid exact inference, but unlike ApproxDPNL they lack certified probability bounds; DPNL retains independent intermediate-symbol assumptions.A-NeSI uses learned prediction and explanation models, whereas ISED samples intermediate symbols; ApproxDPNL instead derives guarantees from unresolved probability mass.Source: §5.2 · pp. 8–9
• Hardware-oriented systems accelerate execution, whereas DPNL changes inference through lazy assignment-space exploration; the directions could be investigated together.Examples include GPU-oriented arithmetic-circuit, Datalog, and neurosymbolic execution approaches.Source: §5.2 · p. 9

6 Conclusion

• DPNL avoids requiring full query provenance by lazily exploring intermediate assignments and resolving regions once their contribution to the target output is determined.A generic oracle interface decouples the inference procedure from the symbolic component’s representation.Source: §6 · p. 9
• DPNL terminates with the exact output probability for valid oracles, while ApproxDPNL can stop early with certified bounds and extend tractability further.The experiments report that DPNL extends the range of instances tractable by exact inference, and ApproxDPNL extends it further through certified approximate inference.Source: §6 · p. 10
• The conclusion identifies pruning, region selection, and branching strategies as opportunities for further improvement.It suggests dynamic, on-demand assignment-space exploration as an alternative to representing all reasoning paths before inference.Source: §6 · p. 10

A Termination and Correctness of DPNL

• For any valid oracle, DPNL terminates and returns the exact completion probability, certifying all-success or all-failure regions and branching on undecided ones.Source: A Termination and Correctness of DPNL · pp. 11–12

B.1 Logic-based characterization of symbolic functions

• Finite-domain values are represented by mutually exclusive, exhaustive formulas, and the symbolic output is characterized by logical entailment.Source: §B.1 · p. 12

B.2 Logic oracle

• A logic oracle applies a decision procedure to determine whether a partial valuation suffices to decide the target output.Source: §B.2 · p. 12, §B.1 · p. 12

B.3 Validity and completeness

• Sound logical consequence makes Algorithm 3 a valid oracle, while sound and complete consequence makes it complete.Source: §B.3 · pp. 12–13

C.1 DeepProbLog as a logic-based symbolic function

• DeepProbLog neural-predicate outcomes define intermediate variables, while its deterministic logic program defines the symbolic function.Source: §C.1 · p. 13

C.2 DeepProbLog oracle

• For DeepProbLog programs without negation, Prolog implements the oracle; monotonicity lets it certify query success or impossibility from partial facts and an optimistic completion.Source: §C.2 · p. 13

C.3 Representing probabilistic choices

• ADs and nADs encode mutually exclusive categorical choices, but their auxiliary rules can enlarge provenance; DPNL avoids materializing that complete representation.Source: §C.3 · p. 14

C.4 Example: Graph reachability

• In dense graphs, path provenance can grow exponentially; the reachability oracle can accept a region with an established path or reject one even with all unknown edges present.Source: §C.4 · p. 14

D Variable Selection Heuristics

• Variable choice affects recursive-call counts but not correctness or termination; oracle-informed splits may improve pruning by separating target-producing from excluding regions.Source: D Variable Selection Heuristics · p. 14

E.1 Hardware

• Symbolic experiments ran on an Apple MacBook Pro with an M1 Max and 64GB RAM.Source: §E.1 · p. 14
• Leaf and MNIST-N-SUM experiments used a CPU-only Dell Precision 7960 with a 12-core Intel Xeon w5-3425 and 512GB RAM.Source: §E.1 · p. 14
• Visual Sudoku experiments ran on a server with two 10-core Intel Xeon Silver 4114 processors, 187GB RAM, and an NVIDIA Quadro P5000 GPU.Source: §E.1 · p. 14

E.2 Implementation Details

• DPNL represents symbolic functions and structured inputs through Symbolic and Input abstractions, then recursively branches on undefined variables while oracles assess whether partial valuations determine the target output.Oracles can return always true, always false, or unresolved; supported variants include enumeration, basic, logic, and combination oracles.Source: §E.2 · pp. 14–15
• A SATLogic interface encodes formulas with literals, clauses, and conjunctions and supports SAT-based reasoning; this is one implementation of the generic logic-oracle interface.The experimental interface uses SAT solvers such as MiniSAT and supports variable declarations, clause generation, and relational constraints.Source: §E.2 · pp. 14–15

E.3 Hyperparameters.

• Experiments hold hyperparameters constant across digit counts, use 10 independent DPNL runs, and set task-specific timeouts; the MNIST digit classifier has two convolutional and three linear layers.The MNIST classifier uses convolutional output dimensions 6 and 16, followed by linear dimensions 120 and 84 and a 10-digit output; Table 6 summarizes the experiment settings.Source: §E.3 · p. 15, Table 6 · p. 16

E.4 Baselines

• Leaf baselines use ISED code, while A-Nesi configurations are reported for explain, predict-only, and prune variants, with five random-seed runs per experiment.The section also identifies publicly available repositories as sources for MNIST-N-Sum baselines.Source: §E.4 · p. 15, Table 7 · p. 15
• Scallop is extended from MNIST-1-SUM to MNIST-N-SUM for N=2, 3, and 4, with exact and approximate reasoning; approximate reasoning uses diff-top-k-proof with k=3.For exact reasoning, k is chosen large enough that the logical provenance formula is not pruned; DPLA∗ uses the geometric mean heuristic to estimate partial-proof probabilities.Source: §E.4 · p. 15