Le Problème Avec La Façon Dont Les Mathématiciens Travaillent

La recherche mathématique est l'un des efforts intellectuels les plus exigeants de l'activité humaine — et, à bien des égards, l'un des moins automatisés. Bien que les systèmes d'IA aient transformé la codification, l'écriture et l'analyse de données, les structures formales des mathématiques supérieures sont restées largement hors de leur portée. Les preuves doivent être vérifiées par une logique rigoureuse ; les modèles dans les structures abstraites ne cèdent pas à la reconnaissance de modèles statistiques qui rend les grands modèles de langage utiles pour le texte. Une startup appelée Axiom Math pense avoir trouvé un moyen de changer cela, et cette semaine, elle a lancé un outil gratuit pour les mathématiciens qui place une capacité importante de découverte de modèles sur un seul ordinateur portable.

L'outil, appelé Axplorer, est une version démocratisée de PatternBoost — un algorithme développé par Francois Charton, un chercheur scientifique maintenant chez Axiom qui a précédemment travaillé chez Meta. En 2024, Charton a utilisé PatternBoost fonctionnant sur des milliers de nœuds de superordinateur pendant trois semaines pour résoudre un problème séculaire en théorie des graphes appelé le problème des quatre-cycles de Turan. Axplorer peut reproduire ce résultat en deux heures et demie sur un Mac Pro.

Ce Que Fait Axplorer

L'algorithme sous-jacent d'Axplorer fonctionne à travers un cycle itératif de recherche classique et d'apprentissage par réseau de neurones. Il commence par générer un grand nombre de solutions candidates aléatoires à un problème mathématique et en conservant les plus performantes. Un réseau de neurones transformer est alors entraîné sur ces exemples réussis pour apprendre quelles propriétés caractérisent une bonne solution. À la manche suivante, le réseau entraîné génère des candidats améliorés qui servent de semences pour une autre phase de recherche classique. Les deux phases alternent, chaque manche produisant des solutions progressivement meilleures.

L'idée clé est que le réseau de neurones n'a pas besoin de comprendre les mathématiques dans aucun sens profond. Il doit seulement reconnaître les modèles structurels dans les solutions trouvées jusqu'à présent et utiliser ces modèles pour guider la génération de meilleurs candidats. Au fil de nombreuses itérations, cela produit des solutions que la seule recherche classique serait peu probable de trouver — particulièrement dans les problèmes avec d'énormes espaces de recherche où l'exploration aléatoire est calculatoirement intraitable.

Le Problème de Turan et Ce Qu'il Révèle

Le problème des quatre-cycles de Turan demande : étant donné un ensemble de points, combien d'arêtes pouvez-vous tracer entre eux sans créer de boucles à quatre points ? Le problème touche des structures profondes en combinatoire et en théorie des graphes qui sont pertinentes pour l'analyse des réseaux réels — graphiques des médias sociaux, chaînes d'approvisionnement et structures de liens des moteurs de recherche. Il avait résisté à la solution pendant environ un siècle avant que PatternBoost le résolve en 2024.

Le fait que PatternBoost nécessitait un superordinateur massif n'était pas un obstacle pour Meta, qui exploite des infrastructures de cette ampleur régulièrement. Mais c'était un obstacle pour essentiellement chaque mathématicien du monde qui aurait pu vouloir appliquer une approche similaire à ses propres problèmes ouverts. En concevant Axplorer pour fonctionner sur une station de travail grand public, Axiom a changé la distribution de l'accès à cette classe d'IA mathématique.

Qui Est Derrière Axiom Math

L'entreprise a été fondée par Carina Hong, une jeune femme de 24 ans qui a abandonné Stanford après avoir étudié au MIT et Oxford. Axiom a été lancée discrètement en 2024 avec 64 millions de dollars de financement initial à une valorisation de 300 millions de dollars, dirigée par B Capital. En plus de Charton, l'équipe de recherche comprend Aram Markosyan, un expert en sécurité et équité de l'IA.

La vision de Hong pour l'entreprise s'étend bien au-delà d'Axplorer. Trouver des solutions n'est pas tout ce que font les mathématiciens — les mathématiques sont exploratoires et expérimentales, a-t-elle déclaré. Parfois, les idées proviennent de la détection de modèles qui n'avaient pas été détectés auparavant, et de telles découvertes peuvent ouvrir des branches entièrement nouvelles des mathématiques. L'ambition déclarée à long terme d'Axiom est ce qu'elle appelle l'superintelligence mathématique — l'IA qui non seulement peut résoudre les problèmes connus mais contribuer à la découverte de nouvelles structures mathématiques.

Axplorer Est Gratuit et Disponible Maintenant

Axiom a lancé Axplorer comme un outil gratuit disponible pour tout mathématicien qui peut l'installer. La décision reflète une stratégie délibérée : en distribuant l'outil largement dans la communauté académique, Axiom peut recueillir des commentaires, identifier quelles classes de problèmes l'algorithme gère bien et construire la crédibilité au sein d'une communauté qui tend à être sceptique face aux entreprises d'IA commerciales.

Le produit séparé de l'entreprise, AxiomProver, qui se concentre sur la génération et la vérification des preuves formelles, a déjà trouvé des solutions à quatre problèmes mathématiques précédemment non résolus. La combinaison d'un outil de découverte de modèles et d'un vérificateur de preuve représente une paire complémentaire de capacités qui reflète les deux phases de la recherche mathématique : générer des conjectures, puis les prouver rigoureusement.

Où Va L'IA Mathématique

Axiom entre dans un domaine qui a connu des investissements importants et plusieurs résultats historiques. AlphaProof et AlphaGeometry de DeepMind ont démontré que l'IA peut résoudre des problèmes au niveau de l'Olympiade Mathématique Internationale. Mais les problèmes de style de compétition, aussi difficiles soient-ils, ne représentent qu'une part étroite des mathématiques. L'objectif plus ambitieux — contribuer à la recherche ouverte dans des domaines comme la théorie des nombres, la topologie algébrique ou la combinatoire — reste largement inexploré.

L'approche d'Axiom, qui met l'accent sur la découverte de modèles et la recherche itérative plutôt que la preuve de théorème de bout en bout, peut être mieux adaptée à la phase exploratoire de la recherche mathématique qu'à la phase de vérification. Si elle peut générer une idée mathématique véritablement nouvelle reste une question ouverte. Mais le fait qu'elle puisse maintenant fonctionner sur un ordinateur portable plutôt que sur un superordinateur est, en soi, un pas significatif vers sa résolution.

Cet article est basé sur les reportages de MIT Technology Review. Lire l'article original.