Réponse courte
Le Logic Theorist était un programme informatique créé en 1955-1956 par Allen Newell, Herbert Simon et Cliff Shaw, qui trouvait des démonstrations de théorèmes des Principia Mathematica de Whitehead et Russell. Il n’essayait pas toutes les démonstrations possibles; il utilisait des règles empiriques, ou heuristiques, un peu comme le ferait une personne, et c’est pourquoi on l’appelle souvent le premier programme d’intelligence artificielle.
Question de suivi Comment l’idée de recherche heuristique du Logic Theorist se retrouve-t-elle dans l’IA d’aujourd’hui?
Avant même qu’on s’entende sur l’expression « intelligence artificielle », deux chercheurs et un programmeur ont entrepris de faire faire à un ordinateur quelque chose qui semblait exiger une vraie réflexion : démontrer des théorèmes de logique. Le résultat, le Logic Theorist, pouvait prendre un énoncé tiré de l’un des livres de mathématiques les plus célèbres du XXe siècle et trouver une suite d’étapes qui montrait qu’il était vrai.
Ce qui le rendait remarquable, ce n’était pas la vitesse brute. C’était la stratégie. Au lieu de passer en revue toutes les combinaisons possibles, le programme travaillait un peu comme un élève au tableau : il regardait ce qu’il devait démontrer, remarquait des ressemblances avec ce qu’il savait déjà et essayait d’abord les coups les plus prometteurs.
Qui l’a créé, et quand
L’équipe réunissait Allen Newell, un jeune chercheur de la RAND Corporation à Santa Monica, en Californie; Herbert A. Simon, professeur au Carnegie Institute of Technology de Pittsburgh et consultant à la RAND; et J. C. « Cliff » Shaw, programmeur à la RAND. Newell et Simon ont commencé le travail en 1955. En janvier 1956, la conception était assez avancée pour que Simon annonce à ses étudiants : « Pendant les Fêtes, Al Newell et moi avons inventé une machine qui pense. »
Aucun ordinateur n’était encore libre pour le faire tourner; ils l’ont donc testé à la main. Simon a réuni sa femme, ses trois enfants et quelques étudiants des cycles supérieurs, a remis à chaque personne une carte décrivant une partie du programme, et leur a fait jouer ensemble ses étapes. Shaw s’est ensuite chargé du gros travail : le faire fonctionner sur l’ordinateur JOHNNIAC de la RAND.
La description formelle est parue dans un document de la RAND signé par Newell et Simon, daté du 12 juillet 1956 et intitulé « The Logic Theory Machine ». Ils l’ont présenté le 10 septembre 1956 lors d’un symposium de l’Institute of Radio Engineers tenu au MIT, à Cambridge, au Massachusetts. Cet été-là, ils avaient aussi montré le programme à l’atelier de Dartmouth sur l’intelligence artificielle, où, selon la plupart des récits, les autres participants ont été moins impressionnés que ses créateurs ne s’y attendaient.
Le problème auquel il s’attaquait
Les théorèmes venaient des Principia Mathematica, l’œuvre immense dans laquelle Alfred North Whitehead et Bertrand Russell tentaient de reconstruire les mathématiques à partir de la logique pure. Le deuxième chapitre part de cinq axiomes, des énoncés tenus pour vrais, et en tire des dizaines de théorèmes à l’aide de quelques règles :
- Substitution : dans un énoncé vrai, on peut remplacer partout une variable par n’importe quelle expression.
- Détachement : si « A » est vrai et que « A implique B » est vrai, alors B est vrai.
- Remplacement : on peut remplacer une expression par sa définition, par exemple « p implique q » par « non-p ou q ».
Une démonstration n’est qu’une liste d’énoncés, chacun étant un axiome, un théorème déjà démontré ou le résultat de l’application de l’une de ces règles.
Comment il fonctionnait
En principe, un ordinateur pourrait trouver n’importe quelle démonstration par force brute : construire tous les énoncés accessibles en une étape, puis en deux, puis en trois, et attendre que la cible apparaisse. Newell et Simon ont montré pourquoi cela échoue. Si chaque étape peut se poursuivre de dix façons, il y a déjà 10 000 chaînes de quatre étapes. Une recherche qui choisit à l’aveugle parmi elles devra en essayer environ 5 000. Mais si des indices permettent au programme d’écarter huit des dix options à chaque étape, il ne reste que 16 chaînes de quatre étapes.
Ces indices sont des heuristiques : des règles empiriques qui fonctionnent souvent, mais sans aucune garantie. Le document trace une ligne nette entre les algorithmes, des procédures systématiques qui sont certaines d’aboutir, et les méthodes heuristiques, plus rapides et plus humaines. Le Logic Theorist en avait plusieurs :
| Méthode | Ce qu’elle tente | Analogie de tous les jours |
|---|---|---|
| Substitution | Trouver un théorème connu qui ressemble au but, puis faire correspondre les deux | Remarquer qu’un nouveau casse-tête est un ancien avec d’autres étiquettes |
| Détachement | Trouver un théorème « B implique le but », puis se donner « démontrer B » comme nouveau sous-problème | « Pour entrer dans la maison, il me faut la clé; alors, où est la clé? » |
| Enchaînement | Relier « A implique B » et « B implique C » pour arriver à « A implique C », vers l’avant ou vers l’arrière | Planifier un trajet en passant par une ville de correspondance |
Toutes ces méthodes travaillent à rebours à partir du but. Chacune peut créer de plus petits problèmes, que le programme met en réserve et attaque à tour de rôle. L’exemple détaillé du document démontre le théorème 2.01 en trois étapes : partir de l’axiome 1.2, substituer « non-p » à p, puis appliquer une définition.
Pour construire tout cela, l’équipe a aussi créé un nouveau type de langage de programmation, l’IPL (Information Processing Language), qui stockait les données sous forme de listes chaînées pouvant grandir et changer pendant l’exécution du programme. C’était inhabituel pour des ordinateurs conçus surtout pour faire des calculs numériques.
À essayer : prenez l’énoncé « s’il pleut, la rue est mouillée; si la rue est mouillée, les voitures ralentissent ». Écrivez la conclusion que vous pouvez tirer en enchaînant ces deux lignes, puis expliquez en une phrase quelle étape consistait à « travailler à rebours » si vous partiez de « les voitures ralentissent ».
Pourquoi il a compté
Le Logic Theorist a fini par trouver des démonstrations pour 38 des 52 premiers théorèmes du deuxième chapitre des Principia. Pour le théorème 2.85, il a trouvé une démonstration plus courte et plus élégante que celle publiée par Whitehead et Russell, et Simon l’a montrée à Russell, qui en aurait été ravi. Une tentative de publier cette démonstration dans The Journal of Symbolic Logic a été refusée.
Son importance plus large tenait à trois idées. Il traitait l’ordinateur comme une machine à manipuler des symboles, pas seulement des nombres. Il montrait qu’une recherche guidée par des heuristiques pouvait résoudre des problèmes que la force brute ne pouvait pas résoudre. Et il était présenté comme un modèle de la façon dont les gens pensent, ce qui a lancé l’étude de la pensée comme traitement de l’information. Newell et Simon sont passés directement à un successeur plus général, le General Problem Solver, et l’idée de traitement de listes derrière l’IPL a nourri le langage Lisp de John McCarthy.
Comment l’idée de recherche heuristique du Logic Theorist se retrouve-t-elle dans l’IA d’aujourd’hui?
Presque tous les systèmes qui doivent choisir parmi de nombreuses options reposent encore sur le marché conclu par le Logic Theorist : renoncer à la garantie de tout essayer en échange d’une bonne chance de trouver vite une réponse. Le planificateur d’itinéraire de votre téléphone ne teste pas toutes les routes du pays; il utilise une estimation de la distance restante pour se concentrer sur les rues prometteuses. Les programmes d’échecs et de go élaguent les coups qui semblent sans espoir pour pouvoir examiner plus en profondeur les autres.
Ce qui a changé, c’est l’origine des règles empiriques. En 1956, Newell et Simon les écrivaient à la main, d’après leur propre idée de la façon dont ils résolvaient des problèmes. Beaucoup de systèmes actuels apprennent plutôt leurs repères à partir de données. Les programmes de jeu de DeepMind, par exemple, entraînent un réseau de neurones à juger quels coups et quelles positions semblent bons, puis se servent de ce jugement pour orienter une recherche.
La démonstration automatique de théorèmes se poursuit aussi comme domaine à part entière. Des programmes aident aujourd’hui à vérifier des démonstrations mathématiques et à s’assurer que des puces électroniques et des logiciels se comportent comme prévu. Ils sont bien plus puissants que le Logic Theorist, mais l’image de base reste la même : un but, un ensemble de règles et une recherche qui doit être astucieuse quant à l’endroit où chercher.
Sources
- The Logic Theory Machine: A Complex Information Processing System — Allen Newell and Herbert A. Simon, RAND Corporation (paper P-868), 12 juillet 1956
- Logic Theorist — Wikipedia (archived December 2018), 18 décembre 2018
- History of Lisp — John McCarthy, Stanford University Artificial Intelligence Laboratory, 12 février 1979