AlphaGeometry, un système d’IA de niveau Olympiades pour la géométrie

 (deepmind.google)
1 points par GN⁺ 2024-01-18 | 1 commentaires | Partager sur WhatsApp
  • Alors que l’Olympiade internationale de mathématiques est devenue un banc d’essai du raisonnement mathématique par IA, AlphaGeometry a résolu 25 problèmes de géométrie sur 30 dans le temps imparti, se rapprochant de la moyenne de 25,9 des médaillés d’or humains
  • Le cœur du système est la combinaison d’un modèle de langage neuronal et d’un moteur de raisonnement symbolique fondé sur des règles, qui traite dans une même boucle les propositions de constructions intuitives et la vérification logique formelle
  • 100 millions d’exemples synthétiques uniques, créés sans démonstrations humaines, ont réduit le goulot d’étranglement de l’apprentissage ; parmi eux, 9 millions incluent des constructions auxiliaires nécessaires aux preuves
  • Toutes les solutions d’Olympiades ont été vérifiées par ordinateur ; Evan Chen estime que les sorties sont vérifiables par machine tout en restant lisibles par l’humain, et qu’elles suivent les règles classiques de géométrie utilisées par les élèves
  • Comme, dans une session de l’IMO, seuls 2 problèmes sur 6 en moyenne relèvent de la géométrie, le champ d’application est limité, mais AlphaGeometry devient le premier modèle d’IA capable, avec ses seules performances en géométrie, de dépasser le seuil de la médaille de bronze aux IMO 2000 et 2015

Performances sur le benchmark de géométrie de l’IMO

  • Publié dans Nature, AlphaGeometry résout des problèmes de géométrie complexes à un niveau proche de celui des médaillés d’or humains aux Olympiades
  • Le benchmark se compose de 30 problèmes de géométrie IMO-AG-30, tirés des Olympiades de 2000 à 2022
    • AlphaGeometry : 25 résolus dans le temps imparti
    • Méthode de Wu, meilleure approche précédente : 10 résolus
    • Moyenne des médaillés d’or humains : 25,9 résolus
  • Google DeepMind a publié en open source le code et le modèle d’AlphaGeometry

Architecture du système neuro-symbolique

  • AlphaGeometry est un système neuro-symbolique : un modèle de langage neuronal et un moteur de raisonnement symbolique travaillent ensemble pour trouver des preuves de théorèmes de géométrie complexes
  • Le modèle de langage identifie rapidement, dans les données, des motifs et des relations générales afin de prédire des constructions potentiellement utiles
    • Il peut toutefois manquer de rigueur dans le raisonnement ou de capacité à expliquer ses décisions
  • Le moteur de raisonnement symbolique parvient à des conclusions en suivant une logique formelle et des règles explicites
    • Il est explicable et rationnel, mais peut être lent et peu flexible lorsqu’il traite seul de grands problèmes
  • En combinant les deux composants, le modèle de langage propose des éléments auxiliaires comme de nouveaux points, droites ou cercles, puis le moteur de raisonnement en déduit des conclusions supplémentaires sur la figure

Une boucle de résolution pour trouver les constructions auxiliaires

  • Les problèmes de géométrie d’Olympiades ne se résolvent pas toujours directement à partir de la figure donnée : il faut parfois ajouter de nouveaux éléments géométriques nécessaires à la solution
  • Le processus de résolution d’AlphaGeometry alterne raisonnement symbolique et propositions du modèle de langage
    • À partir de la figure donnée et des hypothèses du théorème, le moteur de raisonnement symbolique déduit de nouvelles propositions
    • S’il ne trouve pas la solution ou ne peut plus générer de nouvelles propositions, le modèle de langage ajoute un élément auxiliaire susceptible d’être utile
    • L’élément ajouté ouvre de nouvelles pistes au moteur de raisonnement, et le processus se répète jusqu’à trouver la solution
  • Pour le problème 3 de l’Olympiade internationale de mathématiques 2015, la solution d’AlphaGeometry se compose de 109 étapes logiques

Génération de 100 millions de données synthétiques

  • La géométrie repose sur la compréhension de l’espace, des distances, des formes et des positions relatives, et sert de base à de nombreux domaines comme l’art, l’architecture et l’ingénierie
  • La méthode de génération de données synthétiques d’AlphaGeometry imite à grande échelle la manière dont une personne observe une figure et s’appuie sur ses connaissances existantes pour trouver de nouvelles propriétés et relations géométriques
  • Le système génère 1 milliard de figures aléatoires grâce à un calcul fortement parallélisé
    • Il déduit minutieusement toutes les relations entre les points et les droites de chaque figure
    • Il trouve toutes les preuves contenues dans chaque figure
    • Il remonte ensuite à rebours pour déterminer quels éléments supplémentaires sont nécessaires pour parvenir à ces preuves
  • Ce processus est appelé déduction symbolique et traceback (symbolic deduction and traceback)
  • L’immense réservoir de données est filtré afin d’exclure les exemples similaires, pour aboutir à 100 millions d’exemples d’apprentissage uniques de difficulté variée
    • Parmi eux, 9 millions sont des cas avec ajout d’éléments auxiliaires
    • Le modèle de langage apprend sur de nombreux exemples où une construction auxiliaire mène à une preuve, ce qui lui permet de proposer de nouvelles constructions même pour des problèmes d’Olympiades

Vérifiabilité et limites d’application

  • Toutes les solutions de problèmes d’Olympiades fournies par AlphaGeometry ont été contrôlées et vérifiées par ordinateur
  • Les résultats ont été comparés aux méthodes d’IA précédentes et aux performances humaines aux Olympiades
  • Evan Chen, coach en mathématiques et ancien médaillé d’or aux Olympiades, a évalué certaines solutions
    • Les sorties d’AlphaGeometry sont vérifiables et propres
    • Les solutions d’IA à d’anciens problèmes de concours fondés sur des preuves pouvaient auparavant être correctes ou incorrectes, et nécessiter une vérification humaine
    • Les solutions d’AlphaGeometry ont une structure vérifiable par machine tout en restant lisibles par l’humain
    • Plutôt que de forcer de vastes calculs algébriques via un système de coordonnées, elles utilisent, comme les élèves, des règles classiques de géométrie telles que les angles et les triangles semblables
  • Une session de l’IMO comprend 6 problèmes, dont seulement 2 en général sont centrés sur la géométrie
    • AlphaGeometry ne s’applique donc qu’à environ un tiers des problèmes d’une session
    • Il devient néanmoins le premier modèle d’IA capable de franchir, avec ses seules compétences en géométrie, le seuil de la médaille de bronze aux IMO 2000 et 2015

Extension vers l’IA de raisonnement mathématique

  • AlphaGeometry montre que la capacité de l’IA à raisonner logiquement et à découvrir et vérifier de nouvelles connaissances progresse
  • Résoudre des problèmes de géométrie de niveau Olympiades constitue une étape importante vers un raisonnement mathématique plus profond et des systèmes d’IA généralistes plus avancés
  • L’approche consistant à entraîner une IA depuis zéro avec des données synthétiques à grande échelle pourrait influencer, au-delà des mathématiques, la manière dont de nouvelles connaissances sont découvertes en science et en IA
  • AlphaGeometry s’inscrit dans le flux de travaux de Google DeepMind et Google Research sur l’IA de raisonnement mathématique
  • L’objectif à long terme est de généraliser à plusieurs domaines des mathématiques, de développer la résolution de problèmes et le raisonnement sophistiqués nécessaires aux systèmes d’IA généralistes, et de créer des systèmes d’IA qui repoussent les frontières du savoir humain

À lire aussi

1 commentaires

 
GN⁺ 2024-01-18
Avis de Hacker News

  • En tant qu’ancien auteur de problèmes pour des concours comme l’IMO, j’ai trouvé cet article très intéressant. En même temps, je pense que le premier sujet à tomber face à l’IA — c’est-à-dire face à un index intelligent des connaissances et des modes de raisonnement — ne pouvait être que la géométrie.
    Parmi les sujets des olympiades de mathématiques, les problèmes de géométrie sont généralement les plus « mécaniques ». Si l’on peut exprimer un problème en coordonnées, par exemple en coordonnées XY ou dans le plan complexe, on obtient un ensemble fini d’étapes qu’un ordinateur peut utiliser pour trouver une solution. Bien sûr, sur place à l’IMO, les limites de temps et les erreurs humaines empêchent cela d’être pratique. Autrefois, j’utilisais WolframAlpha de cette manière pour vérifier les démonstrations de problèmes de géométrie et de conjectures que j’avais créés.
    L’algèbre, en particulier les inégalités, est similaire : en poussant fortement le calcul, on obtient souvent une réponse.
    Les domaines où j’aimerais voir les systèmes intelligents réellement progresser sont la théorie des nombres et la combinatoire. L’espace de recherche y est beaucoup plus complexe, et il faut souvent démontrer que quelque chose est impossible. Ces problèmes sont difficiles à résoudre par calcul brut.

    • En tant que personne qui résout ces problèmes, merci d’abord. Même des décennies après avoir quitté le lycée, il m’arrive encore d’y prendre plaisir.
      Je suis d’accord pour dire que la géométrie serait la première. D’après ce que j’ai vu ici, ce n’est pas de la « force brute » au sens où l’on s’appuierait sur la géométrie algébrique, les vecteurs ou les solutions par nombres complexes, mais c’est proche d’une recherche exhaustive au sens où l’on cherche systématiquement des constructions auxiliaires « intéressantes ».
      La géométrie a toujours été ma pire matière, mais j’ai toujours eu l’impression qu’une fois la bonne construction donnée, le problème devenait beaucoup plus simple. En revanche, je n’ai jamais acquis l’intuition permettant de trouver rapidement cette construction. Cette IA ne semble pas non plus posséder une telle intuition, mais elle peut en produire beaucoup plus vite. Les candidats possibles — droites perpendiculaires, parallèles, bissectrices — sont au bout du compte limités, et on peut les évaluer de façon assez mécanique, par exemple en développant tous les angles et rapports ou en essayant la puissance d’un point.
      C’est très impressionnant, mais au sens « moteur contre IA », cela ressemble à DeepMind:Kasparov::AlphaGeo:Terry Tao.
      Je suis d’accord pour dire que l’algèbre a de bonnes chances d’être la suivante. Comme en géométrie, il suffit généralement de trouver une, deux ou trois substitutions ingénieuses, et les choix sont limités.
      Certains problèmes de combinatoire peuvent aussi convenir à cette stratégie de recherche. Par exemple, les problèmes où l’on compte le même objet de deux façons. Mais c’est un pont plus lointain, et cela ne couvrirait qu’une partie de l’ensemble des problèmes.
      La théorie des nombres me semble être la dernière frontière avant d’atteindre le score parfait de 42 points.
    • J’aime cette attitude positive face à ces progrès. Je me demande si la possibilité qu’une très grande compétence en mathématiques puisse bientôt être rattrapée par les machines te donne un sentiment de perte. Ou bien penses-tu que cela ne risque pas d’arriver avant un bon moment ?
    • Je suis curieux de savoir comment on accède à ce rôle d’auteur de problèmes. Y a-t-il une sorte de procédure de candidature ?
      Une fois qu’on a vérifié qu’ils sont résolubles, je me demande aussi comment sont choisis les problèmes précis qui entreront dans l’ensemble final. Est-ce un vote, ou un autre mode d’évaluation ?
    • Au début, je pensais que les inégalités à trois variables tomberaient en premier. Parce qu’il y a moins d’ambiguïté sur ce qui compte comme démonstration. Mais je ne savais pas que le problème situé plus loin avait déjà été résolu en 2000 (http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf).
      Quelqu’un devrait transformer la géométrie synthétique en jeu d’aventure. On pourrait utiliser un langage de rédaction de preuves plus simple que Lean, et en faire quelque chose de visuellement agréable.

  • Si j’ai bien lu l’article, ça ressemble à un vrai travail. C’est bien plus légitime que l’article de DeepMind sur les maths en IA qui, le mois dernier, avait été présenté à tort comme ayant résolu un problème de recherche ouvert en mathématiques. Cela dit, la différence entre cette architecture et ce qu’on entend généralement par raisonnement automatique/intelligence est assez frappante.
    D’après ce que j’ai compris, ils entraînent un Transformer sur des millions de théorèmes de géométrie élémentaire, puis l’utilisent pour explorer brutalement des preuves. Le contexte de la géométrie élémentaire rend la structure nécessairement élémentaire, et le vrai/faux peut être décidé symboliquement assez facilement. Si la recherche brute échoue, ils ajoutent au hasard des constructions géométriques auxiliaires, comme l’ajout d’un milieu, puis regardent si ces éléments supplémentaires permettent une recherche.
    Édition : comme l’a corrigé Imnimo, j’avais compris à l’envers. La recherche brute est une recherche purement exhaustive, et le Transformer sert à prédire quelles constructions auxiliaires ajouter.
    De plus, ce n’est pas mentionné dans le billet de blog, mais l’énoncé réel des problèmes a aussi dû être modifié/adapté. Par exemple, un énoncé original du type « Soient AH1, BH2, CH3 les hauteurs du triangle ABC… » a été transformé en une liste de définitions beaucoup plus explicites, du genre « Soit ABC un triangle. L’IA définit un point I tel que AI soit la bissectrice de l’angle BAC et CI la bissectrice de l’angle ACB… », et se termine par une forme comme « prouver que T1I=IZ ».

    • Je pense que cette description n’est pas tout à fait correcte. La recherche exhaustive n’est pas effectuée par le Transformer, mais par le solveur symbolique. Quand il n’y a plus de nouvelles inférences possibles, on demande au Transformer de proposer des constructions auxiliaires possibles ; elles ne sont pas ajoutées au hasard.
    • Je ne vois pas pourquoi ce serait éloigné de l’idée habituelle du raisonnement automatique/de l’intelligence. Le raisonnement est fondamentalement un problème de recherche.
      Le processus décrit est exactement celui qu’emploient les humains. On formule une hypothèse qui semble utile, puis on déroule mécaniquement les détails. Si on est bloqué, on fait une autre hypothèse. Au bout du compte, cela ressemble à l’exploration d’un arbre.
      Les gens avaient déjà compris ce processus en 1955, et avaient même construit un prototype fonctionnel capable de démontrer des théorèmes : https://en.wikipedia.org/wiki/Logic_Theorist L’essentiel repose sur l’utilisation de bonnes heuristiques. Les réseaux neuronaux peuvent extraire des heuristiques à partir des données, donc ils ont du sens ici.
      Je suis curieux de savoir ce que vous entendez par l’idée habituelle du « raisonnement automatique ». Un dispositif magique qui résout n’importe quel problème en une seule passe linéaire ?
    • La méthode consistant à « ajouter des constructions géométriques auxiliaires, comme un milieu, quand la recherche exhaustive échoue, puis voir si ces éléments supplémentaires permettent d’avancer » correspondait exactement à la géométrie qu’on m’a enseignée à l’école, et je la détestais vraiment.
      Ce n’est qu’en arrivant en fac de maths que j’ai appris à la faire correctement et que j’ai pu l’apprécier.
    • Utiliser un LLM pour le rôle qui consiste à tracer des lignes auxiliaires est terriblement inefficace. Il est difficile d’imaginer mobiliser autant de machines pour résoudre de simples problèmes d’IMO.
      Le domaine en est encore à ses débuts, et il semble rester beaucoup de travail. La partie recherche devrait être remplacée par un petit réseau neuronal, tandis que la partie raisonnement n’est pas difficile et ne semble pas nécessiter de grande amélioration.
      Il est maintenant temps d’améliorer les performances par auto-jeu. Dans les problèmes de géométrie plane, on peut voir la conclusion à prouver comme un point de la figure, les conditions comme un autre point, et faire en sorte que deux joueurs se déplacent autant que possible l’un vers l’autre tout en partageant des données. On peut ensuite utiliser la contribution de chaque joueur pour améliorer les performances, par analogie avec le calcul victoire/défaite au go.

  • Ce modèle précis ne semble pas facilement généralisable, mais l’approche neuro-symbolique paraît très prometteuse.
    Elle consiste à connecter les outils « système 1 » de plus en plus puissants, qui constituent l’essentiel du machine learning actuel, à des outils « système 2 » structurés, comme la génération de preuves logiques. Le système 2 peut élaborer des plans et vérifier la véracité ou la valeur des sorties.
    Le système 2 avance jusqu’à être bloqué ; quand il l’est, le système 1 fournit une intuition sur la partie de l’espace d’états à examiner ensuite.
    Ici, ils ont exploité le fait qu’on peut générer des preuves par ordinateur pour créer un jeu de données de 100 millions de preuves, ce qui permet un apprentissage autosupervisé à grande échelle. Les domaines symboliques semblent bien se prêter à ce type de génération de données. Même si chaque instance individuelle a peu de valeur, leur accumulation peut permettre un pré-entraînement utile.
    En combinant ces éléments, c’est une approche qui peut aller assez loin.
    Le jalon clé sera de s’affranchir de la nécessité de dépendre d’un domaine formel/symbolique particulier, et de construire un système de pré-entraînement capable de généraliser les compétences apprises dans ce domaine.

    • Il n’est pas nécessaire de tout résoudre d’un coup. Cette approche a le potentiel de transformer à la fois les mathématiques et la programmation, parce qu’elle peut faire passer la vérification formelle d’un outil de niche utilisé ponctuellement à un élément de la boîte à outils générale de tous les praticiens.
      De plus, dans les domaines où elle s’applique, elle résout complètement l’un des problèmes fondamentaux que l’on appelle aujourd’hui « hallucination » dans la vague actuelle de l’IA. Mais cette solution est possible parce qu’il existe un système non IA qui prouve l’exactitude.
      Dans l’ensemble, cette approche n’est pas vraiment nouvelle. En biochimie, on utilise déjà l’IA pour trouver des molécules candidates, puis des expériences physiques pour les valider.
      Les IA de jeux combinatoires utilisent aussi depuis longtemps l’IA comme entrée pour une recherche Monte-Carlo à l’ancienne.
    • Cela ressemble à la possibilité la plus proche d’atteindre une forme d’intelligence artificielle générale.

  • Je suis reconnaissant qu’ils aient publié le code et les poids avec l’article. À ma connaissance, c’est le premier article connu de DeepMind à publier du code d’inférence exécutable et des checkpoints. Je serais heureux d’être corrigé s’il existe des exemples plus anciens.
    Je ne vois pas encore de jeu d’entraînement publié ni de code d’entraînement d’exemple, mais c’est quand même une bonne avancée, car cela donne aux autres chercheurs quelque chose sur quoi construire. Après tout, c’est aussi le but d’un article académique.

    • C’est dommage que le dataset manque aussi. Ils disent avoir créé 100 millions d’exemples synthétiques ; ces exemples ont-ils été générés avec AlphaGeometry ? Où sont le code de filtrage et les entrées initiales utilisés pour produire ces données synthétiques ?
      Sauf erreur de ma part, ils utilisent un modèle t5 ? Il semble au moins utiliser le vocabulaire SentencePiece de t5.
      Je me demande aussi combien de temps GPU a été consacré à l’entraînement de ce modèle, et quels hyperparamètres d’entraînement ont été utilisés.
      Qu’on ne se méprenne pas : ce système est fascinant et montre à quoi devrait ressembler l’ingénierie appliquée. J’aimerais simplement en savoir plus sur les détails d’entraînement, les données initiales et la méthode de génération des données synthétiques.

  • Je suis très curieux de savoir à quelle fréquence le modèle de langage produit des constructions utiles. Il fait sûrement mieux que du hasard, mais je ne sais pas s’il lance des milliers de constructions avant d’en trouver une bonne, ou s’il propose des suggestions utiles à un taux comparable à celui d’un expert humain
    L’article dit : « Comme le processus de décodage du modèle de langage renvoie k séquences différentes décrivant k constructions auxiliaires alternatives, nous effectuons une recherche en faisceau sur ces k options en utilisant le score de chaque faisceau comme fonction de valeur. Cette configuration se parallélise très facilement entre faisceaux, ce qui accélère fortement le calcul lorsqu’on dispose de ressources de calcul parallèles. Dans les expériences, nous utilisons une taille de faisceau k=512, un nombre maximal d’itérations de 16, et un facteur de branchement à chaque nœud, c’est-à-dire une taille de lot de décodage, de 32. »
    Mais je ne comprends pas complètement comment 512 et 16 se traduisent en nombre total de constructions proposées. Ils disent aussi que même en supprimant la taille de faisceau et le nombre maximal d’itérations, les performances ne baissent que dans une certaine mesure. Est-ce que cela signifie que le modèle classe en fait assez bien les constructions utiles tout en haut, et que les milliers de propositions ne sont nécessaires que pour les problèmes les plus difficiles ?

    • À mon avis, on se heurte ici très fortement aux limites du langage et de l’analogie humain-machine
      Mais si l’on essaie quand même, le résumé serait 262 144, à ne pas prendre au pied de la lettre
      La sortie de la fonction de décodage, ce sont des tokens, grosso modo les 3/4 d’un mot, mais supposons simplement 1 mot
      Le nombre de tokens considérés pour chaque token de sortie est beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262,144
      Il suffit de compter le nombre de mots dans l’exemple de solution : https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      La solution compte au total 2 289 tokens, et le nombre total de tokens considérés est 262,144 * 2289 = 600,047,616
      En calculant de force le « nombre de solutions considérées » comme le nombre total de tokens considérés / le nombre total de tokens de la solution, on obtient 262 144. C’est la même valeur que le nombre de tokens vus à chaque étape d’itération, donc ça se tient

  • Il est intéressant que le Transformer utilisé soit petit. D’après l’article, il a été entraîné avec la configuration par défaut de la bibliothèque Meliad : 12 couches, dimension d’embedding 1 024, 8 têtes d’attention, et une couche dense entre attentions de dimension 4 096 avec activation ReLU
    Si l’on exclut les couches d’embedding de l’entrée et de la tête de sortie, l’ensemble du Transformer compte 151 millions de paramètres. Le tokenizer personnalisé a été entraîné avec le mode « word » de SentencePiece, avec une taille de vocabulaire de 757. La longueur maximale de contexte a été limitée à 1 024 tokens, et des embeddings de position relatifs façon T5 ont été utilisés. Comme plus de 90 % des séquences faisaient moins de 200 tokens, du packing de séquences a aussi été utilisé

    • Difficile de dire que c’est petit. En dehors du domaine des LLM, c’est une taille assez courante. Cela correspond par exemple à un modèle de langage, un modèle de traduction ou un modèle acoustique de taille standard. Certains appelleraient même ça grand
    • Ce résultat suggère que, pour peu qu’on puisse les formaliser correctement, il pourrait rester dans les sciences dures d’autres fruits à portée de main que les Transformers peuvent facilement cueillir. Dans ce cas, il ne semble pas que le passage à l’échelle ait été le problème

  • Ce que j’ai vraiment appris de nouveau, c’est que les meilleurs systèmes précédents pouvaient déjà résoudre 10 de ces problèmes. J’avais entendu dire qu’il existait des algorithmes de décision pour les problèmes de géométrie plane, mais je ne savais pas qu’ils étaient pratiques. En cherchant, je suis tombé sur cette référence : http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf

    • Oui. Et la partie non neuronale d’AlphaGeometry, c’est-à-dire les composants de traitement symbolique et d’algèbre linéaire, suffit à elle seule à dépasser l’ancien meilleur niveau. Une part importante du travail a donc aussi porté sur les composants non neuronaux
    • C’est intéressant, mais j’ai l’impression qu’en poussant à fond le calcul en coordonnées barycentriques avec les formules du livre d’Evan Chen, on pourrait résoudre environ 30 % des problèmes de l’IMO même sur un ordinateur portable moderne. Vu que la plupart sont des problèmes de triangles, ça paraît plausible

  • J’étais prêt à me méfier de ce genre de résultat, qui donne souvent des choses du type « ça ne ressemble pas à une preuve humaine », mais j’ai changé d’avis en voyant qu’Evan Chen disait qu’il s’agissait effectivement de preuves propres et lisibles par un humain
    Evan Chen est une figure connue de la communauté des olympiades de mathématiques et l’auteur d’un célèbre livre de géométrie olympique[1], donc cette fois il faut bien reconnaître que la machine a réellement conquis une partie des problèmes de l’IMO
    [1]: https://web.evanchen.cc/geombook.html

    • Cela dit, dans les preuves complètes du matériel supplémentaire[1], il m’a semblé qu’il y avait une erreur dans la preuve de l’IMO P3, Fig1.f et étape 26. Elle dit ∠GMD = ∠GO2D, ce qui est faux à mon avis ; il faudrait plutôt ∠GMD + ∠GO2D = π. J’ai essayé de suivre le raisonnement, mais je n’ai pas réussi à interpréter l’étape 25. Je me suis demandé si cette étape était une hallucination
      Cela dit, l’idée que O2 se trouve sur le cercle des neuf points est correcte
      Édition : je retire ce que j’ai dit. Il semble qu’ils utilisent des angles orientés[2], auquel cas l’énoncé est correct
      [1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      [2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...

  • À ce sujet, https://www.nytimes.com/2024/01/17/science/ai-computers-math... vaut aussi le détour
    Cela vient de https://news.ycombinator.com/item?id=39030186, et ce fil devrait être fusionné ici

  • En lien : https://aimoprize.com/
    Il s’agit d’un prix de 10 millions de dollars décerné aux modèles qui obtiennent de bons résultats à l’IMO