Mark some facts as uncertain, tell XLOG what you have observed, and ask how likely a conclusion is. You write ordinary rules; XLOG carries the probabilities through them and hands back a probability. You can ask for two kinds of answer:
  • a marginal — how likely a fact is, overall;
  • a conditional — how likely a fact is, given what you observed.
XLOG answers with one of two engines: an exact engine that computes the true probability, or an approximate Monte Carlo engine that estimates it by sampling and reports error bars.

​
Smallest runnable example

The classic wet-grass model: rain and the sprinkler each make the grass wet, you observe that the grass is wet, and you ask how likely each cause was.
Run it with the exact engine:
Probabilistic programs go through xlog prob. xlog run is the deterministic runner — it will not produce a probability. The exact engine is the default, so --prob-engine exact_ddnnf is optional. What you should see. Because the grass is wet, both causes come back more likely than their starting probabilities (0.7 and 0.2), and rain() — the stronger prior — carries most of the posterior mass.

​
When to use each engine

Reach for the exact engine when you need the true answer and your program is small — for example when it uses negation, recursion, or small aggregates. Reach for the Monte Carlo engine when the model is larger, or uses a feature the exact engine does not support, and a sampled estimate with error bars is good enough.

​
Writing a probabilistic program

A probabilistic fact is a fact prefixed with a probability and ::. It holds with that probability and fails otherwise:
An annotated disjunction puts several mutually exclusive outcomes on one line, separated by ;, each with its own probability. Exactly one outcome is chosen. If the probabilities sum to less than 1, the remaining mass is an implicit “none” outcome:
You state what you observed with evidence(...) and ask for a probability with query(...):
Rules are written exactly as in a deterministic program. The probability lives on the facts, and the engine propagates it through the derivations. Rules can also come from another module, imported with use. Pass --module-path so xlog prob can find those modules:
Before 0.12.0, --module-path only checked that the modules loaded — the imported rules were never merged into the program that was actually evaluated, so a probabilistic program that imported its rules reported the wrong probabilities. If you are pinned to an older wheel or binary, keep the rules a probabilistic program depends on in the entry file. See the CLI reference for the full note.
Select the engine with #pragma prob_engine = exact_ddnnf or #pragma prob_engine = mc, declared in the entry file — a pragma in an imported module is ignored and reported as warning[W0510] (see the pragmas guide). From Python, the prob_engine argument to Program.compile(...) takes precedence over the pragma.

​
Exact inference

The exact engine (exact_ddnnf) computes the true probability by turning your program into a circuit and then adding up the probability of every world in which the query holds. Turning a program into a circuit like this is called knowledge compilation; adding up those world probabilities is weighted model counting. The whole path runs on the GPU:
Exact inference pipeline: PIR provenance to CNF (Tseitin), to GPU Decision-DNNF (compile plus CDCL verify), to the XGCF circuit format, to weighted model counting; the compile stages run once and gradients flow backward through XGCF.

The exact path compiles provenance to CNF, then to a verified GPU Decision-DNNF, then to the XGCF circuit; the circuit is compiled once and evaluated many times, with gradients flowing back through it.

1

Provenance

Rule evaluation records, for every derived tuple, which probabilistic choices support it. This record — a graph over the probabilistic facts and annotated disjunctions — is called the tuple’s provenance.
2

CNF

The provenance graph is encoded into a Boolean formula in the standard AND-of-ORs form (CNF, conjunctive normal form), with a variable map that lives on the device.
3

Decision-DNNF

A GPU compiler turns the CNF into a Decision-DNNF circuit — a circuit form whose worlds can be counted exactly in a single pass. A GPU SAT solver (using CDCL, the standard conflict-driven clause-learning algorithm) then checks that the circuit is logically equivalent to the formula before it is trusted.
4

Weighted model counting

The verified circuit — XLOG’s GPU circuit format, XGCF — is evaluated in log-space to produce log P(Q and E) and log P(E). Their difference is the conditional probability log P(Q | E).

​
Reading the exact result from Python

From Python, result = program.evaluate() carries the same two quantities the circuit produced:
  • result.log_z_e is the exact log-evidence — the log P(E) above, as a natural log. It is None for Monte Carlo results.
  • program.prob_var_map() says what each position in result.grad_true / result.grad_false stands for: {"kind": "fact", ...} for a probabilistic fact, {"kind": "choice", ...} for one branch of an annotated disjunction, or {"kind": "other"} for a variable that is not a source of randomness. That is how you attribute a gradient back to the fact that produced it. Those two vectors are filled in only by program.evaluate(return_grads=True); the plain evaluate() above leaves both None.
prob_var_map() is exact-engine only. It raises ValueError for Monte Carlo programs, and also for exact programs compiled through the GPU count-lift fast path, which never builds the encoding the map describes. See the Python reference for the full field list. Gradients flow back through the same circuit, so a probabilistic program stays differentiable end to end and can sit inside a training loop. This works through negation too: a negated literal contributes with the correct sign flip.

​
Conditioning on accepted epistemic evidence

Rust integrations can condition exact inference on a world view accepted by the epistemic GPU runtime. EpistemicProbProductionAdapter validates the runtime provider identity, the typed execution_backend = gpu and fallback_policy = reject_unsupported policy, semantic trace, tuple-membership evidence, and final tuple materialization before it passes that evidence to the exact source or parsed-program path. Eligibility also requires positive observations from the executed route: recorded CUDA-event timing, GPU kernel and dispatch counts, device-backed final output, and transfer accounting. The same accepted-evidence boundary covers PIR and CNF encoding, knowledge compilation, query evaluation, and gradients. The bounded EpistemicCircuit test fixture is excluded from production-path metrics. Methods with conditioned in their name translate accepted assumptions into probabilistic evidence(...) clauses, so they can change the returned probabilities; the other accepted-evidence methods use the world view as an admission gate without modifying the probabilistic model. The policy-key migration also changes every epistemic plan_id: the identifier is the hash of the canonical plan summary, so removing the old fallback keys and adding the typed policy keys deliberately invalidates identifiers generated by earlier versions. Consumers must regenerate plan-id goldens, caches, and evidence-ledger references rather than treating old and new identifiers as interchangeable. production_capabilities() is a static inventory of backend stages implemented by the adapter. It is not a CUDA probe, a Cargo-feature report, or a claim that every epistemic planner returns compatible evidence. The typed policy rejects unsupported shapes instead of reporting a default-zero fallback counter; production eligibility still depends on the observed GPU evidence above. This contract does not claim zero host traffic, because concrete tuple evidence is read from accepted output columns after the certified hot path. The public Rust capability report replaces GpuSolverProductionCapabilities::cpu_oracle_solver_allowed with the exhaustive production_metric_backend policy. Consumers must match its current GpuSolverProductionMetricBackend::GpuOnly variant instead of treating a constant boolean as evidence that CPU solving was excluded. The production metric gate still requires positive accepted-candidate and GPU solver event evidence from the executed route. The public Rust EpistemicGpuSemanticTrace and specialized epistemic runtime JSON no longer include rejection_reason_device_reads. Rust callers and fixed-schema JSON consumers must remove that field or key and use rejection_reason_metadata_bytes for the bounded rejection-reason payload. The retained byte count is derived from the length of the rejection-reason vector returned by the device read and must match one u32 reason slot per generated candidate. The separate bounded read of constraint-violation indices remains part of the runtime boundary but is not folded into this rejection-reason-specific byte count. This handoff consumes EpistemicGpuExecutionResult records produced by the single-pass Generate-Propagate-Test route, including split batches. Recursive epistemic programs take a different route: the high-level LogicProgram evaluator runs the applicable founded, Gelfond-1991 compatibility, or well-founded fixpoint and returns a LogicEvalResult containing relation results. That result type is not an input to EpistemicProbProductionAdapter, so backend availability does not claim recursive-world-view conditioning. A recursive source must use the high-level evaluator; it cannot be sent to compile_epistemic_gpu_execution, whose contract is intentionally limited to acyclic single-pass programs.
XGCF circuit structure: LIT leaf nodes at level 0 feed AND nodes at level 1 and an OR root using logsumexp at level 2, producing the log probability of the query; a dashed backward path carries adjoints from the root back to gradients at the leaves.

The XGCF circuit is a levelized DAG: literal leaves feed AND and OR nodes evaluated one level per kernel launch in log space, and adjoints propagate back down to produce gradients at the leaves.

​
Aggregates in exact inference

The exact engine can push aggregates through uncertainty, up to fixed bounds:
  • For sum, min, max, and logsumexp, it enumerates the outcomes of up to 16 uncertain rows per group exactly.
  • For count, a dedicated count-lifting path handles up to 64 uncertain rows per group.
Beyond those caps the engine stops with a typed rejection rather than silently approximating. The error message tells you to switch to #pragma prob_engine = mc for that program.

​
Monte Carlo inference

The Monte Carlo engine (mc) estimates probabilities by sampling many possible worlds and counting how often the query holds. Its production path is a megakernel — a single GPU kernel that evaluates every sampled world in one launch, followed by one synchronization. Observations are handled by rejection sampling: only sampled worlds that satisfy evidence(...) are counted; the rest are thrown away. Each query reports an estimate prob (with log_prob), a standard error stderr, a two-sided confidence interval (ci_low, ci_high), the sample counts, and the seed. The confidence interval is how you tell whether you drew enough samples: if it is too wide for your needs, draw more.
Monte Carlo resident megakernel: a fragment gate rejects unsupported programs with a typed error; supported programs enter a single GPU-resident kernel launch where each world samples facts, derives, and checks the query in parallel; per-world results accumulate into device-resident counts that produce the estimate with confidence interval and seed.

One kernel launch evaluates every sampled world in parallel on the device; counts stay device-resident, and the host reads back only the final estimate.

​
Limits of the Monte Carlo engine

The megakernel sizes its GPU memory once, up front, before it allocates anything. For that to be possible, a program is accepted only when it stays within these bounds: A program that would exceed this memory budget stops with a ResourceExhausted error before any allocation. There is no fallback to a larger, host-sized path. The engine also rejects — with a typed error — any program that uses negation, aggregates, or annotated disjunctions. In every one of these cases it refuses cleanly rather than guessing (it “fails closed”).
The --allow-cpu-oracle flag (Python: allow_cpu_oracle=True) is an explicit, labeled opt-in that runs a CPU oracle instead of the GPU engine. Its results are marked mc_engine: "cpu-oracle" and are never valid GPU-native or zero-host evidence — treat them as a reference check, not a production result.

​
Diagnostics and guarantees

This section is for readers who need to reason about where computation runs and what the engines promise. You do not need it to write a probabilistic program. Monte Carlo — zero host traffic. For the sampled region, the megakernel keeps all work on the GPU. It performs 0 tracked host-to-device transfers, 0 tracked device-to-host transfers, and 0 untracked metadata reads. This holds constant whether you draw 128 samples or 1024; the host reads back only the final estimate. Exact engine — GPU-accelerated, host-orchestrated. The exact engine runs on the GPU but is driven from a host loop: the forward evaluation launches one kernel per circuit level. No per-level data is read back — the circuit and its intermediate values stay on the device, and only O(1) scalars (the log-partition value and per-query gradients) return to the host after evaluation. It therefore does not offer the single-launch, fully device-resident guarantee that the Monte Carlo engine does. No CPU Decision-DNNF compiler. Production exact inference is always the GPU compiler and verifier described above. XLOG never bundles a CPU d-DNNF compiler and never shells out to an external d4 binary. Decision-DNNF parsing exists only for tests and fixtures.

Rule learning

The exact engine’s differentiable circuits are the same infrastructure that trains neural predicates and learned rules end to end with PyTorch.