Synthesize formally-verified RL policies. Together.
Synthex evaluates discrete boolean predicate boundaries against Gymnasium and MuJoCo physics — embarrassingly parallel work that a single laptop will never finish for Humanoid. Donate a few cores to a friend and tackle environments deep RL needs GPU clusters for.
Install — one line, any laptop
curl -fsSL https://synthex.fit/install | shgit clone) and runs one
Python port per CPU core. First build ~3–5 min; subsequent
re-runs reuse the layer cache.
No token, no signup, no questions asked. Workers are anonymous; results are reconciled at the experiment layer.
Live cluster
Top contributors (all-time)
Workers that pick a name show up here. Choose any handle at install
time, or type anonymous to pool credit
with the rest. Aggregated by display name, so a single human running
multiple machines under alice shows up
as one row.
| # | contributor | candidates | chunks | experiments |
|---|---|---|---|---|
| loading… | ||||
What is this thing?
Coinductive Symmetric Homomorphism Reinforcement Learning (CSHRL) synthesizes RL policies as predicate programs: decision trees over boolean tests of state features. Each candidate is a tiny program; scoring it requires running the environment.
The hub manages a CEGAR loop, dishing out chunks of candidates to whoever's connected. Workers run them, send back reward + survival counts, and the hub picks the winner. Repeat until the policy is verifiably correct.
Donating compute
The one-liner above is all you need. It will:
- verify Docker is installed (and tell you where to get it if not),
- build the worker image directly from
github.com/doctorcorral/synthex-hubusing Docker's remote-build feature (docker build https://….git#main:worker) — no registry, no clone, - start a worker bound to
SERVER_URL=https://synthex.fit/api, - configure a pool of one Python interpreter per CPU core
(override with
POOL_SIZE=N).
To stop:
docker stop synthex-worker
docker rm synthex-workerTo update to the latest worker code, just re-run the
one-liner — it rebuilds from the tip of main
(Docker layer cache makes re-runs fast). Operators who'd rather
pre-build and host on a registry can override with
IMAGE=ghcr.io/….
Starting your own run
Workers donate compute; masters drive the synthesis loop. Today that lives in the synthex repo:
git clone https://github.com/doctorcorral/synthex
cd synthex
mix deps.get
SYNTHEX_HUB_URL=https://synthex.fit/api \
SYNTHEX_HUB_TOKEN=<token> \
mix run experiments/humanoid/round-1.exs
The master script chunks candidates, ships them to the hub,
polls for results. There's a Python smoke-test entrypoint at
test_master.py in
synthex-hub
if you'd rather see something runnable in 30 seconds.
Hidden parts
- Server — Elixir + Bandit + Postgres + Oban on Fly.io. Persistent chunk queue, Lifeline rescue of stale leases, idempotent submission, bearer-token auth.
- Worker — Elixir + Broadway pipeline. Producer pulls chunks, processors fan out across N Python ports, aggregator submits results. Per-port crash isolation; graceful drain on shutdown.
- Oracle — persistent Python interpreters running Gymnasium / MuJoCo, talking JSON-over-stdio with their Elixir parents.