Ankyra: реализация нейро-символических рассуждений

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

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

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

Концепция

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

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

Отсюда сразу становится понятна роль этих двух компонентов в рассуждении:

1. Языковая модель может предполагать, дополнять фактами на основе своей необъятной эрудиции и знаний.

2. Символический решатель проверяет правильность этих фактов, формально сопоставляя новый факт с текущими.

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

Такая классификация кажется с первого взгляда непонятной, но на самом деле все просто. Рассмотрим примеры.

Входной текст: «Идёт дождь. Если идёт дождь, земля мокрая. Земля мокрая?»

В самом начале мы просим модель извлечь из текста факты. Модель извлекает следующее:

• факт raining() - "идет дождь"

• правило raining() => is_wet(ground) - "если идет дождь, то земля мокрая"

Оба факт основаны на текстах, поэтому мы их классифицируем как cited, а значит при извлечении они становятся аксиомами теории этого предложения. Символьный решатель дополняет теорию фактом is_wet(ground) т.к. в теории уже есть raining() как аксиома и правило aining() => is_wet(ground). is_wet(ground) классифицируется как derivable. Таким образов, текст "земля мокрая?", который на самом деле на языке формальной теории - просто проверка, есть ли в теории факт is_wet(ground), получает ответ Yes со статусом proven.

Другой текст: «У машины есть двигатель, четыре колеса, 150 лошадиных сил и четыре двери. Что это за машина?»

Модель извлекает факты:

• x - машина

• has_engine(x) - "есть двигатель"

• wheel_count(x, 4) - "четыре колеса"

• power(x, 150) - "150 лошадиных сил"

• door_count(x, 4) - "четыре двери"

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

Мы подаем сформированную теорию в языковую модель и просим дополнить ее фактами. Модель предлагает правило: has_engine(?x) ∧ wheel_count(?x,4) ∧ power(?x,150) ∧ door_count(?x,4) ⇒ is_a(?x, car). Это пример т.н. правила хорновского вида, где слева стоят предикаты с логически "И", а справа - только один предикат. Иначе говоря, модель формирует вопрос в виде правила: если у этого автомобиля есть двигатель, четыре колеса, 150 лошадиных сил и четыре двери, что что это за автомобиль? Цитаты для этого правила в тесте нет, так что она классифицируется, как гипотеза, скажем H1.

Решатель из фактов теории и этого правила выводи предикат is_a(x, car), однако это слишком общий ответ и не дает новой информации, то что это машина, уже есть в утверждении. Поэтому, снова обращаемся к модели за ответом и получаем новое правило: is_a(?x, car) ⇒ is_a(?x, motor_vehicle). Это уже правило иерархии, не имеет цитаты в тексте классифицируется как derivable, получает статус H2. Теперь символьный решатель уже может вывести факт is_a(x, motor_vehicle) со статусом proven_under(H1, H2).

Формальное описание работы

Внимательный читатель наверняка уже заметил, что в примерах выше модель использовалась для двух разных целей:

1. Построение теории из текста: выделения объектов, предикатов и правил, а также вопроса в виде предиката с переменными.

2. Дополнения теории новыми фактами.

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

1. Синтаксический анализатор, выделяющий из текст элементы формальной теории.

2. Пополнитель теории новыми фактами, которые символический решатель не может вывести принципиально, но модель знает в силу своей эрудиции.

Отсюда и предлагаемый алгоритм нейро-символических рассуждений:

1. Модель строит базовую теорию из переданного на вход текста.

2. Символьный решатель строит формальный вывод из на основе правил теории - "замыкает ее". Если ответ получен, то выдаем его, иначе переходим к шагу 3.

3. Если превышен лимит обращений к модели, то останавливаем работу, ответ не получен. Иначе, обращаемся к модели для получения новых фактов и правил вывода.

4. Переходим к шагу 2 для пополнения теории.

Каждое исполнение шагов 2-3 называется волной. Автор тестировал алгоритм на нескольких популярных коллекциях и, как правило, для решения задачи не понадобилось больше семи волн. Я думаю, что читатель, знакомый с темой, уже узнал ReAct цикл в этом алгоритме. Да, примерно так оно и есть, только в качестве инструмента выступает символьный решатель, который не просто "исполняет инструмент", но и корректирует модель, не давая ей ошибаться, галлюцинировать, поправляя ее формальным выводом при условии истинности тех гипотез, которые выдвигает модель. Мне нравится образ символьного решателя как скелета для мышц, которые символизирует языковая модель.

Логики

Формальные логики тоже имеют свои структуры и разновидности. Простейшая логика первого порядка основана на наличии только хорновских правил: если истинны вместе данные факты, то значит истинен и этот. Выше в примере у нас было хорновское правило: has_engine(?x) ∧ wheel_count(?x,4) ∧ power(?x,150) ∧ door_count(?x,4) ⇒ is_a(?x, car). Хорновсие правила хороши тем, что теория на них монотонно пополняется (растет) - это дает возможность решения любой задачи, сформулированной на языке такой логики. Такую логику обозначим как L0.

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

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

Тестирование

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

ProofWriter

Синтетический бенчмарк от AI2. Коллекция содержит короткие тексты, типа "Anne is nice. All nice people are cold. Is Anne cold?". К каждому пример дается метка True / False / Unknown. Это как раз L0 логика с хорновскими правилами.

ProntoQA

Это тоже синтетика, но с онтологиями: классы, индивиды и т.п. Вопросы типа "принадлежит ли индивид такому-то классу". Для нас это предикат is_a и добавления оператора отрицания, в L0 его нет. решатель так и назвал L1.

ProntoQA-OOD

Это усложненная версия ProntoQA, куда подмешаны дизъюнкции, вложенные конъюнкции, отрицания, доказательства разбором случаев и от противного. Это чуть другой решатель, я его назвал L2.

FOLIO

Бенчмарк серьезный, не синтетика, а написанный вручную экспертами. Каждый пример это целая логическая история на естественном языке. Сопровождается посылками и выводами, а также метками True / False / Unknown. Как и почти все, написанное людьми, бенчмарк достаточно шумный и выглядит сложновато. Поэтому, модель не очень хорошо структурирует тексты этой коллекции, на ней я получил самые худшие результаты именно из-за этого свойства.

AR-LSAT

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

GSM8K

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

Результаты

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

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

• На L2-срезе решатель покрывает 44/45 в gold-fed режиме (т.е. с уже размеченной структурой), а при структурировании моделью дает 29–31/45.

• Отдельный negation-срез: 12/13 gold-fed и 11/13 live - сравнимо.

Сравнительные результаты

Мне также было интересно попробовать сравнить результаты своей работы с другим реализациями нейро-символических рассуждений. Я выбрал в качестве таковых две известны реализации Logic-LM и LINC. Оба решателя построены на тех же принципах, что и Ankyra, но интерфейс перевода в теорию у них чуть другой.

Чтобы результаты были сравнимыми, я также прогнал эти решатели на тех же примерах, на которых гонял Ankyra и на той же модели DeepSeek V4 Flash. Единственное, что оригинальные запуски LINC требовали 10 сэмплов, пришлось потратиться. Однако, результаты того стоили.

Подробно рассказывать, почему так вышло, я не здесь буду. Просто сошлюсь на статью на английском языке https://zenodo.org/records/23039403 где об этом рассказано подробно. Объявить это SOTA решением мне не позволяет честность т.к. я прогнал алгоритм не на всех примерах бенчмарков, но гордиться позволяет.

Зачем это нужно

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

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

Код проекта на Github: https://github.com/merfill/ankyra Проект с открытым исходным кодом, написан на языке Python с использованием библиотек LangChain и LanGraph.

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