◉ COOLJAPAN
← All posts
June 9, 2026 • 8 min read

TensorLogic 0.1.1 Released — Exact LTL Temporal Operators, GPU Autodiff, and Probabilistic Tensor Reasoning

This patch adds exact finite-trace LTL operators (Next/Until/Release/WeakUntil/StrongRelease), tape-based GPU autodiff on OxiCUDA, Monte Carlo + variational probabilistic execution, SPARQL-as-tensor evaluation, neural architecture search, and SVM kernels — all on the SciRS2 stack, all Pure Rust.

release tensorlogic neurosymbolic einsum temporal-logic pure-rust gpu

Time now compiles to tensors — and it’s differentiable.

Today we released TensorLogic 0.1.1 — a follow-up to our first stable that makes Linear Temporal Logic operators exact, adds tape-based GPU autodiff on OxiCUDA, brings probabilistic execution (Monte Carlo + variational inference) into the runtime, and lets you query knowledge graphs as tensor contractions. It builds directly on the first stable 0.1.0 (released 2026-04-27); if you know TensorLogic, this post is about what’s new.

No C. No Fortran. No FFI shims. TensorLogic 0.1.1 is Pure Rust end to end: the SciRS2 backend (now 0.5.0) executes the einsum graphs, the OxiCUDA backend (0.1.8) runs the GPU path, and OxiARC (oxiarc-deflate 0.3.3) handles compression. It ships as a single static binary, with Python bindings (pytensorlogic) via PyO3. Rust 1.90+, Apache-2.0.

Why 0.1.1 matters

The headline is temporal logic. In earlier releases the LTL temporal operators were either unimplemented (they returned errors) or, worse, used mathematically-incorrect single-step approximations. 0.1.1 closes that gap:

Test coverage grew from 6,407 to 7,178 (+771 new tests, 100% pass rate; 37 GPU-only tests skipped in CI).

Technical Deep Dive

The temporal layer. A new temporal_ops.rs module in tensorlogic-scirs-backend is the foundation. It exposes shift_next / shift_prev for the unary time shifts, and a unified temporal_binary_scan / temporal_binary_scan_vjp pair for the binary operators. The scan is parametrised over TemporalBinaryForm (Until / WeakUntil / Release / StrongRelease) crossed with UntilSemantics (MaxMin / ProbSumProduct), with a boundary_val ∈ {0.0, 1.0} distinguishing the strong and weak variants. This generalises the earlier Round-6 until_scan into one exact, reusable recurrence (+16 tests in this module alone).

On the compiler side, tensorlogic-compiler now does the right thing: compile_next emits a temporal_next:<axis> node dispatched through tensorlogic_scirs_backend::temporal_ops::shift_next, and compile_until emits a temporal_until:<tag>:<axis> binary node. Because the backend scans expose VJPs, those temporal nodes are differentiable — temporal logic is now a fully gradient-aware part of the einsum graph.

The GPU layer. tensorlogic-oxicuda-backend gains a TlAutodiff implementation for OxiCudaExecutor that records a tape during forward and replays it in reverse for backward, covering Matmul2D, BatchedMatmul3D, Identity, Unary, Binary, and Reduce ops. The OxiCudaTape exposes gradients: HashMap<usize, OxiCudaTensor> so you can inspect intermediate gradients, and an optional native-broadcast feature routes gradient broadcasts through GPU kernels. Alongside it: tensorlogic-oxicuda-solver adds generic f64 LU/Cholesky/QR-lstsq/CG solvers, a preconditioned CG (pcg_solve) supporting Precond::Jacobi and Precond::IncompleteCholesky, and a tridiagonal solve_tridiagonal via the Thomas algorithm. tensorlogic-oxicuda-sparse generalises SparseCsr<T> over T: Float (f32 stays the default for backward compatibility) and adds SparseCsc<T>, with transpose / to_csc / to_csr / from_dense and f64 SpMV/SpMM plus batched SpMV. tensorlogic-oxicuda-rng adds uniform_f64 / normal_f64 (52-bit mantissa + Box-Muller) and streaming chunked fills.

The probabilistic layer. A new probabilistic/ sub-module in tensorlogic-scirs-backend brings Monte Carlo samplers (sample_bernoulli, sample_uniform, sample_normal, sample_categorical via Gumbel-max) and mc_integrate. A MonteCarloEstimator reports mean / variance / percentile credible intervals; predictive_entropy and bald_epistemic_uncertainty quantify uncertainty. And VariationalInference::fit implements mean-field Gaussian VI with the reparameterization trick + Adam, maximising the ELBO.

Knowledge-graph + ML. tensorlogic-oxirs-bridge adds an InternedGraph (O(1) term dictionary, predicate-indexed adjacency, parallel N-Triples bulk loading) and a TensorBgpEvaluator that evaluates conjunctive SELECT/BGP SPARQL queries as boolean tensor contractions over an EinsumGraph + Scirs2Exec::forward, decoding non-zero entries back to variable bindings. On the learning side: tensorlogic-train gains a nas/ module (ArchSearchSpace / Architecture / LayerSpec, an ArchSampler with 4-operator mutation, RegularizedEvolution with aging evolution + tournament selection and an ask/tell API, plus a RandomArchSearch baseline). tensorlogic-sklears-kernels adds an svm/ module — SvcModel (C-SVM, binary + one-vs-rest multiclass) and SvrModel (ε-SVR) implementing Platt’s SMO with Keerthi two-loop heuristics, all built on Arc<dyn Kernel> — plus a multi_output/ module (MultiOutputKernel trait, ICM, LMC, and VVGP vector-valued GP regression). Finally, tensorlogic-quantrs-hooks adds a VariationalGaussianMixture implementing VBEM with Dirichlet-prior mixing proportions and ELBO monitoring.

Getting Started

cargo add tensorlogic

Here’s the new temporal backend in action — “eventually grant” expressed as Until(true, grant) over a finite trace, computed with the exact backward recurrence instead of a single-step approximation:

use tensorlogic_scirs_backend::temporal_ops::{
    shift_next, temporal_binary_scan, TemporalBinaryForm, UntilSemantics,
};

// "eventually grant": Until(true, grant) over a finite trace along the time axis.
// `cond` is a [batch, time] truth tensor; `temporal_binary_scan` runs the exact
// finite-trace backward recurrence (no single-step approximation).
let satisfied = temporal_binary_scan(
    &antecedent,                 // left operand (e.g. all-ones for "eventually")
    &grant,                      // right operand
    /* time_axis = */ 1,
    TemporalBinaryForm::Until,
    UntilSemantics::MaxMin,
    /* boundary_val = */ 0.0,
)?;

The higher-level path is the same idea: define an LTL rule and compile it, and the compiler emits the matching temporal_until / temporal_next nodes for you — backed by the very same exact recurrences.

What’s New in 0.1.1

Temporal / LTL

GPU autodiff + solvers

Probabilistic execution

SPARQL tensor evaluation

ML (NAS / SVM / GPs / VB-GMM)

Dependency upgrades

Tips

The neurosymbolic foundation

0.1.1 deepens TensorLogic’s role as the neurosymbolic glue of the COOLJAPAN stack — and every integration here is real and shipped. Logic, time, and probability all compile down to SciRS2 tensors (0.5.0). OxiRS knowledge graphs (0.3.1) are now queryable as tensors through the BGP evaluator. The OxiCUDA backend (0.1.8) gives you GPU autodiff, f64 solvers, generic sparse, and f64 RNG. SkleaRS (0.1.1) contributes SVM and multi-output GP kernels, and QuantrS2 (0.2.0) hooks supply the variational Gaussian mixture. All Pure Rust. All in one tensor graph.

Repository: https://github.com/cool-japan/tensorlogic

Star the repo if you want temporal logic that’s both exact and differentiable — running on the GPU, in Pure Rust.

Time, logic, and gradients now live in the same tensor graph.

— KitaSan at COOLJAPAN OÜ June 9, 2026

↑ Back to all posts