Dans une avancée majeure pour l’intelligence artificielle, une équipe de recherche de l’Université de Pékin a développé un système d’IA capable de résoudre par lui-même des problèmes mathématiques complexes et non résolus. Le système a réussi à s’attaquer à une conjecture algébrique vieille de dix ans, marquant le passage d’une IA en tant que simple assistant à une IA en tant que chercheur autonome.
Briser la conjecture algébrique
Le problème au centre de cette avancée était une conjecture algébrique proposée pour la première fois en 2014 par feu Dan Anderson, ancien professeur à l’Université de l’Iowa. Pendant dix ans, le problème est resté un défi ouvert dans le domaine de l’algèbre commutative.
Contrairement aux modèles d’IA précédents qui nécessitaient un guidage humain constant, ce nouveau système a traité des décennies de littérature mathématique pour résoudre la conjecture et, surtout, a vérifié ses propres découvertes sans intervention humaine. L’ensemble du processus a été achevé dans les 80 heures suivant l’exécution.
L’architecture de l’autonomie : Rethlas et Archonte
Pour surmonter les limites traditionnelles de l’IA en mathématiques, les chercheurs se sont éloignés des grands modèles linguistiques standards (LLM), qui sont souvent sujets aux « hallucinations » ou aux erreurs logiques. Au lieu de cela, ils ont construit un cadre à double agent conçu pour imiter le flux de travail rigoureux des mathématiciens humains :
- L’agent raisonneur (Rethlas) : Ce système agit comme le « penseur ». Il utilise un moteur de recherche de théorèmes appelé Matlas pour explorer diverses stratégies et voies mathématiques pour résoudre un problème.
- L’Agent de Formalisation (Archon) : Une fois qu’une preuve potentielle est trouvée, Archon prend le relais. À l’aide de LeanSearch, il traduit le raisonnement informel dans un format formel et vérifiable par machine.
- Le vérificateur (Lean 4) : Le système utilise Lean 4, un langage de programmation spécialisé et un prouveur de théorèmes interactif, pour garantir que la preuve est mathématiquement solide et exempte d’erreurs.
Pourquoi c’est important : de l’assistance à l’automatisation
Les tendances actuelles de l’IA montrent une poussée massive vers des modèles de formation en mathématiques, mais la plupart sont encore aux prises avec un « écart de rigueur ». Même si les humains peuvent rédiger des preuves, ils peuvent commettre des erreurs ; bien que les LLM puissent générer du texte rapidement, ils manquent souvent de la précision logique requise pour les mathématiques de haut niveau.
Cette étude de l’Université de Pékin comble cette lacune en intégrant le raisonnement en langage naturel à la vérification formelle. Cette double approche garantit que l’IA ne se contente pas de « deviner » une réponse, mais construit une preuve dont l’exactitude peut être mathématiquement prouvée.
En outre, les chercheurs ont noté que l’IA a démontré une capacité unique à effectuer des tâches qui nécessitent généralement une collaboration interdisciplinaire, agissant efficacement comme plusieurs experts travaillant en tandem.
L’avenir de la recherche mathématique
Bien que le système fonctionne de manière autonome, les chercheurs ont noté que l’intervention humaine peut toujours agir comme un accélérateur. Un mathématicien guidant l’agent « Archon » peut accélérer le processus de formalisation, suggérant un avenir où les humains et l’IA travailleront dans une boucle symbiotique à grande vitesse.
“Ce travail fournit un exemple concret de la manière dont la recherche mathématique peut être considérablement automatisée grâce à l’IA”, déclarent les chercheurs.
Conclusion
En combinant le raisonnement avec une vérification formelle rigoureuse, ce nouveau cadre fait passer l’IA au-delà du simple calcul et dans le domaine de la découverte scientifique autonome. Cette avancée ouvre la voie à l’IA pour résoudre des problèmes de plus en plus complexes en mathématiques et dans d’autres domaines scientifiques hautement techniques.
