Une grande partie des progrès récents de l’IA en mathématiques s’est faite au même endroit : dans des preuves écrites en Lean. Je ne crois pas que ce soit un hasard. Lean donne à un modèle ce qui manque à la plupart des recherches : une réponse à la question « est-ce juste ? » qui ne dépend de l’avis de personne.
Mutome a besoin de quelque chose de semblable pour la science. Slean est ma tentative de le construire, en commençant par de petits mondes. Cet article explique ce qu’est Slean, ce que nous avons mesuré avec lui et ce qu’il ne montre pas encore.
Ce que Lean apporte aux mathématiques.
Lean est un langage de programmation où les définitions sont exactes et où les preuves sont vérifiées par un petit programme de confiance, le noyau. Un modèle peut proposer mille tentatives de preuve. Le noyau accepte celles qui sont correctes et rejette les autres, sans se fatiguer et sans se laisser impressionner.
Trois choses en découlent. Le vérificateur est automatique : la recherche peut donc être large. Les résultats s’accumulent : Mathlib, la bibliothèque commune, permet à chaque nouvelle preuve de s’appuyer sur tout ce qui a déjà été vérifié. Et la frontière est explicite : à tout moment, on sait exactement quels énoncés sont démontrés.
C’est ce que j’entends par le hasard dans la découverte et la rigueur dans la vérification. En mathématiques, c’est Lean qui apporte la rigueur.
La science n’a pas de noyau.
La science empirique ne fonctionne pas ainsi. Une affirmation sur la nature repose sur des mesures, des modèles et le jugement de ceux qui les vérifient. Aucun programme ne peut lire un article et décider si sa conclusion est vraie. Les expériences sont bruitées, les instruments ont des limites, et deux explications peuvent rendre compte des mêmes données.
Un logiciel n’y changera rien. Mais cela rend difficile la mesure d’un système de recherche qui prétend s’améliorer. Si rien ne peut dire exactement si une découverte est juste, on ne peut pas savoir si le système fait de meilleures découvertes ou s’il devient seulement plus convaincant.
Ce qu’est Slean.
Slean, c’est Science + Lean. Au lieu de partir de la nature, il part de mondes définis exactement en Lean. Aujourd’hui, ce sont des automates cellulaires : des grilles de cellules qui évoluent selon une règle locale fixe. Ils sont simples, mais ils ont des lois, des structures et des mécanismes à découvrir, et chaque affirmation à leur sujet a un sens précis.
Une affirmation ne compte que si elle est vérifiée exactement. Une loi, une structure ou une formule courte qui calcule toute la règle d’un monde est acceptée quand le noyau de Lean la vérifie. Un mécanisme proposé est vérifié par comparaison exacte avec le monde. Une réfutation s’accompagne d’un contre-exemple, lui aussi vérifié. Les résultats acceptés rejoignent une bibliothèque sur laquelle les travaux suivants peuvent s’appuyer.
Slean comporte aussi des laboratoires. Dans un laboratoire, un agent étudie un monde dont les réponses sont cachées. Il ne peut agir qu’au moyen d’une commande ./lab qui compte chaque expérience. À la fin, ses affirmations sont évaluées face aux réponses cachées et comparées à celles d’une référence scriptée qui disposait exactement du même budget.
C’est avec ces laboratoires que Mutome se mesurera. Si une modification de son harnais l’aide, elle doit l’aider sur des laboratoires qu’il n’a jamais vus. Sinon, il ne faut pas la garder.
Ce que nous avons mesuré.
La première leçon a été une leçon d’humilité. Les lois de conservation, ce qu’on cherche classiquement dans ces mondes, sont entièrement résolues par une méthode générique d’une cinquantaine de lignes qui ajuste exactement les données. Cette classe de problèmes sert à étalonner le moteur. Elle ne peut pas démontrer une capacité de découverte.
Sur des mondes générés aux règles cachées, un agent Claude Sonnet a trouvé toutes les lois de conservation cachées et un peu plus de structures que la référence scriptée. Il a utilisé de 150 à 225 fois moins d’expériences, sans aucune fausse affirmation. C’est encourageant, mais chacun de ces mondes peut être identifié par une seule expérience bien choisie. C’est du travail compétent, pas de la découverte ouverte.
Nous avons ensuite donné à l’agent des leçons tirées de laboratoires précédents. Sur cette batterie, elles ont changé les résultats de 0 et de +1 découverte. La batterie était saturée : il ne restait aucune marge pour qu’une amélioration se voie.
Nous avons donc construit des mondes plus durs, que nous appelons compressibles : des règles de 1 024 entrées qui cachent une loi courte, avec un budget d’expériences serré. Lors d’un premier essai, l’agent seul a fait 3 découvertes sur 48, contre 12 pour la référence scriptée. Il n’a jamais essayé d’inférer la loi courte.
Sur trois graines réservées, le même agent, avec des leçons tirées de laboratoires précédents, a fait 13, 13 et 17 découvertes vérifiées, contre 4, 6 et 5 sans elles. Nous avons refait toute la comparaison trois fois. Les leçons l’emportent dans 8 paires sur 9, avec 6 découvertes de plus par laboratoire en moyenne. C’est la première modification du harnais de Mutome qui améliore les résultats sur des mondes jamais vus.
Nous avons ensuite permis à l’agent de soumettre des lois compactes : une formule courte qui calcule toute la règle d’un monde, et que le noyau de Lean vérifie sur les 1 024 voisinages. Pour en trouver une, il faut inférer la règle au lieu de la lire. Avec des leçons, l’agent a trouvé 8, 12 et 8 des 12 lois cachées. Sans elles, il en a trouvé 2, 6 et 5.
Puis le résultat est redevenu humble. Nous avons réécrit la référence scriptée pour qu’elle essaie les familles de règles classiques, comme les règles linéaires et totalistiques. Elle a trouvé 9 lois et de 47 à 54 découvertes par laboratoire. Avec des leçons, l’agent fait jeu égal avec elle. Sans elles, il fait moins bien sur deux graines sur trois. Une partie de ce qu’apprennent les leçons pourrait simplement être les familles qu’utilise cette suite : les prochains mondes devront donc utiliser des familles hors de cette liste.
Ce que cela ne montre pas.
Rien de tout cela n’est une découverte sur le monde réel. Ces mondes sont des jouets, et c’est voulu : ils sont assez petits pour être vérifiés exactement. Une loi démontrée dans un automate cellulaire ne dit rien de la nature, et une amélioration mesurée ici n’est pas encore une amélioration en recherche réelle.
Cela ne montre pas non plus que Mutome s’améliore lui-même. Cela montre une amélioration, répétée sur une batterie conçue pour la détecter, et un simple script qui fait aussi bien. C’est un début que je peux mesurer, et c’est ce que je cherchais.
La suite.
La prochaine étape consiste à laisser Mutome exécuter des laboratoires Slean en continu, dans un budget de 50 $ par mois, et à ne modifier son harnais que si cela améliore les résultats sur des laboratoires qu’il n’a pas vus. Viendront ensuite des mondes plus proches de la physique, puis des prédictions sur le monde réel faites avant que les données existent, pour qu’elles puissent être vérifiées sans connaître déjà la réponse.
Pour voir à quoi ressemblent ces mondes, slean.org les explique simplement, et ses quatre mini-jeux permettent de chercher soi-même les lois d’un monde. Les mesures y sont publiées aussi, y compris celles qui ne nous flattent pas.