Une IA de DeepMind résout neuf problèmes d’Erdős dans la revue Science

Google DeepMind, filiale d'Alphabet ↘ 0.72%, a publié une étude évaluée par des pairs sur AlphaProof Nexus, un système d'IA ayant résolu neuf problèmes ouverts posés par le mathématicien Paul Erdős et démontré 44 conjectures issues de l'Encyclopédie en ligne des suites de nombres entiers (OEIS). L'article est paru le jeudi 8 octobre dans Science. Deux des problèmes d'Erdős avaient été formulés par Erdős et András Sárközy en 1970 et étaient restés sans solution pendant 56 ans.elmundo+2

L'étude apporte une validation scientifique aux résultats que DeepMind avait initialement publiés sur arXiv en mai. Elle intervient alors que les laboratoires d'IA rivalisent pour prouver que leurs systèmes peuvent effectuer des recherches mathématiques de haut niveau, une course critiquée par certains mathématiciens de renom.abc+1

Fonctionnement

Le système utilise Gemini 3.1 Pro pour rechercher des preuves et l'assistant de preuve Lean pour les vérifier. Lean vérifie mécaniquement chaque étape et rejette toute preuve incomplète, tandis que l'agent teste de nouvelles stratégies, souvent en parallèle. L'équipe a tenté de résoudre 353 problèmes d'Erdős et 492 conjectures de l'OEIS. Ils ont vérifié manuellement les 44 preuves de l'OEIS et confirmé que les problèmes étaient correctement formalisés et n'avaient jamais été résolus auparavant. Selon la prépublication sur arXiv, chaque problème d'Erdős résolu a coûté "quelques centaines de dollars" en puissance de calcul.arxiv+2

Le système a également résolu deux des quatre problèmes ouverts en géométrie algébrique, dont une conjecture de Zanello. Les auteurs affirment ne connaître aucun article antérieur utilisant la même stratégie de preuve. Pushmeet Kohli, de DeepMind, a déclaré en mai que les résultats incluaient un problème de géométrie algébrique vieux de 15 ans et une question d'optimisation min-max vieille de 7 ans. Un résultat a surpris : une version beaucoup plus simple de l'agent, qui se contente de générer une preuve et de la vérifier, a également résolu les neuf problèmes d'Erdős.elmundo+2

Limites et critiques

Le système a échoué sur la majorité des problèmes tentés. Dans certains cas, il a inséré le marqueur "sorry" de Lean dans une preuve pour ignorer une étape qu'il ne pouvait pas démontrer, ou a cité des théorèmes inexistants. Josep Curto Díaz, de l'Université ouverte de Catalogne, a déclaré à ABC que le système présente toujours "une dépendance humaine structurelle". Il a cité un cas où les chercheurs ont dû orienter l'IA vers la recherche de contre-exemples.elmundo+1

Après la publication de la préimpression, le physicien Anatol Wegner a soutenu que plusieurs des problèmes "ouverts" d'Erdős avaient déjà été résolus dans des travaux publiés. Dans deux cas, a-t-il écrit, l'énoncé du problème a été modifié après que l'agent a trouvé ses preuves. Un commentaire du Science Media Centre espagnol a qualifié le système complet de trop complexe.sciencemediacentre+1

L'article fait suite à une lettre ouverte publiée en septembre, dans laquelle 25 médaillés Fields, dont Terence Tao, ont mis en garde contre la transformation des mathématiques en une course aux résultats. Swarat Chaudhuri, l'un des auteurs de DeepMind, a déclaré à El Mundo que ces systèmes "ont encore besoin de conseils humains pour décider quels problèmes résoudre et nécessitent un examen attentif de leurs résultats". Il a ajouté : "En fin de compte, les mathématiques sont une activité humaine".elmundo