Théoricien de la logique - Logic Theorist

Logic Theorist est un programme informatique écrit en 1956 par Allen Newell , Herbert A. Simon et Cliff Shaw . C'était le premier programme délibérément conçu pour effectuer un raisonnement automatisé et est appelé "le premier programme d' intelligence artificielle ". Cela prouverait finalement 38 des 52 premiers théorèmes des Principia Mathematica de Whitehead et Russell , et trouverait de nouvelles preuves plus élégantes pour certains.

Histoire

En 1955, lorsque Newell et Simon ont commencé à travailler sur le théoricien de la logique, le domaine de l' intelligence artificielle n'existait pas encore. Même le terme lui-même ("intelligence artificielle") ne serait pas inventé avant l'été suivant.

Simon était un politologue qui avait déjà produit des travaux classiques sur l'étude du fonctionnement des bureaucraties et développé sa théorie de la rationalité limitée (pour laquelle il remportera plus tard un prix Nobel ). L'étude des organisations commerciales nécessite, comme l' intelligence artificielle , un aperçu de la nature de la résolution de problèmes humains et de la prise de décision . Simon se souvient avoir consulté RAND Corporation au début des années 50 et avoir vu un imprimeur taper une carte en utilisant des lettres ordinaires et des signes de ponctuation comme symboles. Il s'est rendu compte qu'une machine capable de manipuler des symboles pouvait tout aussi bien simuler la prise de décision et peut-être même le processus de la pensée humaine.

Le programme qui a imprimé la carte avait été écrit par Newell, un scientifique de RAND étudiant la logistique et la théorie de l'organisation . Pour Newell, le moment décisif a été en 1954 lorsqu'Oliver Selfridge est venu à RAND pour décrire son travail sur le pattern matching . En regardant la présentation, Newell a soudainement compris comment l'interaction d'unités simples et programmables pouvait accomplir un comportement complexe, y compris le comportement intelligent des êtres humains. « Tout s'est passé en un après-midi », dira-t-il plus tard. Ce fut un moment rare d'épiphanie scientifique.

"J'avais un tel sentiment de clarté que c'était une nouvelle voie, et une que j'allais emprunter. Je n'ai pas eu cette sensation très souvent. Je suis assez sceptique, et donc je ne pars pas normalement Complètement absorbé dedans - sans exister avec les deux ou trois niveaux de conscience pour que vous travailliez, et conscient que vous travaillez, et conscient des conséquences et des implications, la normale mode de pensée. Non. Complètement absorbé pendant dix à douze heures.

Newell et Simon ont commencé à parler de la possibilité d'apprendre aux machines à penser. Leur premier projet était un programme qui pourrait prouver des théorèmes mathématiques comme ceux utilisés dans Bertrand Russell et Alfred North Whitehead de Principia Mathematica . Ils ont demandé l'aide du programmeur informatique Cliff Shaw , également de RAND, pour développer le programme. (Newell dit que « Cliff était le véritable informaticien des trois »).

La première version a été simulée à la main : ils ont écrit le programme sur des cartes 3x5 et, comme le rappelle Simon :

En janvier 1956, nous avons réuni ma femme et mes trois enfants avec des étudiants diplômés. A chaque membre du groupe, nous avons remis une des cartes, afin que chacune devienne, en effet, une composante du programme informatique... Ici, c'était la nature imitant l'art imitant la nature.

Ils ont réussi à montrer que le programme pouvait prouver avec succès des théorèmes ainsi qu'un mathématicien talentueux. Finalement, Shaw a pu exécuter le programme sur l'ordinateur des installations de RAND à Santa Monica.

À l'été 1956, John McCarthy , Marvin Minsky , Claude Shannon et Nathan Rochester organisent une conférence sur le thème de ce qu'ils appellent « l' intelligence artificielle » (terme inventé par McCarthy pour l'occasion). Newell et Simon ont fièrement présenté au groupe le théoricien de la logique et ont été quelque peu surpris lorsque le programme a reçu un accueil mitigé. Pamela McCorduck écrit que « la preuve est que personne, à l'exception de Newell et Simon eux-mêmes, n'a ressenti la signification à long terme de ce qu'ils faisaient ». Simon confie que « nous étions probablement assez arrogants à propos de tout cela » et ajoute :

Ils ne voulaient pas entendre parler de nous, et nous ne voulions certainement pas entendre parler d'eux : nous avions quelque chose à leur montrer ! ... D'une certaine manière, c'était ironique parce que nous avions déjà fait le premier exemple de ce qu'ils recherchaient ; et deuxièmement, ils n'y ont pas prêté beaucoup d'attention.

Le théoricien de la logique a rapidement prouvé 38 des 52 premiers théorèmes du chapitre 2 des Principia Mathematica . La preuve du théorème 2.85 était en fait plus élégante que la preuve produite laborieusement à la main par Russell et Whitehead. Simon a pu montrer la nouvelle preuve à Russell lui-même qui « a répondu avec ravissement ». Ils ont tenté de publier la nouvelle preuve dans The Journal of Symbolic Logic mais elle a été rejetée au motif qu'une nouvelle preuve d'un théorème mathématique élémentaire n'était pas notable, négligeant apparemment le fait que l'un des auteurs était un programme informatique.

Newell et Simon ont formé un partenariat durable, fondant l'un des premiers laboratoires d'IA au Carnegie Institute of Technology et développant une série de programmes et d'idées d' intelligence artificielle influents , notamment GPS , Soar et leur théorie unifiée de la cognition .

L'influence du théoricien de la logique sur l'IA

Logic Theorist a introduit plusieurs concepts qui seraient au cœur de la recherche sur l'IA :

Raisonnement comme recherche
Logic Theorist a exploré un arbre de recherche : la racine était l' hypothèse initiale , chaque branche était une déduction basée sur les règles de la logique. Quelque part dans l'arbre se trouvait le but : la proposition que le programme avait l'intention de prouver. Le chemin le long des branches qui menait au but était une preuve  – une série d'énoncés, chacun déduit en utilisant les règles de la logique, qui menait de l'hypothèse à la proposition à prouver.
Heuristique
Newell et Simon se sont rendu compte que l' arbre de recherche allait croître de façon exponentielle et qu'ils devaient « couper » certaines branches, en utilisant des « règles empiriques » pour déterminer quelles voies étaient peu susceptibles de conduire à une solution. Ils ont appelé ces règles ad hoc « heuristiques », en utilisant un terme introduit par George Pólya dans son livre classique sur la preuve mathématique , Comment le résoudre . (Newell avait suivi des cours de Pólya à Stanford ). L'heuristique deviendrait un domaine de recherche important en intelligence artificielle et reste une méthode importante pour surmonter l' explosion combinatoire insoluble des recherches en croissance exponentielle.
Traitement de liste
Pour implémenter Logic Theorist sur un ordinateur, les trois chercheurs ont développé un langage de programmation, IPL , qui utilisait la même forme de traitement de liste symbolique qui constituerait plus tard la base du langage de programmation Lisp de McCarthy , un langage important encore utilisé par les chercheurs en IA.

Implications philosophiques

Pamela McCorduck écrit que la théoricienne de la logique était « la preuve positive qu'une machine pouvait effectuer des tâches jusque-là considérées comme intelligentes, créatives et uniquement humaines ». Et, en tant que tel, il représente une étape importante dans le développement de l' intelligence artificielle et notre compréhension de l'intelligence en général.

Simon a dit à une classe de troisième cycle en janvier 1956 : « À Noël, Al Newell et moi avons inventé une machine à penser », et écrirait :

[Nous] avons inventé un programme informatique capable de penser de manière non numérique et avons ainsi résolu le vénérable problème corps-esprit , expliquant comment un système composé de matière peut avoir les propriétés de l'esprit.

Cette affirmation, selon laquelle les machines peuvent avoir un esprit tout comme les gens, sera plus tard nommée « IA forte » par le philosophe John Searle . Il reste un sujet de débat sérieux jusqu'à nos jours.

Pamela McCorduck voit également dans The Logic Theorist le début d'une nouvelle théorie de l'esprit, le modèle de traitement de l' information (parfois appelé computationalisme ). Elle écrit que « ce point de vue deviendrait central dans leurs travaux ultérieurs et, à leur avis, aussi central pour comprendre l'esprit au vingtième siècle que le principe de sélection naturelle de Darwin l'avait été pour comprendre la biologie au dix-neuvième siècle ». Newell et Simon formaliseront plus tard cette proposition comme l' hypothèse des systèmes de symboles physiques .

Remarques

Citations

Les références

Liens externes