Quivers

A functional probabilistic programming language for PyTorch.

Quivers is a functional probabilistic programming language for PyTorch. The syntax will look familiar if you have used Pyro, NumPyro, Stan, or PyMC, with a few distinguishing features:

  • Programs are first-class composable typed values. A program has a domain, codomain, algebra, and effect signature (Sample, Score, Marginal, Pure), checked at compile time. Programs compose with >>, parallel-compose with @, change base across algebras with change_base, and marginalize discrete latents with marginalize z : K <- ... followed by an indented body.
  • Shared substrate for inference, deduction, and structural compression. A CKY parser written as a deduction block, a transformer-as-encoder over a signature block, and a Bayesian regression all compile to the same underlying semantics, with the same composition operators, and can thus compose with each other.
  • Algebra-parametric semantics. Programs can be parameterized by eleven built-in or user-defined algebras. Homomorphisms between algebras are values along which models can be transported. The compiler checks their source and target types; the algebraic laws remain assumptions of each instance.

The probabilistic-programming surface also includes:

  • An inference toolkit. More than forty distribution families. SVI with automatic guides from mean-field and full-rank multivariate normals through low-rank, mixture, structured, IAF, neural-spline flow, and AutoDAIS guides; seven objectives (ELBO, IWAE, Renyi, VR-IWAE, ChiVI, RWS, and DReGs); and reparameterized, score-function, sticking-the-landing, and DReG gradient estimators. NUTS and HMC use dual-averaging step-size adaptation and Welford mass-matrix adaptation.
  • An analysis toolkit. Static introspection of compiled programs (per-step algebra, chain depth, intermediate shape, source mapping); algebra-aware, saturation-free initialization recipes that adapt to whichever value algebra a program is parameterized over; compile-time diagnostics flagging latents whose default initialization would saturate the active algebra.
  • Diagnostics and model comparison. ArviZ ecosystem integration: posteriors from any inference method (NUTS, HMC, or SVI) export to ArviZ for trace plots, rank plots, ESS, and \(\hat R\). PSIS-LOO (Pareto-smoothed importance-sampling leave-one-out cross-validation) for ranking competing models; posterior-predictive checks against user-defined test statistics; LOO-PIT for calibration.
  • A mixed-effect model API. A brms-style formula frontend for mixed-effect regression compiles formulas to typed QVR programs through a bidirectional lens, taking pandas / polars dataframes as input and using R-canonical conventions (orthogonal polynomials, R-style transforms in the formula evaluation namespace) as defaults. The emitted QVR is inspectable, so a formula-fitted model is a starting point you can hand-edit rather than a closed black box.
  • Interactive tooling. qvr repl is a GHCi-style four-pane Textual TUI with live syntax highlighting, an environment browser, file-watcher reloads, a command palette, and meta-commands (:type, :info, :browse, :edit, :save, :watch, …). qvr-lsp implements LSP 3.17 features including hover, definition, references, document symbols, semantic tokens, completion, formatting, and live diagnostics for VS Code, Cursor, Zed, and Neovim. A Jupyter kernel (qvr-kernel install) drives the same elaborator from notebooks.

Quick start

object Item : FinSet 100
# Predictor `x` flows in as exogenous data via the observations
# dict; free variables in `let` expressions resolve from the
# conditioning data at trace time (host-data channel).
program regression : Item -> Item [effects=[Sample, Score]]
    sample sigma  <- HalfNormal(1.0)
    sample beta_0 <- Normal(0.0, 5.0)
    sample beta_1 <- Normal(0.0, 2.0)
    let mu = beta_0 + beta_1 * x
    observe y : Item <- Normal(mu, sigma)
    return y

export regression

from quivers.dsl import load
from quivers.inference import AutoNormalGuide, ELBO, SVI
import torch

program = load("docs/examples/source/bayesian_regression.qvr")
model   = program.morphism
guide   = AutoNormalGuide(model, observed_names={"y"})
optim   = torch.optim.Adam(guide.parameters(), lr=1e-2)
svi     = SVI(model, guide, optim, ELBO())
# Training loop (illustrative shape; pass real x_data, y_data in practice).

The same regression also expresses through a brms-style formula frontend:

from quivers.formulas import fit
# Call shape: fit("y ~ x + (1 | g)", data=df, family="gaussian", method="nuts")
# returns a result with a `.dump_qvr(path)` method for inspecting the emitted QVR.
print(fit.__name__)

Where to start

  • Installation for setup.
  • Quickstart for a working model in five minutes.
  • QVR tutorial for probabilistic-programming users: seven chapters from linear regression through hierarchical models, sequence models, and inference-algorithm choice, with Pyro / NumPyro / Stan equivalents side-by-side.
  • Python API tutorial for library developers and category-theory-fluent users: seven chapters covering the typed categorical API.
  • Examples gallery: 46 end-to-end models grouped by family.
  • Conceptual guides for feature-area deep dives.
  • API reference for the typed Python API.
  • Denotational semantics for the formal meaning of every well-typed program.

Architecture

The DSL is a thin layer over a typed categorical API. If you want to extend the library, write a new distribution family, or prove anything about a model, the categorical layer is what you read. If you just want to fit models, you can ignore it.

The library decomposes into eight layers. Each is consumable in isolation; each builds on those below it:

flowchart TB
    L8["Layer 8: QVR DSL<br/>.qvr files, tree-sitter grammar, panproto AST"]
    L7["Layer 7: Structural compression<br/>signature, encoder, decoder, loss blocks"]
    L6["Layer 6: Inference<br/>guides, objectives, MCMC kernels, hybrid samplers"]
    L5["Layer 5: Continuous probabilistic programs<br/>MonadicProgram, distribution families, flows, plates"]
    L4["Layer 4: Stochastic morphisms<br/>Markov kernels, Giry monad, chart deduction surface"]
    L3["Layer 3: Monadic and enriched constructs<br/>monads, algebras, ends, coends, Kan, profunctors"]
    L2["Layer 2: Categorical structure<br/>functors, naturals, adjunctions, monoidal, traced"]
    L1["Layer 1: Core V-enriched algebra<br/>FinSet, Morphism, CompositionRule hierarchy, wiring"]
    L8 --> L7 --> L6 --> L5 --> L4 --> L3 --> L2 --> L1

The central abstraction is a morphism between finite sets, parameterized by an algebra (a complete lattice with a monoidal product distributing over joins). A morphism f : A -> B is a PyTorch tensor of shape (|A|, |B|) whose entries take values in the algebra; composition f >> g contracts along the shared dimension under the algebra's tensor product and join. Different algebras give different composition semantics: Boolean composes by AND / OR (relational composition), ProductFuzzy by multiplication / noisy-OR, Real by sum-product, Markov by row-stochastic kernel composition, and so on.

The denotational semantics gives every well-typed QVR phrase a formal meaning in a \(\mathcal{V}\)-enriched symmetric monoidal closed category. The implementation rests on enriched category theory (Kelly, 1982), the categorical foundations of probability (Giry, 1982; Fritz, 2020), and the SVI / HMC inference substrate (Hoffman, Blei, Wang & Paisley, 2013; Neal, 2011; Hoffman & Gelman, 2014).

References

  • Tobias Fritz. 2020. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239.
  • Michèle Giry. 1982. A categorical approach to probability theory. In Bernhard Banaschewski, editor, Categorical Aspects of Topology and Analysis, volume 915 of Lecture Notes in Mathematics, pages 68–85. Springer, Berlin, Heidelberg.
  • Matthew D. Hoffman and Andrew Gelman. 2014. The No-U-Turn Sampler: adaptively setting path lengths in Hamiltonian Monte Carlo. Journal of Machine Learning Research, 15(47):1593–1623.
  • Matthew D. Hoffman, David M. Blei, Chong Wang, and John Paisley. 2013. Stochastic variational inference. Journal of Machine Learning Research, 14(40):1303–1347.
  • Gregory M. Kelly. 1982. Basic Concepts of Enriched Category Theory. Cambridge University Press; reprinted as Reprints in Theory and Applications of Categories 10 (2005):1–136.
  • Radford M. Neal. 2011. MCMC using Hamiltonian dynamics. In Steve Brooks, Andrew Gelman, Galin L. Jones, and Xiao-Li Meng, editors, Handbook of Markov Chain Monte Carlo, chapter 5. Chapman & Hall/CRC.