3. Обучение и адаптация в системе логического вывода

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

ППФ, посредством которых мы таким образом выделяем совокупность объектов, называются аксиомами. Если для какой-либо совокупности объектов, их свойств и отношений некоторые аксиомы истинны, то говорят, что данная совокупность объектов удовлетворяет системе этих аксиом или является интерпретацией данной системы аксиом.

Таким образом, аксиомы можно рассматривать как определения системы объектов, их свойств и отношений между ними. Делая логические выводы из аксиом", мы будем получать ППФ, истинные для любой системы объектов, удовлетворяющей данным аксиомам.

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

Ответ на этот вопрос связан с понятием непротиворечивости системы аксиом. Мы должны быть уверены, что делая всевозможные выводы из данной системы аксиом, не придем к противоречию, т. е. не выведем какие-либо несовместимые ППФ. Появление противоречия означало бы, что рассматриваемой системе аксиом не может удовлетворять никакая совокупность объектов, и, таким образом, эти аксиомы ничего не описывают. Мы будем говорить, что система аксиом {A_i}_i=1ⁿ противоречива, если в ней выводима какая-либо ППФ A, а также и ее отрицание ¯|А. Для проверки (доказательства) непротиворечивости системы аксиом достаточно построить какую-нибудь точную интерпретацию этой системы.

Весьма важным является свойство независимости аксиом. Какая-либо аксиома А называется независимой в данной системе аксиом {A_i}_i=1ⁿ. если она невыводима из остальных аксиом этой системы. Для проверки (доказательства) независимости какой-либо аксиомы достаточно найти совокупность объектов, удовлетворяющую всем аксиомам, кроме исследуемой, и не удовлетворяющей этой последней. Иными словами, для проверки независимости аксиомы А достаточно найти интерпретацию следующей системы аксиом: {A_i}_i=1ⁿ, ¯|А.

Таким образом, система аксиом, которой пользуется робот, должна иметь точную интерпретацию в том мире объектов, свойств и отношений, в котором он функционирует. Этому требованию можно удовлетворить путем правильной формулировки тех интеллектуальных задач, которые робот должен решать. Остановимся на этом вопросе подробнее.

Формулировка задачи на языке робота - это первый и наиболее ответственный этап организации его целенаправленного поведения. На этом этапе от проектировщика требуются глубокие знания не только и не столько исчисления предикатов, сколько существа решаемой задачи, ее специфических черт, той цели, которая должна быть достигнута в результате решения. Возможна, но совершенно бессмысленна постановка на языке робота таких, например, задач: "переместиться туда, сам не знаю куда", или "найти то, сам не знаю что".

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

При построении аксиом будем различать два типа предикатов, использование которых по-разному сказывается на быстроте поиска решения. Предикаты первого типа описывают простейшие свойства конкретных объектов (например, "робот находится в точке х", "объект z большой" и т. п.). Предикаты второго типа определяют общую картину отношений между различными объектами и их свойствами. Один такой предикат может описывать набор свойств большого числа объектов (например, "если между точками а и b нет препятствий, то робот может проехать между этими точками по прямой" и т. п.). Количество подобных предикатов, необходимое для описания (с требуемой степенью подробности) данных и условий задачи, обычно невелико. Однако для сложных предикатов существенно возрастает сложность термов, участвующих в их определении.

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

Из дальнейшего изложения (и, в частности, из примеров) будет ясно, что эффективность системы логического вывода можно увеличить путем уменьшения числа предикатов и аксиом, определяющих данные и условия задачи. С этой целью разумно использовать ранее доказанные теоремы или ввести более сложные предикаты, образующие новые аксиомы, которые можно рассматривать как результат обучения робота в процессе решения задач. Такие аксиомы, описывающие на языке исчисления предикатов приобретаемый роботом опыт, мы будем называть аксиомами обучения. Введение аксиом обучения как бы моделирует феномен мышления, о котором еще Р. Декарт писал в своем "Рассуждении о методе": "Каждая решенная мною задача становилась образцом, который служил впоследствии для решения других задач". Образно говоря, аксиомы обучения играют роль лемм при доказательстве новых теорем, определяющих целевые условия задачи. Тем самым они позволяют оперировать более крупными "блоками" (фрагментами) доказательств, освобождая от рассмотрения многочисленных деталей, имеющих в данном доказательстве лишь вспомогательное значение. Заметим, что введение аксиом обучения позволяет роботу увеличивать и улучшать знания о решаемом классе задач в процессе их непосредственного решения. Таким образом, аксиомы обучения являются средством обучения новым понятиям и фактам и уточнения старых.

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

Построение системы аксиом в каждой задаче важно не само по себе, а имеет целью выявление оптимальных путей логического вывода. Под эффективностью системы логического вывода мы будем понимать меру успешности поиска решения. Для того чтобы выбрать количественный показатель эффективности, нужно прежде всего спросить себя: чего мы хотим от системы логического вывода, к чему стремимся при поиске решения? Выбирая решение, мы предпочитаем такое, которое обращает показатель эффективности в максимум или же в минимум.

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

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

Стратегией логического вывода называется способ выбора очередной пары дизъюнктов и литер в них для образования резольвент. Именно стратегия определяет, в каком порядке будут образовываться резольвенты и, следовательно, насколько быстро будет найдено решение задачи. Стратегия "запускает" процесс доказательства - начинается дедукция: с помощью аксиом, резольвент и теорем строится та или иная конструкция доказательства. При этом стратегия решает, какие понятия и факты (аксиомы и литеры в них) несущественны, а какие - необходимы для доказательства. Таким образом, выбор и подстройка стратегии являются основным средством увеличения эффективности системы логического вывода, определяющим быстроту сходимости реализуемого ею метода поиска доказательства. Если правила резольвенции есть правила дедуктивного вывода следствий, то стратегия - это та активная часть, способная к обучению и адаптации, которая имитирует способ "мышления" искусственного интеллектуального робота, уровень его познаний в логике, степень его интеллектуальности.

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

Стратегия называется полной, если она находит (в конечное число шагов) доказательство любой ППФ, выводимой из аксиом. Примерами полных стратегий являются стратегия опорного множества, стратегия предпочтения единичным элементом, а также тривиальная стратегия полного перебора (см. подробнее [9]). Все перечисленные стратегии характеризуются тем, что для них предикат является "неразложимым" понятием, а критерием выбора очередной пары дизъюнктов могут быть количество предикатов в дизъюнкте, порядок их расположения и т. п. Такие стратегии, не зависящие от внутренней структуры, смысла используемых предикатов, будем называть синтаксическими.

Стратегию будем называть адаптивной, если она целенаправленно меняется (подстраивается) в процессе логического вывода в зависимости от приобретаемого опыта. Примерами адаптивных стратегий могут служить семантические стратегии, в которых критерий выбора очередных дизъюнктов зависит от вхождения в них определенного терма. Согласно семантической стратегии сначала выбираются термы, соответствующие "интересным" объектам, затем - предикаты, описывающие их свойства, и, наконец, ППФ, содержащие эти свойства.

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

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

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

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

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