Enseignement 2023-2024 : La philosophie de la pratique des mathématiques
Séminaire du 09 octobre 2023 : L’AI et l’avenir de la pratique des mathématiques
Intervenant : Amaury Hayat, École des Ponts Paristech
Retrouvez les enregistrements audios et vidéos du cycle :
https://www.college-de-france.fr/fr/agenda/seminaire/la-philosophie-de-la-pratique-des-mathematiques-7
Chaire Combinatoire
Professeur : Timothy Gowers
Retrouvez tous ses enseignements :
https://www.college-de-france.fr/chaire/timothy-gowers-combinatoire-chaire-statutaire
Le Collège de France est une institution de recherche fondamentale dans tous les domaines de la connaissance et un lieu de diffusion du « savoir en train de se faire » ouvert à tous.
Les cours, séminaires, colloques sont enregistrés puis mis à disposition du public sur le site internet du Collège de France.
Découvrez toutes les ressources du Collège de France :
https://www.college-de-france.fr
Suivez-nous sur :
Facebook : https://www.facebook.com/College.de.France
Instagram : https://www.instagram.com/collegedefrance
X (ex-Twitter) : https://twitter.com/cdf1530
LinkedIn : https://fr.linkedin.com/company/collègedefrance
[Musique] [Musique] merci beaucoup j’aimerais beaucoup remercier le professeur Timothy Gers pour l’invitation et c’est un grand honneur pour moi de donner ce le premier séminaire la premierre exposé du séminaire de la philosophie dans la pratique des mathématiques alors moi je m’appelle amoréat je suis professeur de mathématiques à l’École des Ponts
Parytech et en particulier je je ne suis pas philosophe des mathématiques et donc je vais surtout parler de la pratique des mathématique et dans le cas qui nous intéresse de Lia dans le futur de la pratique des mathématiques alors je commencerai par vous dire que si jamais ça j’ à le faire
Fonctionner voilà je commencerai par vous dire que que nous la majorité d’entre nous ici nous utilisons tous des outils d’IA au quotidien depuis un certain moment et parfois sans en avoir conscience c’est le cas par exemple quand vous utilisez des réseaux sociaux quand quand vous utilisez un certain
Nombre de d’ou d’email pour ceux qui ont des assistants virtuels ou encore des plateformes mais en fait tout simplement si vous avez juste un smartphone vous êtes susceptible d’utiliser des outils relativement au quotidien alors ça c’est quelque chose dont on n pas souvent Mo on avait pas
Conscience il y a quelques années même si c’était déjà le cas simplement depuis un an on entend beaucoup plus parler de de Dia et des progrès de Lia grâce à l’arrivée de de grâce grands progrès de la pour le langage et en particulier à l’arrivée d’un d’un outil que vous
Connaissez tous j’en suis sûr qui s’appelle chat GPT alors ce qu’il faut garder en tête c’est que lia pour le langage ça n’est pas quelque chose de récent c’est quelque chose en réalité d’assez vieux ça fait très longtemps qu’on essaie de faire de Lia pour le langage ça commence
À peu près vers la fin de la la Seconde Guerre mondiale au moin ma connaissance avec les premiers travaux sur la traduction automatique donc le but c’était de savoir traduire d’une langue à l’autre de français anglais anglais allemand enfin essentiellement ça c’est un problème quand même relativement dur
Qui était pas du tout résolu à ce moment-là qui était toujours pas aux années 2000 et qui a connu un nouvel essort quand sont arrivés les réseaux de neurones donc c’est un peu ce les réseau neurones c’est lia au sens moderne généralement quand quelqu’un vous parle
D’IA il vous parle de réseau de neurone et un tournant récent qui a permis ch c’est le l’arrivée en 2017 d’une architecture d’un d’un certain type d’IA une architecture de réseau neurone qui s’appelait le transformeer le transformer s éé introduit dans cet article là en 2017 dans attention isol
Unid vous voyez que cet article a eu beaucoup de succès pour c’est un article de 2017 pour les gens qui sont familiux du monde de la recherche un article C 91 1000 fois euh c’est beaucoup c’est C cette architecture elle a à l’intérieur un mécanisme d’attention qui lui permet de
Se concentrer sur les bon morceaux d’une phrase donc par exemple dans cette phrase là alors c’est je pense pas du tout le meilleur exemple mais dans dans cette phrase là vous auriez envie que d’être capable en lisant la phrase de faire un lien entre il et chain puisque
Ça ça ça fait référence à la même personne donc c’est typiquement le genre de chose que cette architecture va pouvoir faire un an plus tard arrive alors dans le dans dans GPT mais pas que arrive l’implémentation de ce transformeer dans un mode qu’on appelle autorégressif et je vous expliquer très
Rapidement ce que c’est juste parce qu’on en aura besoin un peu après donc qu’est-ce que ça veut dire ben vous allez donner en entrée donc c’est c’est c’est comme ça fonctionne chat GPT essentiellement tous les modèles GPT au moins j jusque là que que vous connaissez vous donnez en entrée une
Phrase et mettons que vous ayez une qui entraîné à compléter votre phrase donc vous mettez chîn Tentrée puis le tirer ici ce qu’elle va faire c’est qu’elle va commencer par regarder cette phrase essayer de calculer une densité une distribution de probabilité donc distribution de probabilité du mot
Suivant quel est quels sont les mots en fonction de leur probabilité donc on va donner cette distribution de probabilité là elle va tirer suivant cette distribution de probabilité donc ici vu qu’elle le tirer là je pense que la distribution de probabilité c’est essentiellement un pour il et pas
Grand-chose pour le reste donc ça va probablement tirer il et ça va remettre c’est ça le côté autorogressif ça va remettre à l’intérieur de l’entrée le le ce qui vient d’être tiré donc maintenant le votre modèle va prendre ça en considération chîn tentil regarder une densité de probabilité enfin calculer la densité de
Probabilité ça c’est grâce à son entraînement et puis tirer avec sa densité de probabilité donc là bon elle est un peu plus elle est moins restrictive qu’avant mais il est probable que de est quand même une très bonne probabilité après tant tril mais il y a d’autres choses ça peut être un
Point d’interrogation aurait pu marcher et puis pareil on remet ça dans la phrase chîn tenterait-il de alors là évidemment il y a beaucoup plus de choses qui sont possibles comme mot après mais comme chîn tenterait-il de lever la moustiquaire c’est la c’est le c’est l’ouverture de la Comédie humaine
De malero cette phrase existe sans doute en plein d’exemplaires sur Internet et donc du coup il s’est quand même bon avec une bonne probabilité à mon avis on peut avoir levé et donc du coup à la fin bon on continue comme ça et à la fin on
A votre phrase et puis le toujours un calcul densité de probabilité et on tire un point qui veut dire on arrête la phrase et donc c’est bon c’est fini donc vous ce que vous récupérez c’est ça donc vous avez entré dans votre modèle chîn Tentrée vous avez récupéré chîn tentré
De V Moustier mais c’est ça qui s’est passé au milieu alors c’est la fin de ma ma petite introduction vraiment en deux slides de de ce qui un transformer un modèle GPT et cette présentation sera essentiellement en deux parties je vais commencer par parler de l’IA dans les mathématiques aujourd’hui et j’espère
Vous convaincre que li a c’est déjà utile aujourd’hui pour faire des mathématiques c’est déjà utile pour les mathématiciens aujourd’hui pour prouver des nouveaux résultats on verra si vous êtes d’accord avec moi à la fin de cette partie et une deuxième partie où on va
Aller un peu plus dans le futur on va se demander ce qu’un a pourra un jour prouver des théorèmes qu’est-ce qui est faisable et vers quoi on peut aller alors commençons donc avec avec alors la première chose que j’aimerais vous dire c’est que faire des mathématiques avec un ordinateur ça
N’est pas quelque chose de nouveau prouver des théorèmes avec un ordinateur on a fait ça depuis longtemps un exemple que j’aime beaucoup c’est celui-ci euh ah oui alors là vraiment je je collectionne mais vous inquiétez pas ça va bien se passer alors ah oui ça c’est c’est alors attendez on va essayer faire
Une petite pause technique pour essayer de voir si ça ça règle le problème voilà ça a l’air de régler le problème alors que j’oublie donc mon exemple est un de mes exemples préférés c’est celui-ci alors évidemment en 1769 il y avit pas encore d’ordinateur au moins de
Ce que je sais euh mais il y a eer qui avait fait une conjecture et sa conjecture c’est s’il existe des entiers A1 jusqu’à AK et puis BN tel que a1^iss N + a2^iss N et cetera jusqu’à ak^iss n = B à la puissance n alors K est plus
Grand que N donc autrement dit si vous avez des entier que vous mettez à la puissance N et que c’est égal à un autre entier à la puissance n alors à gauche vous devez avoir au moins n entier voilà c’est une conjectjecture de l’air et c’est un problème qui a été ouvert
Pendant presque 200 ans c’est pendant presque 200 ans les mathématiciens ne savaient pas si c’était vrai ou faux çait pas voilà et donc tout ça jusqu’à l’arrivée de Lander et parkin en 1966 et l parking ils ont résu ce problème de la manière la plus basique que vous pouvez imaginer c’està qu’ils
Ont essayé toutes les combinaisons possibles dans un ordinateur essentiellement et ils ont ob tenu ça et donc là qu’est-ce qu’on voit on voit qu’on a des nombres à la puissance 5 qui sont égaux à un autre entier à la puissance 5 et donc la conjjecture de
L’air dit qu’on doit en avoir cinq à gauche mais là on en a que quatre donc la conjjecture de l’air était fausse et c’est ça ça leur a donné un l’ article c’est à mon avis enfin c’est à ma connaissance l’article de mathématique le plus court que je connaisse puisqu’il
Tient sur une seule slide mais c’était quand même un nouvel article alors c’était une preuve mais c’était quand même surtout la preuve que même quand vous appelezir vous pouvez faire des fautes c’est juste que l’humanité met 200 ans à seen rendre compte donc il y a
Un exemple un peu plus récent qui était la preuve de la conjecture de kellerer dans un cas qui qui qui résistait bien jusque- là en en 2019 alors sans expliquer trop ce que c’est parce que j’aimerais passer plus de temps avec les exemples sur avec de lar mais c’est une preuve dans laquelle
Le mathématicien peut ramener ça un certain nombre de cas simples à vérifier le le problème étant dans cas simple c’est bien le beaucoup c’est moins bien et c’est moins bien parce que ici beaucoup c’est vraiment beaucoup beaucoup trop pour un humain donc c’est pour ça qu’on utilise l’ordinateur à tel
Point quand on vous demande quelle est la taille de la preuve et ben on se demande plus combien de pages fait la preuve mais combien de gig fait la preuve et la réponse c’est 200 c’est peu près 10 fois Wikipédia c’est bien que si je vous montrais la preuve on serait pas
Sorti du séminaire donc je je m’arrêis sur exemples mais ça c’est pour vous illustrer que finalement CD de l’ordina on l’a fait depuis un certain moment alors je vais maintenant donner trois exemples où en fait pour essayer d’illustrer qu’on peut aller encore plus loin je pense avec avec des modèles d’
Et essayer de de de résoudre des difficultés qui posent de vrais problèmes aux mathématiciens des des domaines concernés avec ces modèles di donc je je vais parler d’exemples dans trois domaines des mathématiques le premier c’est la stabilité des St dynamiques le deuxème c’est la théorie du contrôle et le trisème c’est la
Topologie et on va commencer avec le premier alors dans la stabilité des systèmes dynamique euh on a un système d’équation différentielle alors qu’est-ce que c’est qu’un système d’équation différentielle et ben on on a un vecteur x qui dépend d’une variable on peut l’appeler le temps par exemple
Temp qu’à faire le point ici c’est pour la dérivée donc ça c’est la dérivée de cette variable par rapport au temps et c’est égal à une certaine fonction de de de ce vecteur c’est un système d’équations différentielle ça peut représenter plein de choses ça peut être par exemple un point en chute libre
Voilà dans un point chute libre vous AZ l’altitude de votre chuteur qui est y vous prenez la dérivée c’est la vitesse jusque là j’espère que ça va euh vous prenez la déérrivée de la vitesse c’est l’accélération en chute libre c’est – G alors peut-être pas à cette hauteur là
Mais mais normalement c’est Mo- g ça peut être l’avancement d’une réaction chimique donc ça c’est une version extrêmement simplifiée de de de la réaction de fermentation que que j’ai mis là ça peut être un modèle de croissance en économie ça c’est le modèle de Solo eu mais ça peut aussi
Être juste un système mathématique il a pas forcément besoin d’avoir une représentation physique derrière ou économique ou biologique ça peut être juste un système d’équation différentielle pour pouvoir en parler il faut qu’on précise de trois autres choses donc ici X à N comp osante f est une fonction qui est C1 c’estd qu’elle
Est dérivable et sa dérivée est continue et puis F de 0 vaut 0 donc 0 est ce qu’on appelle un équilibre parce que si vous commencez à é0 et ben vous avez F de0 ça fait 0 donc la dérivée vaut 0 et donc vous y restez à votre
Équilibre et donc la question qui se pose c’est la question de la stabilité de cet équilibre la stabilité du système euh évidemment donc si je commence à zé je reste à Z0 mais la question qu’on va se poser c’est si je commence pas très loin de zé est-ce que je peux garantir
Que je suis borné que je je reste pas trop loin quoi donc en terme plus mathématique ça s’écrit comme ça est-ce que pour tout Epsilon il existe Delta tel que si la condition initiale en norme est plus petite que Delta alors la solution existe pour tout temps et et
Puis elle sa norme reste bornée par le Epsilon donc si je donc en terme mathématique c’est ce que je vous ai dit et puis si j’essaie de l’illustrer un peu c’est ça on a une une boule rouge enfin un cercle rouge de de rayon Epsilon et nous ce qu’on aimerait c’est
Que c’est choisir une boule bleue on veut garantir qu’il existe une boule bleue telle que si je commence dans la boule bleue et ben ma trajectoire elle peut faire plein de choses un peu différent j’ai pas la prétention de de savoir ce que la trajectoire va faire
Par contre je peux garantir qu’elle va rester dans le cercle rouge c’est ça essentiellement la notion de stabilité alors ça c’est un problème qui a intéressé les mathématiciens depuis depuis plus de 100 ans je pense que dans les dans les choses connues y avait les les travaux de Point Carré qui étaai
Relativement fondateur il y avait le le le problème à trois corps vous AZ peut-être déjà entendu parler il y a une grande avancée y a un certain temps maintenant il y a un peu plus de 100 ans par un certain Liapunov alors qu’est-ce que Liapunov vous dit et
Ben essentiellement il dit que si jamais vous arrivez à trouver une fonction qui est strictement minimum en zéro qui tend vers l’infini à l’infini et tel que quand je prends le gradient de cette fonction et que je fais scalaire avec la dynamique ma fonction f c’est plus petit
Que zé pour tous les X et bien le système est stable alors évidemment la définition a pas l’air très jolie mais mais essentiellement ce que ça vous dit c’est que si vous trouvez une fonctionof alors votre problème est réglé vous avez répondu à votre problème il suffit de
Trouver une fonction de la Pun donc c’est un théorème très puissant euh très beau il manque juste un petit détail euh ce petit détail c’est bah comment on trouve la fonction de la plof et en fait ça s avéré être pas tant que ça un détail parce que c’est pas un problème
Si simple que ça en particulier là je vais montrre un exemple qui est simple on va voir si vous pensez qu’il est simple mais il est censé être considéré comme simple cette ce système dynamique là il a une donc bon on peut se demander ça peut pas évident est-ce que toutes
Les trajectoires sont bornées sur ce système je sais pas enfin moi moi là juste comme ça en regardant ça c’est pas clair si vous avez un peu l’habitude vous pouvez voir qu’il existe une fonction de la punof qu’on appelle diagonal c’est qu’il y a il y a X1 X2 X3
Il y a pas de terme croisé mais même là sur un exemple relativement simple bon c’est c’est c’est on a déjà l’impression qu’il faut un petit peu d’entraînement pour pour savoir trouver la réponse en fait c’est un problème quand même suffisamment dur pour qu’aujourd’hui ce soit complètement légitime de faire un
Article qui dit regardez tel système a une fonction deapunof ou tel système n’a pas de fonction deapunof euh ça ça fait un article de math tout à fait légitime et puis et puis ouais puis assez B alors ça c’est toujours une question ouverte puisqueaujourd’hui plus de 100
Ans après on ne sait pas avoir de façon systématique on ne sait pas construire de façon systématique une fonctionapunof pour pour ceux qui étaient au au cours de de Timothy ce matin le le la question de savoir trouver un oracle par exemple les pour les graphitoniens on ne sait
Pas construire un oracle qui permet de trouver une fonction de lapof et donc quand on est mathématicien et qu’on a pas de méthode euh qui nous les méthodes March habituelles March pas qu’est-ce qu’on fait bah dans ces cas-là on s’en remet quand même beaucoup à l’intuition alors l’intuition c’est une
Notion qui est importante en mathématique elle amène pas mal de débats est-ce que est-ce qu’on a forcément besoin de l’intuition est-ce qu’on peut toujours expliquer l’intuition est-ce qu’on est-ce qu’on peut s’en passer je vais pas du tout rentrer dans ces débats ce que je vais dire c’est qu’ici et dans un certain
Nombre de de cas l’intuition peut ressembler à une sorte de de reconnaissance de pattern voyez vous vous avez vu beaucoup d’exemples avant vous savez comment il fonctionne et pour une raison que vous savez pas expliquer le fait d’avoir vu ces exemples vous donne une idée de ce
Qui va marcher dans un exemple que vous n’aviez jamais vu jusqu’ici mais mais le point clé c’est que vous sa pas trop expliquer la raison il il y a probablement quelque chose mais mais mais c’est ça c’est un peu ça votre votre fonctionnement d’intuition sur ce genre de problème assez
Spécifique le truc c’est que la reconnaissance de de pattern c’est quand même quelque chose que les ça faire généralement très bien et donc on peut se demander est-ce qu’on pourrait entraîner avoir une meilleure intuition que nous sur ce problème mathématique est-ce qu’on peut entraîner avoir l’intuition d’une fonction d’AP et ben
C’est ce qu’on a essayé de faire et c’est ce qu’on voilà c’est la première tâche qu’on a donné l’entraîner pour devener des fonctionsapof alors qu’est-ce qu’on a fait on alors oui je rappelle le problème le problème c’est on a un système comme ça et on veut que réponde
Bah pour celui-là par exemple oui c’est stable et voici la fonction diapunov donc on veut que donne la formule à la fin alors comment on a fait et ben ce qu’on a c’est ce qu’on a fait avec un avec Alberto alfarano et François Charton on a choisi donc une architecture on a pris
Un transformer comme comme ce dont j’ai parlé au tout début mais beaucoup plus petit pas autorégressif et beaucoup plus petit on a généré plein d’exemple de problème et de fonction la p associé alors ça je je mentiens dans une phrase mais c’est la grosse difficulté de ce problème comme c’est comme c’est quelque
Chose qu’on ne sait pas à résoudre et ben avoir suffisamment d’exemples qui sont suffisamment diversifiés suffisamment nombreux c’est c’est un problème pas simple à faire en fait c’est l’essentiel de l’article et puis une fois qu’on a ça et ben on entraîne en lui montrant des exemples et
Des solutions et on utilise un certain nombre d’exemples on a utilisé 10 millions d’exemples al ça peut sembler énorme mais le le nombre alors évidemment le nombre de de d’équations différentielles non linéaaires possible c’est un espace de dimension infinie en plus dimension infinie qui a même pas de base
Dénombrable mais alors notre générateur est fini mais notre générateur est fini il peut générer quand même plus d’exemples qu’ y a d’atomes dans l’univers donc 100 millions c’est c’est pas beaucoup le le miracle c’est que ça c’est que ça ça fonctionne alors ça fonctionne je vais expliquer ce tableau
Tout de suite le le premier chose que vous pouvez voir c’est que là j’ai mis différents types de de d’équation que soit polynomial ou non polynomial avec différentes tailles différents nombres d’équations liia ça fonctionne essentiellement tout le temps alors je dit qu’on savait pas faire de façon systématique trouver une fonction de
Punof il y a quand même des cas où on n pas trop mauvais ces cas c’est quand le système est polynomial et qu’il a une fonction de la punof qui est aussi un polynôme et qui est aussi une somme de carrés dans ces cas-là on a des méthodes algorithmiques qui fonctionnent plutôt
Bien et l’état de l’art je pense que c’est cette méthode là et donc ici on l’a testé sur le sur les mêmes pour comparer un peu à la alors donc vous voyez que sur deux à trois équations sur un dataset polynomial un peu chargé elle
Arrive à 78 % ensuite 16 % ça peut pas faire le non polynomial puisque justement c’est c’est le cas qu’on sait pas faire li elle voit à peine la différence alors évidemment quand je fais ça il y a quand même une une petite astuce derrière qui est qui pas de la
Triche mais enfin qu’il faut quand même prendre en compte c’est que nous on a appris on a trouvé une méthode pour générer plein d’exemples on a utilisé ça pour entraîner l’a ensuite on a généré d’autres exemples qui sont différents pour tester lia et cette méthode alors
On va être clair il y a aucun exemple que sur lequel la est testé qu’elle a déjà vu avant sinon ce serait vraiment de la triche mais par contre peut-être que le la façon de générer fait que la distribution des systèmes qu’on obtient est similaire et donc du coup ça biaèise
Un peu l donc on s’est dit on va tester sur un autre type de système alors comme on sait pas en générer parce qu’on on sait pas R le problème et ben on sait le faire au moins dans le cas polynomial dans le cas polynomial on peut utiliser cette méthode algorithmique pour trouver
Des systèmes de manière peut-être beaucoup moins bisé et quand on fait ça en fait il a il arrive encore 83 % du temps donc c’est c’est quand même assez spectaculaire je me suis dit pour vous puissiez comparer je voulais vous donner une performance humaine et je voulais
Essayer avec moi mais mais en fait j’ai bon j’ai essayé de semaines j’en ai réussi un sur 4 j’ai essayé hier j’en ai réussi zéro donc je me suis dit que j’allais pas vous vous embêter avec ça je reviendrai quand il aura des meilleurs résultats voilà donc c’était mon premier exemple
Le deuxième exemple c’est un exemple dans la théorie du contrôle et là on va plonger au au cœur des mathématiques appliqué puisqu’on va regarder un système d’évolution de de la population des moustiques quand on est quand on essaie d’injecter des moustiques stériles malâ pour diminuer la population de moustique et limiter les
Propagations d’épidémies pourquoi parce que les femelles vont pas faire différence entre les les mâles et les Mâ stériles et puis ça marche moins bien avec les Mâ stériles donc la population diminue quoi en particulier il y a pas d’insecticide ni rien c’est ça l’intérêt de de cette
Méthode et puis je vois que il y a Louis salmeda dans la pièce comme il fait partie des gens qui ont fait ce modèle je voilà si vous avez des questions ce sera pour lui alors donc ici on a donc un système on a des œufs on a les mâles
On a les femelles on a les moustiques stériles et il y a dans ce système une quantité assez importante c’estu c’est le flux de moustique stéril qu’on relâche et ça c’est quelque chose qu’on peut choisir on élève des moustiques stériles et puis on les relâche c’est ce qu’on on
Appelle le contrôle en mathématique et la théorie du contrôle c’est bah si j’ai quelque chose que je peux choisir comment je le choisis pour atteindre mon objectif c’est ça le le cœur de la théorie du contrôle en mathématique et ici il y a quelques contraintes parce que c’est un problème
Physique la première c’est que le contrôle il doit s’écrire sous la forme fait ça doit être une fonction de M + MS le nombre total de Mâ et et F + FS le nombre total de femelle bon alors quelle est la question bah la question c’est est-ce qu’il est possible de trouver F
Tel que le système est stable maintenant vous savez tous ce que veut dire le système est stable et en plus on aimerait que la population moustique tende vers zéro donc le les œufs les mâles et les femelles on veut que ça tende vers zéro on va demander un
Tout petit peu plus on aimerait aussi que la population de moustique stérile tende vers Epsilon pour Epsilon aussi petit qu’on veut donc on pas forcément besoin que ce soit zéro mais on aimerait quand même que ce soit pas beaucoup et donc la question c’est est-ce que c’est possible de fabriquer F
Et en fait le ce ce problème est un problème très dur pour deux raisons la première c’est le le cette contrainte là qui qui fait que bon ça ça rend le problème assez compliqué d’un point de vue outil de la théorie du contrôle euh et puis le système avant si si vous
Regardez il y a il y a des fractions ça c’est c’est généralement pas chouette dans un système d’équation différentielle ça veut dire que le système va pas être lip sheits euh parce que à cause du point vers zéro et et puis et puis pasue donc donc donc c’est
Un système qui qui est compliqué à traiter et qu’on savait pas traiter et donc on s’est dit ah peut-être que là encore on pourrait avoir une IA qui joue comme un oracle une sorte d’intuition augmentée qui nous suggère une fonction f puisque c’est généralement plus facile enfin pas toujours mais c’estême
Généralement plus facile de montrer que f quand on a l’expression et solution que que de trouver la fonction f céit un peu le le en lien avec le cours de ce matin quand si jamais vous avez un graphe hamiltonien et puis un et puis un ordre c’est c’est plus facile de voir
Que ce graphe cet ordre cet ordre donne un un cycle hiltonien plutôt que de d’essayer d’en trouver un depuis zéro enfin depuis juste le graphe alors la procédure donc ça c’est c’est une question ouverte he et c’est ce qu’on essaie de résoudre donc la procédure c’est ce que c’est quelque
Chose qu’on a fait avec CAC bobidi Jean-Michel coron et Nathan lichely en cette année alors le le ça fonctionne de cette façon on a d’abord un système d’équation qu’on va discrétiser à l’aide d’un schéma numérique pour rendre essentiellement lisible par un ordinateur on va avoir une IA qui va
S’entraîner alors elle va s’entraîner essentiellement elle-même c’est-à-dire elle va essayer quelque chose elle va voir si ça marche ou pas elle essayie autre chose et ainsi de suite en espérant que ça converge vers quelque chose qui marche si ça marche s’il y a va converger elle va vous donner une
Approximation numérique de la fonction que vous cherchez elle va vous donner une genre d’approximation de votre fonction et là commence le travail de mathématicien qui est de dire ok cette approximation de fonction qu’est-ce que c’est enfin quelle fonction mathématique ça correspond et puis une voilà et puis une fois qu’on
Est là est-ce que toutes les parties de la fonction étaient nécessair donc c’est ce qu’on va voir ici donc là ça a marché on calcule ça converge et et et on arrive à ça c’estàdire que là j’ai j’ai j’ai la fonction l’approximation numérique donc u je vous ai dit la
Fonction c’est une fonction deux variables le nombre total de mâles et le nombre de femelles total de femelles donc ça c’est les deux variables là ça va de 0 à 6 millions oui parce que c’est j’ai oublié sur la contrainte physique mais on peut avoir un négatif de
Moustique euh et puis voilà ce que fait la fonction donc bon bah ici c’est zéro euh ici c’est 500000 parce qu’on lui a mis un maximum encore c’est une contrainte physique bon je sais pas vous mais mais moi quand je vois ça ça ça m’inspire pas à grand-chose je sais pas trop quelle
Fonction ça peut correspondre euh forc fort heureusement quand vous avez un un un doctorant très talentueux qui qui est dans le coin il vous dit qu’il faut pas regarder ça il faut regarder en échelle logarithmique euh et il a raison c’est qu’en échelle logarithmique c’est quand
Même beaucoup plus clair on voit qu’il y a l’air d’avoir une zone où c’est tout le temps maximum tout le temps minimum il y a une vague transition au milieu et puis la séparation a l’air d’être essentiellement un truc un peu comme ça et un truc un peu comme ça éidment c’est
Pas exactement parce que c’est une approximation mais ça donne déjà une bonne idée de ce qui a l’air de marcher et donc vous pouvez essayer donc on peut le traduire en terme mathématique don quand mathématique ça donne ça c’est pas très joli mais c’est là que commence vraiment le travail de mathématicien
C’est de se demander dans cette intuition qui m’a été donné par lia quel est le quel est le cœur qu’est-ce qui fait que ça marche et donc on essaie d’isoler ce qui fait que ça marche et on arrive au au bout du compte en fait ce
Qui fait que ça marche c’est c’est cette frontière là c ce ratio de logarithme qui est qui- ce qu’il est moi j’aurais j probablement jamais deviné et au bout du compte ça fonctionne alors ça fonctionne bon ça céit pour illustrer que ça fonctionne je pense que c’est c’est pas si lésible que
Ça en fait ce qui va se passer c’est que la trajectoire va tout le temps rester proche de la frontière donc la frontière a une vraie importance c’est pour ça qu’on s’est dit que c’était le cœur elle va tout le temps rester proche de cette frontière et puis elle va diminuer
Jusqu’à effectivement avoir plus de moustique ce qui est assez intéressant c’est que là ça marche pour tout Epsilon positif ça a l’air de marcher pour tout Epsilon positif on l’a pas encore démontré que on n pas encore démontré ça mathématiquement mais quand on met EPS =
0 ça marche plus du tout ça c’est c’est à peu près une certitude et donc malgré ce côté très approximatif des IA très très très numérique de de la fonction que récupère avant d’en faire une fonction mathématique et ben on arrive quand même à avoir une bifurcation qui est qui
Est assez subtile entre Epson é= 0 EP strictement plus grand que 0 donc c’est la fin de mon deuxème exemple euh je vais passer maintenant au troème exemple sur lequel je vais passer très peu de temps sur lequel je passer très peu de temps je vous rassure le le 3isème
Exemple c’est un exemple en topologie alors enthpologie c’est tiré d’un article qui s’appelle advancing mathematics by guiding human intuition withi c’est sorti dans Nature en 2021 c’est essentiellement par un groupe de Deep mind et et le groupe de Jordi Williamson à l’Université de Sydney et donc le le principe un peu
Général qui qui ressemble beaucoup à ce que j’ai montré c’est le suivant vous avez des objets Z mathématiques qui ont des quantités X de Z y de Z et vous aimeriez savoir s’il a un lien entre X et Y et ben pour ça ce que vous pouvez faire c’est essayer d’entraîner nia à
Prédire l’un en fonction de l’autre et si l’ a y arrive c’est qu’il y avait un lien vousêes pas vous savez pas encore quel est le lien mais siil a il arrive c’est qu’il y a un lien sinon elle pourrait pas y arriver c’est pas de la magie noire non
Plus et donc mettons qu’elle y arrive ça veut dire que votre réseau neurone votre votre Ia c’est essentiellement une fonction c’est une fonction peut-être très compliquée mais c’est une fonction il faut maintenant essayer de comprendre c’est là le travail de maémati il faut essayer de comprendre ce qui se passe à
L’intérieur de cette fonction et en faisant ça ils ont réussi à faire plusieurs choses et en particulier montrer un lien entre les invariants hyperboliques et algébriqu des nœuds oui donc je voulais dire que les nœuds c’est le plongement d’ dans la 3 mais si si vous êtes pas familier avec ça pas vous
Aider beaucoup plus du coup je voilà c’était juste c’est c’est dans un domaine relativement fondamental on peut trouver des liens qu’on avait pas vu avant alorsidment c’est qu’une conjecture c’est que après il faut démontrer qu’il y a vraiment un lien mais on a une bonne idée de ce qui se
Passe de ce qu’on doit démontrer alors je vais conclure avec ça et j’espère cette première parti vous av convaincu que l’IA est déjà utile dans la pratique des mathématiques et a permis de résoudre plusieurs problèmes difficiles comment ben si on résume un peu en formant l’ avoir une intuition
Meilleure que l’humain sur un problème spécifique et puis ensuite on utilise cette intuition pour complètement courcircuiter la difficulté du problème alors évidemment quand on parle de ça à chaque fois c’est l’humain qui fait le la preuve c’est l’humain qui fait le raisonnement l’ a elle est elle est là
Comme une aide même si c’est la grosse partie de la difficulté ça reste juste une aide on pourrait se demander est-ce qu’unea serait capable de prouver un résultat mathématique par elle-même et puis une question sous-jacente à laquelle je je vais bien sûr me garder de répondre c’est estce qu’unia pourrait
Raisonner alors euh donc on on va regarder ça dans cette deuxième partie il y a plusieurs questions liées la la toute première c’est est-ce qu’on peut automatiser le raisonnement humain c’est encore une question à laquelle je vais bien me garder de répondre est-ce qu’una peut trouver mais mais par contre
Ce que je vais regarder c’est est-ce qu’unea peut trouver une preuve à énoncer mathématique je dis qu’il y avait un groupe de recherche par mulers qui qui qui regarde plusieurs questions dont un peu celle-là aussi alors une une première approche un première chose que vous pouvez faire c’est essayer d’entraîner un
Transformeer donc un modèle GPT comme chat GPT mais chat GPT pour les maths ça a été fait en 2020 avant chat GPT c’est s’appelait gptf et donc votre chat GPT il fait quoi vous lui donnez une question et il vous donne une réponse et ben vous allez voir la même chose mais
Au lieu de répondre des phrases vous allez voir répondre des maths alors comment vous allez vouloir que ça fasse ça ben vous allez voir que ça le fasse de façon autorégressive encore donc vous avez un énoncé vous calculez à partirnoncé une distribution de probabilité de quelle est la première étape du
Raisonnement probable donc vous tirez une première étape de raisonnement vous la rajoutez dans la STAC à partir de ça vous calculez une deuxième distribution de probabilité vous tirez une deuxième étape et ainsi de suite et puis à la fin vous espérreer que ça vous dise au bout d’un certain nombre d’étape quand on
Espère la preuve est correcte juste ça vous la densité de probabilité soit très pointé vers c’est la fin de la preuve et donc on dit bah voilà c’est la fin de la preuve fin alors en vrai quand vous avez un moyen de vérifier en live l’effet du
Step 1 sur l’énoncé vous vous pvez faire un tout petit peu mieux que ça vous pouvez dire je prends un énoncé comme tout à l’heure je tire un step 1 je l’applique à l’énoncé et là ça me donne un nouvel énoncé c’est l’état de l’état du problème après le premier state et à
Partir de ça je tire un deuxième step et cetera comme ça à la fin vous savez quand vous avez fini vous avez fini quand il y a plus rien à démontrer si vous êtes à nothing to prove bah vous voilà vous avez fini donc typiquement dans un dans un langage formel ça
Voudrait dire vous obtiendrez quelque chose comme 0 é= 0 par exemple voilà et donc c’est ça l’espoir de de cette approche alors qu’est-ce que vous faites pour faire ça bah vous allez évidemment l’entraîner avec des exemples des exercices et des preuves et quel est l’espoir quand vous faites ça l’espoir
C’est qu’en montrant suffisamment d’exemples à votre Ia juste en lui montrant les exemples elle arrive à apprendre à démontrer alors raisonner je sais pas c’est vrai que j’ai marqué là mais je vis être plus précautionneux à raisonner je sais pas mais au moins à démontrer des des preuves mathématiques juste en prédisant
La prochaine étape à chaque fois alors on peut être sceptique on on peut l’être pour plusieurs raisons he on peut être sceptique parce qu’on peut se dire moi je pense qu’on peut pas apprendre les mathématiques juste en regardant des exemples et des solutions bon moi je suis un peu de la vie inverse
En réalité je pense je pense qu’on peut plutôt y arriver surtout quand on on parle vraiment de ce nombre d’exemples mais mais c’est tout à fait débattable on peut être sceptique parce qu’on peut se dire uneiaa qui à chaque fois regarde un état de preuve et prédit
Juste la prochaine étape sans avoir la moindre idée de ce qui va se passer derrière c’est c’est extrêmement né dans le guidon enfin c’est c’est c’est comment ça pourrait marcher mais d’unutre côté fait exactement pareil vous lu demandzécrire un essai sur la paix dans le monde je suis sûr qu’il
Aura une super conclusion et pourtant chaque étape il regarde les mots un par un quoi vraiment on est dans le guidon il prédit les mots un par un donc à la limite pourquoi pas ce qui est sûr c’est qu’on soit optimiste ou qu’on soit sceptique pour que ça ça puisse marcher
Il y a un truc clé c’est qu’il faut vraiment suffisamment d’exemples désolé mant je connais la procédure donc il faut vraiment qu’il y ait suffisamment d’exemples suffisamment ça veut dire quoi ça veut dire suffisamment diversifiés et suffisamment nombreux il faut évidemment si vous voulez espérer montrer des choses en
Topologie si vous AZ jamais vu un exemple de topologie avant vous allez jamais y arriver suffisamment nombreux parce que il faut que vous en ayez suffisamment pour réussir à apprendre quelque chose derrière à unir et c’est tout le problème on a en fait très peu de données à disposition en particulier des
Données formelles alors qu’est-ce que c’est qu’une donnée formelle et une donnée informelle et bien quand vous faites des mathématiques vous avez deux choix vous pouvez faire des mathématiques en écrivant ça dans un langage informel euh ça veut dire comme nous enfin comme la majorité des gens on
Écrit en français en anglais donc comme ça vous pouvez l’écrire de manière formelle de manière qui peut être lu par un ordinateur et et vérifieré automatiquement par un par un ordinateur par un Carnel donc ça voudrait ressembler à ça c’est le même exercice hein donc on a déclaré deux variables
Dans R on a dit a positif strictement une deuxème hypothèse la troisème hypothèse et puis le le ce qu’il faut démontrer et puis là techniquement on doit mettre la preuve donc donc voilà on a deux choix il y a deux problèmes qui se posent quand vous essayez d’entraîner
Inia à démontrer des maths avec un langage informel le premier problème qui se pose il est assez clair c’est que vous allez vouloir entraîner votre Ia sur un vous allez vouloir entraîner votre Ia sur Internet au tout début puisque vous allez voir en faire un modèle de langage et quand vous l’avez
Entraîner sur internet benah il y a beaucoup de choses sur internet donc si vous lui posez un petit exo comme celui-ci il y a une probabilité assez forte pour qu’il soit sur internet donc quelque part ou qu’il soit de façon très proche sur internet donc quelque part
Vous avez un peu tricher s’il y a vous donne une bonne réponse puisque bon elle l’a déjà vu quelque part avant il y a un deuxième problème qui qui moi je pense plus important qui a un problème à plus à terme c’est c’est très compliqué de vérifier vous AZ pas de manière
Automatique de vérifier de façon sûre que l’IA vous dit pas de bêtises c’est ça peut être soit vous soustraitez à uneia le fait de vérifier la preuve et bon je même pas en parler là tout de suite mais c’est pas forcément mauvais mais mais mais vous avez aucune garantie
Soit vous sraitez un humain mais là encore vous avez pas de garantie surtout si vous arrivez à des problèmes très compliqués on pourra imaginer que ça devienne plus facile à un moment pour une nia de trouver une preuve fausse mais qui a l’air crédible et qui est
Difficile à voir que de démontrer en fait le théorème pour des problèmes difficiles voilà c’est déjà arrivé c’est c’est arrivé quand même régulièrement qu’il a des Artic de mathématique qui se sont avéré être faux après coup et personne l’avait vu à l’avance parce que les les preuves sont très compliquées il
Y a un niveau où ça commence à devenir très compliqué de voir ce qui est vrai et ce qui est faux c’est d’utant plus que l’a est capable de faire des étapes fausses qu’un humain ne ferait jamais voilà alors ça veut pas dire qu’il faut pas le faire mais c’est c’est la raison
Pour laquelle je vais surtout parler de langage formel là maintenant et puis a des approches qui marchent très bien quand même avec ça alors en langage formel vous avez pas assez problème vous pouvez avoir un ordinateur qui vérifie tout de suite si ça a marché ou
Pas et puis vous avez pas ce vous contrôlez beaucoup mieux ce qui était dans l’entraînement et donc du coup c’est vous avez pas ce problème de de tricher de de données contaminées alors par contre en langage formel vous avez quand même assez peu de données vous avez de l’ordre de 100000
Théorèmes sur lin je crois lin c’est c’est le langage dans lequel j’ai écrit ça qui bon c’est beaucoup pour l’humain c’est c’est assez peu pour l’IA euh et donc du coup c’est c’est ça qui va donner une certaine limite à la méthode c’est vous allez réussir à faire
Ça il y a des gens qui l’ont fait en 2020 gptf ça arrive à démontrer des exercices de mathématiques mais il y a une certaine limite que qu’on peut pas dépasser qui est un peu lié au fait que bah on n pas de très très bonnes données
Fa pas suffisamment alors si vous voulez vraiment voir comment comment on peut essayer de dépasser un peu ses limites mais ou disons le maximum qu’on peut faire et ce qu’il faudraitire d’un point de vue ingéniéie pour ça je pense que l’état de l’art sur ce genre d’approche
A été c’est celle de de Fabian glocle en donc un article il y a quelques semaines euh voilà donc c’est le titre de l’article qui qui illustre assez bien à mon avis qu’est-ce qu’on peut essayer de faire quand on a vraiment si peu de données alors il y a une deuxième
Approche maintenant c’est de se dire je vais traiter les mathématiques comme un jeu alors pourquoi je traiterai les mathématiques comme un jeu à part que que tout le tout le monde sait que les mathématique c’est c’est vraiment très fun euh c’est de se dire que finalement en
2017 il y a une IA que dont vous êes sans doute entendu parler qui s’appelle alpha Z0 qui a appris à jouer aux échecs contre elle-même et qui en 3 jours d’entraînement al 3 jours d’entraînement avec beaucoup de GPU mais enfin 3 jours d’entraînement est devenu essentiellement meilleur que tous les
Humains que tous les humains pendant un bon moment et donc on pourrait se dire est-ce qu’on pour pas faire pareil on donne à une juste les règles du jeu mathématique et puis on essaie de voir si elle peut pas devenir meilleur que n’importe quel humain au bout de 3 jours ce serait
Chouette donc voilà donc comment ce jeu se présenter vous avez un énoncé que vous devez démontrer alors ici un énoncé pas très dur he cosinus x + exponentiel X est plus petit strictement que 1 + 2 exponentiel X vous jouz un coup alors jouer un coup ça veut dire appliquer un
Théorème donc vous appliquez un théorème quand vous appliquez un théorème ça c’est vrai si vous arrivez à montrer les hypothèses donc il vous reste plus que les deux hypothèses à démontrer ici vous pouvez de nouveau jouer un coup alors il y a un théorème qui vous dit directement
Que ça c’est vrai pour tout x donc du coup il y a plus rien à démontrer ici vous avez joué un coup pour appliquer un TM vous avez ça à démontrer vous jouez un coup vous avez ça vous jouez votre dernier coup et puis il y a plus rien à
Démontrer vous avez plus rien à démontrer dans dans l’arbre tout court et donc du coup vous avez gagné voilà un peu le jeu alors quand on fait ça il y a quand même pas mal de difficultés la première c’est que entraînera à jouer à un jeu à deux symétrique c’est beaucoup plus
Facile qu’entraîner unea à jouer seul contre son objectif alors pourquoi parce que quand vous avez une nia quand vous commencez à entraîner des vous allez avir des qui sont très très mauvaises et si vous l’entraînez à jouer à jouer des modèles l’un contre l’autre aux échecs
Bon ils sont très mauvais tous les deux il peut toujours avoir un match nul mais au bout d’un moment on peut quand même espérer qu’au bout d’une d’une partie il y a quelqu’un il y a un des modèles qui gagne même s’il est très mauvais siil
Gagne on peut dire que cette façon de jouer était meilleure que cette façon de jouer et on peut se servir de ça comme donnée d’entraînement pour continuer à entraîner les donc au bout d’un moment ça va finir par s’entraîner ça va finir par être assez fort si vous faites la
Même chose avec les mathématiques vous allez commencer avec des modèles qui sont très Nuls vous allez lui donner un problème il va pas y arriver et il va jamais y arriver et donc vous avez pas de données euh une autre façon de voir la chose c’est essentiellement pour gagner aux échecs
Il suffit d’être meilleur que la personne d’en face en math pour gagner et ben il faut être juste on est dans un domaine ou quand vous êtes presque juste c’est faux bon alors on peut on peut tenter de corriger évidemment quand on est presque juste c’est un peu caricatural ce que je dis
Mais alors une deuxième différence c’est caau échec quand on joue un coup on a toujours qu’une seule partie voilà je enfin moi moi généralement quand joue au échecs je joue un coup sur leschiqu il y a toujours qu’un seul échiquier quand on joue de cette façonl
Au math et ben on applique un théorème maintenant il faut vérifier les hypothèses et ben on peut avoir deux choses à démontrer donc on av on est parti de un maintenant on en a deux puis si on fait ça de façon incont contrôler on peut se retrouver avec 100
Différentes choses à montrer on espère qu’elles sont plus plus faciles mais enfin il il y en a quand même un certain nombre à montrer ensuite en mathématique c’est difficile de savoir euh automatiquement au milieu d’une preuve Si vousz quelle est la probabilité que vous allez que que vous
Allez y arriver que vous allez gagner euh aux échecs c’est bon il y a des méthodes qui sont pas du tout parfaites mais qui existaient bien avant l’arrivée de Lia pour dire je je photographie une partie d’échec euh bon la plus basique des méthodes c’est calculer le nombre de
Points de chaque côté mais ENF y a des méthodes un peu moins basiques qui vous permettent de dire celui-là est plutôt en train de gagner que celui-là euh en en mathématique à moins d’avoir fini les étapes cruciales de la preuve et donc de voir que ça va marcher essentiellement
Vous entendez beaucoup deciens dire ça va marcher euh si vous en êtes pas là c’est très dur de savoir si ça va le faire et c’est encore plus dur de donner une probabilité alors si c’est dur pour un mathématicien c’est ça allait encore plus pour de le faire automatiquement
Avec un critère automatique facile à expliquer à un ordinateur et enfin une dernière difficulté c’est qu’il y a beaucoup de possibilités aux échecs c’estd quand vous avez de l’ordre de 100 à 300 coup possible pu au fur à mesure de la partie vous enz de moins en moins au Go vous
Enz vous avez plus de coup possible mais ça n’a rien à voir avec le nombre de choses que vous pouvez faire en math le nombre de théorèmes que vous pouvez appliquer de changement de variable auquel vous pouvez penser de de de l’EM que vous pouvez essayer de faire c’est c’est c’est c’est immense
Euh et donc du coup y a quand même beaucoup plus de possibilités tout ça pour dire que c’est beaucoup plus facile d’entraîner beaucoup plus plus difficile d’entraîner à faire des mathématiques qu’à faire des des échecs alors en pratique malgré ces difficultés comment on ferait ça c’est c’est quelque chose
Qu’on a fait avec avec toute une équipe qui s’appelle équipe Evarist àéta alors en pratique on aurait deux choses donc là je vais utiliser un tout petit peu le tableau vous auriez deux modèles vous auriez un premier modèle qui est P thêta qui cherche à à à prédire une étape de preuve donc
Exactement comme la le modèle GPT que je vous ai montré avant ça regarde l’énoncé et ça fait une densité de probabilité puis ça prédit une une étape et puis vous avez un deuxième modèle qui est assez intéressant qui est celui qui va essayer de d’apprendre puis ensuite de
Prédire la la difficulté à prouver un théorème on regarde un énoncé il va dire ça c’est difficile ça c’est pas difficile évidemment il probement assez mauvais à faire ça mais enfin c’est une estimation pourquoi parce que du coup vous avez deux choses que vous pouvez faire une fois que vous avez ça vous
Pouvez dire bah je fais comme avant j’ai un énoncé voilà j’applique mon ma mon modèle donc ça va donner une une une mon modèle il a été entraîné donc ça ça va me donner une distribution de probabilité je peux tirer une étape de preuve qui est par
Exemple step 1 voilà alors je vais l’appeler a voilà et vous pouvez vous arrêter là et puis dire bah je fais ça je le passe de l’autre côté puis je passe à la suite exactement comme ce que j’ai fait avant et puis vous pouvez aussi dire attendez une petite
Minute qu’est-ce que je peux avoir d’autre que step a donc j’en tire quelquesuns je tire step B je tire step C et là je vais voir qu’est-ce qui se passerait si jamais j’appliquais step a donc step a c’est un théorème il y a des hypothèses à vérifier donc j’aurais par
Exemple G1 à montrer puis G2 à démontrer pour step B j’aurais probablement quelque chose de la forme G2 et G3 et G4 par exempleen met deux à chaque fois mais on pourra en a pas forcément deux ici peut y en avoir qu’une seule ici je peux avoir G5 par exemple pour avoir TR
Pour en avoir 4 donc j’ai ces choses à démontrer et là maintenant c’est là qu’intervient mon mod mod pour essayer de prédire dans un monde idéal la difficulté il va regarder à tout ça et il va me dire si c’est dur à démontrer ou si c’est ou si ça l’IT pas et
Peut-être qu’il va me dire par exemple ou là dans STEP a j’ai2 c’est à peu près impossible à démontrer ça ça va bloquer c’est à peu près impossible à démontrer et donc vous avez peut-être envie de vous dire ah bah peut-être que c’était pas céit pas quiil
Fallait faire peut-être que je peux en choisir un autre et donc vous avez envie de brancher une sorte de de d’ un airz de raisonnement on va on va pas appeler ça non plus un raisonnement un airz de raisonnement qui est qui est une capacité de chercher dans dans dans cet
Arbre de preuve des possibles pour essayer de chercher quelque chose un peu moins basique que ce dont on vient de parler juste avant donc vous AZ vous avez couplé ptta et C TTA ces deux i à vous vous allez à ce que vous propose le enfin avec le le la différentes
Arborescences vous pouvez faire un tout petit peu mieux que ça en fait vous pouvez aller voir si ça marche vous pouvez faire deux étapes vous voyez si ça marche vous donc c’est un peu ce que je montre là vous voyez si ça marche et puis en fonction de des scores c’est’ a
Quelque chose qui qui a été démontré vous dites le score c’est 1 et puis ici sinon vous utilisez le modèle et ensuite vous essayez de revoir et de vous dononner des nouveau scores en fait ça va donner des nouveaux scores à la fin à vos à vos tactiques pour dire quelle est
Celle que je veux utiliser donc l’idée c’est de de faire ça de façon un tout petit peu plus on va dire informé voilà alors ce que vous pouvez faire une fois que ça commence à marcher c’est comme aux échecs quand ça commence à marcher si ça commence à marcher vous pouvez
Utiliser donc vous dit voilà là j’ai une partie que j’ai gagné j’ai un arbre de preuve qui a fonctionné voici ce que j’ai utilisé ben vous pouvez utiliser ces données pour continuer d’entraîner le modèle ptta et C et donc dans l’espoir vous avez une genre de boucle qui finit par vous entraîner votre
Modèle alors comment ça comment ça se passe dans la pratique et dans la pratique ce qu’on a à la fin quand on fait ça c’est une qui est capable de démontrer des exercices de niveau licence alors évidemment pas tous mais mais un certain d’exercices 30 à 60 % d’exercices de collège lycée jusqu’à
Jusqu’à des niveaux parfois durs des niveaux d’olympiade alors ça dépend du dataset qui est utilisé il faut faut voir que pour uneia démontrer un exercice d’olympiade c’est souvent plus dur que démontrer un exercice euh pris au hasard en en licence par exemple parce que la difficulté d’exercice d’application du
Cours existe moins pour une le le apprendre par cœur une définition n’est pas un problème connaître exactement donc les exercices qui sont des exercices où il y a a que deux deux étapes à deux étapes à appliquer mais il faut se souvenir de son cours ne sont
Pas des exercices qui sont durs pour unir des exercices d’olympiad dans lequel il y a pas besoin de connaître grand-chose bon c’est B connait plein de trucs mais du coup il y a pas besoin de connaître grand chose et il faut trouver des astuces sont quand même assez
Difficiles même si ça intéresse moins ça nous intéresse moins nous les mathémaiciens c’est quand même dur pour une voilà de temps en temps ça arrive à faire des exercices tirés des olympies internationales des mathématiques alors j’en ai mis un ici que que lia arrive à faire toute seule montrer que pour tout
N 7 ne divise pas de puiss n + 1 j’espère que je me suis pas trompé dans dans l’énon c’est euh donc voilà alors pour 1 et 2 c’est probl pas très dur pour 3 c’estd ça divise pas de 9 je pense que ça va aller
Mais si maintenant n c’est 2^ 42 bon je sais pas c’est voilà bon bon problème je je vous recommande pour essayer de vous comparer voilà alors c’est un peu tout ce que je voulais dire alors quelles sont les perspectives mais alors j’ai l’impression que j’ai une ligne qui va
Apparître deux fois donc ajouter du raisonnement humain ce serait une des perspectives possibles pourquoi parce que là on a vraiment branché un RZ de raisonnement extrêmement basique si on avait une manière de dire bah voilà dans toutes les steps qui sont proposés il y a des choses qui sont
Vraiment absurdes ENF faudrait juste pas faire ça si on avait un moyen de de de de de de dire ça ou de dire par exemple et c’est un peu mon deuxième point ce qu’il faudrait essayer de démontrer voilà démontrer ce résultat il faudrait d’abord essayer de montrer ces quelques
États intermédiaires ces quelques idées intermédiaires vous vous donner tout de suite beaucoup plus d’information àa et c’est tout de suite un problème beaucoup plus facile al évidemment c’est toujours à double tranchant plus vous le faites ressembler à un humain plus il fera pas il fera pas différent mais mais voilà
Puis un autre un autre un autre espoir c’est le le le fait d’obtenir plus de données formelles avec de l’autoformalisation donc ça il il y a des travaux de de W et de Jang en 2022 mais il y en a d’autres il y a d’autres d’autres façons de faire que
J’ai pas mentionné ici parce que bon parce que ça reste ça aurait un peu dépassé le temps mais je pense que c’est les des belles façons d’essayer de voir ce que ce que sera la la preuve automatique demain alors je vais m’arrêter là j’ai c’est ma conclusion donc j’espère vous avoir convaincu que
Lia est déjà utile dans la pratique des mathématiques mais si c’est pas le cas je serai ravi d’en débattre et que lia pour prouver des théorèmes encore balbuciante et qu’il y a il y a beaucoup d’idées mais il y a encore beaucoup à faire je pense mais ça c’est vraiment un
Avis personnel encore c’est c’est on pourrait en débattre facilement que la que la pratique des mathématiques va sans doute changer euh et ça n’est pas grave en fait ça déjà ça change continuellement ça change régulièrement VO il fut un temps c’était qu’un domaine un peu plus représenté qu’aujourd’hui de savoir calculer les
Décimales de Pi dans dans dans la recherche en mathématique aujourd’hui on fait moins ça il y avait toute une part de calcul qui est un peu disparu avec l’arrivée de l’ordinateur aussi c’est c’est pas plus mal c’est juste dire que ça fait un peu des mathématiciens
Augmentés moi je suis de ceux qui sont convaincus que lia va pas remplacer les mathématiciens juste leur donner de nouveaux outils c’est voilà c’est façon un peu grossière c’est pas parce qu’on a une calculatrice que que que on a arrêté de de de d’avoir des mathématiciens voilà et donc ce sera
Tout et je vous remercie pour votre [Applaudissements] [Musique] attention