Une intelligence artificielle a parcouru des milliers d’articles de mathématiques, puis retenu 77 résultats assez prometteurs pour être examinés par des chercheurs.
Le système, nommé FAR, ne reçoit pas forcément un problème précis à résoudre. Les chercheurs lui indiquent plutôt un domaine de recherche. Il cherche alors dans la littérature scientifique les questions encore ouvertes. Une conjecture est justement une affirmation mathématique que l’on pense vraie, sans disposer encore d’une démonstration reconnue.
Pour comprendre l’intérêt de cette approche, il faut regarder le travail habituel d’un mathématicien. Trouver un problème intéressant demande déjà beaucoup de temps. Vérifier ensuite une démonstration proposée peut en demander davantage. FAR tente d’automatiser une partie de ces deux étapes, sans retirer la validation finale aux spécialistes humains.
Lors d’un essai en combinatoire, une branche des mathématiques étudiant notamment les arrangements et les structures discrètes, le système est parti de 51 110 articles. Il en a identifié 5 245 liés au domaine étudié. FAR y a extrait 6 453 conjectures ou problèmes potentiellement ouverts, puis en a conservé 4 717 après vérification de leur statut.
Chaque problème retenu a ensuite reçu une tentative de résolution. Le système a produit 1 050 réponses présentées comme nouvelles. D’autres agents d’IA ont vérifié ces propositions et en ont accepté 598. Une dernière étape a réduit cet ensemble à 77 résultats jugés assez intéressants pour mériter l’attention de mathématiciens.
Cette sélection reste importante, car une démonstration produite par une IA ne devient pas vraie simplement parce qu’un autre programme l’approuve. Les auteurs ont examiné eux-mêmes 15 résultats qu’ils jugeaient particulièrement intéressants. Tous étaient mathématiquement corrects. L’un d’eux avait toutefois déjà été obtenu quelques mois auparavant, sans que les recherches automatiques ne le retrouvent.
Autrement dit, le système sert autant à choisir où consacrer du temps qu’à tenter des démonstrations. Trois vérifications indépendantes sont notamment appliquées aux résultats présentés comme nouveaux avant la sélection finale.
L’expérience porte pour l’instant sur la combinatoire, domaine que les auteurs maîtrisent suffisamment pour contrôler les résultats. Le dispositif pourrait fonctionner avec d’autres collections d’articles et d’autres thèmes.