AlphaGeometry

Sylvain
Modifié (17 Jan) dans CultureMath
Bonjour,
J'ai vu ce lien sur X : https://www.nature.com/articles/s41586-023-06747-5
J'attends de pied ferme un AlphaNumberTheory ^^

Réponses

  • Je n’ai pas encore tout lu mais visiblement, ils ont entraîné une IA avec plus de 100 millions de théorèmes de géométrie euclidienne avec leurs démonstrations chacune comprenant plus de 200 étapes ! Ça laisse songeur…
  • Ce que je trouve incroyable c'est "AlphaGeometry advances the current state of geometry theorem prover from below human level to near gold-medallist level". Une progression aussi fulgurante me laisse pantois...
  • Seulement 4 à 10 problèmes sur 30 résolus par des méthodes de type CAS (Groebner etc)? J'aurais cru plus.
  • parisse
    Modifié (18 Jan)
    Les 3 premiers problèmes que j'ai testés (la figure 1 de l'article et les 2 premiers problèmes cités dans le document complémentaire https://static-content.springer.com/esm/art%3A10.1038%2Fs41586-023-06747-5/MediaObjects/41586_2023_6747_MOESM1_ESM.pdf sont tous les trois faciles à résoudre avec du calcul formel, j'ai mis des liens vers des sessions pour ces exemples ici: https://xcas.univ-grenoble-alpes.fr/forum/viewtopic.php?f=32&t=2891&p=12831#p12831
    En plus, c'est assez facile.
    Alors, à moins que j'ai été très chanceux, je conjecture qu'il y a plus que 4 à 10 problèmes résolubles par calcul formel.

    N.B.: ceci n'enlève rien à l'intérêt de lier 2 logiciels (une IA pour tester des points supplémentaires, un système de vérification), mais je pense que la comparaison faite dans l'article avec les systèmes de calcul formel mérite d'être creusée, en particulier les 2 articles cités datent du 20ème siècle.
    Et bien sûr, ça n'enlève rien à l'intérêt de faire des preuves élégantes en géométrie synthétique. La géométrie me sert d'ailleurs pour donner des tests de régression au moteur de calcul formel de Xcas.
  • parisse
    Modifié (23 Jan)
    J'ai terminé ce soir, avec si j'ai bien compté, 31 solutions Xcas, dont 29 fonctionnent dans la version web de Xcas (les 2 dernières nécessitent la version PC de Xcas), contre 25 pour AlphaGeometry. L'exécution d'une session se fait en quelques secondes depuis un navigateur sans installation (la puissance de calcul nécessaire est donc plusieurs ordres de grandeur plus faible que pour l'IA d'AlphaGeometry qui peut nécessiter plus de cent "workers" en parallèle pour résoudre un problème en moins d'1h30). Pour les personnes intéressées, mes solutions Xcas sont accessibles depuis le forum de Xcas:
    https://xcas.univ-grenoble-alpes.fr/forum/viewtopic.php?f=32&t=2891
    La construction effective de figures est parfois difficile et représente une partie significative du travail de résolution de certains problèmes, que ce soit avec du calcul formel ou avec AlphaGeometry. Ensuite, il faut veiller à bien choisir son paramétrage pour éviter le plus possible l'introduction de racines carrées dans les calculs de géométrie analytique (j'ai décidé d'ajouter des modèles dans Xcas pour commencer une construction formelle dans les cas classiques: triangle ABC, triangle avec cercle inscrit, triangle avec cercle circonscrit).
    D'autres logiciels utilisant du calcul algébrique sont certainement capables de résoudre plus que les 4 ou 10 problèmes indiqués par les auteurs, qui semblent s'être limité au logiciel JGEX qui sauf erreur de ma part n'a plus d'activité depuis au moins 8 ans et ne dispose pas d'un moteur de calcul formel optimisé.
Connectez-vous ou Inscrivez-vous pour répondre.