Dans quelle mesure les ordinateurs sont-ils proches de l’automatisation du raisonnement mathématique ?

Les outils d’intelligence artificielle façonnent la prochaine génération de théorèmes et, avec eux, la relation entre les mathématiques et la machine, explique Quantamagazine.

Dans les années 1970, le regretté mathématicien Paul Cohen, la seule personne à avoir jamais remporté une médaille Fields pour ses travaux en logique mathématique, aurait fait une prédiction générale qui continue d’exciter et d’irriter les mathématiciens : « à un moment futur non spécifié, les mathématiciens seront remplacés par des ordinateurs ». Cohen, légendaire pour ses méthodes audacieuses en matière de théorie des ensembles, a prédit que toutes les mathématiques pourraient être automatisées, y compris la rédaction de preuves.

Une preuve est un argument logique pas à pas qui vérifie la véracité d’une conjecture, ou d’une proposition mathématique. (Une fois prouvée, une conjecture devient un théorème.) Elle établit à la fois la validité d’une affirmation et explique pourquoi elle est vraie. Une preuve est cependant étrange. Elle est abstraite et n’est pas liée à l’expérience matérielle. « C’est ce contact fou entre un monde imaginaire, non physique, et des créatures biologiquement évoluées », a déclaré le spécialiste des sciences cognitives Simon DeDeo de l’université Carnegie Mellon, qui étudie la certitude mathématique en analysant la structure des preuves. « Nous n’avons pas évolué pour faire cela ».

Les ordinateurs sont utiles pour les gros calculs, mais les preuves nécessitent quelque chose de différent. Les conjectures découlent d’un raisonnement inductif – une sorte d’intuition sur un problème intéressant – et les preuves suivent généralement une logique déductive, étape par étape. Elles nécessitent souvent un raisonnement créatif compliqué ainsi que le travail plus laborieux consistant à combler les lacunes, et les machines ne peuvent pas réaliser cette combinaison.

Les preuves de théorèmes informatisées peuvent être divisées en deux catégories. Les vérificateurs de théorèmes automatisés, ou ATP, utilisent généralement des méthodes de force brute pour effectuer de gros calculs. Les vérificateurs de théorèmes interactifs, ou ITP, agissent comme des assistants de preuve qui peuvent vérifier l’exactitude d’un argument et contrôler les preuves existantes pour détecter les erreurs. Mais ces deux stratégies, même lorsqu’elles sont combinées (comme c’est le cas des nouvelles preuves de théorèmes), ne s’additionnent pas pour former un raisonnement automatisé.

Photo de Simon DeDeo

Simon DeDeo, de Carnegie Mellon, a contribué à montrer que les hommes et les machines semblent construire des preuves mathématiques de manière similaire.

De plus, ces outils n’ont pas été accueillis à bras ouverts et la majorité des mathématiciens ne les utilisent pas ou ne les apprécient pas. « Ils sont très controversés pour les mathématiciens », a déclaré M. DeDeo. « La plupart d’entre eux n’aiment pas l’idée. »

Un formidable défi ouvert dans ce domaine consiste à savoir dans quelle mesure la fabrication de preuves peut réellement être automatisée : Un système peut-il générer une conjecture intéressante et la prouver d’une manière que les gens comprennent ? Une série de progrès récents réalisés par des laboratoires du monde entier suggère des moyens pour que les outils d’intelligence artificielle puissent répondre à cette question. Josef Urban, de l’Institut tchèque d’informatique, de robotique et de cybernétique de Prague, explore diverses approches qui utilisent l’apprentissage automatique pour accroître l’efficacité et les performances des preuves existantes. En juillet, son groupe a présenté un ensemble de conjectures et de preuves originales générées et vérifiées par des machines. Et en juin, un groupe de Google Research dirigé par Christian Szegedy a publié les résultats récents d’efforts visant à exploiter les forces du traitement du langage naturel pour rendre les preuves informatiques plus humaines en termes de structure et d’explication.

Certains mathématiciens voient dans les démonstrations de théorèmes un outil qui pourrait changer la donne en formant les étudiants de premier cycle à la rédaction de preuves. D’autres affirment qu’il est inutile et probablement impossible de faire écrire des preuves par ordinateur pour faire progresser les mathématiques. Mais un système capable de prédire une conjecture utile et de prouver un nouveau théorème permettra d’obtenir quelque chose de nouveau – une version machine de la compréhension, a déclaré M. Szegedy. Et cela suggère la possibilité d’automatiser la raison elle-même.

Machines utiles

Les mathématiciens, les logiciens et les philosophes se sont longtemps disputés sur la partie de la création de preuves qui est fondamentalement humaine, et les débats sur les mathématiques mécanisées se poursuivent aujourd’hui, en particulier dans les profondes vallées qui relient l’informatique et les mathématiques pures.

Pour les informaticiens, les preuves de théorèmes ne sont pas controversées. Ils offrent un moyen rigoureux de vérifier qu’un programme fonctionne, et les arguments concernant l’intuition et la créativité sont moins importants que la recherche d’un moyen efficace de résoudre un problème. Au Massachusetts Institute of Technology, par exemple, l’informaticien Adam Chlipala a conçu des outils de démonstration de théorèmes qui génèrent des algorithmes cryptographiques – traditionnellement écrits par des humains – pour sauvegarder les transactions sur Internet. Déjà, le code de son groupe est utilisé pour la majorité des communications sur le navigateur Chrome de Google.

« Vous pouvez prendre n’importe quel type d’argument mathématique et le coder avec un seul outil, et relier vos arguments entre eux pour créer des preuves de sécurité », a déclaré M. Chlipala.

En mathématiques, les théoriciens ont contribué à produire des preuves compliquées et lourdes à calculer qui, autrement, auraient occupé des centaines d’années de la vie des mathématiciens. La conjecture de Kepler, qui décrit la meilleure façon d’empiler des sphères (ou, historiquement, des oranges ou des boulets de canon), en offre un exemple éloquent. En 1998, Thomas Hales, avec son élève Sam Ferguson, a réalisé une preuve en utilisant diverses techniques mathématiques informatisées. Le résultat était si lourd – les résultats ont pris 3 gigaoctets – que 12 mathématiciens l’ont analysé pendant des années avant d’annoncer qu’ils étaient certains à 99 % qu’il était correct.

La conjecture de Kepler n’est pas la seule question célèbre à être résolue par des machines. Le théorème des quatre couleurs, selon lequel il suffit de quatre teintes pour colorer une carte bidimensionnelle de manière à ce qu’aucune région adjacente ne partage une couleur, a été établi en 1977 par des mathématiciens à l’aide d’un programme informatique qui faisait défiler des cartes en cinq couleurs pour montrer qu’elles pouvaient toutes être réduites à quatre. Et en 2016, un trio de mathématiciens a utilisé un programme informatique pour prouver un problème ouvert de longue date appelé le problème des triples de Pythagore booléen, mais la version initiale de la preuve avait une taille de 200 téraoctets. Avec une connexion internet à haut débit, une personne pouvait le télécharger en un peu plus de trois semaines.

Sentiments compliqués

Ces exemples sont souvent présentés comme des réussites, mais ils ont également alimenté le débat. Le code informatique prouvant le théorème des quatre couleurs, qui a été établi il y a plus de 40 ans, était impossible à vérifier par l’homme lui-même. « Les mathématiciens se disputent depuis lors pour savoir s’il s’agit d’une preuve ou non », a déclaré le mathématicien Michael Harris de l’université de Columbia.

Photo de Michael Harris

De nombreux mathématiciens, comme Michael Harris de l’université de Columbia, ne sont pas d’accord avec l’idée que les démonstrations de théorèmes informatisées sont nécessaires – ou qu’elles rendront les mathématiciens humains obsolètes.

Un autre reproche est que s’ils veulent utiliser des démonstrateurs de théorèmes, les mathématiciens doivent d’abord apprendre à coder et ensuite trouver comment exprimer leur problème dans un langage informatique – des activités qui détournent l’attention de l’acte de faire des mathématiques. « Le temps que je recadre ma question sous une forme qui puisse s’adapter à cette technologie, j’aurais déjà résolu le problème moi-même », a déclaré M. Harris.

Beaucoup ne voient tout simplement pas la nécessité de résoudre des théorèmes dans leur travail. « Ils ont un système, un crayon et du papier, et il fonctionne », a déclaré Kevin Buzzard, un mathématicien de l’Imperial College de Londres qui, il y a trois ans, a fait pivoter son travail des mathématiques pures vers les preuves théoriques et formelles. « Les ordinateurs ont fait des calculs étonnants pour nous, mais ils n’ont jamais résolu un problème difficile par eux-mêmes », a-t-il déclaré. « Tant qu’ils ne l’auront pas fait, les mathématiciens ne vont pas croire à ce genre de choses ».

Mais Buzzard et d’autres pensent qu’ils devraient peut-être le faire. D’une part, « les preuves informatiques ne sont peut-être pas aussi étrangères que nous le pensons », a déclaré M. DeDeo. Récemment, en collaboration avec Scott Viteri, un informaticien actuellement à l’université de Stanford, il a procédé à l’ingénierie inverse d’une poignée de preuves canoniques célèbres (dont une provenant d’Euclid’s Elements) et de dizaines de preuves générées par machine, écrites à l’aide d’un théorème appelé Coq, afin de rechercher des points communs. Ils ont constaté que la structure en réseau des preuves machine était remarquablement similaire à la structure des preuves faites par les gens. Ce trait commun, a-t-il dit, pourrait aider les chercheurs à trouver un moyen de faire en sorte que les assistants de preuve s’expliquent, dans un certain sens.

« Les épreuves machine ne sont peut-être pas aussi mystérieuses qu’elles le paraissent », a déclaré M. DeDeo.

D’autres disent que les preuves de théorèmes peuvent être des outils d’enseignement utiles, tant en informatique qu’en mathématiques. À l’université Johns Hopkins, la mathématicienne Emily Riehl a mis au point des cours dans lesquels les étudiants rédigent des preuves à l’aide d’un théorème. « Cela vous oblige à être très organisé et à penser clairement », dit-elle. « Les étudiants qui écrivent des preuves pour la première fois peuvent avoir du mal à savoir ce dont ils ont besoin et à comprendre la structure logique ».

Mme Riehl dit également qu’elle utilise de plus en plus les démonstrations de théorèmes dans ses propres travaux. « Ce n’est pas nécessairement quelque chose que vous devez utiliser tout le temps, et qui ne remplacera jamais le gribouillage sur un morceau de papier », dit-elle, « mais l’utilisation d’un assistant de preuve a changé ma façon de penser à la rédaction des preuves ».

Les correcteurs théoriques offrent également un moyen de maintenir l’honnêteté sur le terrain. En 1999, le mathématicien américain d’origine russe Vladimir Voevodsky a découvert une erreur dans l’une de ses épreuves. Depuis lors et jusqu’à sa mort en 2017, il s’est fait l’avocat de l’utilisation des ordinateurs pour vérifier les preuves. Hales a déclaré que lui et Ferguson ont trouvé des centaines d’erreurs dans leur preuve originale lorsqu’ils l’ont vérifiée à l’aide d’ordinateurs. Même la toute première proposition dans Euclid’s Elements n’est pas parfaite. Si une machine peut aider les mathématiciens à éviter de telles erreurs, pourquoi ne pas en profiter ? (L’objection pratique, justifiée ou non, est celle suggérée par Harris : si les mathématiciens doivent passer leur temps à formaliser les mathématiques pour être compris par un ordinateur, c’est du temps qu’ils ne passent pas à faire de nouvelles mathématiques).

Mais Timothy Gowers, mathématicien et médaillé Fields à l’université de Cambridge, veut aller encore plus loin : Il envisage un avenir dans lequel les théoriciens remplacent les arbitres humains dans les grandes revues. « Je peux voir qu’il devient habituel que si vous voulez que votre article soit accepté, vous devez le faire passer devant un vérificateur automatique », a-t-il déclaré.

Parler aux ordinateurs

Mais avant que les ordinateurs puissent vérifier ou même concevoir des preuves de manière universelle, les chercheurs doivent d’abord franchir un obstacle important : la barrière de communication entre le langage des humains et le langage des ordinateurs.

Les vérificateurs de théorèmes d’aujourd’hui n’ont pas été conçus pour être à l’aise avec les mathématiciens. Les ATP, le premier type, sont généralement utilisés pour vérifier si une affirmation est correcte, souvent en testant des cas possibles. Demandez à un ATP de vérifier qu’une personne peut conduire de Miami à Seattle, par exemple, et il pourrait rechercher toutes les villes reliées par des routes partant de Miami et trouver finalement une ville dont la route mène à Seattle.

Photo de Timothy Gowers

Tous les mathématiciens ne détestent pas les démonstrateurs de théorèmes. Timothy Gowers, de l’université de Cambridge, pense qu’ils pourraient un jour remplacer les examinateurs humains dans les revues mathématiques.

 

Avec un ATP, un programmeur peut coder toutes les règles, ou axiomes, et demander ensuite si une conjecture particulière suit ces règles. L’ordinateur fait alors tout le travail. « Il suffit de taper la conjecture que vous voulez prouver, et vous espérez obtenir une réponse », a déclaré Daniel Huang, un informaticien qui a récemment quitté l’université de Californie, Berkeley, pour travailler dans une startup.

Mais voilà le hic : ce qu’un ATP ne fait pas, c’est expliquer son travail. Tout ce calcul se fait dans la machine, et pour l’œil humain, cela ressemblerait à une longue chaîne de 0 et de 1. Selon M. Huang, il est impossible de scanner la preuve et de suivre le raisonnement, car cela ressemble à un tas de données aléatoires. Aucun être humain ne regardera jamais cette preuve et ne pourra dire : « J’ai compris », a-t-il dit.

Les ITP, la deuxième catégorie, disposent de vastes ensembles de données contenant jusqu’à des dizaines de milliers de théorèmes et de preuves, qu’ils peuvent scanner pour vérifier qu’une preuve est exacte. Contrairement aux ATP, qui fonctionnent dans une sorte de boîte noire et crachent simplement une réponse, les ITP nécessitent une interaction humaine et même des conseils en cours de route, de sorte qu’ils ne sont pas aussi inaccessibles. « Un humain pourrait s’asseoir et comprendre les techniques de preuve », a déclaré M. Huang. (Ce sont les types de preuves machine que DeDeo et Viteri ont étudiées).

Les ITP sont devenues de plus en plus populaires ces dernières années. En 2017, le trio à l’origine du problème des triples de Pythagore a utilisé Coq, un ITP, pour créer et vérifier une version formelle de leur preuve ; en 2005, Georges Gonthier de Microsoft Research Cambridge a utilisé Coq pour formaliser le théorème des quatre couleurs. Hales a également utilisé des ITP appelées HOL Light et Isabelle sur la preuve formelle de la conjecture de Kepler. (« HOL » signifie « logique d’ordre supérieur »).

Les efforts à la pointe du domaine visent aujourd’hui à combiner l’apprentissage et le raisonnement. Ils combinent souvent les ATP et les ITP et intègrent également des outils d’apprentissage automatique pour améliorer l’efficacité des deux. Ils envisagent des programmes ATP/ITP qui peuvent utiliser le raisonnement déductif – et même communiquer des idées mathématiques – de la même manière que les gens le font, ou du moins de manière similaire.

Les limites de la raison

Josef Urban pense que le mariage du raisonnement déductif et inductif requis pour les preuves peut être réalisé grâce à ce type d’approche combinée. Son groupe a construit des preuves de théorèmes guidées par des outils d’apprentissage machine, qui permettent aux ordinateurs d’apprendre par eux-mêmes grâce à l’expérience. Au cours des dernières années, ils ont exploré l’utilisation des réseaux neuronaux – des couches de calculs qui aident les machines à traiter l’information par une approximation de l’activité neuronale de notre cerveau. En juillet, son groupe a présenté de nouvelles conjectures générées par un réseau de neurones formé sur des données prouvant des théorèmes.

Urban s’inspire en partie d’Andrej Karpathy, qui, il y a quelques années, a formé un réseau de neurones pour générer des absurdités d’apparence mathématique qui semblaient légitimes aux yeux des non-experts. Mais Urban ne voulait pas d’absurdités – lui et son groupe ont plutôt conçu leur propre outil pour trouver de nouvelles preuves après s’être entraînés sur des millions de théorèmes. Ils ont ensuite utilisé le réseau pour générer de nouvelles conjectures et ont vérifié la validité de ces conjectures à l’aide d’un ATP appelé E.

Le réseau a proposé plus de 50 000 nouvelles formules, bien que des dizaines de milliers d’entre elles aient été dupliquées. « Il semble que nous ne soyons pas encore capables de prouver les conjectures les plus intéressantes », a déclaré M. Urban.

[Les machines] apprendront à faire leurs propres messages.
Timothy Gowers, Université de Cambridge

Szegedy, de Google Research, considère le défi de l’automatisation du raisonnement dans les épreuves informatiques comme un sous-ensemble d’un domaine beaucoup plus vaste : le traitement du langage naturel, qui implique la reconnaissance de formes dans l’utilisation des mots et des phrases. (La reconnaissance des formes est également l’idée directrice de la vision par ordinateur, objet du précédent projet de Szegedy chez Google). Comme d’autres groupes, son équipe veut des théoriciens capables de trouver et d’expliquer des preuves utiles.

Inspiré par le développement rapide des outils d’IA comme AlphaZero – le programme DeepMind qui peut vaincre les humains aux échecs, au Go et au shogi – le groupe de Szegedy veut capitaliser sur les récentes avancées en matière de reconnaissance du langage pour écrire des preuves. Les modèles de langage, dit-il, peuvent démontrer un raisonnement mathématique étonnamment solide.

Son groupe à Google Research a récemment décrit une façon d’utiliser les modèles de langage – qui utilisent souvent les réseaux de neurones – pour générer de nouvelles preuves. Après avoir formé le modèle à reconnaître une sorte de structure arborescente dans des théorèmes dont la véracité est connue, ils ont mené une sorte d’expérience de forme libre, demandant simplement au réseau de générer et de prouver un théorème sans autre forme d’orientation. Parmi les milliers de conjectures générées, environ 13% étaient à la fois prouvables et nouvelles (ce qui signifie qu’elles ne reproduisaient pas d’autres théorèmes de la base de données). L’expérience, dit-il, suggère que le réseau neuronal pourrait s’enseigner une sorte de compréhension de ce à quoi ressemble une preuve.

« Les réseaux neuronaux sont capables de développer un style artificiel d’intuition », a déclaré M. Szegedy.

Bien sûr, il n’est pas encore clair si ces efforts permettront de réaliser la prophétie de Cohen d’il y a plus de 40 ans. Gowers a déclaré qu’il pense que les ordinateurs seront capables de surpasser les mathématiciens d’ici 2099. Au début, il prédit que les mathématiciens connaîtront une sorte d’âge d’or, « lorsque les mathématiciens feront toutes les parties amusantes et que les ordinateurs feront toutes les parties ennuyeuses ». Mais je pense que cela durera très peu de temps ».

Après tout, si les machines continuent à s’améliorer et qu’elles ont accès à de grandes quantités de données, elles devraient devenir très douées pour faire les parties amusantes aussi. « Ils apprendront à faire leurs propres messages », a déclaré M. Gowers.

Harris n’est pas d’accord. Il ne pense pas que les démonstrations informatiques soient nécessaires, ou qu’elles rendront inévitablement « les mathématiciens humains obsolètes ». Si les informaticiens sont capables de programmer une sorte d’intuition synthétique, dit-il, cela ne rivalisera pas avec celle des humains. « Même si les ordinateurs comprennent, ils ne comprennent pas d’une manière humaine. »

Via Quantamagazine.

Laisser un commentaire

Ce site utilise Akismet pour réduire les indésirables. En savoir plus sur comment les données de vos commentaires sont utilisées.