Entretien avec Alberto Naibo sur la géométrie des algorithmes

Un logicien en philosophie : démontrer la vérité d’un énoncé

Alberto Naibo : Décrire mon métier n’est pas chose aisée. Tout d’abord, je suis quelqu’un qui étudie la logique du point de vue de la philosophie, ou plutôt du point de vue du questionnement philosophique. La précision s’avère importante, dans la mesure où il existe des logiciens travaillant dans des départements de mathématiques ou d’informatique. En tant que logicien qui travaille dans un département de philosophie, je m’intéresse à la question de la vérité.  Cela suppose des interrogations du genre : qu’est-ce que la vérité et comment y accédons-nous ? Comment montrer que quelque chose est vrai ? 

C’est ainsi que se pose la question de la démonstration. Démontrer est l’action qui permet de montrer ou de rendre évident le fait que quelque chose est vrai ; démontrer permet donc d’acquérir le savoir que quelque chose est vrai. Plus précisément, on peut dire que la démonstration est un type de raisonnement correct permettant de conclure la vérité d’un énoncé. Mais qu’est-ce à dire ? Comment réaliser la distinction entre raisonnement correct et incorrect ? Il s’agit d’identifier les règles qui permettent d’atteindre la vérité, c’est-à-dire des règles qui, en partant de prémisses vraies, entraînent nécessairement une conclusion vraie. On opère ainsi une étude des règles d’inférence, des règles de déduction. Or ce que font les logiciens consiste à étudier ces règles d’un point de vue formel, au sens où ce qui compte est la forme des énoncés sur lesquels elles opèrent, et non pas leur contenu (car on veut étudier la vérité d’un point de vue général, et non pas en relation à des sujets de discours particuliers). 

Pour ce faire, on emploie des langages symboliques : les symboles servent à faire émerger la structure, la forme d’un raisonnement. Cela nous amène alors à la question de la manipulation de ces symboles, qui peut se faire grâce à l’emploi de règles spécifiques. Or, les règles d’inférence finissent elles aussi par devenir des règles symboliques. Ces règles de manipulation de symboles reposent notamment sur l’emploi d’instruments provenant des mathématiques, comme ceux de l’algèbre symbolique. Depuis la fin du 19^e siècle, les liens entre logique et mathématiques sont ainsi devenus prégnants. C’est ce qui a conduit à la naissance de la discipline qu’on appelle aujourd’hui « logique-mathématique ».

Il demeure néanmoins difficile de traiter la logique de manière uniforme. La logique-mathématique s’est spécialisée en de nombreux sous-domaines et chaque sous-domaine s’est lié à différentes théories mathématiques pour développer ses propres instruments d’étude. Par exemple, pour étudier les démonstrations et les règles d’inférence d’un point de vue formel, on est amené à les traiter comme de véritables objets mathématiques, en les représentant sous forme de listes, d’arbres ou encore de graphes. La théorie de la démonstration n’est toutefois pas le seul domaine de la logique. Il existe d’autres domaines, comme la théorie des ensembles, la théorie de la calculabilité, la théorie des modèles, la théorie des modalités, etc. Chacun convoque des instruments et des langages mathématico-formels différents et requiert des enseignements différents et adaptés. On peut en avoir un aperçu si l’on regarde l’offre didactique du parcours de Master « Logique et philosophie des sciences » au sein de l’UFR de Philosophie de Paris 1.

L’étude des algorithmes : le projet GoA

Alberto Naibo : L’étude de la logique m’a amené à cette question de savoir ce qu’est un algorithme pour deux raisons. La première est que si l’on regarde la pratique des mathématiques, notamment des mathématiques anciennes, on remarque que la plupart des démonstrations passent d’abord par la mise en place de procédures de construction qu’on peut appeler « algorithmiques ». Par exemple, si l’on veut démontrer le théorème de Pythagore à la façon d’Euclide, on doit mettre en place une procédure telle que, à partir d’un segment donné – dans ce cas, l’un des côtés d’un triangle – on puisse générer, pas à pas, un carré. Cette procédure de construction correspond à une suite finie et ordonnée d’opérations qui permet de prendre comme entrée des segments et qui peut être suivie, étape par étape, afin d’obtenir comme sortie des carrés. En ce sens, on peut considérer cette procédure comme une procédure « algorithmique ». De manière générale, les procédures algorithmiques employées en mathématiques semblent reconnaissables par certaines caractéristiques communes ; autrement dit, elles partagent entre elles un certain « air de famille ».

Cependant, bien que certaines démonstrations reposent sur des procédures algorithmiques, il ne s’ensuit pas que tout type de raisonnement ou de démonstration corresponde à un algorithme. C’est là la seconde raison qui m’a amené à m’intéresser à la question des algorithmes : comment identifier de manière exacte les raisonnements ou les procédures qui correspondent à des algorithmes ? Et comment les différencier de celles qui ne correspondent pas à des algorithmes ?

Or la notion d’algorithme est l’une des notions les plus présentes dans le débat public actuel. Ce débat est généralement dominé par un style de discussion journalistique, où des déclarations sont faites afin de polariser la discussion autour de scénarios futurs, positifs ou négatifs, concernant les impacts économiques, politiques et sociaux des algorithmes. Ces discussions n’explicitent cependant jamais ce qu’est un algorithme, et lorsqu’elles le font, une image trop simplifiée en est souvent donnée (un algorithme sera par exemple comparé à une recette de pâtisserie). L’objectif du projet GoA est de clarifier le type d’entités dont relèvent les algorithmes, et donc le type de discours qui peut être tenu sur eux. Le projet cherche en particulier à comprendre si la notion d’algorithme est une notion scientifique et mathématisable, ou si le discours scientifique et mathématique n’est pas suffisant pour la saisir. Si tel est le cas, faudra-t-il accepter le fait que, lorsque l’on parle d’algorithmes, l’on parle de quelque chose de vague ? Faudra-t-il se tourner vers d’autres domaines de discours (par exemple, la sociologie ou le droit) pour leur attribuer un statut précis ? Le projet GoA vise à relocaliser ce type de débat au niveau académique. Il s’agit de souligner la grande complexité de la notion, pour empêcher la formulation de prédictions faciles sur la façon dont les algorithmes affectent nos vies.

Par ailleurs, si l’on prête attention au débat philosophique, on voit que la notion d’algorithme est souvent associée à l’idée de mécanisation de la pensée. Comme dit précédemment, les règles d’inférence sont regardées, du point de vue de la logique, comme des règles qui opèrent sur des symboles, c’est-à-dire des signes dépourvus de signification : ce qui compte est le signe en tant que tel et non comme une chose censée renvoyer à autre chose. Pour appliquer ces règles, il suffit de regarder les propriétés de ces signes en tant qu’objets à part entière, comme leur forme ou leur position. Dit autrement, pour opérer sur ces signes, nul besoin de postuler l’existence d’un sujet ou d’une subjectivité qui soit capable de les interpréter ou de comprendre ce qu’ils veulent dire, car aucune ingéniosité n’est requise pour manipuler et combiner ces signes entre eux. Cette activité peut être associée à une sorte de calcul ou de « combinatoire aveugle » (pour reprendre une expression de Kurt Gödel, l’un des plus importants logiciens du 20^e siècle) dans laquelle l’agent humain peut être remplacé par une machine. Ce type de réflexions ont conduit, en logique, à la question de savoir ce qu’est une fonction calculable de manière mécanique. Ainsi, plusieurs outils ont été développés afin de capturer d’une manière mathématiquement précise la classe de ces fonctions. L’outil le plus connu est sans doute celui d’Alan Turing, qui consiste à concevoir des machines théoriques à calculer qu’on appelle « machines de Turing ». Mais d’autres cadres théoriques ont aussi été développés, comme le λ-calcul, la théorie des fonctions récursives ou les systèmes de Post. Or il est possible de démontrer que toute fonction calculable dans l’un de ces cadres est calculable aussi dans les autres. Cela invite à penser que la notion de fonction mécaniquement calculable est une notion théorique « robuste » et qu’elle peut suffire pour capturer la notion d’algorithme. Certes, on pourrait déjà objecter qu'il y a des algorithmes qui ne se comportent pas stricto sensu comme des fonctions, car ils donnent lieu à plusieurs sorties possibles pour la même entrée.

Mais il y a une raison plus profonde de douter que l'étude des fonctions mécaniquement calculables suffise à définir ce qu'est un algorithme. Cette étude se limite à considérer les fonctions d'un point de vue purement extensionnel : une fonction est simplement considérée comme un ensemble de couples « entrée-sortie ». Pour montrer qu'une fonction est mécaniquement calculable, il suffit par exemple de montrer qu'il existe une machine de Turing ou un λ-terme qui la calcule. Mais il est possible que la machine de Turing et le λ-terme en question calculent les mêmes sorties en relation aux mêmes entrées de façon différente. La machine de Turing et le λ-terme correspondraient en ce sens à deux programmes différents pour calculer la même fonction. Ainsi, il peut y avoir deux programmes, l’un plus rapide que l'autre, pour calculer les valeurs de la fonction qui génère la suite de Fibonacci. Peut-on dire que ces deux programmes suivent, ou mieux, implémentent le même algorithme ? Si l’on considère que les algorithmes sont des entités intensionnelles, et non pas seulement des entités extensionnelles comme le sont les fonctions, alors la réponse peut être négative. Plus précisément, la réponse sera négative si l’on considère qu'un algorithme ne correspond pas simplement au fait d'assurer l'existence d’une procédure permettant d'obtenir mécaniquement une sortie à partir d'une certaine entrée, mais prend aussi en considération la manière dont on effectue le calcul qui lie l'entrée à la sortie. En fait, une situation analogue se présente s’agissant des démonstrations. Pour montrer qu'un certain énoncé est un théorème, il suffit de montrer qu'il existe une démonstration de cet énoncé ; mais il peut y avoir différentes manières de démontrer le même théorème. Par exemple, on peut chercher à donner une démonstration plus simple qu'une autre. Comment savoir alors quand deux démonstrations sont en fait la même ?

La branche de la logique intitulée « théorie de la démonstration » étudie les démonstrations comme de véritables objets d'une théorie mathématique. Cette théorie développe notamment des outils techniques spécifiques pour pouvoir effectuer des opérations sur les démonstrations et d’étudier formellement leurs propriétés. Il s’agit en ce sens d’une étude des démonstrations d’un point de vue général et abstrait. L'idée du projet GoA est d'explorer la possibilité de développer une théorie similaire pour les algorithmes et de fonder ainsi une « théorie générale des algorithmes ». Pour ce faire, le projet prend comme point de départ un résultat de logique-mathématique connu sous le nom d’isomorphisme de Curry-Howard. Ce résultat établit une correspondance entre les démonstrations formelles de certaines théories logiques – habituellement écrites dans le formalisme de la déduction naturelle ou du calcul des séquents – et des programmes informatiques – habituellement écrits dans le langage du λ-calcul. Dans ce cadre, se demander si deux démonstrations sont la même revient à se demander si deux programmes sont le même. On peut alors effectuer un transfert de questions et de méthodes d’un domaine à un autre : de la logique et des mathématiques à l’informatique théorique, et vice versa. En outre, si l’on considère qu’écrire un programme est une manière d’implémenter un algorithme, alors se poser des questions sur l’identité entre programmes devient aussi une manière de se poser des questions sur l’identification des algorithmes. Le projet GoA se situe donc tout naturellement au carrefour de la logique, de la philosophie des mathématiques et de la philosophie de l’informatique.

Une recherche interdisciplinaire

Alberto Naibo : Le projet GoA réunit plusieurs collègues français et étrangers. La plupart d’entre eux sont membres de l’Institut d’histoire et de philosophie des sciences et des techniques (IHPST, UMR 8590), mais certains viennent d’autres universités françaises – comme Jean-Baptiste Joinet, professeur à l’université de Lyon 3 ou Liesbeth de Mol, chercheuse CNRS à l’université de Lille – ou d'universités étrangères – comme Mattia Petrolo, maître de conférences à l’université fédérale de l’ABC de São Paulo, ou Walter Dean, maître de conférences à l’université de Warwick (mais qui sera chercheur résident à l’Institut des Études Avancées de Paris pendant l’année 2022-2023). Nous sommes principalement de « jeunes » chercheurs dont les compétences et les formations sont différentes. Par exemple, Walter Dean possède une double formation, avec un doctorat en philosophie et un autre en informatique théorique. Mais nous avons aussi un mathématicien comme Thomas Seiller, qui a reçu une formation de logique et philosophie à Paris 1 ; c’est justement pendant nos études que nous nous sommes rencontrés, il y a désormais une quinzaine d’années, et nous avons depuis continué à collaborer pour des articles et des projets communs. Les compétences et les instruments mathématiques que Thomas a développés pour attaquer des questions de logique et de complexité calculatoire jouent d’ailleurs un rôle fondateur pour le projet GoA. Les philosophes impliqués dans le projet ont aussi des profils interdisciplinaires, orientés vers les mathématiques, l’informatique et la physique. Par exemple, Filippos Papayannopoulos, qui a été recruté comme chercheur postdoctoral au sein du projet, a une double formation en physique et philosophie des sciences. Mais je peux également mentionner Pierre Wagner, qui a écrit l’une des premières thèses sur l’importance philosophique de l’informatique et de l’intelligence artificielle, ou Marco Panza, qui travaille actuellement sur la manière dont le traitement des grosses bases de données change notre manière d’appliquer les mathématiques dans les sciences. Quant à Liesbeth de Mol, Jean-Baptiste Joinet, Mattia Petrolo et Walter Dean, mentionnés auparavant, leur travail s’inscrit également à l’interface entre philosophie, logique et informatique théorique.

Remarquons aussi que c'est cette interdisciplinarité qui a permis, assez naturellement, de créer de nouvelles interactions avec d'autres collègues de Paris 1, intéressés par la question des algorithmes et de l'IA et venant d'horizons différents. Par exemple, au sein des initiatives d'UNA Europa autour de « Sciences des données et IA », j'ai pu faire la rencontre du collègue Stéphane Lamassé, de l'UFR d'Histoire, et commencer à développer avec lui un dialogue et un regard croisé sur les aspects historico-philosophiques de la notion d'algorithme.

En ce sens, l'un des objectifs du projet GoA est d'éviter de faire de notre approche logico-formelle de la notion d'algorithme un dogme, et de nourrir notre analyse d'autres approches d’une notion qui, par nature, ne se borne pas à un seul domaine de discours. C'est pourquoi nous avons organisé, au sein du projet GoA, des journées d'études visant à comparer l'analyse de la notion d'algorithme en logique et en droit.

L’adoption d’une approche géométrique pour étudier les algorithmes

Alberto Naibo : Notre hypothèse de travail est qu’un véritable statut scientifique ne peut être attribué aux algorithmes que si une représentation mathématique précise peut leur être donnée, représentation permettant d’exprimer des propriétés mesurables. L’idée fondamentale du projet consiste à adopter un point de vue géométrique afin de concevoir une telle représentation. Ce point de vue géométrique devrait permettre de préciser les relations entre la notion d’algorithme et d’autres notions similaires – et pourtant distinctes – comme celles de calcul ou de programme. Cette analyse a d’ailleurs pour ambition d’ouvrir la voie à l’élaboration d’une ontologie propre à l’informatique et de considérer cette dernière comme une véritable « théorie mathématisée », à l’instar de la physique.  C’est là un point essentiel du projet : l’analyse technique de la notion d’algorithme est indissociable de son analyse conceptuelle. La notion d’algorithme est une notion que nous retrouvons à la fin d’un processus d’« ascension conceptuelle » partant de la notion de calcul et passant par celle de programme. Pour mieux comprendre cette idée, et pour expliquer en quoi consiste le point de vue géométrique mentionné tout à l’heure, je dois entrer un peu plus dans les détails.

Tout d’abord, la référence à la physique comme idéal de théorie scientifique mathématisée n’est pas hasardeuse. Il existe des travaux, comme ceux de Robin Gandy (un élève de Turing), qui établissent un lien entre calcul et physique. Plus précisément, un processus de calcul peut être vu comme un processus physique représentable au moyen d’un système dynamique, tel qu’il est communément décrit en mathématiques, c’est-dire au moyen d’un espace X et d’une fonction ƒ allant de X vers X. En ce sens, un calcul est analysé comme un phénomène déterministe, puisqu’il est décrit de manière fonctionnelle : à chaque entrée correspond une et une seule sortie. Cependant, la pratique informatique contemporaine invite à considérer des programmes non déterministes, puisque pouvant donner lieu à des sorties différentes en correspondance de la même entrée. Par exemple, un programme probabiliste, quand il est exécuté deux fois sur la même entrée, peut donner lieu à deux résultats différents. Un programme non déterministe permet en ce sens de décrire à la fois plusieurs calculs possibles, même si chaque fois que le programme est exécuté, un seul de ces calculs finit par être actualisé et par donner lieu à un processus qui lui, en revanche, est bien déterministe. Cela suggère l'idée que c'est en passant du niveau du calcul à celui du programme qu'on peut rendre compte des différents modes ou manières possibles de réaliser un calcul. C'est ici que la notion de « modèle de calcul » devient cruciale. Si l'on veut établir un pont entre la dimension du calcul et celle du programme, il faut adopter une notion de modèle de calcul qui puisse donner lieu à quelque chose de plus général que les systèmes dynamiques (en traitant ces derniers comme des cas particuliers), mais être elle-même généralisable pour capturer une notion plus riche comme celle de programme. Notre idée est de concevoir un modèle de calcul comme une action sur un espace. On peut penser cet espace comme celui de toutes les configurations possibles d’une certaine machine (qu’elle soit théorique comme celle de Turing ou concrète comme celle d’un ordinateur) et penser ensuite que les opérations primitives de la machine définissent une action sur cet espace. Or, puisque nous pouvons toujours produire de nouvelles opérations en appliquant les opérations primitives les unes après les autres, d’un point de vue mathématique, ce que nous sommes en train de faire consiste à générer un monoïde à partir de ces opérations primitives. D’une manière abstraite, un modèle de calcul peut être alors conçu comme l’action d’un monoïde M sur un espace X. C’est ici qui émerge le point de vue géométrique à la base du projet GoA. Pour comprendre cela, il faut rappeler l’idée fondamentale du programme développé par le mathématicien Felix Klein à la fin du 19^e siècle, connu sous le nom de « programme d’Erlangen », à savoir la possibilité de classifier les différents types de géométries sur la base de l’action d’un groupe de transformations sur un espace (et des invariants engendrés par ces transformations). Le projet GoA repose sur une idée similaire : classifier les programmes sur la base de l’action d’un monoïde d’opérations sur un espace, et caractériser ensuite les algorithmes comme des structures plus générales implémentées par les programmes. Plus précisément, il s’agit de considérer un programme comme un « graphage », c’est-à-dire comme la réalisation géométrique d’un graphe sur un espace mesurable : les sommets du graphe sont des sous-espaces (notamment des ensembles de configurations d’une machine) et les arêtes sont des éléments du monoïde M (notamment les opérations d’une machine). Pour donner un exemple, dans ce cadre, une instruction pour une machine de Turing comme « si on lit 0, alors on bouge la tête de lecture vers la droite » correspond au fait d’avoir une arête dont la source est le sous-espace des configurations où la tête de lecture de la machine lit le symbole 0 et cette arête correspond à l’élément du monoïde « bouger la tête de lecture vers la droite ». Je ne peux pas détailler davantage ici, mais on peut déjà remarquer que, puisque le sommet d’un graphe peut être la source de plusieurs arêtes et non d’un seul, ce cadre mathématique permet de manière naturelle de rendre compte des programmes non déterministes mentionnés auparavant.

Avec les graphages, il est en outre possible de rendre compte de la dynamique d’exécution d’un programme. Et si l’on associe un « poids » aux arêtes du graphage au moyen d’un nombre réel, il devient alors possible de définir une mesure sur les chemins d’exécution sur l’espace où le graphe est réalisé. Une fois les programmes définis via les graphages, l’idée est de définir les algorithmes comme une généralisation des programmes. On conçoit alors un algorithme comme un graphe étiqueté A et l’on dit qu’un graphage G implémente un A s’il existe un morphisme de A vers G. Or ce qui est important ici est qu’on ne demande pas forcément de faire correspondre, via le morphisme, une arête de A avec une arête de G. On peut aussi faire correspondre une arête de A avec un graphage tout entier, comme une sous-partie de G. Pour comprendre ce point, considérons l’algorithme d’Euclide pour calculer le plus grand commun diviseur (pgcd) de deux nombres entiers. On peut considérer un programme P_¹ qui l’implémente en prenant l’opération modulo – qui donne le reste de la division de deux entiers – comme étant primitive. Mais on peut aussi considérer un programme P_² qui calcule le pgcd en calculant le reste de la division de deux entiers au moyen d’un sous-programme P_³ qui définit l’opération modulo par itération de l’opération de soustraction. Or on peut dire que l’algorithme d’Euclide correspond à un graphe étiqueté A_^E où les arêtes qui portent la même étiquette, disons e, sont toutes mises en correspondance avec l’opération modulo qui est un élément du monoïde sur lequel repose le graphage G_¹ qui représente P_¹. Mais on peut aussi prendre ce même graphe étiqueté A_^E et faire correspondre les arêtes de type e avec le graphage G_³ qui représente P_³, et qui est à son tour une sous-partie du graphage G_² qui représente P_². On pourrait alors dire que P_¹ et P_² implémentent le même algorithme, puisque les graphages G_¹ et G_² implémentent le même graphe étiqueté. Mais on n’est pas du tout obligé de faire une telle identification. En fait, notre manière de traiter les algorithmes est suffisamment générale pour permettre d’associer ces deux programmes au même algorithme, mais elle permet aussi de les associer à deux algorithmes différents : tout dépend du type de morphisme que l’on entend considérer. Ce cadre permet d’ailleurs de rendre compte des situations où deux algorithmes différents sont implémentés par le même programme.

On touche ici à un point essentiel : notre caractérisation des algorithmes ne repose pas sur une analyse syntaxique qui voit les algorithmes comme de simples textes composés par des listes d’instructions ou d’opérations primitives, écrits dans un langage semi-formel comme celui d’un pseudo-code. Notre analyse se fait plutôt en termes d’actions ou d’étapes de calcul qui peuvent comporter l’emploi de plusieurs instructions ou opérations primitives pour être décrites. Une étape de calcul est en ce sens l’unité que nous considérons comme étant pertinente pour décrire une certaine procédure algorithmique. Il y a donc une hypothèse épistémologique cruciale en jeu ici : un algorithme n’est pas une entité qui existe indépendamment de quelqu’un qui l’emploie, d’un utilisateur. La manière de décrire un algorithme n’est pas quelque chose d’absolu mais possède un degré de granularité qui dépend du regard et de l’interprétation donnée par l’utilisateur. Identifier les algorithmes consiste alors à classifier les programmes selon certains types de comportement communs, mais ces types peuvent varier en fonction des aspects sur lesquels on se focalise lorsque l’on compare les programmes entre eux.

J’ai déjà été assez prolixe, mais je tiens à rajouter une chose qui permet de mieux comprendre le lien entre ce type de travail et celui que j’effectue en logique et en théorie de la démonstration mentionné auparavant. L’idée de voir les graphages comme des programmes vient des travaux de Thomas Seiller, qui les avaient employés pour étudier la structure des démonstrations de certains systèmes de logique linéaire sous le prisme de la correspondance de Curry-Howard. Or, puisque la logique linéaire est une logique qui permet de tenir compte des ressources consommées dans un calcul, il devient naturel d’employer le cadre mathématique des graphages pour s’attaquer à des questions de complexité calculatoire. Il s’agit de questions épistémologiques fondamentales, car elles concernent le problème de la faisabilité d’un calcul. Nous pouvons en effet nous demander si les capacités de calcul engendrées par l’emploi d’algorithmes peuvent aller indéfiniment au-delà de nos capacités cognitives et conduire à la création d’une sorte de « super-intelligence », ou s’il existe des limites théoriques que les humains et mêmes les algorithmes ne pourront jamais dépasser. 

⇒ Visionner : Qu'est qu'un algorithme ? Une approche géométrique" (intervention dans le cadre du séminaire du projet ANR CulturIA)

La place de l'IA dans le projet GoA

Alberto Naibo : La question de savoir quelles sont les tâches que nous pouvons réaliser grâce aux algorithmes et où ils se posent leurs limites nous amène tout naturellement à nous poser des questions en lien direct avec l’intelligence artificielle (IA).

De manière générale, on peut caractériser l’IA comme la mise en œuvre de programmes informatiques permettant de simuler des comportements ou d’aboutir à des résultats que nous considérons comme étant caractéristiques de l’intelligence humaine. L’histoire de l’IA s’avère par ailleurs assez complexe, d’autant plus qu’il s’agit d’un domaine qui a subi des changements importants lors de ces dernières années. En fait, on pourrait même dire que l’IA possède « plusieurs âmes », au sens où il existe plusieurs techniques, voire paradigmes, d’IA : il y a l’IA à laquelle on se réfère habituellement lors les débats publics actuels, qui focalise son attention sur le traitement des données avec un emploi massif d’instruments statistiques ; mais il y a aussi l’IA qui porte sur la question de la représentation des connaissances et repose sur l’emploi de langages et de théories logiques – comme les logiques modales, épistémiques ou non monotones –, et il y a également l’IA qui repose sur l’emploi de techniques venant de la combinatoire et du raisonnement automatique.

On remarque d’ailleurs que si, aujourd’hui, les exemples les plus paradigmatiques d’activités abordées par l’IA sont la reconnaissance et la classification d’objets, dans les années 50, au moment de la naissance de l’IA, les exemples paradigmatiques venaient plutôt du domaine des mathématiques. Par exemple, l’un des premiers résultats en IA a été l’élaboration d’un programme, le Logic Theorist, par Allan Newell, Herbert Simon et Clifford Shaw permettant de démontrer – ou mieux, de re-démontrer – une bonne partie des théorèmes des Principia Mathematica d’Alfred North Whitehead et Bertrand Russell. Le Logic Theorist reposait sur l’emploi d’heuristiques, c’est-à-dire sur des méthodes pratiques qui, même si elles ne garantissent pas toujours d’aboutir à une solution, ont le mérite d’être flexibles et de fonctionner dans la plupart des cas, avec des coûts de calcul assez réduits. Mais les travaux en recherche automatique de démonstrations ont aussi bénéficié de l’emploi de résultats de décision et de méthodes venant de la logique (comme la résolution ou l’unification). Ces travaux ont notamment donné lieu à quelques résultats notables, comme la démonstration en 1996 d’un problème d’algèbre abstraite, la conjecture de Robbins, au moyen d’un programme développé par William McCune et par son groupe de recherche. La démonstration de cette conjecture, qui était restée ouverte pendant environ soixante ans, a été générée de manière purement automatique en 8 jours de travail par un programme sur un processeur RS/6000.

C’est toutefois ces dernières années que les succès de l’IA dans le champ des mathématiques semblent devenir moins sporadiques et moins anecdotiques. Un rôle crucial est joué en ce sens par les SAT solvers, programmes fondés sur l’application d’algorithmes ou d’heuristiques pour la résolution du problème de la satisfiabilité de formules de la logique propositionnelle, c’est-à-dire le problème de savoir s’il existe une assignation de valeurs de vérité booléennes (le vrai ou le faux) aux variables propositionnelles d’une formule qui permet de la rendre vraie, ou si cette assignation n’existe pas. Grâce aux techniques venant des SAT solvers plusieurs problèmes ouverts en mathématiques ont été résolus, venant de la géométrie, comme la conjecture de Keller, ou d’une branche de la combinatoire dite théorie de Ramsey, comme le Boolean Pythagorean Triples Problem (BPTP). L’idée, derrière la résolution de ces problèmes, est de traduire ou « coder » l’énoncé du problème en une formule de la logique propositionnelle et de vérifier ensuite si elle est satisfaisante ou non. Or la formule considérée par Marijn Heule, Oliver Kullmann et Victor Marek dans la solution du BPTP contient 7 825 variables propositionnelles, et puisqu'on peut assigner à chacune de ces variables soit la valeur « vrai » soit la valeur « faux », il y a en principe 2^{7 825} cas possibles à examiner. Il s’agit d’un nombre de cas allant bien au-delà du type de grandeurs que nous sommes habitués à traiter. Le nombre 2^{7 825} est en effet plus grand que 10^{2 300}, alors qu’on estime que le nombre de particules dans l’univers n’est pas plus grand que 10¹⁰⁰. Par conséquent, même en faisant correspondre une assignation de valeurs de vérité à chaque particule de l’univers, on serait encore très loin d’avoir considéré toutes les assignations possibles. Cependant, l’application de certains algorithmes de SAT solving à cette formule permet, de façon complètement automatique, de la réarranger et de la décomposer jusqu’à réduire drastiquement le nombre de cas à considérer (en éliminant par exemple les cas non pertinents) et de les rendre vérifiables grâce à la seule force de calcul des ordinateurs. Plus précisément, en faisant tourner ces algorithmes pendant 2 jours sur 800 super-processeurs travaillant en parallèle, Heule, Kullmann et Marek ont réussi à obtenir une réponse qui énonce que la formule initiale n’était pas satisfaisable. La solution au problème initial a été donc trouvée par l’emploi de la force brute des algorithmes et des ordinateurs (le concept de recherche de solution par force brute n'est pas nouveau; en russe on a d'ailleurs un nom pour cela, c'est « perebor »). Cette situation est bien différente d’autres cas de démonstrations assistées par ordinateur, comme la célèbre démonstration du théorème de quatre couleurs de la part de Kenneth Appel et Wolfgang Haken. Là aussi, la démonstration passe par une analyse de cas, un millier environ (cela dépend des versions de la démonstration). Toutefois, non seulement il s’agit ici d’un nombre infime de cas par rapport à celui du BPTP, mais en plus ce nombre de cas est déterminé à la main par les mathématiciens sur la base de leur analyse du problème. L’ordinateur sert juste à vérifier ces cas. Avec le BPTP, en revanche, les cas effectivement vérifiés par l’ordinateur (et qui sont donc inférieurs aux 2^{7 825} cas possibles en principe) sont déterminés par l’application des algorithmes de SAT solving à la formule initiale. Ils sont déterminés d'une manière purement mécanique, qui ne demande aucune intervention ou ingéniosité humaine. La manière de résoudre le problème est donc pour ainsi dire aveugle. Doit-on penser qu’il s’agit alors d’une démonstration vide de toute valeur épistémique et explicative ou est-ce qu'une quelque forme d'« intelligence mécanique » est en jeu ici ? Peut-on penser d'ailleurs qu’en analysant la structure des algorithmes employés dans cette démonstration par le biais des instruments développés au sein du projet GoA il est possible d’extraire des informations pertinentes, qui permettraient finalement de comparer cette démonstration avec d’autres démonstrations plus « traditionnelles » ? En ce sens, l’étude des algorithmes joue un rôle essentiel si l’on veut comprendre la manière dont la notion de démonstration mathématique est en train d’évoluer grâce à l’influence des techniques venant de l’IA.