Explore

Run an explorer on hidden worlds, have the kernel check its results, and compare a cold run with a library run.

Run an explorer

Terminal

python3 -m slean explore --explorer datafit --lean

This runs the exact data-fitting explorer on the suite of hidden worlds. Every proposal goes through the verifier. With --lean, every result is exported to a Lean module that the kernel checks at the end. The run is saved in a runs/ directory, with its verdicts.

The five explorers

Explorer What it does

random proposes densities at random. It is the floor.

datafit exact linear algebra on simulated transitions.

library exact data fitting plus reuse of laws from related worlds.

oracle knows the theory and solves the continuity equations. It is the ceiling.

llm a language model that reads the rules and the verifier’s feedback.

Explorer	What it does
`random`	proposes densities at random. It is the floor.
`datafit`	exact linear algebra on simulated transitions.
`library`	exact data fitting plus reuse of laws from related worlds.
`oracle`	knows the theory and solves the continuity equations. It is the ceiling.
`llm`	a language model that reads the rules and the verifier’s feedback.

Useful options

--budget: the number of proposals allowed, 300 by default.
--suite-seed: the seed that generates the suite of worlds, 7 by default.
--suite eca: the well-known elementary automata, for calibration, instead of the hidden suite.
--llm-command: the command that reads a prompt on standard input, for the llm explorer.

Cold, then with the library

Terminal

python3 -m slean transfer --explorer library

The transfer protocol scores the held-out half of the suite twice at the same budget: cold, then with the library built on the seen half. It prints both results. See Measuring a discovery for how to read these numbers.