Представитель Шуры Люберецкого в ЖЖ (brat_luber) wrote,
Представитель Шуры Люберецкого в ЖЖ
brat_luber

Математика, логика и программирование. Часть третья, доказательство теорем

В предудущей части я упоминал о том, что уже в 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 – то вообще невозможно. Правда, есть технологии, позволяющие делать это более эффективно, и о “логическом программировании” речь пойдет в следующей части.

Запись опубликована в блоге Шуры Люберецкого. Вы можете оставлять свои комментарии там, используя свое имя пользователя из ЖЖ (вход по OpenID).

Tags: программирование
Subscribe

  • Про кофе

    Регулярно в фейсбуке встречаю ужасы от путешествующих по Италии, которые то ли не в то время суток заказали капуччино, то ли неправильно поставили…

  • А как это называется?

    А скажите, как называется то чувство, когда ты сначала хуесосишь чувака в твиторе за тупость, а потом видишь его юзерпик в корпоративном чате? И…

  • Электронный документооборот

    Пока тут Исавнин с Артамоновым кидают друг в друга какахами на хабре из-за дистанционного электронного голосования — реальные электронные…

Comments for this post were disabled by the author