В предудущей части я упоминал о том, что уже в 50-х появились первые попытки «научить компьютер думать», то есть доказывать математические утверждения. Программа, реализующая «традиционную» логику, получается довольно небольшой — я уже упоминал Logical Theorist — но при этом результат ее работы впечатляет. Например, будучи снабженной списком аксиом из книги Рассела и Уайтхеда «Основания математики», эта программа смогла за разумное время доказать 38 из 52 приведенных во второй главе книги теорем.
Это считалось большим успехом в области «искуственного интеллекта», авторы Logical Theorist давали прогнозы, что в ближайшие десять-пятнадцать (то есть к 1965-1970 году) лет ЭВМ смогут доказывать те же математические утверждения, что и люди.
К сожалению, этого не произошло. Не только из-за сложностей формализации любой более-менее содержательной математической теории, но и из-за связанных с теоремами Геделя трудностей. Например, для любой системы аксиом можно привести пример утверждения, которое нельзя ни доказать, ни опровергнуть. С другой стороны, все утверждения, которые можно доказать, перечислимы, то есть существует алгоритм, который будет последовательно выводить их. В простейшем виде он называется «поиск в ширину» и известен любому программисту.
Правда, сегодня существует несколько смежных с доказательством теорем направлений. Есть несколько систем для автоматической проверки доказательств (например, Mizar), важный «побочный продукт» которых — сборники формализованных определений и доказательств. Другое популярное направление — поиск всех утверждений, которые можно доказать, в надежде на то, что среди них найдется что-то новое. По-английски это называется discovery system, «открывающая» система. Одной из первых таких систем стала Automated Mathematician, о «потомке» которой, программе Eurisko, стоит рассказать подробнее.
Automated Mathematician представлял собой программу на Lisp, умевшую по определенным правилам модифицировать другие программы на том же языке, которые интерпретировались, как определения математических понятий. В 1976 Дуглас Ленат выделил «ядро» этой системы — «язык» RRL-1 (Representation Representation Language) — фактически, набор правил логического вывода. Eurisko — система, применявшая эти правила, — была обобщением Automated Mathematician и могла применяться в различных областях знаний — от проектирования СБИС до… настольных стратегических игр.
Да, не смейтесь, в 1981 году правила настолки Traveller (посвященной сражениям в космосе) были формализованы и внесены в Eurisko, и программа выработала довольно парадоксальную, но стопроцентно выигрышную стратегию — удивившую всех, кто пытался применить там, скажем, «законы» военно-морской тактики. Это считалось очень интересной демонстрацией «искуственного интеллекта» и даже привело к изменению правил игры — правда, в 1982 году Eurisko снова «победила» на соревнованиях, найдя очередную лазейку в новых правилах. После этого, во-первых, применение «сгенерированных компьютером» стратегий на соревнованиях по Traveller было запрещено, а во-вторых — проектом заинтересовалось DARPA, агентство Пентагона по перспективным научным разработкам. Уж что у них там вышло — не знаю.
К вопросу об искуственном интеллекте тесно примыкает построение баз знаний. Можно формализовать правила логического вывода, но очень важными оказываются «аксиомы» — а даже в геометрии их, по Гильберту, насчитывается 20 штук. Все тот же Ленат, обосновывая свой последующий проект Cyc, говорил, что «разум — это десять миллионов правил». Разумеется, что с десятью миллионами правил работать эффективно очень и очень сложно — а если ядро системы написано на пользующемся славой «медленного» Lisp — то вообще невозможно. Правда, есть технологии, позволяющие делать это более эффективно, и о «логическом программировании» речь пойдет в следующей части.
Охуенная статья в нью-йоркере, спасибо.