Autonomous Algorithm Discovery Lab

algolab is a modular, plugin-based system that invents, formally verifies, and benchmarks algorithms: search strategies mutate and recombine programs, a three-stage verification pipeline separates correct candidates from broken ones, and a benchmark harness measures whether discoveries are actually faster.

Install

pip install algolab
# Or for development:
pip install -e .[dev,server,verify]

Quick Start

# List available domains / search strategies
algolab domain list
algolab search list

# Run a discovery campaign (evolutionary search over LoopIR programs)
algolab run --domain sorting --search evolutionary --generations 50 --population 20

# Add the formal verification stage: Z3 proves correctness for ALL inputs
# of the bounded domain; refuted candidates come back with counterexamples
algolab run --domain sorting --generations 20 --population 10 --verify property_test,differential,formal

# Benchmark candidate code against domain references
algolab bench best_candidate.py --domain sorting --sizes 1000,10000

# Start the web UI + REST/WebSocket API
algolab serve            # http://127.0.0.1:8080

Architecture

• Core: plugin kernel with entry-point discovery (importlib.metadata) plus register_builtin_plugins() shared by CLI and server
• Domains:
  • sorting — classic comparison sorts as discovery targets
  • graph — Dijkstra, A*, Prim/Kruskal MST, Bellman-Ford
  • linear_algebra — GEMM, LU, QR, SVD
  • query_opt — join-order selection under a System-R cardinality model, with Selinger DP ground truth
  • ml_kernels — quantized integer inference kernels (relu, argmax, matmul, conv1d, gemv), bit-exact for verification
• Representations: loopir (executable DSL), neural (AST-feature encoder
  • online ridge value model for score-guided search), llm_prompt (structured prompts, response parsing, OpenAI-compatible provider)
• Search: evolutionary, MCTS with neural guidance, LLM-guided with critique loop, portfolio controller (UCB1 bandit over strategies)
• Verification pipeline:
  1. property testing — Hypothesis properties (permutation, sortedness)
  2. differential — bit-for-bit agreement with reference implementations
  3. formal — Z3 bounded proofs over the whole input domain: sortedness + permutation proved symbolically for every array of a given length/value-range, with SMT-LIB2 certificates and concrete counterexamples for refuted candidates. Unsupported constructs are reported inconclusive, never passing.
• Executors: local subprocess sandbox, Ray for multi-node/GPU fleets
• Benchmarks: statistical microbench (median/stdev/geometric-mean speedup) and hardware counters via perf/NVML
• Server/UI: FastAPI REST + WebSocket API broadcasting live campaign events; React/TypeScript dashboard (webui/) with dashboard, campaign, candidate explorer, benchmark and settings pages

Extending

Create a plugin package with entry points:

[project.entry-points."algolab.domains"]
my_domain = "my_package:MyDomain"

pip install algolab-mydomain auto-registers it next to the built-ins.

See docs/superpowers/specs/2026-08-20-algorithm-discovery-lab-design.md for the full design document.

Tests

python -m pytest -q      # ~100 tests incl. Z3-backed formal proofs