Mutome (site externe)
Menu

Slean en 5 minutes

L’histoire de Slean en langage simple : un monde, une affirmation, un test, une preuve. Avec un jeu pour chaque étape.

Le problème

Une IA peut proposer mille découvertes en une heure. Certaines sont vraies, beaucoup ne le sont pas, et toutes ont l’air convaincantes. Pour s’en servir, il faut un juge qui dise lesquelles sont vraies, sans se laisser impressionner par une belle explication. Slean est ce juge.

Un monde que l’on connaît par cœur

Pour pouvoir tout vérifier, Slean travaille dans des simulés dont on connaît la exacte. Le premier est une route en anneau. Chaque case est vide ou porte une voiture. À chaque pas, toutes les voitures regardent devant elles en même temps : si la case devant est libre, la voiture avance, sinon elle attend. Appuyez sur Lecture :

Règle 184 : le trafic

Vue

Pas 16 : 14 voitures

pasvoitures0141142143144145146147148149141014111412141314141415141614

voiturecase librenombre conservé

Simulation dans votre navigateur, convention centrée. Le nombre de voitures, à droite, ne change pas. La preuve, elle, vaut pour tous les anneaux.

Ces mondes sont volontairement simples. La science du monde réel est l’objectif de long terme, pas ce que Slean fait aujourd’hui.

Une affirmation

Un d’IA regarde ce monde et propose une idée, par exemple une : « le nombre de voitures ne change jamais ». C’est une affirmation précise : elle est vraie ou fausse, sans entre-deux.

Essayez vous-même : Devinez la loi, puis proposez-en une.

Tester, puis prouver

Slean commence par chercher un : une route où l’affirmation échoue. S’il en trouve un, l’affirmation est réfutée pour de bon, et ce témoin est gardé. Pour le nombre de voitures, il n’en trouve aucun.

Mais tester ne suffit pas : il existe une infinité de routes. Il faut une . Ici, elle tient en une idée : une voiture ne disparaît jamais, elle passe d’une case à la voisine. Il suffit de le vérifier sur les 16 façons d’agencer 4 cases voisines : c’est le . Le de Lean contrôle ces vérifications et en déduit la loi pour toutes les routes, de toutes les tailles :

Lean 4
theorem traffic :
    Conserved (eca 184) (tableFn 2 [0, 1]) 1 :=
  conserved_of_fluxCheck _ _
    (tableFn 2 [1, 1, 1, 1, 1, 1, 0, 0]) 1
    (by decide +kernel)

La page Affirmation et certificat explique pourquoi une vérification finie suffit pour une infinité de tailles.

La boucle

La boucle de Slean

  1. Un agent proposeUne loi, une structure ou une réfutation sur un monde exact.
  2. Slean vérifieLe noyau de Lean accepte le certificat, ou un contre-exemple réfute.
  3. La bibliothèque gardeChaque résultat devient un théorème réutilisable.
  4. La mesure noteContre des réponses cachées, face à des méthodes simples à coût égal.
Mutome explore, Slean vérifie. Rien n’entre dans la bibliothèque sans passer par le noyau.
  1. Un agent propose une loi, une structure ou une réfutation.
  2. Slean vérifie : un contre-exemple réfute, un certificat accepté par le noyau démontre.
  3. La bibliothèque garde le résultat, que les recherches suivantes réutilisent.
  4. La mesure compare l’agent à des méthodes simples, au même coût, sur des mondes que personne n’a vus et dont la réponse est cachée.

Mutome, le laboratoire de recherche autonome, décide quoi explorer : c’est le hasard dans la découverte. Slean dit ce qui est vrai : c’est le déterminisme dans la vérification.

Ce que les agents ont trouvé

Dans des mondes aux règles cachées, un agent a trouvé toutes les lois et plus de structures qu’un programme de référence, avec 150 à 225 fois moins d’expériences, et aucune affirmation fausse. Parmi ses trouvailles, un planeur de période 16 que la référence ne pouvait pas voir : Trouvez un planeur. Son astuce : lire toute la règle d’un monde en une seule expérience, ce que montre Le monde caché.

Ce qui ne marche pas encore

  • Les mondes actuels sont trop faciles : une seule expérience bien choisie révèle toute leur règle. Ce n’est donc pas encore de la découverte ouverte. La page Un monde caché reconstruit montre pourquoi.
  • Un seul type de monde, les automates cellulaires à une dimension.
  • Deux graines de suite, un passage chacune, un seul modèle d’agent. Voir Mesurer une découverte.
  • Rien ici ne dit quoi que ce soit du monde réel. Une loi démontrée dans un monde de cases n’est pas une loi de la nature. Voir Quatre sortes de preuves.

Pour continuer