Autoresearch modules API

Every polynomial of total degree ≤ degree in vars, with unknown coefficients.

poolExprPool

Pool the coefficient symbols are interned in.

varssequence of Expr

Independent variables, in the order the exponent tuples index them.

degreeint

Maximum total degree.

namestr

Coefficient prefix. Names are f"{name}_{i}" for one variable and f"{name}_{i}_{j}..." for several — always predictable, never gensym-ed. Collides → E-ANSATZ-001.

min_degreeint

Drop monomials of total degree below this (min_degree=degree gives the homogeneous forms).

max_termsint

Refuse rather than materialise a family bigger than this (E-ANSATZ-002). C(n + d, d) grows fast.

reservedsequence of Expr or str

Extra symbols (or names) the coefficients must not collide with — pass the target function here when it carries symbols of its own.

Ansatz

AnsatzError

E-ANSATZ-001 on a name collision, E-ANSATZ-002 if the family exceeds max_terms.

>>> import alkahest as ak
>>> from alkahest.ansatz import polynomial
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> A = polynomial(pool, [x], degree=3)
>>> A.names
('c_0', 'c_1', 'c_2', 'c_3')
>>> try:
...     polynomial(pool, [x], degree=99, max_terms=10)
... except ak.AnsatzError as exc:
...     exc.code
'E-ANSATZ-002'

A rational-function family p / q — the Padé case, kept linear.

p/q ≈ f is not linear in the coefficients of p and q, but p − f·q = 0 is linear in them jointly. This constructor records the numerator/denominator split so Ansatz.residual() (and fit(), which clears denominators itself) can apply that transform, keeping the default solve path exact linear algebra with no groebner dependency.

pool, vars, max_terms, reserved

As polynomial().

num_degree, den_degreeint

Total degrees of the numerator and denominator.

name, den_namestr

Coefficient prefixes for the numerator and denominator.

monic_denominatorbool

When true (default), the denominator's constant term is fixed to 1. Without a normalisation p/q and (λp)/(λq) are the same function, so every such fit would report a spurious extra free parameter.

Ansatz

.expr is the quotient; .metadata["numerator"] and ["denominator"] are the two polynomials, and ["numerator_terms"] is how many of .unknowns belong to the numerator.

>>> import alkahest as ak
>>> from alkahest.ansatz import rational
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> A = rational(pool, [x], num_degree=1, den_degree=1)
>>> A.names
('a_0', 'a_1', 'b_1')
>>> A.expr
((a_0 + (x * a_1)) * (1 + (x * b_1))^-1)

Σᵢ pᵢ(x)·e^{λᵢ x} with polynomial pᵢ of the given degree.

The standard ansatz for a linear ODE or recurrence whose characteristic roots λᵢ are already known — the polynomial factor's degree is the multiplicity minus one. Because the λᵢ are given, the family stays linear in the unknowns and fits through the default path.

poolExprPool

varExpr

The independent variable.

ratessequence of Expr or int

The exponents λᵢ. Duplicates are allowed but pointless — raise the corresponding degree instead.

degreeint or sequence of int

Degree of each polynomial factor; a scalar applies to every rate.

name, max_terms, reserved

As polynomial(). Coefficient names are f"{name}_{i}_{k}" for rate i and power k.

Ansatz

>>> import alkahest as ak
>>> from alkahest.ansatz import exponential_polynomial
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> A = exponential_polynomial(pool, x, [1, -1])
>>> A.names
('c_0_0', 'c_1_0')
>>> A.expr
((exp(x) * c_0_0) + (exp((x * -1)) * c_1_0))

Σ cᵢ · basisᵢ — the general escape hatch.

Whenever the family is "an unknown linear combination of these things" — a Lyapunov basis, a set of candidate integrals, ζ(3) and π³ and log³2 — this is the constructor. Everything else in this module is a convenience wrapper that computes a basis for you.

poolExprPool

basissequence of Expr

The basis functions. Not checked for linear independence — a dependent basis simply shows up as free parameters in the fit, which is the honest answer.

varssequence of Expr, optional

Independent variables. Inferred from the basis's free symbols (sorted by name) when omitted — never from reserved, which only reserves names.

name, max_terms, reserved

As polynomial(). reserved keeps the coefficients from colliding with symbols the basis does not mention; it does not make those symbols variables of the family.

Ansatz

>>> import alkahest as ak
>>> from alkahest.ansatz import linear_combination
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> A = linear_combination(pool, [ak.sin(x), ak.cos(x)])
>>> A.expr
((sin(x) * c_0) + (cos(x) * c_1))

Σ_{i ≤ j} q_ij · xᵢ xⱼ — the Lyapunov-candidate family.

Only the upper triangle carries an unknown, because q_ij xᵢxⱼ and q_ji xⱼxᵢ are the same term and carrying both would make every fit report spurious free parameters.

This module's job ends when it has produced the candidate. Deciding whether a fitted form is non-negative is prove_nonneg() / sos_decompose()'s job, and certify_nonneg() is the one-line hand-off — positivity is not reimplemented here.

pool, vars, name, max_terms, reserved

As polynomial(). Coefficient names are f"{name}_{i}_{j}" with i <= j indexing vars.

Ansatz

>>> import alkahest as ak
>>> from alkahest.ansatz import quadratic_form
>>> pool = ak.ExprPool()
>>> x, y = pool.symbol("x"), pool.symbol("y")
>>> A = quadratic_form(pool, [x, y])
>>> A.names
('q_0_0', 'q_0_1', 'q_1_1')

Solve for the coefficients that make residual vanish identically.

The default path is exact linear algebra, not Gröbner. Undetermined coefficients, series matching, Lyapunov forms and Padé are all linear in the unknowns once denominators are cleared, so the system is built by probing with subs() and reduced with Matrix.rref() over exact rationals. Nothing here needs the groebner feature; the one path that does (a residual genuinely nonlinear in the unknowns) refuses with E-ANSATZ-004 when it is absent rather than degrading silently.

ansatzAnsatz

The family to fit.

residualExpr or DerivedResult

The expression that must vanish identically in ansatz.vars — typically ansatz.expr - target. If it is not affine in the unknowns because of an unknown-bearing denominator (the Padé case), the denominator is cleared automatically and the fact is recorded in AnsatzSolution.steps.

certify{"residual", "exact", "none"}

"residual" (default) builds the system by collocation and checks it by exact back-substitution. "exact" builds the system by Taylor-coefficient extraction instead, so the system itself is exact for polynomial residuals, and still back-substitutes. "none" skips the check entirely and returns status="unverified" — for hot loops that will verify downstream, never for anything recorded as a result.

seedint, optional

Sample-point seed. Defaults to budget_seed() (so with ak.context(budget=ak.Budget(seed=7)) controls it), and to DEFAULT_SEED when no budget is active. Two runs with the same seed use the same points on any machine.

oversampleint, optional

Extra equations beyond the unknown count. Defaults to max(4, len(ansatz)). Over-sampling is what lets the rank be read off the rref instead of assumed.

max_pointsint, optional

Cap on sample-point draws, including those skipped for being poles. Applies to collocation only — the certify="exact" path draws a base point, not a system, so capping its equation count here would return a smaller system than the degree bound promises. Size that one with degree_bound=.

degree_boundint, optional

Multi-index degree for certify="exact"; every multi-index up to it contributes an equation, and the bound reached is recorded in AnsatzSolution.steps. Defaults to the smallest degree that supplies at least as many equations as the collocation path would use.

tolerancefloat

Numeric residual below which a non-normalising fit is still reported as "numerically_checked" rather than as a stated failure.

samplesint

Fresh points used for that numeric check.

AnsatzSolution

AnsatzError

E-ANSATZ-003 when the system is inconsistent — no member of the family satisfies the constraints, which is a positive result for a search loop and should be recorded as a closed branch. E-ANSATZ-004 when the residual is nonlinear in the unknowns and this build has no groebner feature to escalate to.

Round-trip a known polynomial:

>>> import alkahest as ak
>>> from alkahest.ansatz import fit, polynomial
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> A = polynomial(pool, [x], degree=2)
>>> sol = fit(A, A.expr - (x**2 + pool.integer(1)))
>>> sol.expr
(1 + x^2)
>>> sol.status, sol.free
('exactly_verified', ())

An underdetermined family returns its free parameters rather than an arbitrary member:

>>> B = polynomial(pool, [x], degree=3, name="d")
>>> under = fit(B, ak.diff(B.expr, x).value - pool.integer(0))
>>> under.rank, [str(f) for f in under.free]
(3, ['d_0'])

Lazily enumerate concrete members over a finite coefficient set.

Enumeration and fitting stay separate on purpose: this feeds stage 2 of a search loop (generate candidates, then hammer them with compile_expr() or batch_map()), while fit() is stage 3 (turn data into a symbolic claim). Fusing them produces an API that does neither well.

The bound is checked before the first member is built, from len(coeffs) ** len(ansatz) — enumeration is lazy and bounded.

ansatzAnsatz

coeffsiterable

Values each coefficient ranges over. Materialised once.

max_membersint

Refuse (E-ANSATZ-002) rather than start an enumeration longer than this.

Expr

One member per assignment, coefficients varying last-unknown-fastest.

AnsatzError

E-ANSATZ-002 when the family size exceeds max_members.

>>> import alkahest as ak
>>> from alkahest.ansatz import enumerate_family, polynomial
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> A = polynomial(pool, [x], degree=1)
>>> [str(m) for m in enumerate_family(A, [0, 1])]
['0', 'x', '1', '(x + 1)']
>>> try:
...     next(enumerate_family(A, range(10 ** 6), max_members=10))
... except ak.AnsatzError as exc:
...     exc.code
'E-ANSATZ-002'

Hand a fitted candidate to prove_nonneg().

The ansatz module's job ends when it has produced the candidate. Positivity is decided by the existing certificate machinery — this is a one-line adapter that unwraps an AnsatzSolution or Ansatz and forwards, so that a Lyapunov workflow reads

cert = certify_nonneg(fit(quadratic_form(pool, [x, y]), residual))

and every outcome (a PositivityCertificate, an E-SOS-003 refutation with a witness, an E-SOS-002 "no certificate of this shape at this degree") comes back unmodified. Nothing about positivity is reimplemented or reinterpreted here.

candidateAnsatzSolution, Ansatz, Expr or DerivedResult

The expression to certify. An AnsatzSolution still carrying free parameters is refused — an undetermined form is not a candidate.

varssequence of Expr, optional

Variables; taken from the ansatz when candidate carries one.

constraintssequence of Expr

Forwarded as prove_nonneg(constraints=...).

**kwargs

Forwarded verbatim.

PositivityCertificate

AnsatzError

E-ANSATZ-003 if the candidate still has free parameters.

SosError

Whatever prove_nonneg() raises — passed through.

alkahest.prove_nonneg_on(expr, vars, constraints=(), *, equalities=(), level=None)

Prove expr ≥ 0 on the semialgebraic set {g_i ≥ 0, h_j = 0} with a Putinar (quadratic-module) certificate expr = σ₀ + Σ σ_i·g_i + Σ λ_j·h_j, every σ an explicit sum of squares of rational polynomials and every λ a rational polynomial.

constraints items are a polynomial g (meaning g ≥ 0) or a comparison built with pool.ge/pool.le/pool.gt/pool.lt (strict ones are relaxed to their closure, which is sound) or pool.pred_eq (an equality). equalities items are h (meaning h = 0) or pool.pred_eq(a, b). level is the relaxation order k: every summand has degree ≤ 2k; None tries the smallest level that can work and two more.

Returns a PositivityCertificate with kind == "putinar", already re-verified exactly; equalities appear in it as the pair h ≥ 0, -h ≥ 0 with λ = σ⁺ − σ⁻. With no constraints and no equalities at all this is sos_decompose() (kind == "sos", level read as its basis_degree).

An inequality predicate passed in equalities is refused (E-SOS-004). A witness always satisfies strict comparisons strictly: a point of the closure only is not a refutation.

Raises SosError E-SOS-003 when a rational point of the set has expr < 0 (the exception's witness attribute maps each variable to its exact value), E-SOS-002 when no certificate was found at the level(s) searched (undecided — raise level; the message says whether the module was found to be Archimedean), E-SOS-001/E-SOS-004 on malformed input.

Example: prove_nonneg_on(1 - x**2, [x, y], [1 - x**2 - y**2]) returns the certificate 1 - x² = y² + 1·(1 - x² - y²).

Run one query through Alkahest and through an oracle, and compare.

operationstr

Name of an OPERATIONS entry; also the alkahest module attribute that is called on the Alkahest side.

*args

The arguments you would pass to alkahest.<operation>.

oracleOracle or str, optional

Which oracle to use. Defaults to the first installed one.

assumptionsAssumptions, optional

Governing assumption context; defaults to active_assumptions(). An assumption with no faithful mapping into the oracle's language yields incomparable.

pointsint

Sample count for the rigorous-numeric rung.

seedint, optional

Sampling seed. Defaults to the active Budget seed, then to DEFAULT_SEED, so a check is reproducible.

poolExprPool, optional

Pool the arguments live in; defaults to active_pool(). Only needed to attempt the Alkahest side of the symbolic rung — the oracle's answer has to be lifted back into a pool to be subtracted there. Without it the rung still runs, in the oracle only, and the record says which system proved what.

**kwargs

Forwarded to the Alkahest call.

CrossCheck

Four-valued: agree / diverge / incomparable / unavailable. A missing oracle is unavailable, never agree.

CrossCheckError

E-XCHECK-003 if operation has no defined comparison rung. Untranslatable input and missing oracles are outcomes, not exceptions; an unknown operation is a caller mistake.

>>> import alkahest as ak
>>> from alkahest.crosscheck import check
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> out = check("diff", ak.sin(x), x)
>>> out.outcome in {"agree", "unavailable"}
True
>>> out.outcome == "agree" or out.reason == "no_oracle"
True

Run a seeded differential sweep and report what diverged.

This is the nightly tier of the two-tier arrangement described in docs/mdbook/src/crosscheck.md. It is deliberately not a per-PR gate: it is randomised, and an oracle upgrade would turn it red for reasons that have nothing to do with the pull request under review. Its findings are meant to be promoted into FROZEN_CORPUS, which is the per-PR gate.

Warning Neither side is bounded, and this module does not pretend otherwise. Alkahest's heavy engines hold the GIL, so a non-terminating call cannot be timed out from Python: a worker thread cannot be stopped, and abandoning one wedges the interpreter anyway. SymPy is no better placed. Run the nightly job under an OS-level timeout, and wrap the sweep in context(budget=...) for the engines that are cooperative (integrate(), best-effort simplify() — see docs/mdbook/src/budgets.md). SWEEP_OPERATIONS is chosen to stay clear of the paths known not to terminate.

seedint, optional

Defaults to the active Budget seed, then to DEFAULT_SEED. Always recorded on the report.

casesint

Number of expressions to generate.

operationssequence of str

Which OPERATIONS entries to exercise.

oracleOracle or str, optional

Defaults to the first installed oracle. With none installed the report is all unavailable — the sweep does not pretend to have run.

poolExprPool, optional

Pool to build candidates in; a fresh one by default.

pointsint

Sample count passed to check().

SweepReport

Re-run FROZEN_CORPUS against the installed oracle.

oracleOracle or str, optional

Defaults to the first installed oracle.

casessequence of FrozenCase

Defaults to the whole corpus.

list of (FrozenCase, CrossCheck or None)

None means the case does not apply to the installed oracle version and was skipped — a skip, never a pass.

Translate an Alkahest expression into SymPy, or refuse.

The one translator this package ships, exposed directly for callers who want the term rather than a comparison. Total over NODE_TAGS: anything it cannot map faithfully raises rather than degrading.

exprExpr or DerivedResult

Expression to translate.

assumptionsAssumptions, optional

Governing assumption context; defaults to active_assumptions().

sympy.Basic

CrossCheckError

E-XCHECK-002 if SymPy is not installed, E-XCHECK-001 if the expression or the assumption context has no faithful mapping.

>>> import alkahest as ak
>>> from alkahest.crosscheck import oracles, to_sympy
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> if oracles()["sympy"]:
...     str(to_sympy(ak.sin(x) ** 2))
... else:
...     'sin(x)**2'
'sin(x)**2'

Register an Oracle implementation under its name.

The comparator resolves oracles through this registry, so a new backend is a class plus one call — no change to the ladder, the outcomes, or the frozen corpus machinery.

oracle_clstype[Oracle]

Class (not instance); it is constructed lazily, and only when Oracle.available() says it can be.

Which oracles are installed, and at what version.

Reports every known oracle, including the absent ones — an agent must be able to tell that SymPy is missing before it plans around a check that will only ever return unavailable.

dict

{"sympy": "1.14.0", "wolfram": None}-shaped; None means "known to this build, not installed here".

>>> from alkahest.crosscheck import oracles
>>> sorted(oracles())
['sympy']

Export a predicate Expr as an SMT-LIB 2 script.

The SMT counterpart of to_lean(): Alkahest emits a standard artifact and an independently maintained external tool consumes it. The emitter itself lives in Rust (alkahest_core::logic::smtlib) so that match exhaustiveness over Formula / PredicateKind enforces total coverage; this wrapper only maps the error type.

formulaExpr

A predicate or quantified expression — built with pool.gt/lt/… and And() / Or() / Not(), or Forall() / Exists().

logicstr

"auto" (default) infers the weakest logic that fits: QF_LIA, QF_NIA, QF_LRA, QF_NRA, QF_LIRA, QF_NIRA, their quantified counterparts, or ALL. Naming a logic too weak for the formula is an error (E-SMT-002), not a silent downgrade.

check_sat, get_modelbool

Append (check-sat) / (get-model) and set :produce-models.

SmtError

E-SMT-002 when the formula is outside the exportable fragment. Use supported() to ask the same question without raising.

>>> import alkahest as ak
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> print(ak.to_smtlib(ak.And(pool.gt(x, pool.integer(0)), pool.lt(x, pool.integer(3)))))
... # doctest: +SKIP
; alkahest SMT-LIB 2 export
(set-logic QF_LRA)
...

Ask an external SMT solver about formula.

formulaExpr

A quantifier-free predicate expression. Quantified formulas export fine with to_smtlib() but are refused here (E-SMT-002): this function guarantees that every sat model is checked exactly in-process, and there is nothing to check for a quantified model.

If you wrote the question as Exists(x, Exists(y, body)), pass body: a sat query already asks whether some assignment satisfies the formula, so the free variables of body are implicitly existentially quantified and the returned model is the witness. The quantifiers are not stripped for you — that would silently answer about a different expression than the one handed in — and the rewrite is not valid under a Forall() anyway.

solverstr

"auto" (first installed, in SOLVERS order) or a name.

logicstr

Forwarded to to_smtlib().

budgetBudget, optional

budget.wall_ms is passed to the solver's own timeout flag and enforced as a parent-side deadline. A timeout raises BudgetExceededError (E-BUDGET-001), so a loop gets the structured "hard, not hung" distinction rather than a bare unknown.

poolExprPool, optional

Pool for SmtResult.model_exprs; defaults to active_pool(). SmtResult.model is exact and present either way.

SmtResult

SmtError

E-SMT-001 no solver installed — a refusal, never a silent fallback to satisfiable(), whose fragments (propositional, and one real variable against rational constants) do not overlap what is asked here. E-SMT-002 formula outside the exportable/solvable fragment. E-SMT-003 a model value (root-obj) cannot be lifted exactly. E-SMT-004 the model failed back-substitution. This is raised, never warned: it means the bridge or the solver is broken.

BudgetExceededError

The solver hit budget.wall_ms.

>>> import alkahest as ak
>>> pool = ak.ExprPool()
>>> n = pool.symbol("n", "integer")
>>> x = pool.symbol("x")
>>> f = ak.And(pool.gt(x, n), pool.lt(x * x, pool.integer(10)))
>>> r = ak.smt.solve(f)                     # doctest: +SKIP
>>> r.status, r.badge                       # doctest: +SKIP
('sat', 'the solver's model was substituted back and ...')

Can this formula be handed to an SMT solver — and should it be?

The plan-ahead predicate, for the same reason certifiable() exists: a loop must be able to choose a route before it commits, not discover a refusal after paying for the setup.

The "should it be" half matters and cuts the opposite way to the usual instinct. For real arithmetic with no integer variables (QF_LRA / QF_NRA), recommendation is "prefer_in_tree": prove_nonneg() and sos_decompose() yield a PositivityCertificate that composes with to_lean(), whereas an SMT solver yields an answer and no artifact. The genuinely new capability the bridge buys is mixed integer/real/boolean problems, which neither CAD nor diophantine() handles — there recommendation is "smt".

A formula the emitter refuses (a transcendental function, a named constant with no exact term such as pi) cannot be handed to a solver at all, so it too gets "prefer_in_tree".

SmtSupport

Truthy when solve() would run.

>>> import alkahest as ak
>>> pool = ak.ExprPool()
>>> n = pool.symbol("n", "integer")
>>> s = ak.smt.supported(pool.gt(n * n, pool.integer(10)))
>>> s.recommendation                                      # doctest: +SKIP
'smt'

Which SMT solvers are installed, and at what version.

Returns a mapping over every name in SOLVERS; the value is the solver's self-reported version string, or None when the binary was not found. Absence is reported negatively and explicitly so an agent can tell before it plans that the hand-off is unavailable, rather than discovering it as a refusal mid-loop.

>>> import alkahest as ak
>>> ak.smt.solvers()                      # doctest: +SKIP
{'z3': 'Z3 version 4.13.0 - 64 bit', 'cvc5': None}