diff --git a/CHANGELOG.md b/CHANGELOG.md index 8cd388c9..f5e7422d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,13 @@ ### Added +- **Docs: autoresearch / search-plumbing guide.** New mdBook chapter + [`search-plumbing.md`](docs/mdbook/src/search-plumbing.md) ties budgets, + batch APIs, compact `DerivedResult` envelopes, claim graphs, and certificate + coverage together; Sphinx gains [`api/workload.rst`](docs/sphinx/api/workload.rst) + plus `DerivedResult.to_dict` / `BudgetExceededError` entries. Cross-links from + getting-started, intro, README, claim-graphs, batch, and budgets. + - **Budgets, cooperative cancellation, and a determinism seed** (P1 search plumbing item 4): `alkahest.Budget(wall_ms=..., max_steps=..., seed=...)` and `alkahest.context(budget=...)` push a wall-clock/step budget into a diff --git a/README.md b/README.md index ae0d7fae..565e953d 100644 --- a/README.md +++ b/README.md @@ -228,9 +228,21 @@ Most transforming operations (`diff`, `simplify`, `integrate`, `sum_*`, …) ret - `.value` — the result expression - `.steps` — derivation log (list of rewrite rules applied) - `.certificate` — Lean 4 proof term, when available +- `.to_dict()` / `.to_json()` — versioned machine-parseable envelope; use `mode="compact"` in agent loops Exceptions: `limit` returns a bare `Expr`, and `series` returns a `Series` (with its own `.polynomial` / `.order` fields). Use `.value` only on `DerivedResult`. +### Search plumbing (agent loops) + +| Need | Entry point | +|---|---| +| Bound one candidate | `Budget` + `context(budget=…)` → `BudgetExceededError` (`E-BUDGET-*`) | +| Fan out without aborting | `batch_map` / `integrate_many` / `simplify_many` / `diff_many` | +| Compact logs | `DerivedResult.to_dict(mode="compact")` | +| Session provenance | `alkahest.research` claim graphs | + +Docs: [Autoresearch / agent loops](https://alkahest-cas.github.io/alkahest/search-plumbing.html). + --- ## Reinforcement learning diff --git a/docs/mdbook/src/SUMMARY.md b/docs/mdbook/src/SUMMARY.md index 09dcbcaa..c46968ee 100644 --- a/docs/mdbook/src/SUMMARY.md +++ b/docs/mdbook/src/SUMMARY.md @@ -18,10 +18,11 @@ - [Interoperability](./interop.md) - [Reinforcement learning](./rl.md) - [Derivation logs](./derivations.md) -- [Batch and streaming evaluation](./batch.md) - [Claim graphs](./claim-graphs.md) - [Lean certificates](./lean-certs.md) - [Certificate coverage](./certificate-coverage.md) - [Error handling](./errors.md) -- [Budgets, cancellation, and determinism](./budgets.md) +- [Autoresearch / agent loops](./search-plumbing.md) + - [Budgets, cancellation, and determinism](./budgets.md) + - [Batch and streaming evaluation](./batch.md) - [Stability policy](./stability.md) diff --git a/docs/mdbook/src/batch.md b/docs/mdbook/src/batch.md index 77c1730c..04b7cc80 100644 --- a/docs/mdbook/src/batch.md +++ b/docs/mdbook/src/batch.md @@ -119,3 +119,22 @@ failed = [(o.index, o.error) for o in outs if not o.ok] `KeyboardInterrupt` or `SystemExit` still propagates and stops the batch, since swallowing those would make the process unkillable. Everything else — including every Alkahest `E-*` error and any exception your own `fn` raises — is captured. + +## Combining with budgets + +Wrap the batch in `context(budget=…)` so each candidate inherits the same +cooperative wall/step limit (and optional seed). A trip surfaces as +`BatchItem(ok=False, error={"code": "E-BUDGET-00x", …})` rather than aborting +the rest of the batch — see [Budgets](./budgets.md). + +```python +with ak.context(pool=pool, budget=ak.Budget(wall_ms=50, max_steps=10_000, seed=7)): + outs = ak.integrate_many(candidates, x, parallel=True) +``` + +## See also + +- [Autoresearch / agent loops](./search-plumbing.md) +- [Budgets, cancellation, and determinism](./budgets.md) +- [Derivation logs — compact envelopes](./derivations.md#machine-parseable-output-to_dict--to_json) +- [Error handling](./errors.md) diff --git a/docs/mdbook/src/budgets.md b/docs/mdbook/src/budgets.md index 99ce9cf5..20f5dfab 100644 --- a/docs/mdbook/src/budgets.md +++ b/docs/mdbook/src/budgets.md @@ -164,3 +164,11 @@ except ak.IntegrationError as e: On the Rust side (`alkahest_core::budget`): `Budget`, `enter`, `BudgetGuard`, `check`, `seed`, `is_active`, `request_cancel`, `clear_cancel`, `is_cancelled`, `BudgetError`. + +## See also + +- [Autoresearch / agent loops](./search-plumbing.md) +- [Batch and streaming evaluation](./batch.md) — budgets compose with `*_many` / + `batch_map`; a trip becomes one failed `BatchItem`, not a killed process +- [Error handling](./errors.md) — `E-BUDGET-*` in the exception hierarchy +- [Claim graphs](./claim-graphs.md) — session-level provenance around budgeted calls diff --git a/docs/mdbook/src/claim-graphs.md b/docs/mdbook/src/claim-graphs.md index 623c0123..a98ec91b 100644 --- a/docs/mdbook/src/claim-graphs.md +++ b/docs/mdbook/src/claim-graphs.md @@ -212,3 +212,12 @@ print(report.to_markdown()) runs the full experimental-mathematics loop — high-precision quadrature, `guess_relation` for the integer relation, a recorded conjecture, symbolic proof, Lean certificate, JSON round trip, and re-verification — and prints the rendered document. + +## See also + +- [Autoresearch / agent loops](./search-plumbing.md) — how claim graphs fit next to + budgets, batch APIs, and compact result envelopes +- [Budgets](./budgets.md) — bound one candidate so a hard instance cannot stall the session +- [Batch](./batch.md) — fan out many `DerivedResult` producers without aborting on one failure +- [Derivation logs](./derivations.md#machine-parseable-output-to_dict--to_json) — + `to_dict(mode="compact")` for token-efficient claim payloads diff --git a/docs/mdbook/src/derivations.md b/docs/mdbook/src/derivations.md index eb1029c7..dca5d1dc 100644 --- a/docs/mdbook/src/derivations.md +++ b/docs/mdbook/src/derivations.md @@ -212,3 +212,10 @@ An invalid `mode` (anything other than `"full"`/`"compact"`) raises `DerivedResult` is per-call. To accumulate many results into a citable, serialisable, re-verifiable artifact — a DAG of claims with stable IDs, hypotheses, and certificate status — see [claim graphs](./claim-graphs.md). + +## See also + +- [Autoresearch / agent loops](./search-plumbing.md) +- [Batch](./batch.md) — produce many `DerivedResult`s without aborting on one failure +- [Budgets](./budgets.md) — bound the call that produced the derivation +- [Certificate coverage](./certificate-coverage.md) — `certificate_status` in the envelope \ No newline at end of file diff --git a/docs/mdbook/src/getting-started.md b/docs/mdbook/src/getting-started.md index 441cea78..ad68c633 100644 --- a/docs/mdbook/src/getting-started.md +++ b/docs/mdbook/src/getting-started.md @@ -259,6 +259,29 @@ with alkahest.context(pool=pool, simplify=True): expr = z**2 + alkahest.sin(z) ``` +### Agent / autoresearch loops + +For a fan-out of candidates under a wall-clock or step budget, with results that +survive context compaction: + +```python +import alkahest as ak + +pool = ak.ExprPool() +x = pool.symbol("x") + +with ak.context(pool=pool, budget=ak.Budget(wall_ms=100, seed=1)): + outs = ak.integrate_many([x**2, ak.sin(x)], x) + for item in outs: + if item.ok: + print(item.value.to_dict(mode="compact")["verification"]["status"]) + else: + print(item.error["code"]) # e.g. E-INT-001 or E-BUDGET-001 +``` + +Full picture: [Autoresearch / agent loops](./search-plumbing.md), +[Budgets](./budgets.md), [Batch](./batch.md), [Claim graphs](./claim-graphs.md). + ## Running the examples The `examples/` directory in the Git repository has runnable end-to-end scripts. With `alkahest` installed (`pip install alkahest` or `maturin develop` as above), from the repository root run: diff --git a/docs/mdbook/src/intro.md b/docs/mdbook/src/intro.md index 52b0670a..8e1d5091 100644 --- a/docs/mdbook/src/intro.md +++ b/docs/mdbook/src/intro.md @@ -14,11 +14,13 @@ A general-purpose symbolic math library designed around three axes: **Ergonomics.** The Python API uses operator overloading for natural expression construction. Results are rich objects with `.value`, `.steps`, and `.certificate` attributes. Error messages carry structured codes, location information, and suggested remediations. +**Agent loops.** Budgets and cancellation, batch APIs that never abort on one bad candidate, versioned compact result envelopes, and session-level [claim graphs](./claim-graphs.md) are first-class — see [Autoresearch / agent loops](./search-plumbing.md). + ## Design principles **Explicit representations.** The type system distinguishes `UniPoly` (FLINT-backed univariate polynomial), `MultiPoly` (sparse multivariate), `RationalFunction`, and the generic `Expr` tree. Converting between them is an explicit call. There are no silent representation changes hiding performance cliffs. -**Stateless by design.** No global assumption contexts. No hidden caches that change behavior. All context (domains, simplification policy, precision) is passed explicitly or bundled into expression structure. This makes results deterministic and parallelism safe. +**Stateless by design.** No global assumption contexts. No hidden caches that change behavior. All context (domains, simplification policy, precision, budgets) is passed explicitly or scoped through `context(...)`. This makes results deterministic and parallelism safe. **Composable transformations.** `trace`, `grad`, `jit`, and `certify` operate on a shared traced representation and stack freely: `jit(grad(f))` compiles a derivative, `jit(grad(grad(f)))` compiles a second derivative. diff --git a/docs/mdbook/src/python-api.md b/docs/mdbook/src/python-api.md index 26c0ad64..440ba5ca 100644 --- a/docs/mdbook/src/python-api.md +++ b/docs/mdbook/src/python-api.md @@ -4,4 +4,14 @@ The Sphinx-generated Python API is published alongside this guide: **[Open the Python API documentation](https://alkahest-cas.github.io/alkahest/api/)** -It includes `ExprPool`, simplification, calculus, polynomials, numerics, transforms, matrices, ODE/DAE, solvers, codegen, and error types. +It includes `ExprPool`, simplification, calculus, polynomials, numerics, transforms, matrices, ODE/DAE, solvers, codegen, error types, and the [search / workload](https://alkahest-cas.github.io/alkahest/api/api/workload.html) surface (`Budget`, `batch_map`, `DerivedResult.to_dict`, …). + +Conceptual chapters for agent-facing plumbing: + +| Topic | Guide | +|---|---| +| Budgets, cancellation, seeds | [Budgets](./budgets.md) | +| Batch / streaming fan-out | [Batch](./batch.md) | +| Compact machine-parseable results | [Derivation logs](./derivations.md#machine-parseable-output-to_dict--to_json) | +| Session provenance | [Claim graphs](./claim-graphs.md) | +| Overview | [Autoresearch / agent loops](./search-plumbing.md) | diff --git a/docs/mdbook/src/search-plumbing.md b/docs/mdbook/src/search-plumbing.md new file mode 100644 index 00000000..353fa492 --- /dev/null +++ b/docs/mdbook/src/search-plumbing.md @@ -0,0 +1,48 @@ +# Autoresearch / agent loops + +Alkahest is useful inside unsupervised or lightly-supervised math search loops +because it is designed to be called **many times under a budget**, with results +that stay auditable. The pieces below are the *search plumbing* that sits next +to the mathematics: + +| Need | API | Guide | +|---|---|---| +| Bound one candidate so a hard instance cannot stall the sweep | `Budget`, `context(budget=…)`, `request_cancel` | [Budgets](./budgets.md) | +| Fan out many candidates without one failure aborting the batch | `batch_map`, `integrate_many`, … | [Batch](./batch.md) | +| Cheap, versioned payloads for logs / LLM context | `DerivedResult.to_dict(mode="compact")` | [Derivation logs](./derivations.md#machine-parseable-output-to_dict--to_json) | +| Accumulate claims across iterations | `alkahest.research` claim graph | [Claim graphs](./claim-graphs.md) | +| Ask “will this call certify?” before spending compute | `certifiable`, `require_certificate` | [Certificate coverage](./certificate-coverage.md) | + +A minimal loop shape: + +```python +import alkahest as ak + +pool = ak.ExprPool() +x = pool.symbol("x") +candidates = [x**2, ak.sin(x), ak.log(ak.log(x))] + +with ak.research.session(title="Sweep", pool=pool, capture=True) as s: + with ak.context(pool=pool, budget=ak.Budget(wall_ms=200, max_steps=50_000, seed=7)): + for item in ak.integrate_many(candidates, x, parallel=True): + if not item.ok: + # E-BUDGET-* → deprioritize; E-INT-* → record and move on + continue + # Token-cheap record for the next iteration / a human referee + _ = item.value.to_dict(mode="compact") + +print(s.graph.to_markdown()) +``` + +Honesty rules that matter in a loop: + +- A **budget trip is a fine answer**, not a crash — catch `BudgetExceededError` + (`E-BUDGET-*`) and deprioritize that candidate. +- A **batch never drops a slot** — failures become `BatchItem(ok=False, error=…)`. +- **Compact mode never hides verification status** — `verification["status"]` + stays readable; Lean source is omitted on purpose. +- **Certificates are withheld rather than lied about** — see + [certificate coverage](./certificate-coverage.md). + +See also the runnable experimental-mathematics demo +[`examples/pslq_research_loop.py`](https://github.com/alkahest-cas/alkahest/blob/main/examples/pslq_research_loop.py). diff --git a/docs/sphinx/api/core.rst b/docs/sphinx/api/core.rst index 541a97f2..2b96d507 100644 --- a/docs/sphinx/api/core.rst +++ b/docs/sphinx/api/core.rst @@ -132,27 +132,56 @@ DerivedResult with ``status == "certificate_available"`` has generated Lean source but has not been checked by Lean in this execution. + .. method:: to_dict(mode: str = "full") -> dict + + Versioned machine-parseable envelope combining ``value``, + ``verification``, ``certificate_status``, and ``steps``. + + :param mode: ``"full"`` (default) or ``"compact"``. Compact mode drops + ``before``/``after`` step text and uses short step keys (``r``/``s``), + but **never** renames or drops ``verification["status"]`` and never + includes Lean certificate source. See the + `derivation logs <../derivations.html#machine-parseable-output-to_dict--to_json>`_ + chapter. + + .. method:: to_json(mode: str = "full") -> str + + ``json.dumps(self.to_dict(mode=mode))``. + + .. attribute:: SCHEMA_VERSION + .. attribute:: STEPS_SCHEMA_VERSION + + Class-level integers matching ``alkahest.RESULT_SCHEMA_VERSION`` and + ``alkahest.STEPS_SCHEMA_VERSION``. + Example:: dr = diff(sin(x**2), x) print(dr.value) # 2*x*cos(x^2) for step in dr.steps: print(step['rule'], step['before'], "→", step['after']) + print(dr.to_dict(mode="compact")["verification"]["status"]) Context manager --------------- -.. function:: context(pool=None, domain="real", simplify=False) +.. function:: context(pool=None, domain="real", simplify=False, assumptions=None, require_certificate=None, budget=None, **extra) - Context manager that sets a default pool and configuration. + Context manager that sets thread-local defaults for a block. Inside the context, :func:`symbol` creates symbols in the active pool - without passing it explicitly:: + without passing it explicitly. Optional ``budget=`` pushes a + :class:`Budget` for the block (see the + `workload API `_ and the + `budgets guide <../budgets.html>`_):: with alkahest.context(pool=pool, simplify=True): z = alkahest.symbol("z") expr = z**2 + alkahest.sin(z) + with alkahest.context(pool=pool, budget=alkahest.Budget(wall_ms=50, seed=7)): + alkahest.integrate(z**2, z) + .. function:: symbol(name: str, domain: str = "real") -> Expr Create a symbol in the active context pool. Raises ``RuntimeError`` diff --git a/docs/sphinx/api/errors.rst b/docs/sphinx/api/errors.rst index 6f10b001..f5c57b20 100644 --- a/docs/sphinx/api/errors.rst +++ b/docs/sphinx/api/errors.rst @@ -169,6 +169,32 @@ Exception subclasses ak.diff(ak.sin(x), x) # fine — certifies ak.integrate(ak.log(x), x) # raises E-CERT-001 +.. exception:: BudgetExceededError + + Code prefix ``E-BUDGET-*``. A cooperative budget or cancellation trip — + not a mathematical failure. Raised when an active + :class:`~alkahest.Budget` is exceeded (or :func:`~alkahest.request_cancel` + was called) at a checkpoint inside an engine that honors budgets + (notably :func:`~alkahest.integrate`). See the + `budgets guide <../budgets.html>`_ and the + `workload API `_. + + - ``E-BUDGET-001`` — wall-clock limit elapsed + - ``E-BUDGET-002`` — step limit exceeded + - ``E-BUDGET-003`` — cancellation requested + + Example:: + + import alkahest as ak + + pool = ak.ExprPool() + x = pool.symbol("x") + try: + with ak.context(pool=pool, budget=ak.Budget(max_steps=0)): + ak.integrate(x**2, x) + except ak.BudgetExceededError as e: + print(e.code) # E-BUDGET-002 + Catching errors by subsystem ---------------------------- diff --git a/docs/sphinx/api/workload.rst b/docs/sphinx/api/workload.rst new file mode 100644 index 00000000..1c523566 --- /dev/null +++ b/docs/sphinx/api/workload.rst @@ -0,0 +1,101 @@ +Search / workload API +===================== + +.. currentmodule:: alkahest + +APIs for running Alkahest inside agent math-search loops: per-call budgets, +batch fan-out that never aborts on one bad candidate, and related helpers. + +Conceptual guide: `Autoresearch / agent loops <../search-plumbing.html>`_, +`Budgets <../budgets.html>`_, `Batch <../batch.html>`_. + +Budgets +------- + +.. class:: Budget(wall_ms=None, max_steps=None, seed=None) + + Immutable per-call resource budget. + + :param wall_ms: Optional wall-clock limit in milliseconds. + :param max_steps: Optional cooperative step limit. + :param seed: Optional determinism seed exposed via :func:`budget_seed`. + + Entered with ``context(budget=...)``. Trips raise + :exc:`BudgetExceededError` (``E-BUDGET-001`` wall, ``E-BUDGET-002`` steps, + ``E-BUDGET-003`` cancelled) from engines that check cooperatively + (notably :func:`integrate`). + +.. function:: request_cancel() + + Set the process-wide cancellation flag so cooperative checkpoints return + ``E-BUDGET-003``. + +.. function:: clear_cancel() + + Clear the cancellation flag before the next candidate. + +.. function:: is_cancelled() -> bool + +.. function:: is_budget_active() -> bool + +.. function:: budget_seed() -> int | None + + Seed of the innermost active budget, or ``None``. + +.. function:: active_budget() -> Budget | None + + The :class:`Budget` from the innermost Python ``context(budget=...)``, or + ``None``. + +.. function:: run_with_wall_fallback(fn, *args, budget=None, **kwargs) + + Python-layer wall-clock fallback for callables that cannot raise + :exc:`BudgetExceededError` through their own return type (e.g. + :func:`simplify`). Prefer ``context(budget=...)`` for engines that already + honor Rust cooperative checkpoints. + +Batch evaluation +---------------- + +.. class:: BatchItem + + One outcome from :func:`batch_map` / ``*_many``. + + .. attribute:: index + .. attribute:: ok + .. attribute:: value + .. attribute:: error + .. attribute:: elapsed_ms + + On failure, ``error`` is a dict with ``code``, ``message``, ``remediation``, + and ``type``. ``code`` is the exception's ``E-*`` code when present, + otherwise ``E-BATCH-001``. + +.. function:: batch_map(fn, items, *, parallel=False, max_workers=None, **kwargs) -> list[BatchItem] + + Call ``fn(item, **kwargs)`` for every item. **Never raises** for a single + bad element. Always returns results in **input order**. + +.. function:: batch_map_iter(fn, items, *, parallel=False, max_workers=None, **kwargs) + + Streaming counterpart. Under ``parallel=True``, yields in **completion + order** (each item still carries its original ``index``). + +.. function:: integrate_many(exprs, var, *bounds, parallel=False, max_workers=None, **kwargs) -> list[BatchItem] + +.. function:: simplify_many(exprs, *, parallel=False, max_workers=None, **kwargs) -> list[BatchItem] + +.. function:: diff_many(exprs, var, *, parallel=False, max_workers=None, **kwargs) -> list[BatchItem] + + Thin :func:`batch_map` wrappers over the common derivation entry points. + +Schema constants +---------------- + +.. data:: RESULT_SCHEMA_VERSION +.. data:: STEPS_SCHEMA_VERSION +.. data:: STEP_FIELDS +.. data:: STEP_FIELDS_COMPACT + + Version and field-name tables for :meth:`DerivedResult.to_dict`. See + `derivation logs <../derivations.html#machine-parseable-output-to_dict--to_json>`_. diff --git a/docs/sphinx/index.rst b/docs/sphinx/index.rst index 5568cf69..8beb5040 100644 --- a/docs/sphinx/index.rst +++ b/docs/sphinx/index.rst @@ -55,6 +55,7 @@ For optional Cargo features (``jit``, ``parallel``, ``cuda``, …) and full deve api/ode api/solve api/codegen + api/workload api/errors For the conceptual guide (kernel design, rule engine, e-graph, derivation logs)