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 gp my_program.ae

The --budget flag sets the time limit in seconds (default: 60).

Available Synthesizers

gp — Genetic Programming (default)

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.

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.

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)

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

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.