psaegert/simplipy-assets

simplipy assets

Rule sets and engine configurations for simplipy, a fast, contract-sound simplification engine for symbolic mathematical expressions.

The engine and these rule sets are described in: Saegert & Köthe 2026, Breaking the Simplification Bottleneck in Amortized Neural Symbolic Regression (ICML 2026), arXiv:2602.08885.

Install an engine by name (downloads this repository's files on first use):

pip install simplipy

import simplipy as sp

engine = sp.SimpliPyEngine.from_config(sp.get_path("acj-4-3"))   # or "acj-3-2", "acj-2-1"

engine.simplify(('/', '<constant>', '*', '/', '*', 'x3', '<constant>', 'x3', 'log', 'x3'))
# ('<mul>', '<constant>', '<div>', 'log', 'x3', '</mul>')

engine.simplify('x3 * sin(<constant> + 1) / (x3 * x3)')
# '<constant>/x3'

Artifact-to-package compatibility is enforced at load (simplipy ≥ 0.12.0, the artifact-generation gate): simplipy ≥ 0.12 (the AC engine with the clean 23-operator vocabulary) pairs with the acj-* artifacts and the base config below — their configs carry an explicit engine_generation: 2 pin. The pre-0.12 artifacts (2-1, 3-2, 4-3, dev_*) use the retired hyper-operator vocabulary (mult3, pow2, ...) and are refused by simplipy ≥ 0.12 with an IncompatibleArtifactError naming the fix — pin pip install "simplipy<0.12" to serve them. The refusal is mutual: artifacts declaring a newer generation than the installed package refuse too.

simplipy ≥ 0.12 artifacts (AC engine, clean vocabulary)

Artifact refresh (2026-08-02): the acj family is re-mined under the unified description-length measure (mu): the engine's reduction ordering IS a minimum-description- length objective, special constants stay symbolic (sin(pi) never becomes 1.22e-16), and exact transcendental identities (cos 0 -> 1, cos pi -> -1, exp(-inf) -> 0) ship as mined, SYMBOLICALLY CERTIFIED rules -- the serve-time fold performs no numeric evaluation at all (exact rational arithmetic lives in the canonical constructors; a certified interval-classification arm carries extended-real collapses). Every mine is gated by an independent symbolic verifier (simplipy.verify.verify_ruleset) that re-judges each rule at its own trigger points at contract precision; f64 near-miss impostors (e.g. tanh(exp(pi)) -> 1, true residual ~1.5e-20) are refused. Rule counts shrank as engine machinery replaced whole rule families (constructor arithmetic, odd-root joins, generalized <constant>-shift absorption): what remains are the genuine identities the machinery cannot derive. rules.json.provenance.json pins the exact producing commit; double mining runs are byte-identical.

Each engines/acj-<S>-<T>/ directory is self-contained and reproducible with the same one-command invocation shown below (deterministic — re-mining produces byte-identical rules, verified by double runs at the pinned core_build). The acj cells mine the complete source universe of the 23-operator vocabulary with the AC engine itself as judge: a candidate rule is accepted only if it strictly descends the engine's own reduction ordering, so nothing ships dead-on-arrival. The LLM proposal channel is off. The provenance sidecar's core_build field pins the exact code commit that produced the mine (<version>+g<sha>). Rule counts are small by design: the AC engine's canonical constructors already perform arithmetic, collection, and ordering natively, so rules only cover genuine mathematical identities.

Release gates (400-expression corpus, recorded at mining time): idempotence 0 failures, commutative-permutation invariance 0 failures on all three artifacts.

Legacy mined artifacts (simplipy ≤ 0.11)

Each artifact directory engines/<S>-<T>/ is self-contained and reproducible from one config and one command:

The (S, T) cell mines the complete universe of source patterns up to length S against all candidate targets up to length T, augments the result with the certified survivors of a fixed 740-candidate LLM proposal batch (LLM_PROPOSALS_v1.json, identical across artifacts, sha256-pinned in each provenance sidecar), prunes rules whose effect the remaining rules already achieve compositionally, and promotes every rule to the strongest sound sort (_ arbitrary subtree, ! certified-finite subtree, ? variable-leaf) so each rule fires as generally as it soundly can. Larger cells subsume smaller ones; the smaller artifacts exist for fast loading and as fully-exhaustive reference points.

Every rule is independently verified: simplipy.verify.verify_ruleset gates each artifact (gate-clean, 0 KILL / 0 ENGINE-MISALIGN) and simplipy.verify.monitor_ruleset sweeps the deployed engine over an adversarial+sampled corpus (0 attributed violations) — a second soundness authority independent of the miner.

Each artifact ships:

• —rules.json — the mined + proposed, covered-pruned, sort-promoted rule set
• —config.yaml — the engine configuration (operator set; points at rules.json)
• —mine.yaml — the exact mining configuration
• —rules.json.provenance.json — everything that determines the mine: package and core build versions, host, parameters, seeds, the evaluation-matrix specification, per-length universe coverage, the proposals file's sha256 and per-outcome counts, per-length rule counts
• —LLM_PROPOSALS_v1.json — the co-located proposal batch (also published once at proposals/LLM_PROPOSALS_v1.json)

Reproduce any artifact byte-for-byte (mining is deterministic, single-command):

pip install "simplipy>=0.8.0,<0.12"    # legacy artifacts; use "simplipy>=0.12" for acj-*
cd engines/2-1
simplipy find-rules -e config.yaml -c mine.yaml -o rules.json -v --reset-rules

The mine.yaml sets promote_sorts: true, so this single command mines, certifies the proposals, prunes, and sort-promotes — the whole pipeline. Verify the result independently:

from simplipy.verify import verify_ruleset, monitor_ruleset
verify_ruleset("rules.json")                         # per-rule gate: only CERTIFIED/TOLERATED
monitor_ruleset("rules.json", "config.yaml", run_selftest=True)   # deployed-corpus sweep

Development engines (simplipy ≤ 0.11)

The development engines predate the 0.5.0 certification overhaul and the 0.7.x special-point certification; they are kept for compatibility with published experiments. The mined artifacts above are the recommended starting point for new work.

LLM proposal batch

proposals/LLM_PROPOSALS_v1.json contains 740 candidate rewrite rules proposed by a language model. Proposals carry zero authority: every candidate runs through the identical certification chain as mined rules (find_rules(..., proposals=...)), and only certified survivors join an artifact. The batch is a permanent, versioned input: artifacts pin it by sha256 in their provenance.