Plusieurs personnes m’ont demandé ce que je pensais de l’annonce de Google d’avoir créé une intelligence artificielle qui avait déjà démontré 1200 théorèmes ; même s’il s’agit d’une annonce de l’an dernier, on continue de me poser des questions dessus, je pense donc pertinent d’écrire un billet.

Tout d’abord, relevons que la démonstration automatique de théorèmes est un vieux champ scientifique à l’échelle de la courte histoire de la discipline informatique (travaux des années 1950, 1960). Mieux encore, la démonstration automatique de théorèmes et les sujets connexes tels que la « programmation logique » ont longtemps été considérés comme un des principaux axes de recherche en intelligence artificielle (ce qui fait, pour la petite histoire, que j’ai moi-même publié dans une collection d’ouvrages d’intelligence artificielle). Il va donc falloir quelque peu préciser les choses afin de dégager la nouveauté de ces travaux : cela fait belle lurette que l’on démontre automatiquement des théorèmes, et qu’il y a même des applications industrielles à cela !

La question de savoir si un théorème admet ou non une démonstration est bien entendu ancienne. Au début du XXe siècle, on s’est demandé s’il existait des procédés mécaniques (au sens de : applicable mécaniquement par un mathématicien inintelligent mais doté d’une obstination, d’une longévité et d’une quantité de papier non limitées) pour résoudre tel ou tel type de problèmes mathématiques (équations diophantiennes…), pour aboutir au problème de la décision (Entscheidungsproblem) : étant donné un énoncé mathématique, dire si celui-ci admet ou non une démonstration(et fournir celle-ci).

Toutefois, on démontra (travaux de Gödel, Church, Turing…) qu’il ne pouvait exister de tel procédé. J’insiste ici, car parfois on a voulu me reprendre sur ce type d’affirmations en m’expliquant que ce que je voulais certainement dire, c’est que la science n’avait pas encore trouvé de tel procédé, mais que cela n’excluait pas qu’ils pussent exister. Il ne s’agit pas de cela : on a démontré qu’un tel procédé ne peut exister, en supposant son existence et en en dérivant une conséquence absurde. Les développements autour de ces questions forment la théorie de la calculabilité.

Toutefois, l’impossibilité d’avoir une procédure automatique traitant de l’arithmétique, et plus généralement des mathématiques, n’exclut pas d’en avoir pour certains fragments restreints des mathématiques. On dégagea donc des classes d’énoncés mathématiques admettant des procédés mécaniques de décision (des algorithmes). On s’aperçut aussi que même si un procédé existait, celui-ci pouvait avoir un coût (temps de calcul, espace mémoire utilisé) absolument prohibitif. Ainsi, on sait depuis les travaux de Tarski (années 1950) que la « géométrie élémentaire » et l’« algèbre élémentaire » (je ne donnerai pas ici la définition de ces termes dans ce contexte) admettent des algorithmes de décision, mais les premiers algorithmes proposés à cet effet avaient un coût tel qu’ils étaient impossibles à appliquer sur quoi que ce soit d’intéressant ; et encore actuellement, ces problèmes sont coûteux à résoudre.

On s’intéressa donc à la question de savoir si certains problèmes étaient intrinsèquement difficiles à résoudre, s’il était inévitable qu’ils n’admettent que des algorithmes de décision coûteux ; cela donnala théorie de la complexité algorithmique, qui à ce jour comprend d’ailleurs encore de formidables conjectures non démontrées, notamment P vs NP.

Le fait qu’une classe de questions mathématiques n’admette pas d’algorithme de décision, ou que tout algorithme pour la décider est trop coûteux, ne doit cependant pas nous décourager. En effet, cela n’implique nullement qu’il n’existe pas d’algorithme qui, sur de nombreux cas d’espèce intéressants en pratique, résolve le problème avec un coût tolérable. En d’autres termes, ce n’est pas parce que le pire cas est défavorable qu’on doit perdre tout espoir.

Depuis les années 1950, on a donc cherché à obtenir des algorithmes qui se comportent bien sur des cas intéressants en pratique. En matière de recherche de solutions à des problèmes mathématiques, ou de recherche de preuves à des théorèmes, les algorithmes procèdent souvent par une sorte d’exploration des possibles : on essaye une direction de recherche, elle ne fonctionne pas, on en essaye une autre, etc. On cherche donc à concevoir des algorithmes qui d’une part arrivent à exclure rapidement des mauvaises directions de recherche (en se rendant compte que quoi qu’on fasse une fois parti dans cette direction, on n’arrivera à rien), d’autre part tendent à chercher dans la bonne direction.

Lorsqu’un·e mathématicien·ne professionnel·le, voire même un·e étudiant·e, recherche une preuve à un théorème, il y a aussi souvent des tâtonnements, qui d’ailleurs aboutissent parfois à se rendre compte que finalement, ce n’est pas le bon énoncé de théorème, pas les bonnes définitions. Je ne connais pas la littérature sur les processus psychologiques en cause et m’exprimerai donc comme le grand public : il semble y avoir en mathématiques une forme de « flair » pour les bonnes définitions, les bons énoncés, les bonnes directions de preuve, ce « flair » étant nourri par l’expérience.

On a donc cherché à produire des algorithmes intégrant une forme de « flair » sous formes d’heuristiques de choix : par exemple, l’algorithme va estimer que, « vu la tête du problème et les essais précédents, c’est une bonne idée que d’essayer de distinguer les cas où x>0 et x0». Là encore, ce n’est pas nouveau, et les bonnes performances des SAT et SMT-solveurs (des outils de décision de théorèmes mathématiques utilisés dans certaines applications industrielles) actuels sont en partie dues à ces heuristiques. Il en est de même, à ma connaissance, pour les prouveurs par superposition en logique du premier ordre.

Où ce situe donc l’innovation décrite dans l’article des chercheurs de Google, et dans des articles d’autres chercheurs qui n’ont pas fait l’objet de communiqués de presse, ou du moins pas aussi bien relayés ? Il s’agit d’utiliser de l’apprentissage automatique pour en quelque sorte apprendre à l’heuristique de choix, au vu de démonstrations précédentes, quels sont les bons choix qui tendent à permettre d’arriver à une démonstration (l’apprentissage automatique, c’est ce qui permet, par exemple, d’apprendre à un système informatique que telles photos dépeignent des chiens, telles photos dépeignent des chats, et ensuite d’obtenir qu’il classe automatiquement entre chiens et chats des photos qu’il n’a jamais examinées auparavant). Bref, cela reprend l’idée du « flair » humain guidé par l’expérience.

Voyons maintenant les limites de l’approche utilisée, tant dans cet article que dans d’autres. Le travail mathématique ne se limite pas à produire des petites preuves de théorèmes dont on connaît déjà l’énoncé (cela, c’est ce que l’on demande aux étudiants lors des examens) ; il s’agit plutôt de proposer de bonnes définitions de concepts, des énoncés de théorèmes intéressants à démontrer dessus, et, pour la preuve de théorèmes un tant soit peu complexes, des étapes de démonstration (décomposition du problème en sous-problèmes, décomposition des théorèmes en lemmes). Les approches décrites ne s’attaquent pas à ces questions.

Même pour de simples preuves, les approches décrites sont limitées en ce qu’elles sont incapables de suggérer des objets mathématiques qui ne sont pas déjà fournis dans l’énoncé. Expliquons. Si je demande de démontrer qu’il existe un entier supérieur à deux, on peut me suggérer « trois » ou « quatre ». D’une façon générale, quand on aura besoin de démontrer que quelque chose existe, soit comme but soit comme étape de démonstration, il va falloir le fournir, et en général c’est plus dur que suggérer « trois » comme « entier plus grand que deux ». Dans certaines preuves, la principale difficulté est justement de « tirer de son chapeau » un objet dont on a besoin d’établir l’existence, la preuve qu’il satisfait aux critères imposés étant ensuite relativement simple. Les approches décrites sont incapables de tirer quoi que ce soit de leur chapeau, si ce n’est des objets qui figurent déjà dans le problème étudié. C’est, à mon avis, le grand problème de recherche qu’elles posent (problème relié, par exemple, à la synthèse d’invariants en preuve de programmes).

Je ne veux évidemment pas ici dénigrer les travaux évoqués, qui me semblent très intéressants, mais seulement donner une certaine perspective et les inscrire dans une chronologie déjà bien fournie.