Экспертные системы и автоматическое доказательство теорем

Методы интеллектуальных БД получили дальнейшее развитие при разработке автоматических консультирующих систем. Такие экспертные системы (Expert Systems) способны предоставить компетентный ответ пользователю на конкретный вопрос. Первые экспертные системы были созданы для применения, например, в медицине (диагностика заболеваний) и в геологии (оценка месторождений).

Одна из самых главных проблем в этой области заключается в том, как следует представлять и использовать знания экспертов, которые по своей сути являются в достаточной степени разнородными и противоречивыми данными.

Экспертные системы — системы искусственного интеллекта, включающие в себя знания об определенной, слабо структурированной и трудно формализуемой узкой предметной области и способные предлагать и объяснять пользователю разумные решения задач в этой области.

В настоящее время считается общепринятым, что структура экспертных систем состоит из пяти блоков (рис. 1.4). Совокупность трех блоков — Правила, Модель ситуации и Вывод — по сути, является интеллектуальной БД. Модули, позволяющие извлекать знания и объяснять выводы, превращают интеллектуальную БД в экспертную систему.

Рис. 1.4. Архитектура экспертной системы.

Сейчас чаще всего база знаний для экспертной системы — это набор правил. Простейший случай, когда правила имеют детерминированный характер^[1] и позволяют из имеющихся фактов выводить новые факты, как в интеллектуальной базе данных. Такой вариант детально рассматривается в гл. 2, где мы говорим о представлении знаний системами продукций.

Блок объяснений вывода фактически представляет машинный вывод результата в человеко-читаемой форме, так что пользователь может проследить, какие шаги рассуждений применяла экспертная система при решении задачи. Таким образом, доверие пользователя к ответу возрастает.

Наиболее важным и сложным является блок извлечения знаний. Результат работы этого блока понятен — это пополнение и изменение базы знаний. Исходные же данные могут быть различными. Не следует надеяться на то, что эксперт в предметной области просто так, «из головы», сформулирует эффективные правила рассуждений, причем сразу в том формате, который требуется в системе.

Одним из наиболее надежных считается метод постепенного пополнения и изменения базы знаний, причем поводом к изменению является каждый случай, когда система не смогла решить задачу или решила ее неправильно. В таком случае эксперт анализирует с помощью блока объяснения ход машинных рассуждений, определяет, какое правило было неудачным или какого правила не хватает, и добавляет его в базу знаний посредством блока извлечения знаний. Можно сказать, что экспертная система, подобно человеку, учится на ошибках.

В центре структуры экспертных систем находится блок вывода. В этом блоке правила применяются к фактам из модели ситуации, в результате получаются новые факты, к которым также применяются правила и т. д., пока не будет достигнута цель, т. е. требуемый факт. Этот процесс по существу является процессом поиска вывода в формальной теории (см. п. 4.1.2). Действительно, исходные факты из модели ситуации — это аксиомы. Мы применяем к ним правила, получаем новые факты, причем каждый новый факт получается из ранее полученных фактов. В конце концов, мы доходим (или не доходим) до целевого факта, т. е., говоря языком логических теорий, получаем заключение целевой теоремы. Таким образом, ядро всякой экспертной системы можно рассматривать как систему автоматического поиска вывода в некоторой формальной теории, т. е. как доказательство теорем.

Доказательство теорем безусловно предполагает затрату интеллектуальных усилий, требующих не только дедуктивных навыков, но и в значительной степени интуитивных догадок (например, какие леммы необходимы для той или иной теоремы). Другими словами, доказательство теорем подразумевает, в том числе, поиск уже доказанных теорем и решенных подзадач, которые могут оказаться полезны для достижения конечной цели. К настоящему времени разработано несколько программ с элементами ИИ, способных работать в этом направлении, т. е. программ автоматического доказательства теорем {Automatic Theorem Proving).

При первом взгляде на предмет мы сразу отмечаем обстоятельства, известные из курса математической логики:

• • язык исчисления предикатов первого порядка является общепринятым средством для аксиоматизации в большинстве предметных областей (т.е. практически любое утверждение может быть сформулировано как формула прикладного исчисления предикатов);
• • алгоритм перечисления правильно построенных формул позволяет генерировать гипотезы исчерпывающим образом (т.е. все правильно построенные формулы могут быть перечислены);
• • метод резолюций является частично корректным (т.е. для любой доказуемой формулы вывод может быть найден автоматически, а для недоказуемой формулы алгоритм может не завершить свою работу).

Возникает следующая идея, подкупающая своей незатейливостью и простотой. Запишем аксиомы предметной области на языке исчисления предикатов первого порядка. Запустим алгоритм, который будет генерировать новые гипотезы одну за другой. Каждую гипотезу будем пытаться автоматически доказывать методом резолюций, и если получится, то компьютер сам будет добывать все новые и новые знания. Процесс можно запустить на 24 часа в сутки, 7 дней в неделю, 365 дней в году, и не на одном компьютере, а на всех незанятых в данный момент. Отметим, что сейчас в среднем 90% времени персональные компьютеры простаивают, и их суммарная неиспользуемая вычислительная мощность довольно велика, так что у человечества хватает неиспользуемых ресурсов.

Таким образом, автоматическое доказательство теорем возможно, и его нетрудно запрограммировать, но такой прямолинейный подход оказывается безнадежно неэффективным. Сложные, интересные теоремы при лобовом подходе автоматически доказать не удается, потому что пространство перебора столь велико, что даже самые быстродействующие компьютеры не в состоянии ничего сделать за разумное время.

Однако существуют примеры, правда, пока немногочисленные, когда в очень узком классе математических теорий, применяя очень специфические методы, удавалось автоматически находить и доказывать нетривиальные содержательные теоремы, которые были ранее неизвестны. Одному из таких примеров уже много лет¹. Член-корреспондент РАН В. М. Матросов придумал удивительный способ перечисления и доказательства математических фактов в одной узкой области, относящейся к теории дифференциальных уравнений. Коллеги-программисты составили программу, которая генерировала гипотезы и автоматически строила к ним доказательства. Таким образом, были найдены и доказаны некоторые действительно новые, нетривиальные теоремы. При этом результаты (теоремы и доказательства) публиковались в престижном математическом журнале как новые научные результаты в математике. Мировое сообщество пока не знает, как отнестись к этому факту, однако прецедент есть.

Следует подчеркнуть, что автоматическое доказательство теорем является основным инструментом всех прикладных систем с элементами искусственного интеллекта, которые в той или иной степени используют формулы логических исчислений для представления знаний. Формулы исчисления предикатов первого порядка используются, практически, всегда — это основной способ формальной записи любых утверждений^[2][3], известный человечеству в настоящее время. Поэтому можно смело утверждать, что автоматическое доказательство теорем — это фундаментальная тема ИИ. В следующих главах показано, что все рассматриваемые нами методы ИИ, а возможно и все методы ИИ вообще, прямо или косвенно сводятся к автоматическому доказательству теорем.

• [1] Довольно часто встречается ситуация, когда правила имеют не детерминированный, а вероятностный характер: «если А, то В с вероятностью р». Большинство выводов, сделанных экспертной системой по вероятностным правилам, имеют вероятностный характер. Па свой вопрос пользователь получает один или несколько различных ответов, каждомуиз которых приписана своя вероятность достоверности.
• [2] Матросов В. М. Алгоритмы вывода теорем метода векторных функций Ляпунова /В. М. Матросов [и др.|; под ред. В. М. Матросова. Новосибирск: Наука, Сибирское Отделение, 1981.
• [3] Уместно отметить, что речь идет о категорических суждениях (принимающих значение"истина" или «ложь», но не то и другое одновременно) и не подразумевающих использование модальностей «возможно» и «необходимо».