Explorer

Lancer un explorateur sur des mondes cachés, faire vérifier ses résultats par le noyau, et comparer un passage à froid et un passage avec bibliothèque.

Lancer un explorateur

Terminal

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

Cette commande lance l’explorateur d’ajustement exact sur la suite de mondes cachés. Chaque proposition passe par le vérificateur. Avec --lean, tous les résultats sont exportés dans un module Lean que le noyau vérifie à la fin. Le passage est enregistré dans un dossier runs/, avec ses verdicts.

Les cinq explorateurs

Explorateur Ce qu’il fait

random propose des densités au hasard. C’est le plancher.

datafit algèbre linéaire exacte sur des transitions simulées.

library ajustement exact plus réutilisation des lois de mondes apparentés.

oracle connaît la théorie et résout les équations de continuité. C’est le plafond.

llm un modèle de langage qui lit les règles et les retours du vérificateur.

Explorateur	Ce qu’il fait
`random`	propose des densités au hasard. C’est le plancher.
`datafit`	algèbre linéaire exacte sur des transitions simulées.
`library`	ajustement exact plus réutilisation des lois de mondes apparentés.
`oracle`	connaît la théorie et résout les équations de continuité. C’est le plafond.
`llm`	un modèle de langage qui lit les règles et les retours du vérificateur.

Options utiles

--budget : nombre de propositions autorisées, 300 par défaut.
--suite-seed : la graine qui génère la suite de mondes, 7 par défaut.
--suite eca : les automates élémentaires connus, pour calibrer, au lieu de la suite cachée.
--llm-command : la commande qui lit un prompt sur l’entrée standard, pour l’explorateur llm.

À froid, puis avec la bibliothèque

Terminal

python3 -m slean transfer --explorer library

Le protocole de transfert note la moitié réservée de la suite deux fois, au même budget : à froid, puis avec la bibliothèque construite sur la moitié vue. Il imprime les deux résultats. Voir Mesurer une découverte pour la lecture de ces chiffres.