Deduction Systems¶
The public API for weighted chart deductions consists of the model
type, its abstract primitives, and operations for fitting, Bayesian
lifting, and sampling. quivers.stochastic.deduction re-exports the
public symbols.
| Submodule | Job |
|---|---|
primitives |
Abstract building blocks (Axiom, Deduction, Goal, Schedule, DeductiveSystem). Most users do not touch these directly. |
fit |
Point-estimate gradient fitting (MAP / MLE) of the deduction's learnable log-weights. |
bayes |
Lift the parameters into a Bayesian MonadicProgram whose posterior NUTS / SVI can target. |
sample |
Exact length-conditional forward sampling of yields from the chart's distribution. |
deduction
¶
The deduction-system surface: model type, abstract primitives, and the three independent operations on a deduction.
This package gathers everything a user needs for working with a weighted deduction system in one importable path. The contents fall into three orthogonal groups:
- Model type (
DeductionSystem): the concrete agenda-based chart deduction that compiles from adeductionblock in the QVR DSL. Re-exported fromquivers.stochastic.agenda. - Abstract primitives (
.primitives):Axiom,Deduction,Goal,Schedule,DeductiveSystem: the protocol layer the agenda implementation derives from. Most users will not need these directly; they exist for custom-deduction subclasses and for the inside-algorithm framework (quivers.stochastic.inside). - Operations: three independent surfaces over a
DeductionSystemwith no overlap in purpose:.fit: point-estimate gradient fitting (MAP / MLE);.bayes: Bayesian wrapping for NUTS / SVI;.sample: exact length-conditional forward sampling of yields.
These three live in separate submodules because they answer different questions (estimate parameters at a point vs. sample a posterior vs. generate synthetic data) and so that adding more operations in the future does not bloat any one module.
DeductionSystem
dataclass
¶
DeductionSystem(rules: tuple[InferenceRule, ...], semiring: ChartSemiring, axiom_injector: Callable[[Any], list[tuple[Item, Tensor]]], goal: Callable[[Item], bool], agenda_factory: Callable[[], Agenda] = FIFOAgenda, chart_factory: Callable[[], Chart] = HashChart, max_iterations: int = 100000, tolerance: float = 0.0)
A weighted deductive system parameterized over its components.
The system is parameterized by:
- An item algebra (implicit in the patterns the rules use).
- A list of arity-n
InferenceRulehyperedges. - A
ChartSemiringfor weight aggregation. - An axiom injector
In -> [(Item, Weight)]producing the input's lexical / boundary items. - A goal predicate
Item -> boolselecting the result items. - (Optional) a chart constructor and an agenda strategy.
The same data structure subsumes CKY (FIFO agenda, span items, Boolean / inside semiring), Viterbi (priority agenda with the current weight as priority, max-times semiring), A* parsing (priority agenda with an admissible heuristic, tropical semiring), MLTT type-checking (LIFO agenda, judgment items, Boolean semiring), and weighted Datalog (FIFO, atoms, any naturally-ordered semiring).
run
¶
run(input_value: Any) -> AgendaResult
Run the deduction system on an input value.
Injects the input's axioms, runs the agenda to fixed point, attaches the item encoder when one is set, and sums any rule-attached and chart-attached losses.
| PARAMETER | DESCRIPTION |
|---|---|
input_value
|
The input the axiom injector reads.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
AgendaResult
|
The completed chart, its goal items, and any attached loss. |
Source code in src/quivers/stochastic/agenda.py
1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 | |
__call__
¶
__call__(input_value: Any) -> ChartView
Run the deduction and return a ChartView.
Convenience for the user-facing presheaf-evaluation API:
the chart's weights are differentiable tensors, and the
view exposes weight, enumerate, derivations,
and goal_weight methods for downstream programs.
| PARAMETER | DESCRIPTION |
|---|---|
input_value
|
The input the axiom injector reads.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ChartView
|
A view onto the completed chart. |
Source code in src/quivers/stochastic/agenda.py
parameters
¶
Yield every learnable parameter owned by this system.
Walks the optional _axiom_module (lexicon log-weights)
and _rule_module (per-rule, per-binding log-weights)
submodules attached by the compiler. The recurse flag
is the standard torch.nn.Module.parameters signature
so user code can pass a DeductionSystem anywhere a
nn.Module parameter iterator is expected.
| PARAMETER | DESCRIPTION |
|---|---|
recurse
|
Whether to include parameters of nested submodules.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Iterable of torch.nn.Parameter
|
The learnable parameters. |
Source code in src/quivers/stochastic/agenda.py
named_parameters
¶
Yield (name, parameter) pairs over all learnable parameters.
| PARAMETER | DESCRIPTION |
|---|---|
prefix
|
A prefix prepended to every parameter name.
TYPE:
|
recurse
|
Whether to include parameters of nested submodules.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Iterable of (str, torch.nn.Parameter)
|
The named learnable parameters. |
Source code in src/quivers/stochastic/agenda.py
Axiom
¶
Bases: Module
Initial items in a weighted deductive system.
An axiom creates the chart tensor and populates it with initial weights derived from the input. For span-based chart parsing, this is the lexical step.
forward
abstractmethod
¶
forward(input: Tensor, semiring: ChartSemiring) -> Tensor
Create and populate the initial chart.
| PARAMETER | DESCRIPTION |
|---|---|
input
|
Raw input (e.g. token indices).
TYPE:
|
semiring
|
The scoring semiring.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Tensor
|
The chart tensor with initial items filled in. |
Source code in src/quivers/stochastic/deduction/primitives.py
Deduction
¶
Bases: Module
A weighted inference step in a deductive system.
A deduction reads from the chart, applies inference rules, and writes updated weights. This is a morphism in the V-enriched category of chart states.
forward
abstractmethod
¶
forward(chart: Tensor, semiring: ChartSemiring, **context) -> Tensor
Apply this deduction step.
| PARAMETER | DESCRIPTION |
|---|---|
chart
|
Current chart state.
TYPE:
|
semiring
|
The scoring semiring.
TYPE:
|
**context
|
Schedule-provided context (e.g.
DEFAULT:
|
| RETURNS | DESCRIPTION |
|---|---|
Tensor
|
Updated chart. |
Source code in src/quivers/stochastic/deduction/primitives.py
DeductiveSystem
¶
DeductiveSystem(axiom: Axiom, deductions: list[Deduction], goal: Goal, schedule: Schedule, semiring: ChartSemiring | None = None)
Bases: Module
A weighted deductive system evaluated to fixpoint.
This is the abstract core of all parsing algorithms::
input -> axiom -> schedule(deductions) -> goal -> output
The system is an nn.Module whose learnable parameters come from the axiom (e.g. lexical weights) and deductions (e.g. rule weights).
| PARAMETER | DESCRIPTION |
|---|---|
axiom
|
Initial item population.
TYPE:
|
deductions
|
Inference rules.
TYPE:
|
goal
|
Result extraction.
TYPE:
|
schedule
|
Evaluation strategy.
TYPE:
|
semiring
|
Scoring algebra (default: LOG_PROB).
TYPE:
|
Source code in src/quivers/stochastic/deduction/primitives.py
forward
¶
Run the deductive system on input.
| PARAMETER | DESCRIPTION |
|---|---|
input
|
Raw input (e.g. token indices).
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Tensor
|
Goal item weights. |
Source code in src/quivers/stochastic/deduction/primitives.py
Goal
¶
Bases: Module
Extract the result from a completed chart.
A goal identifies which chart items constitute the answer and extracts their weights.
Schedule
¶
Bases: ABC
Evaluation strategy for a deductive system.
Different schedules compute the same fixpoint in different orders. CKY processes spans bottom-up; an agenda schedule uses a priority queue. The schedule is independent of the deduction rules.
run
abstractmethod
¶
run(chart: Tensor, deductions: ModuleList, semiring: ChartSemiring) -> Tensor
Execute deductions on chart to fixpoint.
| PARAMETER | DESCRIPTION |
|---|---|
chart
|
Chart with axioms filled in.
TYPE:
|
deductions
|
The deduction steps.
TYPE:
|
semiring
|
The scoring semiring.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Tensor
|
Completed chart. |
Source code in src/quivers/stochastic/deduction/primitives.py
nuts_program_from_deduction
¶
nuts_program_from_deduction(ded: DeductionSystem, corpus: Sequence[Sequence[str]], *, prior_scale: float = 1.0, site_prefix: str = 'log_w') -> tuple[MonadicProgram, Tensor, dict[str, Tensor]]
Lift a deduction system's learnable parameters to a
MonadicProgram suitable for NUTS / SVI.
The returned program has one
torch.distributions.Normal sample site per learnable
parameter (lexicon entries and rule bindings alike) plus one
score step that substitutes the sampled values into the
deduction's parameter slots and adds
:math:\sum_n \log Z(s_n; \mathbf{w}) to the joint.
| PARAMETER | DESCRIPTION |
|---|---|
ded
|
Deduction whose parameters are lifted.
TYPE:
|
corpus
|
Corpus the score step closes over.
TYPE:
|
prior_scale
|
Standard deviation of the Normal prior on each parameter.
TYPE:
|
site_prefix
|
Stem of each sample-site's name (the parameter's path is appended for round-trip mapping).
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
(model, x, observations)
|
The lifted program plus a |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the deduction has no learnable parameters. |
Source code in src/quivers/stochastic/deduction/bayes.py
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 | |
adam_fit_deduction
¶
adam_fit_deduction(ded: DeductionSystem, corpus: Sequence[Sequence[str]], *, steps: int = 300, lr: float = 0.05, prior_scale: float | None = None) -> list[float]
Maximise the corpus log-marginal under an optional Normal prior on the parameters.
| PARAMETER | DESCRIPTION |
|---|---|
ded
|
Deduction whose
TYPE:
|
corpus
|
Each sentence is a sequence of token strings the deduction's axiom injector accepts.
TYPE:
|
steps
|
Adam steps.
TYPE:
|
lr
|
Adam learning rate.
TYPE:
|
prior_scale
|
If supplied, adds a Gaussian regulariser
:math:
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
list[float]
|
The loss trajectory; length == |
Source code in src/quivers/stochastic/deduction/fit.py
sample_corpus
¶
sample_corpus(ded: DeductionSystem, *, length: int, n_samples: int, seed: int | None = None) -> list[list[str]]
Sample n_samples yields of length length from the
chart's length-conditional distribution under the deduction's
current parameters.
| PARAMETER | DESCRIPTION |
|---|---|
ded
|
The deduction with materialised parameters.
TYPE:
|
length
|
Length of yields to enumerate.
TYPE:
|
n_samples
|
Number of sentences to draw.
TYPE:
|
seed
|
Seed for the multinomial draws.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
list of list of str
|
|
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the deduction's vocabulary cannot be determined, or if no
yield of length |
Source code in src/quivers/stochastic/deduction/sample.py
bayesian_lift_parameters
¶
bayesian_lift_parameters(inner_model: Module, x: Tensor, observations: dict[str, Tensor], *, prior_scale: float = 1.0, site_prefix: str = 'theta', additional_latents: dict[str, tuple[int, ...]] | None = None, latent_placeholder_scale: float = 10.0) -> tuple[MonadicProgram, Tensor, dict[str, Tensor]]
Lift model parameters and selected latents into sample sites.
Each learnable parameter receives an independent
:math:\mathcal{N}(0, \sigma_\theta^2) prior. Entries in
additional_latents receive placeholder Normal priors. The score term
subtracts those placeholder log densities from inner_model.log_joint,
so they cancel pointwise; latent_placeholder_scale affects
initialization and adaptation, not the represented density.
Learnable parameters must use unconstrained real coordinates. Use explicit priors when an independent zero-centered Normal does not represent the intended parameter prior.
| PARAMETER | DESCRIPTION |
|---|---|
inner_model
|
Module exposing
TYPE:
|
x
|
Input passed to
TYPE:
|
observations
|
Observations passed to
TYPE:
|
prior_scale
|
Standard deviation of each parameter prior.
TYPE:
|
site_prefix
|
Prefix for parameter sample-site names.
TYPE:
|
additional_latents
|
Latent names and tensor shapes, excluding any batch dimension.
TYPE:
|
latent_placeholder_scale
|
Standard deviation of each placeholder latent prior.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[MonadicProgram, Tensor, dict[str, Tensor]]
|
Lifted program, placeholder input, and empty observation mapping. |
Source code in src/quivers/inference/lifts.py
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 | |