Мивары: 25 лет создания искусственного интеллекта. Олег Варламов
изначально предназначен для решения сложных реальных задач, поэтому он другой, и надо это признать.
Автоматическое доказательство теорем – одна из старейших областей возможного применения ИИ, где было много достижений, исследований и программ, включая Универсальный решатель задач Ньюэлла и Саймона. Люгер подчеркивает, что именно "…эта ветвь принесла наиболее богатые плоды…" [264, стр. 44]. Благодаря исследованиям в этой области были формализованы алгоритмы поиска и разработаны языки формальных представлений, такие как исчисление предикатов и логический язык программирования Пролог. Приведем обоснование Дж. Люгера: "… привлекательность автоматического доказательства теорем основана на строгости и общности логики. В формальной системе логика располагает к автоматизации. Разнообразные проблемы можно попытаться решить, представив описание задачи и существенно относящуюся к ней информацию в виде логических аксиом и рассматривая различные случаи задачи как теоремы, которые нужно доказать. Этот принцип лежит в основе автоматического доказательства теорем и систем математических обоснований" [264, стр. 44]. Далее следует замечательный вывод и итог 20 века в этой наиболее богатой ветви: "К сожалению, в ранних пробах написать программу для автоматического доказательства, не удалось разработать систему, которая бы единообразно решала сложные задачи" [264, стр. 44]. Таким образом, Дж. Люгер подтверждает наш тезис о том, что в прошлом веке даже в самых передовых областях ИИ ученые не смогли решить сложные задачи, а значит, нужны принципиально новые подходы и исследования, к числу которых относится и миварный подход.
Приведем обоснование ограниченности возможностей автоматического доказательства теорем, которое имеет важное значение для дальнейших исследований, как минимум, показывая, куда НЕ надо идти. Как говорится, отрицательный результат – это тоже результат!!! Итак, обоснование Дж. Люгера: "Это было обусловлено способностью любой относительно сложной логической системы сгенерировать бесконечное количество доказуемых теорем: без мощных методик (эвристик), которые бы направляли поиск, программы доказывали большие количества не относящихся к делу теорем, пока не натыкались на нужную. Из-за этой неэффективности многие утверждают, что чисто формальные синтаксические методы управления поиском в принципе не способны справиться с такими большими пространствами, и единственная альтернатива этому – положиться на неформальные, специально подобранные к случаю (лат "ad hoc") стратегии, как это, похоже, делают люди. Это один из подходов, лежащих в основе экспертных систем… и он оказался достаточно плодотворным" [264, стр. 44]. Таким образом, возникают новые проблемы: работа с бесконечными множествами теорем и разработка эвристик, про которые ранее было показано, что они не гарантируют решение задачи. Конечно, за прошедшее время ученым удалось разработать мощные эвристики, основанные на оценке синтаксической формы логического выражения,