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.

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.

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.

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.

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/synthesis/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/synthesis/rl_mcts_training.smt2 --output /tmp/aeon-rl-data
python -m aeon.synthesis.modules.rl_mcts train \
  examples/synthesis/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.

Unlike the numerical search backends, rl_mcts currently supports correctness specifications only and rejects objective decorators (including property-fitness objectives). 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.

synquid — Type-Directed Synthesis

This backend implements a Synquid-style enumerator: type-directed decomposition, Q-aware conditional guards (same finite qualifier set as Horn predicate abstraction), and search ordering heuristics.

Search. Default synquid_search: "size_merge" uses a lazy min-heap over synthesis levels (term_size, then shallower level) via aeon.synthesis.modules.synquid.search.iter_candidates_size_then_level. synquid_search: "iterative_deepening" restores strict “exhaust level L before L+1”. Within each level, candidates are sorted by term_size. Tunables: synquid_max_level, synquid_seed_levels, synquid_max_candidates (hard cap on candidates tried per hole, both search modes); optional synquid_typecheck_candidate_first runs check_type on the candidate in the hole context before full-program validation.

Enumeration. Level 0 supports Bool, Int, Float, String, Unit (small fixed literal sets where applicable), variables matching the goal, and type variables satisfied from the typing context. Arrow goals at level 0 only enumerate matching functions in scope (no ill-scoped literal fall-through). At level ≥ 1 the enumerator emits λ-abstractions (Abstraction), optionally annotated when the goal is a refinement over an arrow, plus applications from the typing context. if branches try quaternary, ternary, binary, then unary relational guards built from Q, then plain boolean enumeration. Function applications are pruned when the callee’s result type does not match the goal (spine decomposition); refined argument types are preserved on the spine. aeon.synthesis.modules.synquid.modular exposes application_subgoal_types, check_hole_term, qualifier_atoms, and modular VCs via build_modular_vc / ModularVC (re-exported from aeon.typechecking.partial_vc); aeon.synthesis.modules.synquid.build re-exports the same surface. A modular VC is the Constraint from check before entailment, so callers can inspect it, pass a custom Q to solve, or use explain_failures — distinct from a single check_type boolean.

Fitness. If the hole has no goals metadata, the first fully valid candidate is returned.

Not in scope (vs the PLDI Synquid paper or ideal liquid tooling): MUSFIX-style weakest-guard abduction (only bounded &&-products over Q); no core-level match / fix (those live in sugar + elaboration); Horn lifting still skips polymorphic and refinement-polymorphic value binders (see comments in aeon/typechecking/entailment.py). Modular VCs still rely on check internally, which calls check_type in a few places (e.g. if conditions) rather than returning those as nested VC objects. For further background on Q and refinement Horn encodings, see Jhala & Vazou, Refinement Types: A Tutorial.

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. This is an example-driven backend, not an optimizer for arbitrary fitness objectives; unsupported goals/types are reported explicitly. Search is bounded by adjusted weight 40, 20,000 distinct values, and the time budget. See examples, training instructions, and differences from the paper.

decision_tree — Decision Tree Regressor

Fits a scikit-learn DecisionTreeRegressor to training data provided via the @csv_data or @csv_file decorators, then converts the resulting tree into a nested if-then-else Aeon term. This synthesizer is data-driven: it learns a piecewise-constant function from examples rather than searching a grammar.

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

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 @prompt("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 the @prompt decorator to provide a natural-language description of the desired behaviour.

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.

Search is breadth-first over partial ASTs (capped by a depth bound). When the worklist is exhausted, the search restarts with a shuffled expansion order so that subsequent iterations explore different term shapes until the budget runs out. If no optimization goals are present, the first valid term is returned; otherwise the best-scoring term across iterations wins.

tdsyn_random — Type-Directed Synthesis (Random Walks)

Same expansion rules as tdsyn, but instead of a BFS worklist it performs independent random walks from the initial hole. Each walk repeatedly picks a random open hole and a random candidate expansion, falling back to SMT completion when only base-type leaves remain. Lighter than the BFS mode, useful when the term space is wide and shallow.

tdsyn_backward — Backward Step (Combined)

Demonstrative single-step backend: applies the backward action exactly once to the hole. Candidates are derived from the hole’s expected type (literals, variables and function applications whose result type matches, abstractions, if-then-else). Returns the first complete candidate that typechecks, or otherwise the first partial expansion with fresh ?<fun>_goal_<i> subgoal holes, so the step can be applied again. No search is performed — use tdsyn for actual synthesis.

This is the union of the granular backward_* steps; use those to apply one backward construction at a time.

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).

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
synquid Type-directed enumeration Type-rich problems, correctness-only goals
smt SMT solving Arithmetic / boolean constraints on base types
decision_tree Data-driven Regression from input–output examples
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 Single combined backward step (no search) Demonstrating how the backward action decomposes a goal
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.