Forum TI-Planet.org

Certains ont peut-être vu cet article récent du Monde
https://www.lemonde.fr/sciences/article/2024/01/17/une-intelligence-artificielle-fait-ses-preuves-en-maths_6211368_1650684.html
où l'on apprend que Google vient de sortir une IA capable de résoudre des problèmes de géométrie (AlphaGeometry), et utilise en guise de benchmark les problèmes des olympiades de maths (https://www.imo-official.org/problems.aspx) posés depuis 2000. Il y en a une trentaine (30 d'après eux, en fait un peu plus), et ils sont capables d'en résoudre 25, en prétendant être bien meilleurs que les systèmes de calcul formel qui selon eux ne seraient capables que d'en résoudre 4 à 10.
Comme c'est un domaine de prédilection de Xcas, j'ai décidé de relever le défi, et j'ai travaillé là-dessus pendant les 5 derniers jours. Au final Xcas en résoud 31 [Edit 35, re-edit 37, re-re-edit 38, re-re-re-edit 40]. Pour les personnes intéressées, j'ai mis des solutions sur le forum de Xcas https://xcas.univ-grenoble-alpes.fr/forum/viewtopic.php?f=32&t=2891
Vu que le temps de calcul de ces sessions web est de quelques secondes au plus, je me demande si on ne pourrait pas en faire tourner certaines sur calculatrices (sur une Prime G2 ça passerait peut-être!). AlphaGeometry nécessite lui beaucoup plus de ressources, pour certains problèmes il faut plusieurs dizaines de processeurs en parallèle pour le résoudre en moins d'1h30.

C'est intéressant ce sujet.

Mais soit j'ai loupé quelque chose, soit je n'ai pas ce qu'il faut d'affiche sur les sessions en ligne sur mon téléphone (soit les 2).

D'après la page de Google, je comprends que les inputs de leur programme seraient simplement l'énoncé des problèmes, sous forme textuelle + graphique le cas échéant. Puis ça mouline en analysant text+image, puis ça résout, en donnant des étapes, sous formes graphique + textuelle aussi.

Dans les sessions XCas (j'en ai testé 4 ou 5 depuis le forum), est-ce qu'on peut donner un input de la même forme, puis le faire travailler jusqu'à ce qu'il ait compris + résolu le problème, en en donnant donc la solution ? Je n'ai peut être pas compris ce qu'il se passait dans les sessions partagées... je retenterai sur ordinateur (et plusieurs navigateurs, au cas où) demain pour voir si j'y vois plus clair.
Si la réponse est oui, en tout cas, il va falloir frapper à la porte de Google pour leur montrer Même si j'imagine que vu les systèmes mis en place dans leurs R&D à DeepMind, c'est généraliste et plus puissant que certains exemples qu'ils ont pu montrer. Après tout, ils veulent aller plus loin: "Pioneering mathematical reasoning with AI", s'en donnent les moyens, et donc ça va être intéressant. Il ont publié un papier mais je ne l'ai pas encore regardé. Ça doit être rempli d'infos techniques intéressantes...

Alors la référence de l'article nature est https://www.nature.com/articles/s41586-023-06747-5 et le détail des problèmes des olympiades résolu par AlphaGeometry https://static-content.springer.com/esm/art%3A10.1038%2Fs41586-023-06747-5/MediaObjects/41586_2023_6747_MOESM1_ESM.pdf
Sur le détail, on voit qu'il y a une étape de traduction (Translated), et cette étape est dans certains cas loin d'être évidente, il s'agit de passer d'un problème de géométrie avec des contraintes à une suite de commandes permettant de construire la figure, et il me semble que cette étape n'est pas automatique, mais réalisée par les auteurs de l'article, peut-être avec l'aide des corrigés des olympiades. Ce n'est qu'ensuite que l'IA tourne.

Pour tester avec Xcas, il faut peut-être purger le cache du navigateur. Je ne pense pas que c'est une bonne idée de tester sur téléphone, les figures sont relativement complexes, on parle de problèmes d'olympiades...
Xcas ne fait pas le travail tout seul, il faut aussi lui fournir la suite de commandes pour construire la figure, mais ensuite il fait la preuve tout seul, comme AlphaGeometry, avec des techniques de géométrie analytique vs des techniques de géométrie pure (synthétique). L'IA intervient dans AlphaGeometry en créant des constructions auxiliaires permettant de faire une preuve, mais je ne pense pas que c'est le cas dans l'étape de création de la construction.

J'en suis à 34 solutions pour Xcas ce matin (+ 1 partielle). Je suis en train de parcourir les énoncés depuis le site des olympiades, car certains ne sont pas cités comme non résolus par AlphaGeometry, il devrait logiquement y en avoir plus de 40 à raison de 2 par an depuis 2000 et pas juste 30.
D'autre part, il faudra que je recompte précisément les réponses de AlphaGeometry, car elles ne sont pas toujours complètes, pour certaines équivalences (2003p4 et 2004p5), il montre seulement l'implication dans un sens.
Il semblerait donc que l'article de Nature a un peu enjolivé les performances de AlphaGeometry...

Voilà, score final 37 à 25. En fait un score plus adéquat serait plutot 37.5 à 24, car j'ai une solution partielle pour oim2018p6 et AlphaGeometry n'a fait qu'un des deux sens dans les équivalences demandées en 2003p4 et 2004p5.
Cette fois-ci j'ai traité les 38 problèmes traitables en géométrie analytique, donc c'est bien le score final. Après je crois que c'est surtout moi que ça intéresse, pour voir jusqu'où on peut aller par des preuves faites par un humain en géométrie analytique en utilisant le calcul formel pour faire les calculs. Ca permet de tester la puissance et les limites de mon noyau de calcul formel (37.5/38 c'est pas mal!)
Mais je m'attends à ce que la grande majorité des matheux considèrent que faire des preuves en géométrie analytique c'est une hérésie, et les informaticiens (alias google) s'intéressent à une solution par IA avec le minimum d'intervention humaine possible (voire 0), même si ce n'est pas encore vraiment le cas pour les problèmes d'olympiade.

Et j'ai fini par trouver une preuve complète pour le dernier qui me manquait. Donc score final 38 à 25, ou plutôt 38 à 23 en tenant compte du fait que AlphaGeometry décompte 2 solutions pour un même problème 2002p2, et prouve une implication au lieu d'une équivalence pour 2 problèmes (2003p4 et 2004p5). J'ai rédigé un petit document:
https://www-fourier.univ-grenoble-alpes.fr/~parisse/irem/alphageo.html

Le score passe à 40 pour Xcas en tenant compte des olympiades de juillet 2023 (+2 problèmes résolus). AlphaGeometry n'en parle pas, ce qui est compréhensible pour l'article de Nature, envoyé en avril 2023, même s'ils auraient pu faire une mise à jour avant l'acceptation en octobre 2023, et surtout dans le communiqué de presse du 17 janvier 2024. J'estime probable qu'ils soient capables de résoudre un des deux problèmes de géométrie de 2023, mais pas l'autre. En tout cas, ce serait intéressant de le savoir, d'autant plus qu'il n'y a pas encore de solution officielle publiée pour les problèmes de 2023

Je réalise (seulement maintenant!) qu'en fait AlphaGeometry n'est pas capable de résoudre certains énoncés parce qu'ils ne sont pas constructibles sans calcul préalable pour satisfaire à des contraintes non triviales (et même dans ce cas le calcul risque d'être faisable uniquement en approché). Ce qui fait une différence notable avec la façon de raisonner d'un être humain : on trace une figure approximative pour faciliter le raisonnement, mais il n'y a pas besoin d'une figure exacte. C'est aussi une différence notable avec une preuve assistée par calcul formel.