Комплексная верификация продукционных баз знаний с использованием VTF-логик

Проблема верификации баз знаний (БЗ) экспертных систем (ЭС) продукционного типа известна давно. В [1] отмечается, что некоторые из первых результатов в этом направлении были представлены в [2]. В [3, 4] была подчёркнута важность этой проблемы. Уже на ранних этапах сложился терминологический аппарат, и были сформулированы такие основные требования к качеству БЗ, как полнота (способность работать во всех допустимых входных ситуациях) и отсутствие противоречий в ходе вывода [5-7]. В [7] рассмотрен ряд известных на тот момент систем и методов верификации БЗ и отмечено, что нет универсального подхода к верификации, и полноценной она становится, когда эти методы применяются в комплексе или для специальных БЗ. Сходное мнение выражено в [8]. Это делает, в частности, актуальными работы по верификации БЗ для отдельных предметных областей (см. напр. [9]). Для обнаружения и удаления артефактов было предложено генерировать соответствующие метазнания, тесты [7, 10], использовать подходы, аналогичные доказательству правильности компьютерных программ, разработаны языки спецификаций [11-13].

В частности, в работе [14] рассмотрены вопросы применения логик с векторной семантикой для обнаружения дефектов продукционных БЗ. Основное внимание было уделено артефактам, ведущим к появлению противоречий, обрыву цепочек вывода. Показано, что при использовании машины вывода, работающей на основе логик с векторной семантикой в варианте V ^тр-логик, в которых истинность формализуется вектором ( a ⁺; а - ) (где a ⁺, a - е [0,1]; а ⁺ - степень уверенности, что суждение а истинно, а а ^- , - что оно ложно), противоречивость, неопределённость или ложность посылок в общем случае не обрывает вывод, но порождает проходящие через всю последующую цепочку аномальные значения истинности, которые можно отследить. Это позволяет предложить метод поиска артефактов: организация прямого вывода для различных допустимых сочетаний истинности входных фактов с последующей регистрацией аномального результата. Если допустимый вход порождает «неправильный» выход, это считается следствием артефакта. Далее организуется обратная трассировка вывода для обнаружения причин аномалии.

Одной из проблем верификации является экспоненциальный рост вычислений с увеличением объёма БЗ. Верификация во многом реализуется с помощью дополнительных компонентов, выходящих за рамки «штатных» средств ЭС. В предлагаемой работе описан комплекс процедур и алгоритмов, развивающих подход к проблеме верификации, представленный в [14]. При этом верификация может выполняться без включения в состав архитектуры ЭС дополнительных составляющих.

1    Подготовка и статическая верификация БЗ

Подготовка БЗ начинается с формирования множества атомарных утверждений (базы фактов). Каждое утверждение представляется четвёркой:

• (1)                                              A = ( а , C 1 , C 2 , || а ||).

Здесь а - содержательная часть утверждения, например, «Температура воздуха высокая» или «Скорость объекта больше 30 м/сек», «У пациента наблюдается сыпь» и т.п.; C 1 и C ₂ - счётчики числа вхождений A , соответственно, в левую и правую часть правил;

• (2)                                         || а || = { [ а ⁺ь а ⁺2 ];[ а "ь а ’2 ] ) ,

• -    вектор истинности а в интервальном представлении. Если а строго истинно, || а || = ( [1; 1]; [0; 0] ) ; если строго ложно - { [0; 0]; [1; 1] ) . Когда свидетельства «за» или «против» а отсутствуют (т.е. имеет место неопределённость), || а || = ( [0; 0]; [0; 0] ) . Наконец для полностью противоречивого случая || а || = ( [1; 1]; [1; 1] ) . Первоначальное значение истинности для всех фактов выставляется в неопределённость. Далее она задаётся пользователем или вычисляется в ходе присоединённого вывода.

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

Каждое вхождение факта A в ту или иную продукцию сопровождается увеличением соответствующего счётчика C 1 или C 2 на единицу, а его удаление - уменьшением. Это позволяет разбить множество фактов на подмножества:

• ■    стартовые факты ( C 1 > 0, C ₂ = 0);

• ■    промежуточные факты ( C 1 > 0, C ₂ > 0);

• ■    терминальные факты (гипотезы) ( C 1 = 0, C ₂ > 0);

• ■    неиспользуемые факты ( C 1 = 0, C ₂ = 0).

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

Далее факты связываются в правила R , которые представляются пятёркой:

• (3)                                              R = ( i , K 1 , K 2 , | i II, L ).

Здесь i - импликация (ядро продукции), K 1 и K ₂ - счётчики числа фактов в левой и правой частях правила, || i || - истинность ядра, также представляющая собой вектор с интервальными значениями:

|| i || = ( [ i ⁺ i ; i ⁺2]; [ i ^—i ; i '2] ) .

Значение || i || задаётся разработчиками. L - положение (уровень) продукции в причинноследственном порядке.

Счётчики K 1 и K ₂ в (3) позволяют автоматизировать выявление незавершённых правил, в которых отсутствует антецедент или консеквент (также один из возможных артефактов [1]).

Серьёзной проблемой разработки ЭС является рост объёма вычислений с увеличением БЗ, если не пользоваться специальными методами и алгоритмами. Классическим примером такого метода служит алгоритм Rete [15]. Для решения задачи верификации на завершающем этапе формирования БЗ предлагается использовать причинно-следственное упорядочение продукций. Под причинно-следственным упорядочением понимается такая расстановка правил, что если две продукции R 1 и R 2 содержат общее утверждение a , причём в одном правиле, например R 1, оно входит в консеквент, а в другом ( R 2) в антецедент, правило R 1 при выводе всегда предшествует R 2. В результате для любой продукции R все логически предшествующие ей продукции выполняются прежде R [16]. Логический вывод при этом выполняется за один проход БЗ, а объём вычислений с увеличением числа правил растёт не экспоненциально, а линейно. Если использовать машину вывода, в том числе для задач верификации [14], это существенно упрощает дело.

Подобное упорядочение при неизменной БЗ выполняется однократно и до начала работы с системой (редактирование БЗ требует переупорядочения).

Упорядочение может выполняться по следующему принципу:

• ■    начальные значения уровней всех правил, антецедент которых состоит только из стартовых фактов, выставляется в 0 (т.е. L = 0);

• ■    если в антецедент правила входят факты, входящие в консеквенты правил с уровнями L 1 ,^, L n , текущему правилу приписывается уровень L = max ( L 1 ,^, L n ) + 1;

• ■    процедура выполняется за несколько проходов БЗ, пока не прекратится изменение уровней.

При следовании такому принципу правила одного уровня никогда не ссылаются друг на друга, а правила уровня L никогда не ссылаются на правила с уровнями, предшествующими L . Обеспечивается однопроходность вывода и линейный рост объёма вычислений с увеличением БЗ. Часть вывода, требующая больших затрат времени, переносится на этап настройки БЗ и не затрагивает пользователя ЭС.

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

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

2    Динамическая верификация БЗ

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

В [14] эти ситуации обсуждались с точки зрения их выявления средствами V ^TF-логик. Основная идея сводится к тому, что ситуации, порождающие эти артефакты, как то:

• ■    совместное получение утверждения и отрицания какого-либо факта (противоречие), ■ постоянно ложный антецедент или (в векторном случае) постоянно неопределённый антецедент (все компоненты вектора истинности близки к нулю) -

• не препятствуют процедуре логического вывода, но порождают заключения с аномальными значениями истинности соответствующего типа. Этот факт устанавливается на завершающем этапе вывода выявлением гипотез с такими же аномальными значениями истинности. Обратной трассировкой цепочки вывода можно установить причину аномалии. Важной составляющей такого вывода служит процедура объединения свидетельств, которая в VTF-случае опирается на одну из следующих операций [16].

• ■   «10»-композицию, которой называется суждение (первая форма дизъюнкции), образо

ванное из а и b с вектором истинности:

|| a v b || = { а ⁺ Ф b ⁺; а ^- • b ”) .

• ■   «01»-композицию с вектором истинности (первая форма конъюнкции):

|| а &  b || = { а ⁺ • b ⁺; а ^- Ф b ^-) .

• ■   «11»-композицию с вектором истинности (вторая форма дизъюнкции):

|| а v ₂ b || = { а ⁺ Ф b ⁺; а ^- Ф b ^-) .

• ■   «00»-композицию с вектором истинности (вторая форма конъюнкции):

• || а &₂ b || = { а ⁺ • b ⁺; а ^- • b ^-) .

Первые формы дизъюнкции и конъюнкции аналогичны дизъюнкции и конъюнкции в классическом и нечётком случаях, вторые формы - специфика V ^TF-логик. Здесь • и Ф - триангулированная (треугольные - triangle ) норма и ко-норма в инфиксной записи с дополнительным свойством [17]:

x • у = 1 - (1 - x ) Ф (1 - у );

либо:

x Ф у = 1 - (1 - x ) • (1 - у ).

Это свойство связывает векторное и нечёткое представления истинности в случае, когда а ^- + а ⁺ = 1 [18].

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

• 1)    объединение по схеме «10»/«11»-композиции - стратегия нарастающего доверия . Свидетельства в пользу истинности b , как и свидетельства в пользу истинности — b , объединя-

• ются раздельно по правилу «10»-композиции (дизъюнкции). Полученные после этого векторы ||b|| и ||—b|| «складываются» в единый вектор по правилу «11»-композиции. При таком объединении доверие к b возрастает по мере получения утвердительных доказательств факта, доверие к — b - по мере вывода его отрицаний. Итоговый вектор объединяет свидетельства как за, так и против.

• 2)    объединение по схеме «11»-композиции - стратегия полного доверия . Доверяем и подтверждающим и опровергающим свидетельствам, это упрощённый вариант стратегии нарастающего доверия. Здесь быстрее растёт степень противоречивости промежуточных фактов и гипотез, что проще с алгоритмической точки зрения.

Оба подхода при получении взаимоисключающих утверждений b и — b генерируют вектор истинности, фиксирующий противоречие. Т.е., если по некоторой ветви вывода получено заключение b с истинностью || b || = ( 1; 0 ) , а по другой — b также с истинностью ||— । b || = ( 1; 0 ) , то объединение на основе «11»-композиции даёт (с учетом, что ||— । b || = ( b ^- ; b ⁺ ) ):

|| b || = ( 1 Ф 0; 0 Ф 1 ) = ( 1; 1 ) - полное противоречие.

Возможна ситуация, когда противоречие имеет неявную форму: из одних и тех же посылок генерируются логически несовместимые заключения b и c [1, 19]. Введение дополнительной продукции с ядром b ^ — c (или c ^ — b ) позволит выявить и этот случай.

Верификация выполняется в ходе прямого вывода и предполагает перебор всех допустимых значений истинности входных фактов. Поскольку предлагаемая модель истинности непрерывна, следует ограничиться конечным набором проверочных комбинаций. Чтобы избежать маскирующего влияния нестрогих значений истинности, истинность малых посылок целесообразно задавать в виде допустимых комбинаций строгой истины ( [1; 1]; [0; 0] ) и/или строгой лжи ( [0; 0]; [1; 1] ) при строгой истинности импликации.

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

Если дополнить (3) счётчиком числа обращений к продукции, легко установить «молчащие» продукции, к которым не было ни одного обращения. Однако при использовании причинно-следственного порядка этот артефакт можно обнаружить уже на этапе статического анализа.

3    Снижение вычислительной сложности

Остаётся прояснить вопрос о процедуре выставления значений истинности стартовых фактов - посылок. В предельном случае N посылок порождают 2 N комбинаций истинности. Даже для небольшой БЗ, содержащей несколько десятков входных фактов, это приводит к взрывообразному росту числа проверок. Простой перебор может оказаться невозможным. Количество проверок необходимо уменьшить без потери полноты перебора. Для решения этой задачи предлагается использовать то обстоятельство, что в основе каждой гипотезы лежит относительно небольшое количество стартовых посылок. Тогда для каждой гипотезы можно выделять только относящиеся к ней факты. Поскольку в реальных задачах обычно n существенно меньше N , где n - число стартовых фактов гипотезы, получаем кардинальное снижение вычислительной нагрузки. Далее приводится дополненная схема алгоритма, представленного в [14].

• 1)    объявить все продукции строго истинными (запомнив, при необходимости, значения истинности, выставленные экспертами).

• 2)    выделить терминальный факт (гипотезу).

• 3)    установить все связанные с ним стартовые факты.

• 4)    выставить значения истинности стартовых фактов в одну из допустимых комбинаций - 〈 1; 0 〉 или 〈 0; 1 〉 , - а истинность промежуточных и терминальных - в 〈 0; 0 〉 .

• 5)    выполнить прямой логический вывод, получив истинность гипотезы.

• 6)    проверить истинность заключения на допустимость.

• 7)    если заключение недопустимо:

  • 7.1)    выполнить обратную трассировку вывода для выяснения источника проблемы – артефакта БЗ;

  • 7.2)    устранить артефакт (или внести его в соответствующий список);

  • 7.3)    вернуться к шагу 4.

• 8)    если не все возможные входные значения посылок проверены, вернуться к шагу 4.

• 9)    если не все возможные гипотезы проверены, вернуться к шагу 2.

• 10)    вернуть исходные значения истинности продукций.

• 11)    стоп.

Такая верификация не требует генерирования дополнительных структур данных, например таблиц принятия решений или их аналогов.

Заключение

В работе представлена комплексная процедура верификации продукционных БЗ на основе V TF -логик с введением в факты и правила дополнительных элементов, а также специальным упорядочением правил. Решаются следующие вопросы:

• ■   выявление несвязанных фактов;

• ■    выявление незавершённых продукций;

• ■    выявление логических кругов;

• ■    контроль соответствия между множеством гипотез и множеством терминальных фактов;

• ■   выявление противоречий;

• ■   выявление «молчащих» продукций;

• ■    выявление нештатных обрывов цепочек вывода.

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

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