Программные продукты и системы

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

Обсуждение основных идей

Теоретические основы аргументации. Необходимость теории аргументации возникает из-за неполноты и недостоверности данных и знаний. Обычно, говоря об аргументации, выделяют три типа информации [1].

1.     Объективная информация – информация, которая получена из надежных источников или может быть напрямую измерена или подтверждена. Например, утверждение «В центральной части России весной продолжительность светового дня увеличивается» является объективной информацией, подтверждаемой наукой и нашими наблюдениями. Такая информация, как правило, используется как неоспоримый аргумент.

2.     Субъективная информация – информация, полученная из менее надежных источников. Это могут быть некоторые предположения, суждения. Они часто формулируются с помощью фраз «как правило», «обычно», «скорее всего». Такая информация и служит «источником» противоречий и конфликтов.

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

Все названные типы информации могут быть использованы для аргументации: объективная служит фактами и исходными посылками, субъективная является источником пересматриваемых выводов, а гипотетическая помогает строить пред­положения.

Существуют несколько формализаций теории аргументации, например [2–5].

В данной работе будет подробно рассмотрена система аргументации, основанная на пересматриваемых рассуждениях, предложенных Д. Поллоком [5].

Пересматриваемые рассуждения. Прежде всего дадим необходимые определения и введем обозначения [6].

Определение 1. Аргумент – пара, состоящая из множества посылок и заключения. Записывать такие пары будем в виде p/X, где p – заключение; X –множество посылок.

Например, аргумент (p ® q)/{~A, B} означает, что из посылок ~A, B следует p ® q. На всех иллюстрациях будем обозначать аргументы овалами. Для аргументов с пустым множеством посылок (такие аргументы называют фактами) будем писать только заключение. Например, фактом является утверждение, что Земля вращается вокруг Солнца.

Определение 2. Интерес – аргумент, который мы хотим обосновать в ходе монотонного и/или пересматриваемого вывода. На графе вывода будем обозначать интересы прямоугольниками.

Определение 3. Граф вывода – граф, показывающий взаимосвязи между аргументами и интересами. Он отображает, из каких аргументов порождается новый аргумент и из каких интересов получаются новые интересы, а также конфликты между аргументами при пересматриваемых рассуждениях.

Определение 4. Дедуктивное следствие – простые дедуктивные правила вывода, означающие, что, если истинно P, то истинно и Q. Такие правила не являются пересматриваемыми. Записывать их будем как PÞQ и на графе вывода отображать обыкновенными стрелками (см. аргументы P и Q на рис. 1).

Определение 5. Пересматриваемое следствие – это пересматриваемые правила вывода, которые могут быть получены, например, в результате индукции или абдукции. В данной работе нас не интересует конкретный механизм получения таких выводов, поэтому такие правила подаются декларативно на вход программы. Аргументы, полученные в результате таких выводов, будем называть пересматриваемыми. Записывать эти правила будем как M|ÞN. На графе вывода такие связи будем отображать пунктирными стрелками, а пересматриваемые аргументы – двойным овалом (см. аргументы M и N на рис. 1).

Понятие конфликта – основа системы аргументации. Будем рассматривать два типа конфликтов – опровержение и подрыв [6].

Определение 6. Опровержение (rebutting) – ситуация, когда некоторые аргументы опровергают заключения других аргументов. Иными словами, аргумент A_1=p_1/X_1 опровергает аргумент A_2=p_2/X_2, когда заключение p_1 опровергает заключение p_2. Опровержение является симметричной формой атаки.

Определение 7. Подрыв (undercutting) – несимметричная форма атаки, когда один аргумент отрицает связь между посылками и заключением другого аргумента.

Определение 8. Подрывающие доводы. Это аргументы, поражающие связь между двумя другими аргументами, соединенными пересматриваемым следствием. Например, имеется аргумент E, подрывающий пересматриваемую связь C|ÞD между аргументами C и D. Такие правила подрыва будем записывать в виде EÞ(C@D). На графе вывода подрывающие аргументы и пораженные ими аргументы будем соединять жирной пунктирной стрелкой, пораженные аргументы – помечать темно-серым цветом (см. аргумент D на рис. 1).

Обнаружение конфликтов. Обнаружение конфликтов является наиболее сложной частью системы аргументации. Основные сложности обусловлены необходимостью поддержки логики предикатов первого порядка. Если говорить о логике высказываний, то конфликт типа «опровержение» – это ситуация, когда одновременно существуют два аргумента – A и ~A. Однако для логики предикатов первого порядка все несколько сложнее. Основная идея – применение механизма унификации для обнаружения конфликтов. Подстановка U={t1/x1, t2/x2, …, tn/xn}, где ti – термы и xi – переменные, называется унификатором для выражений W1 and W2, если W1*U = W2*U, где W1*U – результат замены переменных x1, x2, …, xn на термы t1, t2, …, tn и предполагается, что W1 и W2 не содержат переменные с одинаковыми именами (если это так, их необходимо переименовать) [6]. Например, выражения P(x1)&G(x2)®H(x1, x2) и P(f(a))&G(b)®H(f(a), b) унифицируются унификатором U={f(a)/x1, b/x2}.

Будем говорить, что аргументы A1=p1/X1 и A2=p2/X2 вступают в конфликт типа «опровержение», если существует такой унификатор U, что

1.     ~p1×U=p2×U;

2.     X1×UÎX2×U или X2×UÎX1×U.

Аргумент A1 подрывает пересматриваемую связь между аргументами A2 и A3.

1.     Существует пересматриваемая связь между A2 и A3.

2.     Существуют подрывающее правило EÞ(C@D) и такие унификаторы U1 и U­2, что

a.     E×U1=A1×U1;

b.     (C×U1) ×U2=(A2) × U2;

c.     (D×U1) ×U2=(A3) ×U2.

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

Степени обоснования в пересматриваемых рассуждениях

Перед переходом к способам и алгоритмам вычисления степеней обоснования рассмотрим, как они могут задаваться и откуда получены. В данной работе для задания степеней обоснования используется числовая шкала [0, 1], где 0 соответствует пораженному аргументу, а 1 – наиболее обоснованному аргументу. Степени обоснования могут быть двух типов:

–      степени обоснования исходных аргументов;

–      степени обоснования пересматриваемых правил.

Первый тип степеней обоснования присваивается каждому исходному аргументу и представляет собой некую оценку достоверности источника, из которого получен данный аргумент. Например, по телевидению сообщили, что вероятность осадков составит 70 %. Соответственно мы можем построить аргумент А1: Завтра(дождь) со степенью обоснования 0,7. Степени обоснования будем записывать функцией Jus(A). То есть для приведенного примера Jus(Завтра(дождь))=0,7. Конкретные механизмы получения степеней обоснования зависят прежде всего от предметной области. Например, это могут быть статистические данные (в 90 % этот источник дает верные данные) или экспертные оценки (вероятность роста акций – 60 %).

Второй тип степеней обоснования связан с пересматриваемыми правилами. Как уже говорилось, часто пересматриваемые правила появляются в результате формализации знаний эксперта вида «Если A, то чаще всего B». Такие правила могут нести в себе и некоторую числовую оценку. Например, применение анальгина в 85 % приводит к снижению температуры тела пациента (формально R1: (" x) прием(анальгин,x)| Þ понижение_температуры(x)).

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

Итак, нам необходимо задать функцию Jus(A) для вычисления любого из аргументов в графе вывода. Будем считать, что для изначальных аргументов эта величина является определенной. На значение этой функции будут оказывать влияние два фактора – дерево вывода аргумента (то есть степень обоснования аргументов, используемых в выводе данного аргумента) и конфликты с другими аргументами. Для удобства рассмотрим эти два фактора отдельно: Jusanc(A) – унаследованная степень обоснования и Juscon(A) – насколько конфликт подрывает обоснование аргумента. Пусть Anc = {Anci}, 1

.                             (1)

Формулу (1) называют принципом слабейшей связи [7]. Надо отметить, что это не единственный подход к вычислению степени обоснования, в ряде работ применяется байесовский подход (см., например, [8]).

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

Если при вычислении Jusanc ищутся наиболее слабые аргументы, то при определении того, насколько конфликт уменьшает обоснования, используются наиболее сильные аргументы. Пусть Aconfl – множество аргументов, вступающих в конфликт с A, n=| Aconfl |, тогда

    (2)

В формуле (2) используется Jusanc для того, чтобы верно обрабатывать случаи, когда между аргументами есть конфликт типа опровержение.

Итак, окончательно имеем:

                        (3)

Программная реализация

Система аргументации реализована в среде Visual Studio 2010. При реализации системы был применен объектно-ориентированный подход. Основные модули реализованной системы приведены на рисунке 2.

Остановимся на каждом модуле подробнее.

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

Приведем грамматику записи аргументов в форме Бэкуса–Наура:

::=|()

::=

::=

::=" | $

::=|Ø|()

::=|()

::=|,

::=

::=’&’ | ‘|’ | ‘«’ | ‘®’

:: =|

::=|

::=a|b|c|…z|A|B|C|…Z|а|б|…я|A|Б…Я

::a|b|c|…z|A|B|C|…Z|а|б|…я|A|Б…Я|1|2|3..0

Пример аргумента (" x)( $ y) (big_town(x) ® (small_town(y)&near(x, y)))

Поясним значение логических операций: & – конъюнкция, | – дизъюнкция, Ø – отрицание, ® – импликация, « – эквивалентность.

Без системы монотонного вывода система аргументации была бы статической, то есть в ней отсутствовали бы механизмы для порождения новых аргументов из уже имеющихся. Такие системы рассматриваются в теории абстрактной аргументации. Отсутствие механизмов вывода существенно сужает возможности таких систем. Поэтому в разрабатываемой системе предлагается использовать механизм натуральной дедукции [9] для вывода новых аргументов. На рисунке 3 приведены основные модули данной системы.

Блок прямых рассуждений позволяет строить новые аргументы из уже имеющихся.

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

Блок пересматриваемого вывода, структура которого приведена на рисунке 4, позволяет находить конфликты и вычислять статусы аргументов.

Реализации системы аргументации на основе пересматриваемых рассуждений

При создании данной системы использовались следующие основные алгоритмы.

Алгоритм прямых рассуждений.

Входные данные: аргумент q, граф вывода G.

Выходные данные: список новых аргументов New_ arguments.

Шаг 1. Для данного аргумента q проверить возможность применения простых правил прямого вывода, не требующих участия других аргументов (упрощение, устранение эквивалентности, устранение двойного отрицания, преобразование дизъюнкции, правило де Моргана, отрицание дизъюнкции, отрицание импликации [10]).

Шаг 2. Если хотя бы одно правило вывода подходит, сделать вывод согласно правилу, при этом посылки у заключительного аргумента будут такими же, как и у аргумента q.

Шаг 3. Если ни одно простое правило не подошло и аргумент q/X имеет вид A®B/X (где A и B – любые правильно построенные формулы, X – множество посылок), то запустить цикл перебора по всем аргументам pi/Yi из G (1

Модус поненс: если для некоторого аргумента pi/Yi существует унификатор U для A/X и pi/Yi, то вывести аргумент (U*B/U*X).

Модус толенс: если для некоторого аргумента pi/Yi = ~ ri/Yi существует унификатор U для B/X и ri/Yi, то вывести аргумент (U*(~B)/U*X).

Шаг 4. Аргументы, полученные на шагах 2 и 3, добавить в выходной список новых аргументов. Завершить процедуру.

Алгоритм подтверждения интересов.

Входные данные: граф вывода G.

Выходные данные: очередь вывода, граф вывода.

Шаг 1. Для каждого неподтвержденного интереса pi/Xi (1

Шаг 2. Для интересов, которые унифицируются унификатором U с аргументом qj/Yj, проверить, вложен ли результат применения унификатора U*(Yj) в U*( Xi). Если вложен, то применить к этому интересу унификатор U, пометить интерес как доказанный, добавить его в список аргументов, добавить в очередь вывода. Рекурсивно пометить как подтвержденные интересы (и применить к ним унификатор U), которые порождают данный интерес, если они порождали только один интерес или все другие порожденные им интересы уже подтверждены.

Шаг 3. Изменить граф вывода в соответствии с шагом 2 и завершить процедуру.

Алгоритм поиска конфликтов.

Входные данные: граф вывода, список подрывающих следствий undercut_rules.

Выходные данные: граф вывода с конфликтами.

Шаг 1. Для каждого аргумента Arg­1 = a1/{X1} проверить, имеется ли такой Arg­2 = a2/{X2}, что для a1 и ~a2 существует унификатор U и X1*UX2*U или X2*UX1*U. Если такой унификатор существует, добавить конфликт между Arg­1 и Arg­2.

Шаг 2. Для каждого подрывающего правила uc_rule вида pÞ(q@r) из undercut_rules выполнить следующие шаги.

Шаг 3. Взять левую часть правила – p. Для каждого аргумента Arg = a/{X} проверить, существует ли унификатор Uleft для выражений a и p.

Шаг 4. Для тех аргументов Arg, которые унифицируемы с левой частью подрывающего правила, выполнить следующие шаги.

Шаг 4.1. Применить унификатор Uleft к q и r (qu=q* Uleft и ru=r* Uleft).

Шаг 4.2. Составить массив X=[{xq1,, xr1}, {xq2,, xr2}, …, {xqn,, xrn}], состоящий из пар аргументов, соединенных пересматриваемой. Для каждого элемента этого массива выполнить

шаг 4.2.1. Проверить, существует ли унификатор Uright для qu и xqi. Если найденный унификатор также является унификатором для ru и xri­­, добавить новый конфликт в граф вывода.

Шаг 5. Изменить граф вывода в соответствии с найденными на шагах 1–4 конфликтами и завершить процедуру.

Алгоритм вычисления степеней обоснова­ния.

Процедура calculate_justification_degree().

Входные данные: граф вывода.

Выходные данные: граф вывода.

Шаг 1. Составить очередь Qlist вычисления степеней обоснования из аргументов, входящих в граф вывода, начиная от изначально заданных аргументов.

Шаг 2. Пока очередь Qlist непуста, извлечь из нее очередной элемент q и выполнить процедуру Jus(q).

Шаг 3. Изменить степени обоснования аргументов графа вывода в соответствии с найденными степенями и завершить процедуру.

Процедура Jus(argument q, [argument ex]).

Входные данные: аргумент q, необязательный параметр – аргумент ex, который не учитывается при определении степени обоснования аргумента q, граф вывода.

Выходные данные: граф вывода.

Шаг 1. Если q – изначально заданный аргумент, то положить Jusanc(q) равным изначально заданной степени доверия для этого аргумента. В противном случае из всех Anci, являющихся непосредственным предком q (то есть q получается из Anci за один шаг), найти Anc_min с минимальной степенью обоснования. Положить Jusanc(q) = = Jus(Anc_min).

Шаг 2. Если аргумент q не имеет конфликтов, положить Juscon(q)=0. В противном случае составить множество {Ai}, состоящее из аргументов, имеющих конфликт с q. Если параметр ex задан, исключить его из множества {Ai}. Если к моменту вычисления Jus(q) среди Ai нет аргументов с неопределенной степенью обоснования, то найти среди них тот аргумент A_max, у которого Jus(A_max) максимален. Положить Juscon(q)=max(Jus(A_max), Jusanc(ex)), выполнить Jus(ex), перейти к шагу 4. В противном случае (то есть среди {Ai} есть аргументы с неопределенными степенями обоснования) выполнить шаг 3.

Шаг 3. Для каждого Ai, для которого не определена степень доверия, выполнить

шаг 3.1. Если Ai имеет конфликт с q, но аргумент q не имеет с ними конфликта (несимметричная форма конфликта), выполнить Jus(Ai). В противном случае выполнить Jus(Ai,q), то есть рассчитать Jus(Ai) без учета конфликта с q.

Шаг 4. Положить Jus(q) = = Jusanc(q) – Juscon(q), если Jusanc(q) > > Juscon(q). В противном случае Jus(q) = 0.

Шаг 5. Изменить степени обоснования аргумента q и завершить процедуру.

Пример работы системы аргументации

Имеется следующая задача. Предприниматель хочет вложить некоторую сумму в развивающийся бизнес и получить от этого доход. Есть компания CMP, которая занимается IT-бизнесом.

По статистике, IT-рынок находится на подъеме и 75 % IT-компаний показывают положительную динамику развития. Компания CMP занимается разработкой ПО под операционные системы семейства Linux. В России менее 10 % пользователей Linux, следовательно, спрос на продукцию будет невелик. Однако 80 % производства компании направлено на международный рынок ПО для веб-серверов, которые в основном работают на Linux.

Запишем условия формально на языке ЛППП:

А1. IT(CMP) justifiacation: 0,75

А2. под_Linux(CMP) justifiacation: 1

А3. рынок_сбыта(для_серверов) justifiacation: 0,8

А4. (" x)(инвестировать(x)>доход)

R1. (" x) (IT(x) ) |=> (V x) рост_акций(x)

R2. (" x) (рост_акций(x) |=> инвестировать(x))

R3. (" x) (под_Linux(x) |=> плохой_спрос(x))

R4. (" x) (плохой_спрос(x) |=> ~инвестировать(x))

R5. (" x) рынок_сбыта(для_серверов) ==> ((под_Li­nux(x)) @ плохой_спрос(x))

На рисунке 5 приведен граф вывода для данной задачи.

Рассмотрим решение данной задачи поэтапно.

1. Из аргумента А1: IT(CMP) и правила вывода R1 получается пересматриваемый аргумент А6 Jus(А6)=Jus(A1)=0,75.

2. Из аргумента А2: под_Linux(CMP) и правила вывода R3 получается пересматриваемый аргу­мент A8: плохой_спрос(CMP). Jus(A8)=Jus(A2)=1.

3. Аргумент A8: плохой_спрос(CMP) с помощью правила R5 вступает в конфликт типа «подрыв» с аргументом A3: рынок_сбыта(для_серве­ров). Согласно формуле (3) Jus(A3)=Jusanc(A3)– –Jus(A8)=0,2.

4. Из аргумента А6 и правила R2 получается аргумент А7: Инвестировать(CMP). Jus(A7)= =Jus(A6)=0,75.

5. Из аргумента А8 и правила вывода R4 получается аргумент А9: ~Инвестировать(CMP).

6. Аргументы А9 и А7 вступают в конфликт типа опровержение, степень обоснования аргумента А7 выше, следовательно, Jus(A7)=0,55, а аргумент А9 становится полностью пораженным с Jus(A9)=0.

7. Используя правила обратного вывода, из интереса In5 получается интерес In11, а из него интерес In14.

8. Из аргумента А10: Инвестировать(_x)->до­ход и аргумента А7: Инвестировать(CMP), применяя унификацию и правило Modus Ponens, получаем аргумент А12. Согласно принципу слабейшей связи, Jus(А12)=0,55. Этот аргумент подтверждает интерес In14.

9. Окончательно получаем, что интересы подтверждены со степенью обоснования 55 %. То есть инвестиция в компанию CMP принесет доход с вероятностью 55 %.

Итак, сделаем следующие выводы. Конфликты в базах знаний являются серьезной проблемой при построении любых интеллектуальных систем. Поиск, анализ и, возможно, разрешение этих конфликтов – важная и интересная задача. В настоящей статье был рассмотрен один из подходов к данной проблеме – использование аргументации, а именно теории пересматриваемых рассуждений. Были рассмотрены теоретические основы пересматриваемых рассуждений и дан обзор системы, разработанной на данной теории. Разработанная программная система справилась со многими задачами, не решаемыми с точки зрения классической логики. Она была протестирована и отлажена на многих тестовых задачах из [11].

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

Литература

1.     Besnard P., Hunter A. Elements of Argumentation. Cambridge MA: MIT Press, 2008, 298 p.

2.     Bondarenko A., Dung P.M., Kowalski R.A., Toni F. An Abstract Argumentation-Theoretic Framework for Defeasible Rea­soning. Artificial Intelligence, 1997, vol. 93, no. 1–2, pp. 63–101.

3.     Lin F., Shoham Y. Argument Systems. A Uniform Basis for Nonmonotonic Reasoning. Proc. 1st Intern. Conf. on Principles of Knowledge Representation and Reasoning. San Mateo CA: Morgan Kaufmann Publ. Inc, 1989, pp. 245–355.

4.     Vreeswijk G.A.W. Abstract Argumentation Systems. Artificial Intelligence. 1997, vol. 90, pp. 225–279.

5.     Pollock J.L. How to Reason Defeasibly. Artificial Intelligence. 1992, vol. 57, pp. 1–42.

6.     Вагин В.Н., Головина Е.Ю., Загорянская А.А., Фоми- на М.В. Достоверный и правдоподобный вывод в интеллектуальных системах. 2-е изд. М.: Физматлит, 2008. 712 с.

7.     Pollock J.L. Defeasible reasoning with variable degrees of justification. Artificial Intelligence. Artificial Intelligence. 2001, vol. 133, pp. 233–282.

8.     Haenni R., Kohlas J., Lehmann N. Probabilistic Argumentation Systems, Handbook of Defeasible Reasoning and Uncertainty Management Systems. Algorithms for Uncertainty and Defeasible Reasoning. 1999, vol. 5, pp. 221–287.

9.     Pollock J.L. Natural Deduction. Technical Report, Depart­ment of Philosophy, Univ. of Arizona, Tucson, 1996, p. 35.

10.  Вагин В.Н., Моросин О.Л. Исследование систем аргументации для пересматриваемых рассуждений. В кн. Интеллектуальные системы. Вып. 6; [под ред. В.М. Курейчика]. Р-н-Д: Изд-во ЮФУ, 2013. С. 163–178.

11.  Vreeswijk G.A.W. Interpolation of Benchmark Problems in Defeasible Reasoning. Proc. of the 2nd World Conf. on the Fundamentals of Artificial Intelligence (WOCFAI 95). Paris, France, 1995, pp. 453–468.