L’IA de DeepMind résout des problèmes de l’Olympiade internationale de mathématiques à un niveau médaille d’argent

 (deepmind.google)
3 points par GN⁺ 2024-07-26 | 3 commentaires | Partager sur WhatsApp
  • AlphaProof et AlphaGeometry 2 de Google DeepMind ont résolu des problèmes de l’Olympiade internationale de mathématiques
    • AlphaProof : système de raisonnement mathématique fondé sur l’apprentissage par renforcement
    • AlphaGeometry 2 : système amélioré de résolution de problèmes de géométrie
    • Les deux systèmes ont résolu 4 problèmes sur 6 à l’Olympiade internationale de mathématiques (IMO) de cette année, atteignant un niveau équivalent à une médaille d’argent

Les avancées de l’IA dans la résolution de problèmes mathématiques complexes

  • Présentation de l’IMO

    • Le plus ancien et le plus prestigieux concours annuel de mathématiques pour les jeunes, organisé depuis 1959
    • Les problèmes du concours portent sur l’algèbre, la combinatoire, la géométrie, la théorie des nombres, etc.
    • De nombreux lauréats de la médaille Fields sont issus de l’IMO

  • Le défi IMO pour les systèmes d’IA

    • AlphaProof et AlphaGeometry 2 ont résolu les problèmes de l’IMO de cette année
    • Les problèmes ont été notés selon les règles officielles du concours
    • AlphaProof a résolu 2 problèmes d’algèbre et 1 problème de théorie des nombres
    • AlphaGeometry 2 a résolu 1 problème de géométrie
    • Les 2 problèmes de combinatoire n’ont pas été résolus
    • Le score total a été de 28 points sur 42, soit un niveau équivalent à une médaille d’argent

AlphaProof : une approche de raisonnement formel

  • Fonctionnement d’AlphaProof

    • Prouve des énoncés mathématiques dans le langage formel Lean
    • Combine un modèle de langage préentraîné et l’algorithme d’apprentissage par renforcement AlphaZero
    • Traduit les problèmes en langage naturel en énoncés formels pour résoudre des problèmes de niveaux de difficulté variés
    • Lorsqu’un problème lui est présenté, AlphaProof génère des candidats de solution puis les prouve ou les réfute
    • Les résultats prouvés renforcent le modèle de langage d’AlphaProof, améliorant sa capacité à résoudre des problèmes plus difficiles

  • Processus d’entraînement

    • Entraîné en prouvant ou réfutant des millions de problèmes
    • Pendant la compétition aussi, une boucle d’entraînement a été appliquée pour prouver des variantes des problèmes

AlphaGeometry 2, encore plus compétitif

  • Les améliorations d’AlphaGeometry 2

    • Modèle de langage basé sur Gemini et système hybride neuro-symbolique
    • Entraîné avec 10 fois plus de données synthétiques que la version précédente
    • Amélioration de la vitesse et de la précision dans la résolution de problèmes de géométrie
    • Utilise un mécanisme de partage des connaissances lors de la résolution de nouveaux problèmes

  • Résultats à l’IMO 2024

    • A résolu 83 % des problèmes de géométrie de l’IMO des 25 dernières années
    • A résolu le problème 4 en 19 secondes lors de la compétition de cette année

Une nouvelle frontière pour le raisonnement mathématique

  • Expérimentation d’un système de raisonnement en langage naturel

    • Expérimentation d’un système de raisonnement en langage naturel basé sur Gemini
    • Capable de résoudre des problèmes sans les traduire en langage formel
    • Exploration des possibilités de combinaison avec d’autres systèmes d’IA

  • Perspectives d’avenir

    • Les mathématiciens pourraient collaborer avec des outils d’IA pour explorer de nouvelles hypothèses, tester de nouvelles approches de résolution et raccourcir le processus de démonstration
    • Des systèmes d’IA comme Gemini améliorent les capacités en mathématiques et en raisonnement général

Le résumé de GN⁺

  • AlphaProof et AlphaGeometry 2 montrent le potentiel de l’IA en raisonnement mathématique
  • Leur performance de niveau médaille d’argent à l’Olympiade internationale de mathématiques démontre les capacités de l’IA à résoudre des problèmes mathématiques
  • Ils ouvrent la voie à une collaboration entre mathématiciens et IA pour explorer de nouvelles approches de résolution de problèmes
  • Parmi les projets aux fonctionnalités similaires figurent des modèles de traitement du langage naturel comme GPT-3 d’OpenAI

À lire aussi

3 commentaires

 
chabulhwi 2024-07-26

Plus il y aura de mathématiciens contribuant au développement de bibliothèques de mathématiques formelles, plus il sera facile de créer une IA mathématique performante. À ma connaissance, il y a actuellement trois Coréens qui transfèrent vers Mathlib, la bibliothèque mathématique de Lean, des théories mathématiques qu’ils ont eux-mêmes formalisées dans le langage de l’assistant de preuve Lean.

L’an dernier, j’ai participé un peu au travail de portage de Mathlib de Lean 3 vers Lean 4, et cette année, j’ai démontré un théorème non résolu de la bibliothèque Batteries de Lean 4.
 
GN⁺ 2024-07-26
Avis Hacker News

  • Premier avis

    • Très enthousiaste à propos de ce projet, mais il n’est pas clair dans quelle mesure l’ordinateur a contribué au processus de traduction des problèmes de maths en langage formel
    • Dans les solutions téléchargeables, on ne distingue pas clairement ce qui a été décidé par un humain lors de la traduction et ce qui a été trouvé par l’ordinateur

  • Deuxième avis

    • À l’IMO, des médailles sont attribuées à 50 % des participants, avec un ratio or, argent, bronze de 1:2:3
    • Il est impressionnant que l’IA ait mieux réussi que 75 % des élèves
    • Cependant, le temps pris par l’IA pour résoudre les problèmes diffère du temps accordé aux élèves pendant l’épreuve, donc une comparaison directe n’est pas appropriée

  • Troisième avis

    • AlphaGeometry a résolu des problèmes limités, mais cette méthode aura cette fois un impact plus large sur les mathématiques
    • Un pipeline est en cours d’implémentation pour convertir des mathématiques en langage naturel en mathématiques formalisées, et il pourrait aussi apprendre à construire des théories de base
    • C’est le Graal des assistants de preuve, et cela aidera les humains à formaliser les mathématiques de manière plus naturelle

  • Quatrième avis

    • Si le système a mis 3 jours à résoudre le problème, cela ne diffère guère d’une simple recherche par force brute
    • Ce n’est pas un véritable raisonnement

  • Cinquième avis

    • Utilise Lean
    • C’est important non seulement pour les problèmes de maths, mais aussi plus généralement pour éviter des résultats dénués de sens
    • Espère que davantage de personnes écriront des types dans des systèmes comme Lean

  • Sixième avis

    • Envie les personnes qui participent à ce projet
    • Faire progresser une technologie de pointe doit être très amusant et gratifiant

  • Septième avis

    • Les meilleures discussions ont lieu sur le chat Zulip de LeanProver

  • Huitième avis

    • Tim Gowers, médaillé Fields, propose un bon aperçu qui explique les principales réserves et fournit du contexte

  • Neuvième avis

    • La démonstration de théorèmes est un jeu solo avec un espace de recherche extrêmement vaste
    • Les plus grands contributeurs à AlphaProof sont les développeurs de Lean et de Mathlib
    • Le manque de formalisation dans les articles de mathématiques a freiné les tentatives d’automatisation

  • Dixième avis

    • Les machines sont meilleures que les humains aux échecs depuis des décennies
    • Pourtant, les gens regardent toujours Magnus Carlsen
    • Les humains s’intéressent aux actions d’autres humains
    • Les machines n’intéressent les humains que dans la mesure où elles leur sont utiles
 
chabulhwi 2024-07-26

  • Septième avis

    • Les meilleures discussions ont lieu sur le chat Zulip de LeanProver

Ces meilleures discussions peuvent être consultées ici : https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learnin…