aeon

Programming Language designed for Program Synthesis with SMT-validation.

Project maintained by alcides Hosted on GitHub Pages — Theme by mattgraham

Synthesizers

Aeon supports automatic synthesis of program holes (?hole). When a hole is present, a synthesizer searches for an expression of the correct type that satisfies all refinement constraints. The synthesizer is chosen with the -s / --synthesizer flag:

uv run python -m aeon --budget 30 -s tdsyn_enumerative my_program.ae

The --budget flag sets the time limit in seconds (default: 60). The default synthesizer is tdsyn_enumerative (type-directed BFS); pass -s gp (or another id) to override.

Attach @minimize_size to a definition to minimize the core AST size of its hole replacements. This objective is supported by backends that rank or enumerate candidates; see the matrix below for limits. Use a joint backend for several interacting holes.

See the specification support matrix for each backend’s handling of examples, both CSV decorators, optimization, properties, refinement conversions, and planned improvements.

The shared candidate validators name intermediate constructor values in a temporary copy before typechecking. This keeps deep dependent-measure proofs compact for expression and whole-program backends, including GP, random search, enumerative search and CP-SAT. Bindings stay inside their original lambda or branch. Returned programs, runtime evaluation, expression-size scores, and resource objectives use the original candidate.

Expression grammar nonterminals carry both a domain and a type: Term[T] produces executable code, and Refinement[T] produces logical expressions. Runtime values and reflected functions contribute term productions; logical predicates and uninterpreted functions contribute refinement productions. First-order runtime values can participate in both. Lexical shadowing is resolved before either set of productions is built. Application arguments, lambda bodies, and conditional branches retain their parent’s domain, and component caches keep the two nonterminals distinct even when their types match. Explicit erased predicate arguments use the refinement domain. Both domains retain normal type checking; logical expressions are not treated as existential runtime values.

See the 50-item knapsack comparison for measured results and remaining limitations across ten backends.

Available Synthesizers

gp — Genetic Programming

Native genetic programming with a linear genome: each individual is a sequence of integer codons that select among Aeon’s grammar expansions when mapped to a core term. There is no fixed max depth — choice budgets grow with the generation index and mutation can lengthen genomes, so trees deepen as evolution advances.

GP decodes executable candidates through the term nonterminal. It uses ordinary grammar expansion for lists, including goals whose refinements fix their length.

Population size is chosen from a timing probe of the first ten random individuals so that initial evaluation uses at most 10% of the wall-clock budget. Crossover rate and mutation rate are sampled randomly each run; tournament size, novelty rate and related operator knobs are re-sampled every generation. Elitism keeps the best 5% of the population. Fitness comes from the synthesis decorators (@minimize_*, @maximize_*, @property, …). When objectives are present the shared Pareto driver returns a random non-dominated candidate; otherwise the first well-typed term wins. No GeneticEngine dependency.

Best suited for problems with a rich fitness landscape and sufficient budget.

With two or more objective components, parent tournaments and elitism use Pareto ranks computed once per generation. Rank 0 contains all valid non-dominated individuals; removing them exposes rank 1, and so on. Tournaments prefer the lowest rank among their contestants, and elitism keeps individuals from the lowest ranks first. Equal-rank ties, including a front that crosses the elite cutoff, are broken randomly using the run’s seed. Neither selection step prioritizes the first objective. Mixed minimize/maximize directions are respected, and invalid or unevaluated individuals rank below valid ones. Single-objective problems retain scalar fitness selection.

random_search — Random Search

Native random walks over Aeon’s core term grammar (the same backward and forward actions as enumerative). Each sample expands holes at random until a complete term is produced (or the depth bound is hit); the shared driver rejects those that fail typechecking, evaluates the rest, and keeps a Pareto front — returning a random non-dominated candidate when objectives are present, or the first well-typed term otherwise. No GeneticEngine dependency. Simple but effective as a baseline or for problems where the search space is small.

enumerative — Enumerative Search

Native breadth-first enumeration over Aeon’s core term grammar (backward and forward actions, plus SMT completion of refinement-constrained leaves). A generator yields complete terms; the driver rejects those that fail typechecking, evaluates the rest, and keeps a Pareto front — returning a random non-dominated candidate when objectives are present, or the first well-typed term otherwise. No GeneticEngine dependency. Works well for small, tightly-constrained holes.

amaze — Standard-Library-Trained Grammar Optimization

Offline AMaze-style learning mines typed macro compositions only from the packaged standard library, fits rank-based cost models and searches additions to a finite Int/Bool grammar. The inference backend consumes the immutable selected profile, expands candidates into Core, and uses normal whole-program validation and objective evaluation. It includes a package-only trainer, audited source/split manifest, independent tiny-grammar rank tests and a held-out stdlib comparison. See training, supported features and measured limitations.

rl_mcts — Reinforcement-Learning Guided Grammar Tree Search

An Aeon adaptation of Parsert and Polgreen’s Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis, sections 3–4. Search expands the leftmost typed hole, uses policy-weighted UCT and value-guided backpropagation, and commits to the most-visited child at each big step. Complete programs must pass the normal whole-program verifier; predictions never establish correctness and no axioms are introduced.

Without a checkpoint it uses the paper’s baseline: policy 1 and value 0.95 ** remaining_holes. Defaults follow the reported search parameters: 30 big steps, 6500 rollouts, decay 0.98 ** big_step. Additional safety limits are 100,000 nodes and eight recursive grammar expansions. These finite limits make search incomplete; timeout is not evidence that no solution exists.

python -m aeon -s rl_mcts --budget 10 examples/benchmarks/rlmcts/rl_mcts.ae

Learned guidance is optional and requires pip install 'AeonLang[synthesis-rl]'. Set AEON_RL_MCTS_MODEL=/path/to/checkpoint to load it. Checkpoints contain XGBoost policy/value models and a versioned feature manifest, not executable Python pickles. Only load model files from trusted sources.

Training uses hashed symbols and parent/child term walks, with hash base 4093. Value labels are 0.9 ** distance_to_solution on successful paths and zero on visited states of failed searches. Policy labels are child visits divided by all sibling visits on successful paths. XGBoost tree depths are 20/25 for value/policy. Training iteratively reruns problems and retains replay from the last four iterations. Inference never updates models.

To train on Aeon, supply files with exactly one independent refinement hole:

python -m aeon.synthesis.modules.rl_mcts train-aeon train1.ae train2.ae \
  --output /tmp/aeon-model --iterations 2 --budget 10
AEON_RL_MCTS_MODEL=/tmp/aeon-model python -m aeon -s rl_mcts held-out.ae

The data-generation tool instead starts from universally valid quantifier-free Int/Bool SMT formulas (satisfiability alone is insufficient). Anti-unification preserves repeated disagreement pairs, lifts source variables into parameters, and replaces selected, non-overlapping Int subterms with synthesis calls. It checks the resulting generalizer as a witness, but never gives it to search. The grammar includes constants from the source, addition/subtraction, constant multiplication/division/modulo, comparisons, Boolean operators, and conditionals. Nonlinear generalizers, quantifiers, arbitrary uninterpreted functions, other sorts, and unknown solver answers are rejected. Automatic selection prefers large same-head subterms; it does not reproduce the paper’s corpus filtering or published dataset.

python -m aeon.synthesis.modules.rl_mcts generate \
  examples/benchmarks/rlmcts/rl_mcts_training.smt2 --output /tmp/aeon-rl-data
python -m aeon.synthesis.modules.rl_mcts train \
  examples/benchmarks/rlmcts/rl_mcts_training.smt2 --output /tmp/aeon-smt-model \
  --iterations 2 --limit 2 --budget 10

Both adapters share the same search/replay implementation, but SMT syntax and Aeon compiler ASTs have different feature vocabularies. Train on Aeon problems for Aeon inference; a generated-SMT checkpoint is not a demonstrated transfer model. Keep training and held-out tasks separate. Training fails explicitly if no iteration finds a successful policy path.

rl_mcts checks examples, sampled properties, and exact-fit CSV data before acceptance. With numerical objectives it continues exploring after solutions, keeps successful visits as positive rewards, and ranks feasible terms in the shared Pareto archive. Its grammar comes from Aeon’s shared backward/forward actions, not an imported arbitrary SyGuS grammar. Constants and supported polymorphic/ADT components inherit that grammar’s limitations. Calls into the compiler/verifier are synchronous, so a final in-flight check can overrun the search time budget. This implementation is not a reproduction of the paper’s performance results; no pretrained model or published 1901-task dataset is bundled.

regus — Reward-Guided Controller Structure Synthesis

Bounded ReGuS adaptation with high-level loop-sketch UCT, persistent low-level completion queues, execution-guided gap expansion, and conditional repair triggered by abstract-state disagreements. Existing ControlProgram bindings can be reused as procedures in an explicit curriculum. The controller interpreter and environment callbacks are ordinary Aeon.

python -m aeon -s regus --budget 60 examples/synthesis/control/thermostat_structure.ae
python -m aeon -s gp --budget 60 examples/synthesis/control/thermostat_structure.ae

Targets ControlProgram holes with standard numerical objective decorators and an @cluster feature returning ControlObservation (or a deferred function returning one). Goals, action/sensor vocabularies, initial states, and penalties remain in the problem file and can be used by other ADT-capable fitness backends. The current backend handles one program hole at a time. Scalar gain holes should use the existing numerical backends; the structure examples search finite numeric action palettes.

Uses the shared validation, worker containment, and Pareto selection paths. Partial controllers guide search but cannot be returned. The implementation uses all training starts together and budgeted optimization; it does not implement the paper’s progressive seed/threshold protocol, automatic task ordering, or full abstract-contract merging. See the control examples and protocol for supported semantics, bounds, and differences from the paper.

structure_guided — Structure-Guided Recursive Synthesis

Synthesizes recursive list-producing functions from constructor-literal @example pairs using size recurrences, partial-structure pruning, and local element synthesis. Inspired by Lin and Morihata’s Recursive function synthesis based on structural relationships and Structure-Element Separation (GPCE 2026). This is a bounded adaptation to Aeon’s constructor representation, not a reproduction of the full published synthesizer or benchmark results.

python -m aeon -s structure_guided --budget 10 examples/synthesis/structure_guided/paired_map.ae
python -m aeon -s structure_guided --budget 10 examples/synthesis/structure_guided/tree_inorder.ae

The target must have one value parameter, a body hole, @allow_recursion, and literal input/output examples. It may accept a list or binary-tree datatype; the result is a list of integers. Datatypes must be registered inductives with exactly two constructors: one nullary base and one recursive constructor with one or two immediate recursive fields and one or two Int fields. Outputs need exactly one recursive field and one Int field. Constructor names, declaration order and field order are discovered from the typing context, rather than hardcoded. Parametric datatypes instantiated at Int are supported. Explicit type applications such as List.nil{Int} may be needed in examples when the frontend cannot infer a nullary constructor’s type arguments.

Search. First infer every bounded recurrence consistent with the examples:

length(f empty) = d
length(f node)  = c + sum(a_i * length(f child_i))

For lists there is one child; for binary trees there are two. Sizes are computed by recursively expanding the input structure, not by assuming recursive outputs have the input children’s sizes. Ambiguous examples retain all fitting models.

The output-constructor/append grammar normalizes to a word whose tokens are individual element holes or calls on immediate input children. Top-down prefix expansion tracks constructor and call counts. Prefixes incompatible with every inferred model are pruned before element expressions are enumerated. A stutter task requiring two new elements per recursive step therefore rejects a complete one-constructor skeleton while its element hole is still open. Constructor order and the order of recursive calls remain search choices, supporting such tasks as reverse, repeated maps and tree traversal.

Next, symbolic execution unrolls each candidate skeleton into diamond atoms carrying a hole identity and its local integer inputs. Positional alignment with expected outputs produces small PBE tasks for each hole. Conflicting observations reject a skeleton immediately. Each task is solved by size-ordered enumeration of local Int fields, literals and +, -, *, with observational equivalence on that task’s examples. No reference stutter, reverse, map or traversal program is supplied to search.

The resulting core term uses actual datatype constructors, recursors and immediate-child self-calls. When concatenation is needed, a local recursive append is generated from the output datatype and checked with the rest of the candidate. No arbitrary library function is assumed to implement append. Acceptance requires both the normal whole-program validator and execution against every supplied I/O example. The runtime probe ties the recursive self name to the candidate, so it cannot accidentally test the placeholder body.

Bounds. Each Config field can be set with an integer environment variable AEON_STRUCTURE_<FIELD_NAME>, or through StructureGuidedSynthesizer(Config(...)) (import Config from aeon.synthesis.modules.structure_guided.search). Defaults are:

The wall-clock budget covers recurrence inference, structural and element search, and runtime example checks. Compiler validation and individual synchronous evaluation calls can overrun the budget; no new process-based timeout is added. Search counters are available as backend.stats, including pruned prefixes, alignment/local-task counts and candidate validation/runtime rejections.

Limits and guarantees. This backend learns from examples; inferred size relationships do not prove a universal functional specification. Any declared refinement still has to pass Aeon’s ordinary verifier. Fixed-recurrence search does not cover value-dependent filtering, arbitrary recursion, accumulator parameters, tree-valued results, nested/mutual datatypes, opaque library calls, Boolean element computations, or relational examples without a usable I/O corpus. Additional examples and @property checks validate candidates alongside the corpus; numerical, size and resource objectives rank the explored recurrences. Unsupported goals are reported explicitly. Search bounds, finite literal and element grammars, and observational merging make search incomplete: exhaustion is not evidence that no implementation exists. Like other per-hole backends, this backend does not jointly solve coupled holes.

synquid — Type-Directed Synthesis

This backend implements round-trip checking, incremental shape/refinement constraints, MUSFIX condition abduction, polymorphic function and fixpoint introduction, and datatype match synthesis. See the implementation and validation notes for supported fragments, bounds, and differences from PLDI 2016 Synquid.

The result’s retained relations instantiate constructors directly; inferred predicates are materialized from the solved assignment rather than replaced with fresh inference holes. Executable components use the term grammar, and erased predicate arguments use the refinement grammar. Lists use ordinary search. Candidates carry completed construction proofs, so Synquid skips repeated whole-program typechecking.

Search. Default synquid_search: "paper" streams rule-directed candidates at increasing application depth, with independent synquid_match_depth (default 2). "size_merge" merges candidates by AST size and depth; "iterative_deepening" exhausts each sorted level. Tunables remain synquid_max_level, synquid_seed_levels, and synquid_max_candidates. The time budget also applies during candidate construction. Each level yields at most 4,000 candidates. Term memoization is disabled because (context, level, goal) does not identify the pending constraint state.

Applications. The expected result constrains liquid polymorphic instantiations before arguments are chosen. Independent result obligations are checked immediately; dependent obligations remain pending. Selected arguments contribute their inferred refinements and existential witnesses. Consistency checks ask whether remaining arguments and the result can jointly satisfy their contracts, including datatype measures and branch assumptions. Only proved failures prune partial applications. Completed constructions require discharged proofs; unknown or unsupported obligations cannot certify a candidate. Higher-order arguments can be deferred until first-order arguments determine their types.

Conditionals. Search proposes a branch under an unknown path predicate, derives its verification conditions, and strengthens the predicate from true using MUSFIX-style minimal-subset enumeration. It retains incomparable solutions, removes semantically stronger guards, realizes a Boolean expression, and builds the other branch under the guard’s negation. MARCO enumerates syntactically minimal sufficient qualifier sets; semantic minimization compares only the resulting valuations. No eager pairwise qualifier ordering is performed.

Validation and observability. Typing and termination obligations are discharged during construction. The entrypoint skips per-candidate whole-program typechecking for Synquid; non-type checks such as @bounded_cnf remain active. With no fitness goals, the first certified candidate satisfying those checks is returned. SynquidSynthesizer.stats records generated arguments, partial rejections, specification checks, abduction proposals/guards, fallback guards, solver queries, and explicit solver outcomes. The compatibility counter full_validations stays zero. modular.py continues to expose the compatibility decomposition API and ModularVC.

Validity queries reuse a bounded SMT solver and translated constraints across search forks and application-depth levels. Each obligation has its own assumption selector, so assertions from other branches cannot change its result. Queries are rechecked with the current deadline; unknown results are never treated as proofs. Compilation-session changes and datatype resets invalidate the cache. MUSFIX keeps its separate tracked-assumption solvers.

polynomial — Polynomial Certificate Synthesis

Synthesizes bounded-degree polynomial expressions using algebraic certificates, inspired by Goharshady et al., Template-based Program Synthesis using Stellensätze. It fills all program holes jointly using the compiler’s shared verification conditions, including when there is only one hole. Refinement contracts, surrounding code, @example relations, and @property functions contribute logical obligations; properties are checked universally by the certificate encoding, rather than only on their runtime corpus.

python -m aeon -s polynomial --budget 10 examples/synthesis/polynomial.ae
python -m aeon -s polynomial --budget 10 examples/synthesis/polynomial_sketch.ae

Each numeric hole receives a polynomial template over its lexical inputs with unknown coefficients. For example, an Int -> Int hole at degree two searches c0 + c1*x + c2*x*x. Int holes use integer coefficients; Float holes use real coefficients. Explicit coefficient holes can also fill a programmer-supplied larger sketch, as the second example demonstrates.

For an obligation g_i >= 0, h_j = 0 => p >= 0, the backend constructs:

p = sum(lambda_alpha * product(g_i ** alpha_i))
    + sigma_0 + sum(sigma_i * g_i) + sum(q_j * h_j)

The lambda coefficients are nonnegative (Handelman products); every sigma is a sum of polynomial squares (Putinar-style multipliers); the q polynomials are unrestricted equality multipliers. Coefficient matching makes this a purely existential SMT problem: universal input variables disappear from the synthesis solver. Linear cases include Farkas-style certificates. Equalities are proved in both directions; strict conclusions additionally require a positive constant margin. Without numerical objectives it returns a feasible program. With objectives it blocks previously emitted program coefficients and retains a Pareto front within the budget. Complete candidates must pass Aeon’s ordinary whole-program validator before fitness evaluation or publication to the UI.

Configure the finite search space through environment variables:

The Python API accepts PolynomialConfig, including limits of 4096 monomials / product expansion pairs, 10,000 unknown coefficients, and 64 premise branches. The budget covers template construction, certificate expansion and solving; the final synchronous compiler validation / objective evaluation is additional.

Supported subset and guarantees. Numeric holes need homogeneous Int or Float parameters and results. Expressions support constants, variables, hole calls, addition, subtraction and multiplication. Conclusions are conjunctions of numeric equalities/inequalities; premises also allow disjunction and negation. Boolean compiler value binders are eliminated when they are definitions; arbitrary Boolean inputs and Boolean-valued holes are unsupported. Integer division, modulo, division in source specifications, conditional arithmetic, ADTs and opaque native calls are rejected explicitly. A positive SOS degree uses a full square factorization of the bounded monomial Gram matrix, rather than only diagonal squares; no external SDP solver is needed.

Certificates prove obligations over mathematical reals. Int variables are conservatively relaxed to reals while program coefficients remain integers; strict premise inequalities are conservatively closed. These choices are sound but can miss programs valid only on discrete or open domains. Float follows Aeon’s existing real-arithmetic refinement semantics, not an IEEE-754 roundoff guarantee. Rational program coefficients are emitted as ratios of exactly representable integer-valued Float literals; irrational or excessively large coefficients are rejected.

Failure means no certificate was found at these bounds, or the solver timed out / returned unknown; it does not establish unrealizability. This is a bounded Handelman/SOS backend, not the paper’s full imperative-program frontend, automatic loop-invariant synthesis, Real Nullstellensatz procedure, or its semi-completeness theorem. The generated constraints can be higher than quadratic when holes occur in assumptions or are composed; no general QP reduction or published performance result is claimed.

noisy — Regularized Synthesis from Noisy Examples

Treat scalar I/O examples as soft observations while keeping refinement checking mandatory. A bounded native generator and history-based sampler minimize mismatch rate plus a configurable complexity penalty. See noisy-example synthesis for configuration, residual reports, supported inputs, and reproducible adaptive/uniform/full-data comparisons.

boolean_bounded — Bounded Boolean CNF with CEGIS

Opt-in, solver-based synthesis using the existing Z3 dependency. Each target must declare a literal, nonnegative clause bound in the Aeon source:

@bounded_cnf(2)
def xor (x:Bool) (y:Bool) : {r:Bool | r = (x != y)} := ?body;

python -m aeon --no-main --budget 10 -s boolean_bounded examples/synthesis/boolean_bounded/xor.ae
python -m aeon --no-main --budget 10 -s boolean_bounded examples/synthesis/boolean_bounded/partial_relation.ae

@bounded_cnf(K) is a hard maximum of K CNF clauses per completed definition, not a fitness penalty. A clause contains Boolean input variables or their negations, joined by OR; clauses are joined by AND. True is the empty conjunction (zero clauses); false is one empty clause and requires K ≥ 1. Duplicate literals and clauses, tautologies, and Boolean constants are normalized before counting. Lexical let aliases are expanded with their defining scope. Conditionals, arbitrary helper calls, conjunctions inside disjunctions, and negated compound expressions are rejected rather than treated as literal atoms or distributed exponentially. Type annotations do not change the count. No hidden auxiliary inputs or Tseitin variables are admitted. The structural checker is independent of the solver encoding and checks the actual completed function.

The first version supports one hole per annotated definition, including nullary constants, function bodies with Boolean lexical captures, and full function holes. Multiple annotated definitions are solved together, with their individual bounds and lexical scopes preserved. Unknown functions have only unrestricted Boolean parameters and a Boolean result. Arithmetic, native/opaque logical specifications, recursive specifications, higher-order unknowns, unresolved polymorphism and other multiplicities produce capability errors. Surrounding sketches and captures must still normalize to CNF over the definition’s Boolean parameters; a solver candidate that fails this or Aeon’s typechecker is reported as a validation error, never accepted or reported as bounded infeasibility.

Compiler-generated verification conditions, refinements, @example assertions, and compatible @property laws constrain a shared family of CNF templates. Counterexamples add instances of the full relation, preserving multiple valid output choices. The same selectors are reused at every call, including nested Boolean calls. Properties are checked universally, independently of their sampled fitness corpus. A partial relation must explicitly state its Skolem law in the source, as in partial_relation.ae: witnesses belong to the law’s quantification, not the synthesized functions’ parameters. Ordinary total refinements are never automatically weakened to a feasibility domain.

The solver returns the first feasible bounded candidate. Optional objectives are evaluated only after structural and full Aeon validation; this release does not optimize them, minimize K, or prove global synthesis impossibility. Other backends may parse the same annotation, but the shared acceptance/scoring gate still enforces it. Program-level adapters without that gate, and non-joint adapters handling multiple annotated holes, reject the annotation explicitly. Unannotated programs keep their existing behavior.

AEON_SEED controls solver seeds. Each run owns fresh selectors and solvers. BooleanBoundedSynthesizer.report records status, iterations, counterexamples, selector count and elapsed time for the bounded operation. BoundedBooleanFailure.category distinguishes bounded_unsat, timeout, resource_limit, unknown, and validation_error; capability mismatches use UnsupportedSynthesisGoal. bounded_unsat means no solution in the fixed, supported CNF family. Limits of 100,000 selector bits and 100,000 translated predicate/template nodes prevent unbounded allocation; the Python API can configure these limits. The independent normalizer limits each definition to 10,000 visited syntax nodes. Shared compiler preparation, search, extraction, final validation and optional fitness evaluation run in the same killable worker used by noisy, under one wall-clock budget. Z3 calls also receive the remaining budget as their timeout. At the deadline the parent terminates the worker, escalating to kill if necessary, and reports timeout without accepting or publishing a candidate. Worker cleanup has a short bounded grace period. Direct calls to the Boolean adapter similarly contain search, extraction, validation and evaluation. Parsing/compilation before entering synthesis is outside this budget.

This implements a solver-based bounded Boolean search, not BNSynth’s neural learner. The separate benchmark corpus and evaluation harness are tracked in #650.

smt — SMT-Guided Synthesis

Constructs a candidate expression top-down using the typing context:

Once the term structure is fixed, all constraints are discharged in a single z3 call. If satisfiable, the placeholders are replaced with the concrete values from the model and the result is validated.

Best suited for problems whose solution is primarily determined by arithmetic or boolean constraints on integers and floats — for example, finding a concrete value satisfying a chain of liquid-type inequalities.

Configurable option: max_depth (default 5) controls how deeply the synthesizer recurses when building non-SMT subterms.

bustle — Learning-Guided Bottom-Up Synthesis

Implements the core of BUSTLE (ICLR 2021): enumerate typed expressions bottom-up by weight, execute them on scalar or closed-constructor @example inputs, merge observationally equivalent output vectors, and use a trained property-signature MLP to adjust intermediate-expression weights. Predictions are batched; the paper’s probability bins add penalties from 0 to 5. Inputs and constants remain at weight 1. An expression must match every example and pass Aeon’s type validation before acceptance.

The bundled model was trained reproducibly on synthetic bottom-up searches. It uses NumPy when installed and otherwise standard-library inference, with no model downloads or PyTorch dependency. AEON_BUSTLE_MODEL selects a compatible JSON checkpoint. -s bustle_baseline explicitly disables learned guidance for comparison.

Supports one to three scalar or registered ADT inputs, scalar or ADT results, first-order in-scope components, and conditionals. ADT guidance uses constructor identity, depth, size, and subtree relations; merging uses full structural identity, including scalar field types. Concrete polymorphic ADT instantiations are supported. ADTs are bounded to depth 16 and 128 constructor nodes. With numerical objectives it continues enumeration and ranks feasible terms in a Pareto archive, retaining syntactically distinct subterms that may differ on objectives. Search is bounded by adjusted weight 40, 20,000 distinct values, and the time budget. See examples, training instructions, and differences from the paper.

arborist — Lifted Interpretation with Local Variables

Adapts the lifted interpretation algorithm from Li et al., POPL 2024, Section 3 and Appendix A. A bounded typed grammar is stored as a packed tree language. Interpreting the enclosing Aeon sketch discovers reachable local bindings; specializing the grammar under each binding context constructs observational classes bottom-up while retaining all their alternatives. A subsequent call specializes the surviving language, allowing classes to split and ensuring that every fold iteration uses the same candidate body.

Select it with python -m aeon --no-main --budget 10 -s arborist examples/benchmarks/arborist/list_fold.ae. It accepts literal Int/Bool or closed registered-constructor inputs, Int/Bool outputs, and one Int/Bool expression hole inside a supplied pure functional sketch. Supported surrounding Core forms include lambdas, applications, local bindings, conditionals, recursive functions, and compiler-generated constructors/eliminators (match). The supplied fold combinators are interpreted from their Aeon definitions; their accumulator contexts depend on candidate outputs. Generated expressions use lexical scalar variables, small constants, arithmetic, comparisons, Boolean operations, and conditionals. list_fold.ae preserves the paper’s ambiguous [1,2,4] → 7 example; list_sum.ae adds distinguishing examples.

The backend uses the program-level synthesis interface to observe the enclosing execution. Every extracted solution passes the usual whole-program type/refinement validator and the examples in Aeon’s normal evaluator. Rejection of one example-equivalent representative does not discard its alternatives. Search observes the wall-clock budget, with default limits of three nested grammar operations, 100,000 packed states, one million interpreter steps, and 4096-bit integers. An in-flight compiler check or final runtime check can overrun the budget.

This implementation searches bodies in a fixed sketch, not arbitrary loop structures or the paper’s web-automation language. Constructor inputs/intermediates are bounded to 128 total nodes and depth 32. ADT-valued holes/results, Float/String leaves, arbitrary native/effectful components, and multiple holes are unsupported. Numerical objectives continue extraction from the surviving language and rank candidates in a Pareto archive. Recognizing compiler-generated inductives does not enable general native execution in the lifted interpreter. Unlike fta and bustle, its equivalence classes account for execution-dependent local bindings; unlike afta, it uses exact concrete observations rather than abstraction refinement. See the examples, invariants, restrictions, and compression experiment.

decision_tree — Decision Tree Regressor

Fits a scikit-learn DecisionTreeRegressor to training data provided via @example, @csv_data, or @csv_file, then converts the resulting tree into a nested if-then-else Aeon term. Without explicit data, the shared synthesis entrypoint derives examples from the function’s input and output refinements. Inputs and outputs must be numeric, and the output must be uniquely determined for each sampled input. Integer splits use an equivalent integer threshold so refinement checking retains the branch condition.

Recognized minimized squared errors, or maximized negative squared errors, also provide training labels. A signed difference such as @minimize(f 1.0 - 5.0) does not specify the label 5.0 and is no longer converted into an example.

Useful for regression problems where input–output pairs are available and a readable, interpretable result is desired.

Examples derived from refinements

When decision_tree, contata, or bustle needs examples and no explicit corpus is present, the entrypoint samples the function’s refinement with SMT. It preserves dependent input preconditions, decodes scalar and registered inductive values, and typechecks each concrete input/output pair. Explicit examples and source metadata are preserved. Candidate acceptance still requires the full refinement; a sampled corpus is not a proof of correctness.

Generation is bounded to 32 distinct inputs and four constructor levels, with a two-second generation budget (or one fifth of the synthesis budget, whichever is smaller). Its elapsed time is deducted from the search budget. It applies to a hole in the function’s result position, including one wrapped in local bindings. Finite domains can be exhausted, including all eight zero-depth input combinations in nand_full_adder.ae; infinite domains yield a bounded corpus.

Exact labels are emitted only when SMT proves the output unique for each sampled input. Otherwise observations retain the original relation: for example, the adder refinement fixes the sum and carry bits while leaving circuit depth free for optimization. BUSTLE can use relational observations for guidance and checks outputs against the refinement. Decision trees and Contata require exact labels and report unsupported non-unique outputs. Their existing datatype, arity and grammar limits still apply; generating examples does not add circuit terms to a numeric decision tree. Additional objectives rank the candidates each backend can generate.

llm — Large Language Model (Ollama)

Uses a locally running Ollama instance to generate candidate expressions. The default model is qwen2.5-coder:32b; per-model backends are also available (e.g. -s llm_qwen2.5-coder-14b). The LSP menu lists each model by its Ollama tag. The model is prompted with a description of the synthesis problem, including the target type and any @doc("description") decorator. Generated expressions are parsed, type-checked, and validated in a loop until the budget expires or a valid candidate is found.

Curated models for Apple Silicon with ≤64 GB RAM. Models are pulled automatically on first use (disable with AEON_OLLAMA_AUTO_PULL=0). Before synthesis, other loaded Ollama models are unloaded from memory to stay within AEON_OLLAMA_MEMORY_BUDGET_GB (default 56). After synthesis, the active model is released from RAM (disable with AEON_OLLAMA_RELEASE_AFTER=0).

Synthesizer id Ollama model Approx. size (Q4)
llm / llm_qwen2.5-coder-32b qwen2.5-coder:32b ~20 GB
llm_qwen2.5-coder-14b qwen2.5-coder:14b ~9 GB
llm_deepseek-coder-v2-16b deepseek-coder-v2:16b ~10 GB
llm_codellama-13b codellama:13b ~8 GB
llm_starcoder2-15b starcoder2:15b ~9 GB
llm_deepseek-coder-6.7b deepseek-coder:6.7b ~4 GB

Requires Ollama to be running locally. Use @doc("description") to describe the desired behaviour. The same string supplies the definition’s documentation when generating HTML with --doc.

llm_type_constrained — Type-constrained local LLM decoding

Constrains tokens before they are committed, using bounded ordinary-type completion witnesses. For example, f : Int -> Bool remains viable for a Bool goal because f 0 completes it, whereas f true is rejected. Complete expressions still pass Aeon’s original refinement validator before fitness evaluation. A well-typed 0 can therefore be rejected for {v:Int | v > 0}.

Install AeonLang[llm-type-constrained], set AEON_TC_MODEL to a local Transformers causal model directory or model ID, and run:

AEON_TC_MODEL=/path/to/model AEON_SEED=0 python -m aeon --no-main \
  -s llm_type_constrained --budget 60 examples/synthesis/type_constrained/application.ae

This provider uses token logits; Ollama and OpenAI whole-text clients remain separate baselines. Unsupported providers fail explicitly. Dependencies load only when this backend runs. See the fragment, bounds, adapter, and smoke-test contract for limitations and configuration.

tdsyn / tdsyn_enumerative — Type-Directed Synthesis (BFS) (default)

Top-down, type-directed synthesizer that grows a partial AST by applying backward and forward actions to each open hole. Subtyping queries are discharged by an SMT solver, and when every remaining hole is a base-type leaf the synthesizer asks z3 to solve them all in one shot.

Full synthesis is limited by the time budget, with no fixed depth or expansion-count cap. Breadth-first exploration alternates with constructor continuations so that deep data can be built while other expressions remain in the search. Structural holes are expanded before scalar payloads, which SMT can complete jointly. If no optimization goals are present, the first valid term is returned; otherwise candidates contribute to the shared Pareto front.

Use --tdsyn-expansion eager|lazy to compare expansion strategies across tdsyn, tdsyn_enumerative, tdsyn_backward, and tdsyn_random. The default is eager, which prepares and checks every alternative before continuing. lazy constructs and checks alternatives on demand. BFS keeps resumable expansions in its ordinary queue, allowing constructor children to progress through the guided queue while postponed siblings still receive FIFO turns. Both modes use the same productions, feasibility checks, final validation, and objective evaluation. Their visitation order can differ.

python -m aeon -s tdsyn_backward --tdsyn-expansion eager --budget 30 examples/synthesis/puzzle/knapsack_50.ae
python -m aeon -s tdsyn_backward --tdsyn-expansion lazy --budget 30 examples/synthesis/puzzle/knapsack_50.ae

Python callers can use AeonConfig(..., tdsyn_expansion="lazy") or TDSynSynthesizer(..., expansion="lazy").

Unchosen application arguments are existential witnesses during feasibility checks. Argument preconditions, dependent return contracts, and the goal refinement travel with the holes, including through type and refinement applications. Choosing one argument constrains its siblings. Only an unsatisfiable query prunes a candidate; unknown or unsupported queries leave it available for the final whole-program validator. For example, List.size xs = 10 permits cons with a tail of size 9 and rejects closing that tail with nil too early. These rules are shared by all three full TDSyn variants.

Property-test input generation has a separate, explicitly bounded sampling API; its caller-supplied limits do not limit full synthesis.

Constructor relations retained in the result type are instantiated from the hole’s goal, including predicates with several arguments. For example, a goal Mask{|fun w => fun rest => w + rest <= 100|} supplies that relation to Mask.cons and its argument holes. Predicates left for Horn inference keep their declared arity. The final validator still checks every completed candidate against the original specification.

Completed definitions keep the compiler’s logical reflection in hole contexts, including array literals and indexed reads. Constructor equations constrain pending arguments even after a nullary constructor closes a hole. Thus an exact length refinement can force a fixed list shape before SMT solves its scalar elements jointly with constraints such as total weight. The search checks these obligations separately during reflection so large lists do not leave array expressions opaque merely because their combined formula is large. Completed constructor trees name intermediate data values before final checking to keep dependent measure proofs compact. Ordinary calls and control flow retain their original form and evaluation order.

Related constructor steps reuse a session-local SMT solver and the translated constraints they share. Branch assumptions and model-blocking clauses remain isolated. Constant arrays, indexed reads, and reflected substitutions are cached. Final validation reuses successful proofs for unchanged obligations, keyed by their premises, variable sorts, function signatures, and reflected definitions; new or changed obligations still require a proof. These caches are bounded and cleared between compilation sessions.

tdsyn_random — Type-Directed Synthesis (Random Walks)

Same expansion rules as tdsyn, using random walks with a preference for constructor expansions. Walks prioritize structural holes and check available completions before growing deeper. Probabilistic restarts avoid spending the whole budget on one unproductive walk; there is no maximum walk length. SMT solves the remaining scalar leaves jointly.

With lazy expansion, random walks shuffle production descriptions before checking them and take the first usable child. They try constructor productions first on 90% of steps, falling back to ordinary productions when necessary. This avoids checking all siblings, but changes the sampling distribution from eager random search; the flag is not a promise of identical seeded candidates.

tdsyn_backward — Type-Directed Synthesis (Backward BFS)

Runs the same time-budgeted search, SMT completion, validation and Pareto selection as tdsyn, using backward expansions at every open hole. These introduce literals, variables, applications, abstractions and conditionals. Search continues until it finds a complete term or exhausts its budget; it never returns partial subgoals.

Examples, both CSV decorators, properties, min/max, multiple objectives, expression size and CPU/energy goals have the same semantics as tdsyn. Examples and properties supply fitness, while refinements remain hard checks. With objectives, search retains the explored Pareto front and returns a seeded member. Without objectives it returns the first valid complete term. @doc remains documentation, just as with tdsyn.

The granular backward_* commands apply individual constructions once.

backward_abs / backward_lit / backward_close / backward_app / backward_if — Backward Steps

Demonstrative single-step backends: each applies one slice of the backward action exactly once to the hole, so the constructions bundled in tdsyn_backward can be applied one by one:

Backend Candidates
backward_abs fun x -> ?body for a function-typed goal, with ?body typed by the codomain and x in scope (other steps auto-abstract function-typed goals, so this step makes that introduction explicit)
backward_lit literals of the goal’s base type (Int, Bool, Float)
backward_close an in-scope variable whose type already proves the goal — the same candidates as forward_close, exposed under both directions’ menus
backward_app f(?h1, ..., ?hn) for each in-scope (possibly monomorphized) function whose return type matches the goal, leaving holes for the arguments
backward_if if ?c then ?t else ?e with branches typed by the goal

Each returns the first complete candidate that typechecks, or otherwise the first expansion with fresh ?<fun>_goal_<i> subgoal holes, so steps can be chained. No search is performed — use tdsyn for actual synthesis.

forward_close / forward_let_* — Forward Steps

Demonstrative single-step backends: each applies its forward action exactly once to the hole. forward_close closes the goal with a variable whose type already proves it. The forward_let_* tactics grow the scope with a let v := <value> in ?goal binding, reopening the goal with v in scope; each variant binds one term former as the value:

Backend Let value Type of v
forward_let_app forward application f(x, ?...) (in-scope function applied to an in-scope variable, result matching the goal) the application’s unrefined result type
forward_let_if if ?c then ?t else ?e with branches typed by the goal the goal type
forward_let_tapp monomorphic instantiation of a polymorphic in-scope variable (operators insert as sections, e.g. (=)) the instantiated type
forward_let_abs fun x -> ?body with ?body typed by the goal, for each built-in base domain (x:domain) -> goal
forward_let_tabs Λa:B. ?body with ?body typed by the goal forall a:B, goal

Each returns the first complete candidate that typechecks, or otherwise the first expansion with fresh ?<fun>_goal_<i> subgoal holes, so steps can be chained. No search is performed — use tdsyn for actual synthesis.

When a function has several holes (e.g. the subgoals a previous step inserted), the LSP Synthesize action targets exactly the hole it was invoked on and leaves the siblings open; on the CLI, synthesis fills the first hole of each function.

tactics — Random Tactic Search

A Lean-style tactic synthesizer. The proof obligation (the hole’s goal type in its typing context) is reduced step by step by repeatedly choosing a random open hole and a random tactic from:

Each iteration starts a fresh walk (up to 20 tactic steps); walks that fail to close all holes are abandoned. When optimization goals are present, the best-scoring closed walk across the budget is returned.

lta — Liquid Tree Automata

Component-based synthesis via Liquid Tree Automata (Algorithm 1 of the LTA paper). An automaton is seeded from the library functions in scope, the parameters of the goal type, and a minimal set of constants. It is then iteratively expanded by an explore-reduce-check loop:

  1. Transition — one round of E-app expansion pairs every function state with every argument state.
  2. Prune — drops states whose refinements are unsatisfiable.
  3. Similarity / Minimize — collapses observationally equivalent states.
  4. Goal check — Q-goal transitions try to connect candidate states to the goal type; a non-empty final state yields a candidate term.

Polymorphic library functions are kept as cyclic template states and finitely unrolled into monomorphic instantiations against a small type universe. The expansion is depth-bounded (default max_depth = 4).

ortools / cpsat — Fixed-length lists

CP-SAT can fill one hole with an entire list, including a custom list datatype. Only CP-SAT uses this fixed-list specializer; the other backends expand their ordinary expression grammars. For example, {xs:(List Bool) | List.size xs = 50} fixes the constructor spine and leaves 50 Boolean decisions for the solver. Integer and fixed-point Float elements use the same bounds and precision as scalar holes.

The datatype must have an empty constructor and a two-field constructor with one scalar element and one recursive tail, in either order. The length must be a literal equality in the hole’s refinement. The backend recognizes length by the constructor equations length empty = 0 and length node = length tail + 1, so custom measure names work too. Lengths from 0 through 1000 are supported; variable-length lists and nested lists require another backend.

Constructor relations and whole-list measure refinements constrain the symbolic model. Every completed list is also checked against the original program’s type and hard specifications. Constraints outside symbolic translation use the backend’s validated assignment search.

The 50-item knapsack example uses @maximize for value and a refined Boolean list for logical weight. Its synthesis body is simply ?solution; list nodes contain only a Boolean and a tail, while item weights and values live in arrays.

Choosing a Synthesizer

Synthesizer Strategy Best for
gp Native linear-genome GP Complex expressions, multi-objective problems
random_search Native random walks over the core grammar Baselines, small search spaces
enumerative Native BFS over the core grammar Small holes, tight type constraints
rl_mcts Policy/value-guided Monte-Carlo grammar search Refinement-only synthesis, learned search experiments
amaze Stdlib-trained additions and rank-cost grammar optimization First-order Int/Bool synthesis with an immutable profile
synquid Type-directed enumeration Type-rich problems, correctness-only goals
boolean_bounded Constraint solving Boolean CNF within a source-declared clause bound
smt SMT solving Arithmetic / boolean constraints on base types
decision_tree Data-driven Regression from input–output examples
noisy Regularized native search with adaptive sampling Scalar examples with outliers or contradictory observations
llm LLM generation Problems that are easy to describe in natural language
tdsyn / tdsyn_enumerative Type-directed BFS with SMT leaves Tightly-typed holes where leaves reduce to arithmetic
tdsyn_random Type-directed random walks with SMT leaves Wider, shallower term spaces than tdsyn
tdsyn_backward Backward-only type-directed BFS Complete synthesis with the same specification support as tdsyn
backward_abs / backward_lit / backward_close / backward_app / backward_if Single backward step (no search) Applying one backward construction at a time
forward_close Single forward step (no search) Closing a goal with a variable already in scope
forward_let_app / forward_let_if / forward_let_tapp / forward_let_abs / forward_let_tabs Single forward step (no search) Demonstrating how forward reasoning grows the scope with let bindings
tactics Random tactic walks (Lean-style) Goals whose proof decomposes into tactic steps
lta Component-based via Liquid Tree Automata Reusing a library of refined functions to assemble a term

Benchmarks

The Hakank common CP starter suite contains 25 standalone, finite constraint and optimization models drawn from the archived catalogue. Run these with -s ortools; decisions remain numeric holes, with constraints expressed through comparisons, Boolean combinations, and numeric conditionals. The suite includes pinned provenance, explicit instance sizes, objective targets, regeneration tooling, and independent checks of synthesized assignments.

For the catalogue of synthesis and verification benchmarks bundled with Aeon — where they live, how many there are, and how to run them — see benchmarks.md.

Satisfaction backends with numerical objectives expose all explored nondominated solutions as backend.pareto_front and through SynthesisUI.register_front; the hole-filling API selects one member. See the specification support matrix for acceptance policies, limits, and the distinction between objective-guided search and external Pareto enumeration.