nouvelles

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Nouveau rapport de sagesse

Editeur : Service éditorial

[Introduction à la nouvelle sagesse] Tout à l’heure, le dernier modèle mathématique de Google DeepMind a remporté la médaille d’argent de l’Olympiade mathématique de l’OMI ! Non seulement il a résolu 4 des 6 questions avec des scores parfaits, à seulement 1 point de la médaille d'or, mais il n'a également fallu que 19 secondes pour résoudre la 4ème question. La qualité et la rapidité de résolution du problème ont stupéfié les juges humains qui ont marqué. .

L'IA a remporté la médaille d'argent de l'Olympiade mathématique de l'OMI !

Tout à l’heure, Google DeepMind a annoncé que les vraies questions de l’Olympiade mathématique internationale de cette année étaient produites par son propre système d’IA.

Parmi eux, AI a non seulement répondu avec succès à 4 des 6 questions, mais a également reçu la note maximale pour chaque question, ce qui équivaut au score le plus élevé d'une médaille d'argent - 28 points.

Ce résultat n'est qu'à 1 point de la médaille d'or !

Parmi 609 concurrents, seuls 58 ont remporté des médailles d'or.

Dans le cadre du concours officiel, les participants humains soumettront leurs réponses en deux sessions, avec un délai de 4,5 heures à chaque fois.

Fait intéressant, il n'a fallu que quelques minutes à l'IA pour répondre à l'une des questions, mais les questions restantes ont pris trois jours complets, ce qui peut être considéré comme un délai d'attente important.

Cette fois-ci, deux systèmes d'IA ont apporté de grandes contributions : AlphaProof et AlphaGeometry 2.

Point important : 2024 IMO n'est pas dans les données d'entraînement de ces deux IA.

Scott Wu, l'un des fondateurs de l'ingénieur en IA Devin (trois fois médaillé d'or de l'IOI), a déploré : « Quand j'étais enfant, les Olympiades étaient tout ce que j'avais. Je n'aurais jamais pensé qu'à peine 10 ans plus tard, elles seraient remplacées par l'IA. . résolu".

Le concours de l'OMI de cette année comporte six questions portant sur l'algèbre, la combinatoire, la géométrie et la théorie des nombres. Six chemins font quatre, ressentons le niveau de l'IA——

La capacité de raisonnement mathématique de l’IA choque un professeur

Nous savons tous que l’IA précédente était limitée dans la résolution de problèmes mathématiques en raison des limites des capacités de raisonnement et des données d’entraînement.

Les deux joueurs IA qui sont apparus ensemble aujourd'hui ont brisé cette limitation. ils sont respectivement...

- AlphaProof, un nouveau système de raisonnement mathématique formel basé sur l'apprentissage par renforcement

- AlphaGeometry 2, le système de résolution de problèmes géométriques de deuxième génération

Les réponses données par les deux IA ont été notées selon les règles par les célèbres mathématiciens, le professeur Timothy Gowers (médaillé d'or de l'OMI et médaillé Fields) et le Dr Joseph Myers (deux fois médaillé d'or de l'OMI et président du comité de sélection des questions de l'OMI 2024). .

En fin de compte, AlphaProof a résolu correctement deux questions algébriques et une question de théorie des nombres. L'une des questions les plus difficiles a été résolue par seulement 5 participants humains à l'OMI de cette année ;

Il n’y a que deux problèmes de mathématiques combinatoires qui n’ont pas été résolus.

Le professeur Timothy Gowers a également été profondément choqué pendant le processus de notation——

Qu'un programme puisse proposer une solution aussi non évidente est vraiment impressionnant et bien au-delà de ce à quoi je m'attendais compte tenu de l'état actuel de la technique.

AlphaProof

AlphaProof est un système capable de prouver des propositions mathématiques dans le langage formel Lean.

Il combine un grand modèle de langage pré-entraîné avec l'algorithme d'apprentissage par renforcement AlphaZero, qui a appris tout seul à maîtriser les échecs, le shogi et le Go.

Un avantage clé des langages formels est qu’ils peuvent être formellement vérifiés pour les preuves impliquant un raisonnement mathématique. Cependant, leur application dans l’apprentissage automatique a été limitée en raison de la quantité très limitée de données pertinentes écrites par les humains.

En revanche, les approches basées sur le langage naturel, même si elles ont accès à de grandes quantités de données, peuvent produire des étapes et des solutions de raisonnement intermédiaires plausibles, mais incorrectes.

Pour surmonter ce problème, les chercheurs de Google DeepMind ont affiné le modèle Gemini pour traduire automatiquement les énoncés de problèmes en langage naturel en énoncés formels, créant ainsi une vaste bibliothèque contenant des problèmes formels de difficulté variable, établissant ainsi un pont entre les deux domaines complémentaires.

Lors de la résolution d'un problème, AlphaProof génère des solutions candidates et les prouve ou les infirme en recherchant des étapes de preuve possibles dans Lean.

Chaque preuve trouvée et vérifiée est utilisée pour renforcer le modèle de langage d'AlphaProof afin qu'il puisse résoudre des problèmes plus difficiles à l'avenir.

Pour former AlphaProof, les chercheurs ont prouvé ou réfuté des millions de questions couvrant un large éventail de difficultés et de domaines mathématiques au cours des semaines précédant et pendant le concours.

Pendant la compétition, ils ont également appliqué une boucle d'entraînement en renforçant les preuves sur des variations auto-générées du problème de compétition jusqu'à ce qu'une solution complète soit trouvée.

Infographie du flux de la boucle d'entraînement par apprentissage par renforcement AlphaProof : environ un million de problèmes mathématiques informels sont traduits par le réseau formel en un langage mathématique formel ; le réseau de solveurs s'entraîne ensuite progressivement à l'aide de l'algorithme AlphaZero en recherchant des preuves ou des réfutations de ces problèmes , pour résoudre des problèmes plus difficiles

AlphaGéométrie 2

AlphaGeometry 2, la version améliorée d'AlphaGeometry, est un système hybride neuronal-symbolique formé à partir de zéro sur la base du modèle de langage de Gemini.

Basé sur un ordre de grandeur de données synthétiques supérieur à celui de la génération précédente, il peut résoudre des problèmes géométriques plus difficiles, notamment des équations impliquant le mouvement des objets, les angles, les proportions, les distances, etc.

De plus, il dispose d’un moteur symbolique deux fois plus rapide que son prédécesseur. Lorsque de nouveaux problèmes sont rencontrés, il utilise un nouveau mécanisme de partage des connaissances qui permet des combinaisons avancées de différents arbres de recherche pour résoudre des problèmes plus complexes.

Avant de participer à l'OMI cette année, AlphaGeometry 2 avait déjà obtenu beaucoup de succès : elle pouvait résoudre 83 % des problèmes de géométrie de l'OMI au cours des 25 dernières années, alors que la première génération ne pouvait en résoudre que 53 %.

Dans cette OMI, la vitesse d'AlphaGeometry 2 a choqué tout le monde : dans les 19 secondes suivant la réception de la question formelle, il a résolu la question 4 !

La question 4 nécessite de prouver que la somme de ∠KIL et ∠XPY est égale à 180°. AlphaGeometry 2 recommande de construire un point E sur la droite BI tel que ∠AEB=90°.Le point E aide à déterminer le milieu L de AB, formant de nombreuses paires de triangles similaires, tels que ABE ~ YBI et ALE ~ IPC, prouvant ainsi la conclusion

Processus de résolution de problèmes d'IA

Il convient de mentionner que ces questions seront d’abord traduites manuellement en langage mathématique formel avant d’être soumises à l’IA.
P1

De manière générale, la première question (P1) de chaque test OMI est relativement simple.

Les internautes ont déclaré : « P1 ne nécessite que des connaissances en mathématiques au lycée, et les joueurs humains le complètent généralement en 60 minutes. »

La première question de l'OMI 2024 examine principalement les propriétés du nombre réel α et nécessite de trouver un nombre réel α qui satisfait certaines conditions.

AI a donné la bonne réponse : α est un nombre entier pair. Alors, quelle est la réponse exacte à cette question ?

Dans la première étape de résolution du problème, l’IA a d’abord donné un théorème selon lequel les ensembles gauche et droit sont égaux.

L'ensemble de gauche représente que tous les nombres réels α qui remplissent les conditions, pour tout entier positif n, n peuvent diviser ⌊i*α⌋ de 1 à n ; l'ensemble de droite représente qu'il existe un entier k, k est un nombre pair, et le nombre réel α est égal à k.

La preuve suivante est divisée en deux directions.

Montrez d’abord que l’ensemble de droite est un sous-ensemble (direction simple) de l’ensemble de gauche.

Ensuite, prouver que l’ensemble de gauche est un sous-ensemble de l’ensemble de droite (direction difficile).

Jusqu'à la fin du code, l'IA a proposé une équation clé ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋), en utilisant l'équation pour prouver que α doit être un nombre pair.

Enfin, DeepMind a résumé les trois axiomes sur lesquels l'IA s'appuie dans le processus de résolution de problèmes : propext, Classical.choice et Quot.sound.

Voici le processus complet de résolution de problèmes de P1 : https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

P2

La deuxième question examine la relation entre la paire d’entiers positifs (a, b), qui implique la propriété du plus grand diviseur commun.

La réponse résolue par l’IA est :

Le théorème est que pour une paire d’entiers positifs (a, b) qui satisfont certaines conditions, son ensemble ne peut contenir que (1,1).

Dans le processus de résolution de problèmes suivant, la stratégie de preuve adoptée par l’IA consiste d’abord à prouver que (1,1) satisfait aux conditions données, puis à prouver que c’est la seule solution.

Montrer que (1,1) est la solution finale, en utilisant g=2, N=3.

Montrer que si (a,b) est la solution, alors ab+1 doit diviser g.

Dans ce processus, l'IA a utilisé le théorème d'Euler et les propriétés des opérations modulaires pour raisonner.

Enfin, prouvez que a=b=1 est la seule solution possible.

Voici le processus complet de résolution de problèmes de P2 : https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

P4

P4 est une question de preuve géométrique qui nécessite de prouver une relation d'angle géométrique spécifique.

Comme mentionné ci-dessus, AlphaGeometry 2 a réalisé cette opération en 19 secondes, établissant ainsi un nouveau record.

En fonction de la solution donnée, comme avec l'AlphaGeometry de première génération, les points auxiliaires de toutes les solutions sont automatiquement générés par le modèle de langage.

Dans la preuve, tout suivi d'angle utilise l'élimination gaussienne, et d(AB)−d(CD) est égal à l'angle directionnel de AB à CD (modulo π).

Au cours du processus de résolution de problèmes, l’IA marquera manuellement les paires de triangles similaires et de triangles congruents (marqués en rouge).

Ensuite, il y a les étapes pour résoudre le problème d’AlphaGeometry, qui est complété en utilisant la « méthode de recontradiction ».

Utilisez d’abord Lean pour formaliser les propositions à prouver et visualiser la construction géométrique.

Les étapes clés de la preuve sont les suivantes.

Voir l'image ci-dessous pour le processus complet de résolution de problèmes : https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

P6

La sixième question de l'OMI est le « patron ultime », qui explore les propriétés des fonctions et nécessite de prouver des conclusions spécifiques sur les nombres rationnels.

L'IA résout, c = 2.

Examinons d'abord l'énoncé du théorème, qui définit les propriétés de la « fonction aquaesulienne » et déclare que pour toutes ces fonctions, l'ensemble de valeurs de f(r)+f(-r) a au plus 2 éléments.

La stratégie de preuve consiste d'abord à prouver que pour toute fonction aquaesulienne, l'ensemble de valeurs de f(r)+f(-r) a au plus 2 éléments. Construisez ensuite une fonction aquaesulienne spécifique pour que f(r)+f(-r) ait exactement 2 valeurs différentes.

Montrer que lorsque f(0)=0, f(x)+f(-x) prend au plus deux valeurs différentes, et prouver qu'il n'existe pas de fonction aquaesulienne f(0)≠0.

Construisez la fonction f(x)=-x+2⌈x⌉ et prouvez que c'est une fonction aquaesulienne.

Enfin, prouvez que pour cette fonction, f(-1)+f(1) =0 et f(1/2)+f(-1/2)=2 sont deux valeurs différentes.

Voici le processus complet de résolution de problèmes : https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

Vous pouvez répondre aux questions mathématiques de l'Olympiade, mais pouvez-vous dire laquelle est la plus grande, 9,11 ou 9,9 ?

Andrew Gao, chercheur à l'Université de Stanford et à Sequoia, a affirmé l'importance de cette percée de l'IA——

L'essentiel est que les dernières questions du test de l'OMI ne sont pas incluses dans l'ensemble de formation. C’est important car cela montre que l’IA peut gérer de nouveaux problèmes invisibles.

De plus, les problèmes géométriques résolus avec succès par l’IA ont toujours été considérés comme extrêmement difficiles en raison de la nature de l’espace impliqué (nécessitant une pensée intuitive et une imagination spatiale).

Jim Fan, scientifique principal chez Nvidia, a publié un long article disant que les grands modèles sont des existences mystérieuses——

Ils peuvent remporter des médailles d'argent aux Olympiades de mathématiques et faire fréquemment des erreurs sur des questions telles que « Quel nombre est le plus grand, 9,11 ou 9,9 ? »

Non seulement les Gémeaux, mais aussi GPT-4o, Claude-3.5 et Llama-3 ne peuvent pas répondre correctement à 100 %.

En entraînant des modèles d’IA, nous explorons de vastes domaines au-delà de notre propre intelligence.Ce faisant, nous avons découvert une zone très étrange : une exoplanète qui ressemble à la Terre mais qui regorge de vallées étranges.

Cela semble déraisonnable, mais nous pouvons l'expliquer en utilisant la distribution des données d'entraînement :

AlphaProof et AlphaGeometry 2 sont formés sur des preuves formelles et des moteurs symboliques spécifiques à un domaine. Dans une certaine mesure, ils sont plus efficaces pour résoudre les problèmes spécialisés des Olympiades, même s'ils reposent sur un LLM à usage général. L'ensemble de formation de GPT-4o est mélangé à une grande quantité de données de code GitHub, qui peuvent dépasser de loin les données mathématiques. Parmi les versions du logiciel, "v9.11 > v9.9" peut sérieusement fausser la répartition des données. Cette erreur est donc compréhensible dans une certaine mesure.

Le responsable des développeurs de Google a déclaré que les modèles capables de résoudre des problèmes mathématiques et physiques difficiles constituent la voie clé vers l'AGI, et aujourd'hui nous avons franchi une nouvelle étape sur cette voie.

D'autres internautes ont déclaré qu'il y avait trop d'informations cette semaine.

Les références:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://x.com/DrJimFan/status/1816521330298356181