diff --git a/.github/tickets/m4/m4-p2-2-superopt.md b/.github/tickets/m4/m4-p2-2-superopt.md index a4e277b..fefb948 100644 --- a/.github/tickets/m4/m4-p2-2-superopt.md +++ b/.github/tickets/m4/m4-p2-2-superopt.md @@ -18,6 +18,7 @@ Its responsibilities are: * A map keyed by neurons and latency, scored by `HardwareCost`, holding only verified networks * Output: the best network per cell, its cost, the step it was verified to, and its export as Verilog and NIR when it fits the profile +The command should extend the `superopt` command and part superoptimiser built for library parts with `--spec`, because a contract is already a spec with cases, and a second superoptimiser would drift from the first. Every seed should pass the verifier before the search starts, because a wrong seed would make every descendant compete against a wrong reference. A network should enter the map only after passing the verifier's held-out step, and the bounded proof should run on each new elite once, because proofs on every candidate cost too much and an unproven elite must not be reported. Evaluations should be charged to the shared evaluation budget in the same units as the other searches, because the synthesis arm is compared on the same budget. diff --git a/.github/tickets/m4/m4-p2-4-library-superopt.md b/.github/tickets/m4/m4-p2-4-library-superopt.md new file mode 100644 index 0000000..991072f --- /dev/null +++ b/.github/tickets/m4/m4-p2-4-library-superopt.md @@ -0,0 +1,40 @@ +--- +number: 143 +title: Superoptimise kept parts against their contracts +milestone: M4 +labels: + - area: search + - area: cli +parent: m4-p2-superoptimisation +--- + +The library already holds correct parts (evolved delays and sequencers, and hand-built count parts that evolution has not found), and each has a contract to check against, but the only time a part is made smaller is the short shrink when it is first found, and nothing ever makes one faster. +We want a `superopt` command that takes kept or hand-built parts as seeds, searches for smaller and faster networks that still meet the part's contract, and saves an improvement to the library only when it is verified and proven at least as far as the seed. + +Its responsibilities are: +* Seeds, picked by option: `--part FILE`, `--only NAMES` from the library folder, or `--hand-built` for the hand-built parts, each verified before the search starts +* The search: the shrink search's edits and admission, with a MAP-Elites map keyed by neurons and latency, scored by `HardwareCost` and then latency +* Proof: `BoundedCheck` on each new elite once, to at least the bound the seed was proven to +* Write-back: replacing the library's part when the new one is no worse on cost and latency and better on one, with its origin saying which part it was superoptimised from +* A report per seed: cost and latency before and after, the bound proven, and the evaluations spent + +A seed that fails its contract should be refused with the failing case, because every descendant would be compared against a wrong reference. +A part should replace a kept one only when it is proven to at least the kept part's bound, because a smaller part that is less proven is not like for like. +Under the hardware profile, seeds and edits should stay inside the profile, and a profile part should be saved to the profile library only, because conforming can change behaviour and the two libraries hold different rule forms. +Latency should be an objective beside cost, because a part that is just as small but answers sooner makes every composition built from it faster. +Evaluations should be charged to the shared evaluation budget, because spec superoptimisation and the synthesis arm will be compared in the same units. +The command should be one `Command` with a registry line and a menu item on the library parts page, because every command is run the same way from the menu and the command line. +This command should be the one that later takes `--spec`, because a contract is already a spec with cases and a superoptimiser for specs only adds seeds and verification steps to it. + +Where: new `Search/PartSuperoptimiser.cs`, new `Application/SuperoptService.cs`, new `Cli/Commands/SuperoptCommand.cs`; `Search/ShrinkSearch.cs`, `Search/PartSearch.cs`, `Search/Algorithms/MapElites.cs`, `Specs/Verification/Verifier.cs`, `Specs/Verification/BoundedCheck.cs`, `Specs/Parts/HardwareCost.cs`, `Specs/Parts/LibraryPart.cs`, `Specs/Parts/HandBuiltParts.cs`, `Specs/Parts/ReferenceParts.cs`, `Specs/Parts/ModuleLibrary.cs`, `Application/PartLibraries.cs`, `Storage/PartLibraryFiles.cs`, `Cli/Commands/CommandRegistry.cs`, `Cli/Menus/MainMenu.cs`. + +Done when: +- [ ] `superopt --hand-built` returns, for at least three hand-built count parts, a part with fewer neurons or a lower latency than its seed, verified and proven to the seed's bound, on at least 8 of 10 seeds +- [ ] `superopt --only "delay 2,sequencer 2"` on `parts/` and `parts-profile/` never saves a part that is worse than the one kept +- [ ] A seed that fails its contract is refused with the failing case +- [ ] A saved part's origin names the part it was superoptimised from, and the `parts` command shows it +- [ ] RESEARCH.md has a table of every seed's cost, latency and bound before and after +- [ ] The README command table and menu list `superopt` +- [ ] `dotnet test` green + +Read first: RESEARCH.md "Spec to verified circuit", "Proving contracts", README "Compile, then shrink" diff --git a/.github/tickets/m4/m4-p2-5-speed-and-size.md b/.github/tickets/m4/m4-p2-5-speed-and-size.md new file mode 100644 index 0000000..2178589 --- /dev/null +++ b/.github/tickets/m4/m4-p2-5-speed-and-size.md @@ -0,0 +1,32 @@ +--- +number: 144 +title: Keep the smallest and the fastest part for each contract +milestone: M4 +labels: + - area: modules + - area: search +parent: m4-p2-superoptimisation +--- + +The library keeps one part per contract and replaces it only with a cheaper one of the same behaviour, so a part that is larger but answers in fewer steps is thrown away, even though some compositions are limited by time and not by size. +We want the library to keep, for each contract, every part on the front of hardware cost against latency, with composition and superoptimisation able to ask for the smallest or the fastest. + +Its responsibilities are: +* The front: a new part joins when no kept part is at least as cheap and at least as fast, and kept parts it beats on both leave +* Files: one file per part on the front, named so the smallest keeps today's file name +* Choosing: compositions take the smallest by default, and a `--prefer small|fast` setting picks otherwise +* Showing the front in the `parts` command + +The smallest part should keep today's file name, because saved libraries, exports and tests name parts by it. +Parts on the front should be compared by the same `HardwareCost` order the shrink search uses, because two orders would disagree on which part is smaller. +The front should be small, because a part that is a step faster and a neuron larger is rarely worth a file; parts should join only when they are faster by at least one step or smaller by at least one neuron. + +Where: `Specs/Parts/ModuleLibrary.cs`, `Specs/Parts/LibraryPart.cs`, `Specs/Parts/HardwareCost.cs`, `Storage/PartLibraryFiles.cs`, `Application/PartLibraries.cs`, `Application/LibraryView.cs`, `Search/CompositionSpace.cs`, `Application/Settings.cs`. + +Done when: +- [ ] A library given a smaller-but-slower and a larger-but-faster part for one contract keeps both, and drops a third part beaten by one of them on both +- [ ] A library saved before this change loads unchanged, with each part as the smallest on its front +- [ ] `parts --only NAME` lists the front, and composition with `--prefer fast` uses the fastest part +- [ ] `dotnet test` green + +Read first: RESEARCH.md "Spec to verified circuit", "A verified spiking parts library, and search beyond evolution" diff --git a/.github/tickets/m4/m4-p2-6-rebuild-composites.md b/.github/tickets/m4/m4-p2-6-rebuild-composites.md new file mode 100644 index 0000000..8859e32 --- /dev/null +++ b/.github/tickets/m4/m4-p2-6-rebuild-composites.md @@ -0,0 +1,30 @@ +--- +number: 145 +title: Rebuild composite parts when a part they use gets smaller +milestone: M4 +labels: + - area: modules +parent: m4-p2-superoptimisation +--- + +A promoted part (the add loop, or a promoted composition) is saved with its recipe, but its network is the flattened one from when it was promoted, so a smaller copy of one of its children later does not make it smaller. +We want superoptimising or replacing a part to rebuild every composite part whose recipe uses it, verify the rebuilt part on its contract, prove it to its old bound, and keep it when it is cheaper. + +Its responsibilities are: +* Finding the composites whose recipes name the replaced part, nested ones included, innermost first +* Rebuilding each from its recipe with the new child, and its glue unchanged +* Verifying and proving the rebuilt part, keeping it only when it passes and is cheaper or faster +* Logging each rebuild: the part, the child that changed, the cost before and after, and the result + +A rebuilt part should be verified again even though its children are, because a child with a different latency can break timing the glue relies on. +A rebuild that fails should keep the old composite and say which check failed, because the old one is still correct. +Rebuilding should be offered after the superoptimiser saves a part and on its own as `superopt --rebuild`, because a library edited by hand needs it too. + +Where: `Specs/Parts/PartRecipe.cs`, `Specs/Parts/Composition.cs`, `Specs/Parts/PartWiring.cs`, `Search/Modules/Promotion.cs`, `Specs/Parts/ModuleLibrary.cs`, `Specs/Verification/Verifier.cs`, `Specs/Verification/BoundedCheck.cs`, `Application/PartLibraries.cs`. + +Done when: +- [ ] Replacing the register with a smaller verified register rebuilds the add loop, which passes its contract to its old bound with fewer neurons +- [ ] A child that breaks a composite's timing leaves the old composite kept and logs the failing check +- [ ] `dotnet test` green + +Read first: RESEARCH.md "Composing modules into machines", "Proving contracts" diff --git a/.github/tickets/m4/m4-p2-7-saved-networks.md b/.github/tickets/m4/m4-p2-7-saved-networks.md new file mode 100644 index 0000000..ef8c2d9 --- /dev/null +++ b/.github/tickets/m4/m4-p2-7-saved-networks.md @@ -0,0 +1,32 @@ +--- +number: 146 +title: Superoptimise a saved network on its task, with held-out values +milestone: M4 +labels: + - area: search + - area: cli +parent: m4-p2-superoptimisation +--- + +Runs of `evolve`, `compose` and `compile` save correct networks for tasks with no contract (Fibonacci, the natural numbers), and shrinking them is scored only on the values the task checks, so a smaller network can be right on those and wrong just past them. +We want `superopt --network FILE --task NAME` to superoptimise a saved network on its task, admitting a network only when it passes the task's values and a set of held-out values the search never scored. + +Its responsibilities are: +* Loading the network and refusing it, with the first wrong value, when it does not solve the task +* Held-out values: for sequence and generator tasks, the values after the last one scored; for other tasks, inputs the task does not check +* The search: the same superoptimiser as for parts, with the task's check and the held-out values as admission +* Output: the smallest and the fastest admitted networks, saved to a run folder as the compile run's files are + +Held-out values should never be scored during the search, because a search that sees them overfits to them as it does to the training values. +A task with no held-out values should be refused with a message saying so, because an unchecked shrink is what this ticket exists to stop. +The run should report how many candidates passed training but failed held-out values, because that is the overfitting rate the spec route is meant to remove. + +Where: `Search/ShrinkSearch.cs`, `Application/CompileService.cs`, `Application/NetworkRunService.cs`, `Application/RunFolders.cs`, `Storage/NetworkFiles.cs`, `Specs/Tasks/SequenceTask.cs`, `Specs/Tasks/GeneratorTask.cs`, `Search/Benchmarking/TaskSuite.cs`, the superoptimiser from this epic. + +Done when: +- [ ] The compiled Fibonacci network from a `compile` run shrinks to at most 10 neurons and gives the next 4 values past the ones it was scored on +- [ ] A network that fails its task is refused with the first wrong value +- [ ] The run reports how many candidates failed only the held-out values +- [ ] `dotnet test` green + +Read first: RESEARCH.md "Spec to verified circuit", README "Compile, then shrink" diff --git a/.github/tickets/m4/m4-p2-superoptimisation.md b/.github/tickets/m4/m4-p2-superoptimisation.md index b6c71fc..eae7625 100644 --- a/.github/tickets/m4/m4-p2-superoptimisation.md +++ b/.github/tickets/m4/m4-p2-superoptimisation.md @@ -13,12 +13,14 @@ Its responsibilities are: * Verification steps for a spec: training cases, held-out cases, a bounded proof, and counterexamples fed back * The superoptimiser: seeds, edits, a cost map, and re-verification of every elite * Synthesis from the same spec on the same budget, as the comparison arm +* Superoptimising what is already solved: kept and hand-built parts against their contracts, the composite parts built from them, and saved networks against their tasks with held-out values +* Keeping the smallest and the fastest part for each contract Correctness should be a hard constraint, not a weighted term, because a smaller network that is wrong on one held-out case is not an improvement, and weighting would trade them. Cost should be `HardwareCost` under the hardware profile, because results that only hold for regex rules do not transfer to integrate-and-fire chips. The superoptimiser should take its search through the search interface from M2.5, with evolution as the first method, because exact synthesis, windowed improvement and rewrites in M5 are further methods for the same command. -Order: after the counterexample loop in M3 Part 3 and the compiled parts in M3 Part 1; verification steps; superoptimiser; synthesis comparison. +Order: parts first, since they need only what exists today: superoptimise kept parts; keep the smallest and the fastest; rebuild composites; saved networks on their tasks. Then, after the counterexample loop in M3 Part 3 and the compiled parts in M3 Part 1: verification steps; the superoptimiser for specs; synthesis comparison. Done when: `superopt` on the add and multiply specs, seeded from compiled networks, returns networks smaller than their seeds that pass held-out cases and a bounded proof, and the synthesis arm's results on the same budget are reported next to them. diff --git a/README.md b/README.md index fc6ec3f..66685eb 100644 --- a/README.md +++ b/README.md @@ -36,56 +36,67 @@ dotnet tool install --global --add-source ./nupkg SNP_Evolution To remove the command, run `dotnet tool uninstall --global SNP_Evolution`. Evolved networks are saved under the folder you run the command from. -## Using the GUI +## Using the menu -Move with the arrow keys and press Enter to select, or press an option's number. ESC, Backspace or the left arrow goes back a level. Every submenu stays open until you leave it. The top of each screen shows the current task, search settings and simulation settings. +Run the program with no command (`dotnet run --project Cli`, `snp-evolution`, or by double-clicking the built executable on Windows) to open the menu. Move with the arrow keys and press Enter to select, or press an option's number. ESC, Backspace or the left arrow goes back a level. Every page stays open until you leave it. The top of each screen shows the current task, search settings and simulation settings. + +The menu and the [commands](#commands) are one program and share their code: every menu entry that runs something runs one of the commands below, the same way it runs from the command line. Choosing an entry opens the command's form: + +- **Run** parses the form as a command line and runs the command. The form shows that line, `$ snp-evolution ...`, so the same run can be scripted. It lists the form's options and every setting the command takes whose menu value is not the default. While it runs, ESC stops it early: each search finishes the generation it is on and keeps its best so far, a command running several searches or proofs (evolve-parts, verify, benchmark, reach) starts no more, and the command reports what it had. A run that has printed nothing for 15 seconds says it is still working. +- The command's own options follow, such as `--target`, `--seed` or `--part`. Pick one to type its value, or to choose from its values. Leave a value empty to take the option off. Some entries fill options from the settings, such as the selected target or task. +- Then a page for each group of settings the command takes (Evolution, Search, Simulation, Benchmark). Settings changed on a form apply to that command's runs only. Settings changed in **Settings** apply to every run. + +Commands start from the menu's settings where the command line starts from the defaults. The pages: - **Evolve a system** - - *Match a target*: type the output you want and a maximum number of generations (1000 if left empty), then evolve a network for it from scratch. A target is one of three kinds: + - *Match the target* or *For the task*: `evolve` for the task chosen in Settings > Evolution, either a target or a suite task. A target is one of three kinds: - **Set**: the numbers a run can produce, in any order, e.g. `2,4,6,8`. Each run gives one number: the steps between the output neuron's first two spikes. - **Sequence**: the gaps between successive output spikes, in order and with repeats, e.g. `1,1,2,3,5,8,13`. - **Binary word**: the output spike train step by step, 1 for a spike, e.g. `001001001001`. - - *For the selected task*: evolve from scratch for the task chosen in Settings > Evolution: the target or a suite task. - - *Starting from the natural numbers or even numbers network*: evolve a hand-designed network towards the target. To evolve only its rules, as in the original paper, first pick a "rule expressions only" algorithm in Settings > Evolution. - - *Suggest settings*: show what the advisor recommends for the selected task, apply it if you agree, and optionally run a quick pilot that picks the algorithm. *Match a target* does this before every run. - - *Compile a target, then shrink it*: type a sequence or set target, then build a network that is correct by construction and evolve it smaller (see [Compile, then shrink](#compile-then-shrink)). For a set you can give a register program file, or leave it empty to evolve one. Leave the shrink generations empty for 300, or enter 0 to only compile. - - *Evolve the first library parts*: run `evolve-parts` (see [Evolving library parts](#evolving-library-parts)) with a seed you give, 1 if left empty. - - *Redo a saved run*: after a run you can save it under a name. Saved runs can be run again as they were, have their settings loaded to change first, or be deleted. -- **Run a network**: run the natural numbers or even numbers network, or import one from a JSON file. -- **Benchmark**: run every algorithm on the task suite, or find the best algorithm for the selected task. + - *Starting from the natural numbers or even numbers network*: `evolve --start natural` or `--start even`, which evolves a hand-designed network towards the target. To evolve only its rules, as in the original paper, pick a "rule expressions only" algorithm. + - *Suggest settings*: `advise` for the selected task, then an offer to apply the suggestions to the settings. To apply them and evolve in one go, set `--advise on` on the evolve form; `--pilot on` picks the algorithm with a quick pilot. + - *Compile a target, then shrink it*: `compile` (see [Compile, then shrink](#compile-then-shrink)). + - *Compare setups on a target*: `reach`. + - *Redo a saved run*: after an evolve run you can save it under a name. Saved runs can be run again as they were, have their settings loaded to change first, or be deleted. +- **Library parts**: `evolve-parts` (see [Evolving library parts](#evolving-library-parts)), `compose` for a suite task, `verify`, and `parts`. *Browse the kept parts* lists the parts in the library folder; choosing one shows it in full. +- **Run a network**: `run` on the natural numbers or even numbers network, or on a saved network file. +- **Export**: `export-verilog`, `export-nir` and `export-uppaal` (see [Exporting to hardware](#exporting-to-hardware)). +- **Benchmark**: `benchmark`, which also saves the table to a run folder; `select`, which offers to use the winner from then on; and the `tasks` and `algorithms` lists. - **Settings**: grouped into: - **Evolution**: task, target, fitness function, algorithm, population, mutation rate, generations, maximum neurons and experimental rules. - - **Search**: iterative evolution and its stages, stagnation recovery, genome limits (delay, spikes produced, initial spikes, duplicate neurons), lexicase parents, modules (build from modules, freeze, triggered, incubation, and module files that start the library), and composition search (part library folder, part copies, glue, proposing parts when stalled, and starting from the hand-built parts). - - **Simulation**: engine, steps, runs per network, rule form and output timing. - - **Benchmarks**. + - **Search**: iterative evolution and its stages, stagnation recovery, genome limits (delay, spikes produced, initial spikes, duplicate neurons), lexicase parents, modules (build from modules, freeze, triggered, incubation, and module files that start the library), the evaluations per library part, and composition search (part library folder, part copies, glue, proposing parts when stalled, and starting from the hand-built parts). + - **Simulation**: engine, steps, runs per network, rule form, output timing and the hardware profile. + - **Benchmark**: seeds, evaluations per run and population. - *Reset to defaults* restores the default configuration. + *Reset to defaults* restores the default configuration. Every setting is also an option of the commands that use it, so a run set up in the menu can be repeated from a script. Sequence and binary targets have some limits: - Only a network that gives the output on every sampled run solves the target. Spike trains are always sampled, even on the exhaustive engine. - Runs are lengthened automatically to fit the whole target. - Small SN P systems produce spike trains that eventually repeat. An evolved network matches the numbers you typed but need not continue the pattern after them. For example, one evolved network for `1,1,2,3,5,8,13` continued with `6,8`. -- The default algorithm, MAP-Elites, evolves structure as well as rules. If you pick a rule-only algorithm, the menu offers to switch back before evolving from scratch, since a random network's structure would never change. Long or irregular targets need a larger population than the default. +- The default algorithm, MAP-Elites, evolves structure as well as rules. If you pick a rule-only algorithm for a run from scratch, `evolve` warns that a random network's structure never changes. Long or irregular targets need a larger population than the default. ## Commands -Every menu run also runs without the menu, from scripts. Each command declares its options, and an unknown option, a missing value or a value the option cannot take is refused with a message naming it. Commands exit with 0 on success, 1 for a bad command line or input they cannot use, 2 when a run solved nothing or a proof found a counterexample, and 3 when an outside tool's check differs from our engine. Options in brackets are optional; `NAME` matches any task, search or contract whose name contains it, ignoring case, unless one name is exactly `NAME`. +Every menu run is one of these commands, so it also runs without the menu, from scripts. Each command declares its options, and an unknown option, a missing value or a value the option cannot take is refused with a message naming it. Commands exit with 0 on success, 1 for a bad command line or input they cannot use, 2 when a run solved nothing or a proof found a counterexample, and 3 when an outside tool's check differs from our engine. Options in brackets are optional; `NAME` matches any task, search or contract whose name contains it, ignoring case, unless one name is exactly `NAME`. | Command | What it does | Options | |---|---|---| -| `evolve` | Evolves a network from scratch for a target and saves the run; exits with 2 when no network solved it. | `--target VALUES` `[--kind set\|sequence\|binary]` `[--seed N]` `[--advise on\|off]` `[--pilot on\|off]` `[--generations N]` `[--population N]` `[--neurons N]` `[--patience N]` `[--iterative on\|off]` `[--lexicase on\|off]` `[--profile hardware\|none]` `[--modules on\|off]` `[--freeze on\|off]` `[--triggered on\|off]` `[--incubate N]` `[--evaluations N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` `[--propose on\|off]` `[--proposal-budget N]` `[--max-parts N]` `[--glue N]` `[--glue-weight X]` `[--module-files a.json,b.json]` `[--algorithm NAME]` | -| `advise` | Prints the settings the advisor suggests for a target, without evolving. | `--target VALUES` `[--kind set\|sequence\|binary]` `[--generations N]` `[--population N]` `[--neurons N]` `[--patience N]` `[--iterative on\|off]` `[--lexicase on\|off]` `[--profile hardware\|none]` `[--modules on\|off]` `[--freeze on\|off]` `[--triggered on\|off]` `[--incubate N]` `[--evaluations N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` `[--propose on\|off]` `[--proposal-budget N]` `[--max-parts N]` `[--glue N]` `[--glue-weight X]` `[--module-files a.json,b.json]` `[--algorithm NAME]` | +| `evolve` | Evolves a network for a target or a suite task and saves the run; exits with 2 when no network solved it. | `[--target VALUES]` `[--kind set\|sequence\|binary]` `[--task NAME]` `[--start scratch\|natural\|even]` `[--seed N]` `[--advise on\|off]` `[--pilot on\|off]` `[--generations N]` `[--population N]` `[--neurons N]` `[--mutation-rate X]` `[--experimental on\|off]` `[--fitness NAME]` `[--patience N]` `[--recovery on\|off]` `[--iterative on\|off]` `[--first-stage N]` `[--stage-step N]` `[--max-delay N]` `[--max-produce N]` `[--initial-spikes N]` `[--duplicates on\|off]` `[--lexicase on\|off]` `[--profile hardware\|none]` `[--rule-form legacy\|standard\|mixed]` `[--modules on\|off]` `[--freeze on\|off]` `[--triggered on\|off]` `[--incubate N]` `[--evaluations N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` `[--propose on\|off]` `[--proposal-budget N]` `[--max-parts N]` `[--glue N]` `[--glue-weight X]` `[--module-files a.json,b.json]` `[--algorithm NAME]` `[--simulator NAME]` `[--steps N]` `[--repetitions N]` `[--timing legacy\|interval]` | +| `advise` | Prints the settings the advisor suggests for a target or a suite task, without evolving. | `[--target VALUES]` `[--kind set\|sequence\|binary]` `[--task NAME]` `[--generations N]` `[--population N]` `[--neurons N]` `[--mutation-rate X]` `[--experimental on\|off]` `[--fitness NAME]` `[--patience N]` `[--recovery on\|off]` `[--iterative on\|off]` `[--first-stage N]` `[--stage-step N]` `[--max-delay N]` `[--max-produce N]` `[--initial-spikes N]` `[--duplicates on\|off]` `[--lexicase on\|off]` `[--profile hardware\|none]` `[--rule-form legacy\|standard\|mixed]` `[--modules on\|off]` `[--freeze on\|off]` `[--triggered on\|off]` `[--incubate N]` `[--evaluations N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` `[--propose on\|off]` `[--proposal-budget N]` `[--max-parts N]` `[--glue N]` `[--glue-weight X]` `[--module-files a.json,b.json]` `[--algorithm NAME]` `[--simulator NAME]` `[--steps N]` `[--repetitions N]` `[--timing legacy\|interval]` | | `compile` | Compiles a sequence target's recurrence or a set target's register program into a network that is correct by construction, then shrinks it. | `--target VALUES` `[--kind set\|sequence\|binary]` `[--program FILE]` `[--generations N]` `[--lexicase on\|off]` `[--shrink N]` `[--seed N]` `[--population N]` | -| `reach` | Runs each setup on seeds 1 to N with the same budget and compares how far into the target they get. | `--target VALUES` `--evaluations N` `[--kind set\|sequence\|binary]` `[--setups flat,modules,composition]` `[--seeds N]` `[--charge-parts on\|off]` `[--generations N]` `[--population N]` `[--neurons N]` `[--patience N]` `[--iterative on\|off]` `[--lexicase on\|off]` `[--profile hardware\|none]` `[--modules on\|off]` `[--freeze on\|off]` `[--triggered on\|off]` `[--incubate N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` `[--propose on\|off]` `[--proposal-budget N]` `[--max-parts N]` `[--glue N]` `[--glue-weight X]` `[--module-files a.json,b.json]` `[--algorithm NAME]` | -| `evolve-parts` | Evolves, verifies, shrinks and saves a part for each first-part contract the library has no part for, and reports robustness to jitter. | `[--seed N]` `[--budget N]` `[--only "NAME,NAME"]` `[--library DIR]` `[--engine exact\|sampled]` `[--configurations N]` `[--redo on\|off]` `[--profile hardware\|none]` `[--robust J]` | -| `compose` | Composition search for one suite task; a solved contract is promoted to a part and the library saved. | `--task NAME` `[--seed N]` `[--generations N]` `[--population N]` `[--neurons N]` `[--patience N]` `[--iterative on\|off]` `[--lexicase on\|off]` `[--profile hardware\|none]` `[--modules on\|off]` `[--freeze on\|off]` `[--triggered on\|off]` `[--incubate N]` `[--evaluations N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` `[--propose on\|off]` `[--proposal-budget N]` `[--max-parts N]` `[--glue N]` `[--glue-weight X]` `[--module-files a.json,b.json]` `[--algorithm NAME]` | +| `reach` | Runs each setup on seeds 1 to N with the same budget and compares how far into the target they get. | `--target VALUES` `--evaluations N` `[--kind set\|sequence\|binary]` `[--setups flat,modules,composition]` `[--seeds N]` `[--charge-parts on\|off]` `[--generations N]` `[--population N]` `[--neurons N]` `[--mutation-rate X]` `[--experimental on\|off]` `[--fitness NAME]` `[--patience N]` `[--recovery on\|off]` `[--iterative on\|off]` `[--first-stage N]` `[--stage-step N]` `[--max-delay N]` `[--max-produce N]` `[--initial-spikes N]` `[--duplicates on\|off]` `[--lexicase on\|off]` `[--profile hardware\|none]` `[--rule-form legacy\|standard\|mixed]` `[--modules on\|off]` `[--freeze on\|off]` `[--triggered on\|off]` `[--incubate N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` `[--propose on\|off]` `[--proposal-budget N]` `[--max-parts N]` `[--glue N]` `[--glue-weight X]` `[--module-files a.json,b.json]` `[--algorithm NAME]` `[--simulator NAME]` `[--steps N]` `[--repetitions N]` `[--timing legacy\|interval]` | +| `evolve-parts` | Evolves, verifies, shrinks and saves a part for each first-part contract the library has no part for, and reports robustness to jitter. | `[--seed N]` `[--budget N]` `[--only "NAME,NAME"]` `[--library DIR]` `[--engine exact\|sampled]` `[--configurations N]` `[--redo on\|off]` `[--profile hardware\|none]` `[--robust J]` `[--staged on\|off]` | +| `compose` | Composition search for one suite task; a solved contract is promoted to a part and the library saved. | `--task NAME` `[--seed N]` `[--generations N]` `[--population N]` `[--neurons N]` `[--mutation-rate X]` `[--experimental on\|off]` `[--fitness NAME]` `[--patience N]` `[--recovery on\|off]` `[--iterative on\|off]` `[--first-stage N]` `[--stage-step N]` `[--max-delay N]` `[--max-produce N]` `[--initial-spikes N]` `[--duplicates on\|off]` `[--lexicase on\|off]` `[--profile hardware\|none]` `[--rule-form legacy\|standard\|mixed]` `[--modules on\|off]` `[--freeze on\|off]` `[--triggered on\|off]` `[--incubate N]` `[--evaluations N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` `[--propose on\|off]` `[--proposal-budget N]` `[--max-parts N]` `[--glue N]` `[--glue-weight X]` `[--module-files a.json,b.json]` `[--algorithm NAME]` `[--simulator NAME]` `[--steps N]` `[--repetitions N]` `[--timing legacy\|interval]` | | `verify` | Proves each part's contract for every input up to a bound, raised until the time per part runs out, and records it in the part's file. | `[--part FILE]` `[--library DIR]` `[--only "NAME,NAME"]` `[--seconds N]` `[--bound N]` | +| `parts` | Lists the parts kept in the library, or shows each part asked for in full: contract, ports, cost, proof, origin, what it reads on each case and its network. | `[--library DIR]` `[--only "NAME,NAME"]` `[--part FILE]` | | `export-verilog` | Writes a deterministic network as Verilog with a testbench, and co-simulates it under iverilog when installed. | `[--part FILE]` `[--network FILE]` `[--steps N]` `[--out DIR]` `[--check on\|off]` | | `export-nir` | Writes a hardware-profile network for tools/snp_nir.py, which makes the NIR file and co-simulates it in norse. | `[--part FILE]` `[--network FILE]` `[--steps N]` `[--out DIR]` | | `export-uppaal` | Writes a part as Uppaal timed automata with queries for its contract, and model-checks them with verifyta when installed. | `--part FILE` `[--out DIR]` `[--check on\|off]` | | `benchmark` | Runs every matching search on every matching suite task over several seeds, with a budget of evaluations per run, and prints the table. | `[--task NAME]` `[--algorithm NAME]` `[--engine exact\|sampled]` `[--configurations N]` `[--lexicase on\|off]` `[--budget N]` `[--seeds N]` `[--population N]` `[--repetitions N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` | | `select` | Picks the best of the matching searches for one suite task by successive halving. | `--task NAME` `[--algorithm NAME]` `[--engine exact\|sampled]` `[--configurations N]` `[--lexicase on\|off]` `[--budget N]` `[--seeds N]` `[--population N]` `[--repetitions N]` `[--library DIR]` `[--hand-built on\|off\|leaves]` | +| `run` | Runs a saved or reference network and prints the numbers it generated and one run's spike train, or its score on the task when it has inputs. | `--network FILE\|natural\|even` `[--target VALUES]` `[--kind set\|sequence\|binary]` `[--task NAME]` `[--seed N]` `[--simulator NAME]` `[--steps N]` `[--repetitions N]` `[--timing legacy\|interval]` | | `tasks` | Lists the suite tasks. | | | `algorithms` | Lists the searches. | | @@ -101,7 +112,7 @@ When evolving, the console shows the best network after every generation: its ne Sequence and binary lines add "(varies between runs)" when the network is nondeterministic. With the MAP-Elites algorithm, the end of the run also lists the fittest network of each size. -Running a network shows the numbers it generated, one run's spike train with the intervals between its spikes, and how long the run took. For a network with input neurons, it shows its score on the selected task instead of the spike train. Evolved networks are saved to a timestamped folder inside `runs/` at the root of the repository (or of the working directory outside one), named in the message at the end of a run; git ignores it. To load one, choose *Run a network > Import* and give that path, such as `../runs/6234234242322/TargetNet.json` from the `SNP_Evolution` folder. `Test Data/`, `Combined Data/` and `CompositeLowHighGen/` hold earlier runs. +Running a network shows the numbers it generated, one run's spike train with the intervals between its spikes, and how long the run took. For a network with input neurons, it shows its score on the selected task instead of the spike train. Evolved networks are saved to a timestamped folder inside `runs/` at the root of the repository (or of the working directory outside one), named in the message at the end of a run; git ignores it. To run one again, choose *Run a network > A network from a file* and give that path, or run `run --network ../runs/6234234242322/TargetNet.json` from the `SNP_Evolution` folder. `Test Data/`, `Combined Data/` and `CompositeLowHighGen/` hold earlier runs. ## Rule forms @@ -111,7 +122,7 @@ Two rule forms are supported, and one network can mix them: - **Standard** (`E/a^c -> a^p;d`, as in the SN P literature): when the expression matches and the neuron holds at least c spikes, the rule consumes exactly c spikes and sends p along each synapse. A delayed rule closes the neuron for d steps: spikes sent to it in that time are lost, and it fires when it reopens. The notation leaves out `E/` when E only matches a^c, so `aaa -> aa` consumes 3 spikes and sends 2. - **Axonal delays** (`a+ -> a;2 axonal`): either form's delay can instead be axonal, as integrate-and-fire hardware has it. The rule consumes at once, the neuron stays open and can fire again, and its spikes reach the targets d steps later. Only the hardware profile (see [Exporting to hardware](#exporting-to-hardware)) makes these; the Metal engine runs such networks on the CPU. -The *Rule Form* setting (Legacy, Standard or Mixed) picks the form of the rules evolution creates. The *Output Timing* setting picks how the output neuron's spikes become a number. *Legacy* counts every non-spiking step from the start, as the original program did. *Interval* counts the steps between the first two spikes, as the literature does. JSON files gain optional `Consume`, `Produce`, `Axonal` and `IsInput` fields, and older files load as legacy rules. +The *Rule Form* setting (Legacy, Standard or Mixed, `--rule-form`) picks the form of the rules evolution creates. The *Output Timing* setting (`--timing`) picks how the output neuron's spikes become a number. *Legacy* counts every non-spiking step from the start, as the original program did. *Interval* counts the steps between the first two spikes, as the literature does. Standard rules and Interval timing are the defaults, as the parts, compiler and verifier use. To reproduce the original program, pass `--rule-form legacy --timing legacy`, or pick them in Settings > Simulation. The suite's Generate tasks keep Mixed rules and Legacy timing, so benchmarks stay comparable with the original program. JSON files gain optional `Consume`, `Produce`, `Axonal` and `IsInput` fields, and older files load as legacy rules. ## Tasks @@ -134,7 +145,7 @@ The last two read the whole output spike train (`Readout.SpikeTrain`), not just - **Auto: fastest available** is the default. It is the GPU engine below on a Mac, and CPU, all cores elsewhere. - **CPU, all cores** and **CPU, single thread** sample a number of random runs of each network, as before. -- **Exhaustive (exact outputs)** follows every possible computation, merging those that reach the same configuration. Its outputs are therefore the exact set the network can produce within the step limit, with no luck in the score. An exact solution is accepted without retesting. If a network's computations branch too widely, the engine samples it instead. Spike trains and port readings are kept in the merge key, so only computations with the same record so far are merged and each distinct train is reported once; a deterministic network costs one configuration a step. It refuses jitter (see Timing robustness). +- **Exhaustive (exact outputs)** follows every possible computation, merging those that reach the same configuration. Its outputs are therefore the exact set the network can produce within the step limit, with no luck in the score. An exact solution is accepted without retesting. If a network's computations branch too widely, the engine samples it instead; so it does when one step would build more than 16 successors for each configuration it may keep, even if most of them merge, since each is built before it can be merged. Spike trains and port readings are kept in the merge key, so only computations with the same record so far are merged and each distinct train is reported once; a deterministic network costs one configuration a step. It refuses jitter (see Timing robustness). - **GPU (Metal), for large networks** is listed on Macs. It samples like the CPU engines, but runs every run of every network in the population at once on the GPU, with one threadgroup per run. On an M5 Pro it is about 6 to 12 times faster than all CPU cores for networks of a thousand neurons or more. Its rule choices come from a hash of the seed rather than `System.Random`, so individual runs differ from the CPU engines' while following the same distribution, and the same seed repeats them. Batches too small to repay the GPU round trip, and networks with more than 64 output neurons, delays above 65,535 or emissions above 32,767, run on the CPU instead. ## Algorithms @@ -230,7 +241,11 @@ snp-evolution evolve-parts --seed 1 snp-evolution evolve-parts --only "add,fan-out" --budget 200000 --redo on ``` -For each contract the library has no part for, the command evolves one from scratch with MAP-Elites (lexicase parents, standard rules), verifies it on the exhaustive engine over every computation of every case, then shrinks it with MAP-Elites over hardware-cost cells and keeps the cheapest network that still verifies. Hardware cost orders by neurons, then synapses, then rules, then register width (the most spikes any neuron holds during the cases); distinct rules and lasso table size break any remaining tie. +For each contract the library has no part for, the command evolves one from scratch with MAP-Elites (lexicase parents, standard rules, deterministic neurons), verifies it on the exhaustive engine over every computation of every case, then shrinks it with MAP-Elites over hardware-cost cells and keeps the cheapest network that still verifies. Hardware cost orders by neurons, then synapses, then rules, then register width (the most spikes any neuron holds during the cases); distinct rules and lasso table size break any remaining tie. A deterministic neuron never has two rules that apply to the same spike count: a contract must hold on every computation, and a network of such neurons has one per input, so the exhaustive engine follows one configuration a step instead of every branch. New neurons and added rules are drawn to leave their neuron deterministic, and an edit or crossover that would give a neuron rival rules is made again, keeping the parent after eight tries, since dropping a rule there cost sequencer 3 half its solves. The search logs its best fitness at each quarter of its budget. + +A network is scored on five rules per case: quiet before start, done once (exactly one done, the right one), right values, back to start and on time. The values are read up to the right done, or the first done, or the end of the run when no done fires, so a network that computes the right values but misfires done still scores for them. For a part with data out-ports the values are half of each case's score and the other four rules the other half, since a network that ignores its input meets all four by firing done on time and keeping quiet; with every rule weighted alike that scored about 0.8, above most networks that compute anything. Lexicase still picks parents on each rule separately. A part without data out-ports, such as a delay or a zero test, scores the four rules alike. + +The search learns a contract a few cases at a time: first on the three cases with the smallest inputs, then twice as many each time a stage is solved, ending with every case (a stage holding more than three quarters of the cases is skipped). The archive is scored again at each stage, so its stepping stones carry over, and only networks on the last stage are verified. A contract with one case has one stage. `--staged off` scores every case from the start. - `--seed N` (1 by default): each contract gets its own seed from it, so the same seed writes the same library whichever contracts run together. - `--budget N` (50000 by default): search evaluations per contract; shrinking spends a quarter as many again. @@ -239,12 +254,20 @@ For each contract the library has no part for, the command evolves one from scra - `--engine exact|sampled`: the engine the search scores on; verification is always exhaustive. - `--redo on`: evolve contracts the library already has a part for; the new part replaces the old only if it is cheaper. - `--robust J`: shrink towards the most robust part at jitter J rather than the smallest (see Timing robustness). +- `--staged on|off` (on by default): learn the contract a few cases at a time, smallest inputs first. The library folder holds one JSON file per contract (`delay-1.json`, `zero-test.json`) with the network (in the usual network file format), contract, port binding, hardware cost, latency, seed, run and evaluations. Loading verifies every part again and refuses a file whose part fails its contract or whose contract differs from the catalogue, naming the file. Two parts that read the same on every case of a contract count as one, and the cheaper is kept under the first one's id. +`parts` shows what the library holds: a table of the kept parts (cost, latency, proof, seed and evaluations) and the first-part contracts with no part yet. `--only NAMES` or `--part FILE` shows each part in full, with its ports, what it reads on each case and its network. + +``` +snp-evolution parts +snp-evolution parts --only sequencer +``` + The run ends with a table of each contract, whether it was solved, the evaluations it used, and the kept part's neurons, synapses, latency and robustness to jitter. It exits with 2 when a contract is left without a part. -With seed 1 and the default budget (47 minutes on a 15-core machine), the run solved delay 2, 3 and 4 (2 neurons, 1 synapse each) and sequencer 2 (6 neurons, 8 synapses). Delay 1 was solved by other seeds but not this one, and sequencer 3 and the zero test came close (best fitness 0.97). None of the parts with count ports was solved. Their best networks score about 0.8, getting every rule right except putting the right values out and firing done once. A part that holds a count until start needs the parity trick of the hand-built register: each input spike is stored as two, and start makes the total odd so that a rule matching odd counts drains it. Larger networks, lexicase off, and partial credit for right values when done misfires all left the best near 0.8 within 50000 evaluations. The `parts/` folder in the repository holds the parts this run found. +With seed 1 and the default budget (47 minutes on a 15-core machine; about 70 seconds since part search keeps its neurons deterministic, when it also solves delay 1), the run solved delay 2, 3 and 4 (2 neurons, 1 synapse each) and sequencer 2 (6 neurons, 8 synapses). Delay 1 was solved by other seeds but not this one, and sequencer 3 and the zero test came close (best fitness 0.97). None of the parts with count ports was solved. Their best networks score about 0.8, getting every rule right except putting the right values out and firing done once. A part that holds a count until start needs the parity trick of the hand-built register: each input spike is stored as two, and start makes the total odd so that a rule matching odd counts drains it. Larger networks, lexicase off, and partial credit for right values when done misfires all left the best near 0.8 within 50000 evaluations. Weighting the values as half of each case and learning a few cases at a time solved none of them over 10 seeds either, but moved where the search stalls: increment and register get the right values on their first three cases and leave one neuron holding a spike, add and register get all but one case right, the zero test never fires done for n = 0, and fan-out and double each reached all their cases on one seed. The `parts/` folder in the repository holds the parts this run found. ## Composing machines from parts diff --git a/SNP_Evolution/Application/ComposeService.cs b/SNP_Evolution/Application/ComposeService.cs index eb2ec31..998c96a 100644 --- a/SNP_Evolution/Application/ComposeService.cs +++ b/SNP_Evolution/Application/ComposeService.cs @@ -1,6 +1,5 @@ using System; using SnpEvolution.Search; -using SnpEvolution.Search.Benchmarking; namespace SnpEvolution.Application { @@ -9,21 +8,16 @@ public static class ComposeService { public const string FileStem = "ComposedNet"; - // The settings compose starts from, before any options: the task's rule form and timing, composition search with - // tournament selection and lexicase parents, and a budget large enough for the arithmetic contracts. - public static Settings SettingsFor(CatalogEntry task) + // The settings compose starts from, before its task and options: composition search with tournament selection and + // lexicase parents, and a budget large enough for the arithmetic contracts. + public static Settings Starting(Settings settings) { - BenchmarkTask suiteTask = task.Create(new Settings()); - return new Settings - { - Task = task, - RuleForm = suiteTask.RuleForm, - OutputTiming = suiteTask.Timing, - Algorithm = SearchCatalog.CompositionTournament, - MaxEvaluations = 30_000, - MaxGenerations = 5_000, - Lexicase = true, - }; + Settings starting = settings.Copy(); + starting.Algorithm = SearchCatalog.CompositionTournament; + starting.MaxEvaluations = 30_000; + starting.MaxGenerations = 5_000; + starting.Lexicase = true; + return starting; } // Why these settings cannot compose, or null when they can. diff --git a/SNP_Evolution/Application/EvolutionSession.cs b/SNP_Evolution/Application/EvolutionSession.cs index 2676491..88a7cf2 100644 --- a/SNP_Evolution/Application/EvolutionSession.cs +++ b/SNP_Evolution/Application/EvolutionSession.cs @@ -169,6 +169,10 @@ private static void RunGenerations(Settings settings, EvaluationBudget evaluatio { log($"Fitness over {Solved.Sampled}, stopping . . ."); } + else if (stop == SearchStop.Cancelled) + { + log("Stopped early, keeping the best so far . . ."); + } else if (stop == SearchStop.BudgetSpent && generations < settings.MaxGenerations) { log($"The budget of {settings.MaxEvaluations} evaluations is spent, stopping . . ."); diff --git a/SNP_Evolution/Application/LibraryView.cs b/SNP_Evolution/Application/LibraryView.cs new file mode 100644 index 0000000..ce58433 --- /dev/null +++ b/SNP_Evolution/Application/LibraryView.cs @@ -0,0 +1,91 @@ +using System; +using System.Collections.Generic; +using System.Globalization; +using System.Linq; +using System.Text; +using SnpEvolution.Model; +using SnpEvolution.Specs.Contracts; +using SnpEvolution.Specs.Parts; + +namespace SnpEvolution.Application +{ + // Reading a part library without opening its files: a table of the parts kept, with the first-part contracts that + // have none yet, and each part in full. + public static class LibraryView + { + public static string Table(IReadOnlyList parts) + { + var table = new List { new[] { "Contract", "Neurons", "Synapses", "Rules", "Latency", "Proof", "Seed", "Evaluations", "File" } }; + table.AddRange(parts.OrderBy(file => file.Part.Contract.Name, StringComparer.Ordinal).Select(file => new[] + { + file.Part.Contract.Name, + Number(file.Part.Cost.Neurons), + Number(file.Part.Cost.Synapses), + Number(file.Part.Cost.Rules), + Number(file.Part.Latency), + Proof(file.Part.Proven), + Number(file.Part.Origin.Seed), + Number(file.Part.Origin.Evaluations), + System.IO.Path.GetFileName(file.Path), + })); + int[] widths = Enumerable.Range(0, table[0].Length).Select(column => table.Max(cells => cells[column].Length)).ToArray(); + var text = new StringBuilder(); + foreach (string[] cells in table) + { + text.AppendLine(string.Join(" ", cells.Select((cell, column) => cell.PadRight(widths[column]))).TrimEnd()); + } + List missing = Missing(parts); + text.AppendLine(missing.Count == 0 ? "Every first-part contract has a part." : $"No part yet for: {string.Join(", ", missing)}."); + return text.ToString(); + } + + // The first-part contracts the library has no part for, in the order the catalogue lists them. + public static List Missing(IReadOnlyList parts) => + FirstParts.Contracts.Select(contract => contract.Name).Where(name => parts.All(file => file.Part.Contract.Name != name)).ToList(); + + public static string Describe(PartFile file) + { + LibraryPart part = file.Part; + Contract contract = part.Contract; + var text = new StringBuilder(); + text.AppendLine($"{contract.Name} ({file.Path})"); + if (FirstParts.All.FirstOrDefault(first => first.Contracts.Any(each => each.Name == contract.Name)) is FirstPart first) + { + text.AppendLine($"Goal: {first.Goal}"); + } + text.AppendLine("Ports: " + string.Join(", ", part.Part.Ports().Select(port => $"{port.Port.Name} ({port.Port.Direction.ToString().ToLowerInvariant()}, {port.Port.Kind.ToString().ToLowerInvariant()}) on neuron {port.Position}"))); + text.AppendLine($"Latency: {part.Latency}, contract allows {contract.MinLatency} to {contract.MaxLatency}"); + text.AppendLine($"Cost: {part.Cost}"); + text.AppendLine($"Proof: {part.Proven?.ToString() ?? "not checked yet (run verify)"}"); + text.AppendLine($"Found by: {part.Origin.Run}, seed {part.Origin.Seed}, {part.Origin.Evaluations} evaluations"); + if (part.Recipe is PartRecipe recipe) + { + text.AppendLine($"Built from: {string.Join(", ", recipe.Children)}, with {recipe.Glue.Count} glue neuron(s)"); + } + text.AppendLine("What it reads on each case:"); + foreach ((string label, string reading) in Readings(part)) + { + text.AppendLine($" {label}: {reading}"); + } + text.AppendLine("Network:"); + text.Append(NetworkNotation.Format(part.Part.Network)); + return text.ToString(); + } + + // The behaviour key holds the contract's name, then each case's readings in case order. + private static IEnumerable<(string Label, string Reading)> Readings(LibraryPart part) + { + string[] readings = part.Behaviour.Split(" | ").Skip(1).ToArray(); + return part.Contract.Cases.Select((@case, index) => + { + string label = @case.Label(part.Contract.DataIn); + return (label.Length > 0 ? label : $"case {index + 1}", index < readings.Length ? readings[index] : "?"); + }); + } + + private static string Proof(ProvenBound? proven) => + proven == null ? "-" : proven.AllInputs ? "all inputs" : proven.UpTo < 0 ? "none" : $"up to {proven.UpTo}"; + + private static string Number(long value) => value.ToString(CultureInfo.InvariantCulture); + } +} diff --git a/SNP_Evolution/Application/PartsService.cs b/SNP_Evolution/Application/PartsService.cs index 2443109..5ad5e2e 100644 --- a/SNP_Evolution/Application/PartsService.cs +++ b/SNP_Evolution/Application/PartsService.cs @@ -15,7 +15,7 @@ namespace SnpEvolution.Application { // Seed is the run's seed, which each contract's own seed comes from. - public sealed record PartsRequest(IReadOnlyList Contracts, int Seed = RunSeed.Repeatable, bool Redo = false, EngineChoice? Engine = null, int RobustJitter = 0); + public sealed record PartsRequest(IReadOnlyList Contracts, int Seed = RunSeed.Repeatable, bool Redo = false, EngineChoice? Engine = null, int RobustJitter = 0, bool StagedCases = true); // Error says why nothing was evolved, when the library folder cannot be used. public sealed record PartsResult(IReadOnlyList Rows, string? Error = null) @@ -43,11 +43,16 @@ public static PartsResult Run(Settings settings, PartsRequest request, Action(), loaded.Error); } - string run = $"evolve-parts --seed {request.Seed} --budget {budget}{engine.CommandLineFlag}{(settings.HardwareProfile ? " --profile hardware" : "")}{(request.RobustJitter > 0 ? $" --robust {request.RobustJitter}" : "")}"; - PartSearchSettings search = SearchSettings(budget, engine.Factory) with { HardwareProfile = settings.HardwareProfile, RobustJitter = request.RobustJitter }; + string run = $"evolve-parts --seed {request.Seed} --budget {budget}{engine.CommandLineFlag}{(settings.HardwareProfile ? " --profile hardware" : "")}{(request.RobustJitter > 0 ? $" --robust {request.RobustJitter}" : "")}{(request.StagedCases ? "" : " --staged off")}"; + PartSearchSettings search = SearchSettings(budget, engine.Factory) with { HardwareProfile = settings.HardwareProfile, RobustJitter = request.RobustJitter, StagedCases = request.StagedCases }; var rows = new List(); foreach (Contract contract in request.Contracts) { + if (EarlyStop.Requested) + { + log("Stopped early: the contracts left are not evolved."); + break; + } Module? kept = library.PartFor(contract.Name); if (kept != null && !request.Redo) { @@ -70,7 +75,7 @@ public static PartsResult Run(Settings settings, PartsRequest request, Action written = PartLibraryFiles.Save(library, folder); diff --git a/SNP_Evolution/Application/ReachService.cs b/SNP_Evolution/Application/ReachService.cs index 6eacea1..bd61918 100644 --- a/SNP_Evolution/Application/ReachService.cs +++ b/SNP_Evolution/Application/ReachService.cs @@ -59,15 +59,26 @@ public sealed record Outcome(string Setup, int Seed, int Reach, int Neurons, lon } long partCost = library.Value.PartEvaluations; var jobs = (from setup in setups from seed in Enumerable.Range(1, seeds) select (setup, seed)).ToList(); - var outcomes = new Outcome[jobs.Count]; + var started = new Outcome?[jobs.Count]; int finished = 0; Parallel.For(0, jobs.Count, new ParallelOptions { MaxDegreeOfParallelism = Environment.ProcessorCount }, index => { + // After an early stop no run starts, and the report covers the setups that ran. + if (EarlyStop.Requested) + { + return; + } (Setup setup, int seed) = jobs[index]; - outcomes[index] = RunOnce(settings, setup, seed, chargeParts ? partCost : 0); - log($"[{Interlocked.Increment(ref finished)}/{jobs.Count}] {setup.Name}, seed {seed}: reach {outcomes[index].Reach}, " + - $"{outcomes[index].Neurons} neurons, {outcomes[index].Evaluations} evaluations, {outcomes[index].Seconds:0}s"); + Outcome outcome = started[index] = RunOnce(settings, setup, seed, chargeParts ? partCost : 0); + log($"[{Interlocked.Increment(ref finished)}/{jobs.Count}] {setup.Name}, seed {seed}: reach {outcome.Reach}, " + + $"{outcome.Neurons} neurons, {outcome.Evaluations} evaluations, {outcome.Seconds:0}s"); }); + List outcomes = started.OfType().ToList(); + setups = setups.Where(setup => outcomes.Any(outcome => outcome.Setup == setup.Name)).ToList(); + if (setups.Count == 0) + { + return "Stopped early, before any run finished."; + } string report = Report(settings, setups, outcomes, partCost, chargeParts, command); log(""); log(report); diff --git a/SNP_Evolution/Application/Settings.cs b/SNP_Evolution/Application/Settings.cs index 798b03b..0ea6415 100644 --- a/SNP_Evolution/Application/Settings.cs +++ b/SNP_Evolution/Application/Settings.cs @@ -29,8 +29,8 @@ public sealed class Settings public int SolvedRetestCount { get; set; } = 5; public OutputTarget Target { get; set; } = OutputTarget.Set(new[] { 1, 2, 3, 4, 5, 6, 7, 8, 9 }); public bool ExperimentalRules { get; set; } = true; - public RuleForm RuleForm { get; set; } = RuleForm.Legacy; - public OutputTiming OutputTiming { get; set; } = OutputTiming.Legacy; + public RuleForm RuleForm { get; set; } = RuleForm.Standard; + public OutputTiming OutputTiming { get; set; } = OutputTiming.Interval; public int MaxNeurons { get; set; } = 7; public int MaxDelay { get; set; } = 1; public int MaxProduce { get; set; } = 2; @@ -92,6 +92,17 @@ public sealed class Settings public IReadOnlyList MutationTemplates => ExperimentalRules ? ExpressionGenerator.ExperimentalTemplates : ExpressionGenerator.SimpleTemplates; + // Makes the task the one to evolve for; a suite task brings the rule form and timing it is meant for. + public void UseTask(CatalogEntry task) + { + Task = task; + if (task != Catalog.TargetTask) + { + BenchmarkTask chosen = task.Create(this); + (RuleForm, OutputTiming) = (chosen.RuleForm, chosen.Timing); + } + } + // The selected task, built with the rule form and output timing chosen here. public BenchmarkTask SelectedTask => Task.Create(this) with { RuleForm = RuleForm, Timing = OutputTiming }; diff --git a/SNP_Evolution/Application/VerifyService.cs b/SNP_Evolution/Application/VerifyService.cs index c63b4b9..9f17ce1 100644 --- a/SNP_Evolution/Application/VerifyService.cs +++ b/SNP_Evolution/Application/VerifyService.cs @@ -22,6 +22,10 @@ public static IReadOnlyList Run(IReadOnlyList parts, Pro var results = new List(); foreach ((var part, string path) in parts) { + if (EarlyStop.Requested) + { + break; + } var clock = Stopwatch.StartNew(); BoundedResult result = BoundedCheck.Prove(part.Part, limits, new EvaluationBudget()); string? counterexample = result.Verdict is Verdict.Failed failed ? CounterexampleText.Of(part.Part, failed.Counterexample) : null; diff --git a/SNP_Evolution/Cli/BenchmarkMenu.cs b/SNP_Evolution/Cli/BenchmarkMenu.cs deleted file mode 100644 index 61e1a82..0000000 --- a/SNP_Evolution/Cli/BenchmarkMenu.cs +++ /dev/null @@ -1,89 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics; -using SnpEvolution.Application; -using SnpEvolution.Model; -using SnpEvolution.Search; -using SnpEvolution.Search.Benchmarking; -using SnpEvolution.Search.Fitness; - -namespace SnpEvolution.Cli -{ - // Both race the searches that start from nothing, as the benchmark and select commands do, on the settings' engine. - internal static class BenchmarkMenu - { - public static void Show(MenuState state) - { - int selection = 0; - while (ConsoleUi.Choose(state.Settings, "Benchmark", new[] { "Every algorithm on the task suite", "Find the best algorithm for the selected task" }, selection) is int choice) - { - selection = choice; - if (choice == 0) - { - RunBenchmark(state.Settings); - } - else - { - SelectAlgorithm(state.Settings); - } - } - } - - private static void RunBenchmark(Settings settings) - { - Console.Clear(); - BenchmarkSettings benchmark = settings.BenchmarkSettings; - Console.WriteLine("Runs {0} algorithms on {1} tasks, {2} seeds each, with up to {3} evaluations per run, on the {4} engine.", - SearchCatalog.FromScratch.Count, TaskSuite.All.Count, benchmark.Seeds, benchmark.EvaluationBudget, settings.Engine.Name); - if (!ConsoleInput.WaitForEnterOrEscape("Press enter to start, or ESC to go back; this can take a while.") || Plan(settings) is not BenchmarkPlan plan) - { - return; - } - Stopwatch stopwatch = Stopwatch.StartNew(); - IReadOnlyList rows = BenchmarkService.Run(plan, TaskSuite.All, Console.WriteLine); - Console.WriteLine("\n{0}\nTime elapsed: {1}", Benchmark.FormatTable(rows), stopwatch.Elapsed); - BenchmarkService.Save(rows); - ConsoleInput.WaitForEnter("Press enter to return to the menu."); - } - - private static void SelectAlgorithm(Settings settings) - { - Console.Clear(); - BenchmarkTask task = settings.SelectedTask; - Console.WriteLine("Successive halving over {0} algorithms for: {1}, starting at {2} evaluations per run.", - SearchCatalog.FromScratch.Count, task.Name, BenchmarkService.InitialBudget(settings.BenchmarkSettings)); - if (!ConsoleInput.WaitForEnterOrEscape("Press enter to start, or ESC to go back; this can take a while.") || Plan(settings) is not BenchmarkPlan plan) - { - return; - } - SelectionResult> result = BenchmarkService.Select(plan, task, Console.WriteLine); - Console.WriteLine("\nBest algorithm for {0}: {1}", task.Name, result.Winner.Name); - if (result.BestFound is Individual best) - { - Console.WriteLine("Best network found (fitness {0}, {1}):\n{2}", best.Fitness, best.Description, NetworkNotation.Format(best.Genes)); - } - ConsoleInput.WaitForEnter("Press enter to continue."); - if (result.Winner is EvolutionSearch winner && ConsoleUi.Confirm(settings, $"Use {winner.Name} from now on?")) - { - settings.Algorithm = winner; - } - } - - // Null, after showing why, when composition search's part library cannot be read. - private static BenchmarkPlan? Plan(Settings settings) - { - Loaded plan = BenchmarkService.Plan(settings, settings.BenchmarkSettings, SearchCatalog.FromScratch); - if (plan.Value == null) - { - Console.WriteLine(plan.Error); - ConsoleInput.WaitForEnter("Press enter to return to the menu."); - return null; - } - if (plan.Value.PartsNote != null) - { - Console.WriteLine(plan.Value.PartsNote); - } - return plan.Value; - } - } -} diff --git a/SNP_Evolution/Cli/Commands/AdviseCommand.cs b/SNP_Evolution/Cli/Commands/AdviseCommand.cs index 1548f9f..f5c76e7 100644 --- a/SNP_Evolution/Cli/Commands/AdviseCommand.cs +++ b/SNP_Evolution/Cli/Commands/AdviseCommand.cs @@ -9,20 +9,23 @@ internal sealed class AdviseCommand : Command { public override string Name => "advise"; - public override string Summary => "Prints the settings the advisor suggests for a target, without evolving."; + public override string Summary => "Prints the settings the advisor suggests for a target or a suite task, without evolving."; public override IReadOnlyList