Ankyra: нейро-символический движок, который честно говорит «не знаю»

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

Существует немало техник, улучшающих способность моделей к рассуждению: chain-of-thought, self-consistency, tree-of-thought и другие. Однако ни одна из них не даёт гарантии корректности. Это не недостаток конкретных моделей, а прямое следствие метода их построения: модель не учится рассуждать, она представляет собой снимок того, как люди рассуждают в текстах. Знание о мире и способность делать выводы — разные вещи. Люди обычно их различают, и вторая является предметом отдельной науки — формальной логики.

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

В этой статье я описываю один из способов такой организации, реализованный в открытом проекте Ankyra. Исходный код, документация и все проверки доступны для свободного использования без ограничений. Ключевая идея — не заставить модель рассуждать правильно, а разделить роли: языковая модель предлагает, символический движок решает. Надеюсь, читатель получит от этого текста такое же удовольствие, какое я получил от реализации.

Идея

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

Языковая модель читает текст и предлагает формализацию: какие в задаче есть объекты, какие факты, какие правила, какие гипотезы. Она свободна в своих предложениях и может предлагать что угодно. Но она не владеет истиной — и не претендует на неё. Её роль — поставлять материал, а не выносить вердикт.

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

Контракт предложения

Чтобы такое разделение работало, каждое предложение модели должно быть классифицировано. Причём не «на усмотрение» движка, а детерминированно — по формальным признакам. В Ankyra существует четыре категории:

Ключевое здесь — различение cited и hypothesis. Утверждение, подкреплённое цитатой, — это факт. Утверждение без цитаты — это допущение, и оно помечается как допущение. Модель не может выдать одно за другое: классификация не зависит от её «намерений».

Обоснованность ответа

Из этого соглашения напрямую следует главное свойство системы: обоснованность ответа никогда не превышает обоснованности его посылок.

Если вывод опирается только на цитаты из текста — это proven. Если в выводе участвуют допущения — это proven_under(H), и ответ перечисляет эти допущения поимённо. Если ничего установить не удалось — not_proven.

Это может показаться мелочью, но на практике это меняет всё. Пользователь видит не просто «да» или «нет», а на чём держится ответ. Если ответ получен с допущениями, он знает, какими именно. Если допущения его не устраивают, он может их отвергнуть и посмотреть, что останется.

Маленький пример

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

Модель извлекает два утверждения: факт raining() и правило raining() => is_wet(ground). Оба подкреплены дословными цитатами, поэтому оба получают категорию cited и попадают в аксиомы. Движок замыкает теорию, выводит is_wet(ground) и отвечает yes с обоснованностью proven. Модель в этом выводе больше не участвует.

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

Модель извлекает факты, но правил классификации в тексте нет. Движок ничего не выводит и честно сообщает, что цель не сопоставлена. Тогда запускается цикл, в котором модель предлагает правила: «двигатель — признак моторного средства», «моторное средство с четырьмя колёсами — автомобиль». Цитат под этими правилами нет, поэтому они получают категорию hypothesis и заносятся в журнал с пометками. Движок применяет их, выводит ответ, но помечает его как proven_under(H1, H2). Ответ получен, но пользователь видит, что он держится на допущениях.

Если те же правила предложить в режиме, где гипотезы запрещены, система честно ответит not_proven. Разница между двумя режимами не косметическая — она показывает, где заканчивается текст и начинается догадка.

Почему промпта недостаточно

Проблему галлюцинаций часто пытаются решить через промпт: попросить модель быть аккуратнее, не выдумывать, ссылаться на текст. Это работает — иногда. Но у промпта есть принципиальное ограничение: он вероятностен. Модель может его выполнить, а может и нет. Сегодня послушалась, завтра — нет. И самое неприятное: проверить, выполнила ли она его, невозможно без внешнего контроля.

Ankyra добавляет этот внешний контроль. Модель по-прежнему получает промпт и по-прежнему свободна в предложениях. Но её предложения попадают в систему, где каждое классифицируется — и утверждение без цитаты не может попасть в аксиомы. Не потому что модель «постаралась», а потому что движок его не примет. Это не замена промпта. Это то, чего промпту не хватает: проверки.

Как это работает

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

Декомпозиция

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

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

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

На выходе — формальная теория и формальный вопрос, выраженные в одном словаре.

Решение

В дело вступает символический движок. Он достраивает все следствия теории до неподвижной точки и проверяет, следует ли цель. Каждый выведенный факт несёт историю: какие факты и какое правило его породили. Движок не добавляет знания от себя — он работает относительно той формализации, которую получил.

Если цель следует из теории — ответ готов. Если нет, движок не останавливается на «неизвестно». Он сообщает, где именно возникла трудность: цель не сопоставлена ни с чем, посылка осталась неиспользованной, найдено противоречие. Эти структурированные пробелы — не отладочный вывод, а рабочий сигнал для следующего этапа.

Управляемый цикл

Если теория не решает вопрос, модель получает ограниченную возможность помочь. Это не свободное рассуждение, а по одному шагу за итерацию. Каждая итерация устроена так:

1. Движок замыкает текущую теорию и проверяет цель, порождая вердикт и пробелы.

2. Модель получает подсказку: структуру задачи, допустимые предикаты, сводку выведенного, текущие пробелы и цель.

3. Модель возвращает ровно одно типизированное предложение: переформулировать вопрос, добавить правило, утвердить цитируемый факт или выбрать подцель.

4. Движок классифицирует предложение по четырём категориям и применяет или отклоняет.

5. Итерация записывается в журнал, цикл начинается заново.

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

Цикл останавливается, когда вердикт определён, когда две итерации подряд ничего не изменили, когда исчерпан бюджет или когда гипотезы запрещены. Каждый из этих исходов — честная точка остановки, а не сбой.

Объяснение

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

Модель может позже пересказать готовую трассу связным текстом. Но она не может вставить в неё новые факты. Объяснение — это изложение доказательства, а не второе мнение о нём.

Что это даёт

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

Какие логики под капотом

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

Сейчас реализовано шесть формализмов. Каждый включается своим переключателем и покрыт собственным набором проверок.

L0 — определённые хорновские клаузы. Базовая линия. Факты, правила вида «если A, то B», транзитивное отношение is_a, отрицание парами P и ¬P в открытом мире. Процедура — полунаивный прямой вывод (forward chaining) до неподвижной точки. Это самая простая логика, и на ней держится всё остальное.

L1 — стратифицированное отрицание. Добавляет к L0 отрицательные ограничения и объявленный закрытый мир. Позволяет отвечать «нет» не потому, что не удалось доказать, а потому, что одна категория несовместима с другой. Мир — открытый или закрытый — задаётся запросом, а не угадывается по формулировке.

L2 — позитивная логика первого порядка. Дизъюнкция, кванторы существования и всеобщности, доказательство разбором случаев. Теория опускается в ground-клаузы, и ограниченная резолюция ищет противоречие при явно заданном бюджете шагов. Когда бюджет исчерпан без доказательства, ответ — честное insufficient: логика лишь полуразрешима, и исчерпание нельзя принять за опровержение.

L3 — конечно-доменные ограничения. Отдельный движок. Задачи вида «расставьте объекты при таких условиях» — это не логическая выводимость, а удовлетворение ограничений. Свой IR (Intermediate Representation), свой поиск по конечным областям. «Обязательно» означает истинность во всех моделях, «может быть» — хотя бы в одной.

L4 — точная арифметика. Тоже отдельный движок. Задача даёт число, а не следствие. Граф величин, линейная система, решение в точных рациональных числах. Арифметическая ошибка здесь невозможна по построению: неверное число может быть только ошибкой моделирования, но не счёта.

D — умолчания со специфичностью. Каждое правило — дефолт, строги только утверждённые факты. Более конкретный класс перевешивает более общий вдоль иерархии is_a. Если специфичность не может решить конфликт — правила одинаково конкретны или несравнимы, — система честно сообщает об этом, а не угадывает победителя.

Как выбирается процедура

Раз логик несколько, нужно решить, какая из них запускается. И сделать это, никогда не угадывая.

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

Отдельно запуск объявляет свою семантику: какие процедуры включены и читается ли запрос в открытом или закрытом мире. Решение о выборе процедуры сводит эти два начала и проверяет их друг против друга.

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

Это важно. Многие системы в такой ситуации «понижают» задачу до той логики, которую умеют решать, и выдают ответ, не предупреждая, что он получен в ослабленной форме. Ankyra так не делает. Она говорит: «эта задача требует логики, которой у меня нет», — и останавливается.

Что общего у всех движков

Каждый движок корректен относительно переданной ему формализации и честно воздерживается вместо угадывания. Символические компоненты полны относительно формализации — прямой вывод достигает неподвижной точки, — но полнота перевода не заявляется: модель всегда может упустить посылку в тексте.

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

Примеры

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

Отрицание через несовместимость

Текст: «Ни одно действительное число не является мнимым. Число a — действительное. Является ли a мнимым?»

Модель не формализует это как общее правило. Утверждение «ни одно действительное не мнимо» — это ограничение несовместимости: два класса не могут пересекаться. Вместе с фактом is_a(a, real_number) оно даёт ¬is_a(a, imaginary).

Вердикт — refuted, ответ «нет». Здесь важно, почему система отвечает «нет». Не потому что не удалось доказать обратное — в открытом мире это означало бы всего лишь unknown. А потому что найдено явное противоречие: два класса объявлены несовместимыми. Если бы такого ограничения не было, система честно воздержалась бы.

Разбор случаев

Теория: is_a(rex, prim). Правило: is_a(?x, prim) => is_a(?x, a) ∨ is_a(?x, b). Два правила: is_a(?x, a) => is_a(?x, c) и is_a(?x, b) => is_a(?x, c). Цель: is_a(rex, c).

Хорновская логика здесь бессильна: дизъюнкция в голове правила не помещается в её синтаксис. Включается клаузальная процедура. Она разбирает случаи: если Рекс попадёт в a, он окажется в c; если в b — тоже в c. Третьего варианта дизъюнкция не даёт. Значит, c следует в обоих случаях, а не в каком-то одном. Вердикт — supported.

Если бы L2 был выключен, та же задача получила бы out_of_fragment. Не «неизвестно». А именно: «эта задача требует логики, которой у меня сейчас нет».

Порядок и ограничения

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

Это не логический вывод. Это удовлетворение ограничений. Формализация — пять переменных с областью 0..4, ограничение all_different, порядковые и составные условия. Ответ ищется перебором по конечному домену: «обязательно» означает истинность во всех допустимых размещениях, «может быть» — хотя бы в одном.

На закодированных вручную реальных играх режим эталонного входа даёт 27/27. На живом прогоне — 23/30, и все семь промахов — честные воздержания, а не неверные ответы.

Точная арифметика

Задача GSM8K: «Генри сделал две остановки в поездке на 60 миль; первая — через 20 миль, вторая — за 15 миль до конца. Сколько миль он проехал между остановками?»

Модель строит граф величин: total=60, first=20, before_end=15. Искомая величина between задаётся уравнением. Линейная система решается в точных рациональных числах: 60 − 20 − 15 = 25.

Здесь работает отдельный движок — потому что арифметическая задача даёт число, а не следствие. И арифметическая ошибка в нём невозможна по построению: неверное число может быть только ошибкой моделирования, но не счёта. Если модель построила граф неверно — система получит неверное число, но не потому, что «ошиблась в вычислении».

Реальный текст

Строка из FOLIO: посылки содержат дизъюнкцию шести подвидов дикой индейки и факт WildTurkey(tom). Условные отрицания вместе с этим фактом дают ¬Eastern(tom), ¬Osceola(tom) и отрицание дизъюнкции Goulds, Merriams и Riogrande. Цель — Eastern(tom), метка False.

Клаузальная процедура опровергает цель: она следует из посылок с отрицанием. Вердикт — refuted, ответ «нет». Совпадает с меткой.

А вот другая строка, «Марвин»: цель помечена False, но размеченные посылки не влекут ни саму цель, ни её отрицание. Система честно отвечает unknown. Метка говорит «False», система говорит «не знаю». И это правильный ответ: она не выдаёт неподтверждённое «нет» за доказанное.

На срезе отрицания (13 строк) эталонный вход даёт 12/13 при нуле уверенно неверных выводов. Одна строка — та самая, где посылки недостаточны для метки. Система это видит.

Вывод с исключением

Текст: «Птицы летают. Пингвины — птицы, но пингвины не летают. Твити — пингвин. Твити летает?»

Модель извлекает два факта и два правила-умолчания. При обычном замыкании сработали бы оба правила и получилось бы противоречие. При включённом слое умолчаний правило про пингвинов оказывается строго специфичнее — оно опирается на ребро is_a(penguin, bird) — и побеждает. Вердикт refuted, ответ «нет», признак defeasible=true.

Симметричный пример — «птицы не летают, пингвины летают» — даёт supported и ответ «да»: специфичность не зависит от полярности. А если взять классический случай «Никсон — квакер и республиканец» с правилами «квакер — пацифист» и «республиканец — не пацифист», специфичность не определена: оба правила одинаково конкретны. Система честно сообщает unsupported с пробелом undecided_conflict, а не угадывает победителя.

Результаты

Проект проверялся на стандартных коллекциях. Ниже — сводка. Полные таблицы и методология — в статье, здесь только главное.

Синтетические проверки

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

Ни одной уверенно неверной ошибки. Это чистый сигнал движка — без извлечения, без разброса провайдера LLM. Для тестов я использовал провайдера RouterAI и модель DeepSeek-V4.1-Flash с выключенным режимом рассуждений. RouterAI на самом деле агрегатор провайдеров, на которых эта модель развернута с разными квантизациями, поэтому сведение температуры к нулю ил установка seed для выбора провайдера ничего не давала, все равно модель могла выдавать разные структуры при запусках.

Внешние коллекции

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

Главное — не проценты. Главное — то, что ни на одном срезе нет ни одного уверенно неверного вывода. Все промахи — честные воздержания: unknown, out_of_fragment, insufficient. Система может не решить задачу. Она не может решить её неправильно и не заметить этого.

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

Где больно

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

На срезе L2 (45 строк) охват — 44/45, то есть реализованная логика выражает почти всё. Но при живом прогоне получается 29/44. Разрыв между режимом эталонного входа (42/44) и живым (29/44) показывает: движок справляется, а извлечение — нет. Потолок метода достигнут, потолок перевода — нет.

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

Где это можно применить

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

Юридический ассистент

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

Прототип работает. Он умеет читать нормативный текст, извлекать правила, проверять их на совместность и выводить следствия с указанием источника. Каждый ответ можно проверить: вот цитата из нормы, вот правило, вот вывод. Также, прототип умеет разбирать договоры и судебные решения, говорить о возможных проблемах и предлагать исправления в договорах и возможные зацепки в решениях

Но прототип — это не продукт. Нужна юридическая отладка: корпус реальных документов, проверка на живых задачах, уточнение извлечения. Нужны дополнения — работа с исключениями, приоритетами норм, ссылками между документами. Это отдельная работа, и я ищу людей, которым такая задача интересна.

Комплаенс и проверка регламентов

Близкая область — проверка внутренних регламентов и политик на непротиворечивость. Когда в компании сотни документов, и никто не помнит, какие из них друг другу противоречат. Здесь работают те же механики: извлечение правил, проверка на совместность, вывод следствий с указанием источника. И тот же принцип: система не «решает», она показывает, где именно противоречие и на чём оно держится.

Медицинские протоколы

Ещё одна область, где важна проверяемость. Клинические рекомендации — это набор условных правил: если такие-то показатели, то такое-то вмешательство. Модель может извлечь эти правила из текста, движок — проверить, совместны ли они, что следует из конкретной ситуации и где рекомендации противоречат друг другу. Ответ с цитатой и обоснованием здесь не роскошь, а необходимость.

Финансовый и налоговый анализ

Правила налогообложения, условия договоров, регуляторные требования. Везде, где есть условные правила и нужно понять, что из них следует для конкретного случая. Система может помочь не «посчитать налог», а показать, из каких норм складывается результат и на чём держится каждое утверждение.

Техническая документация и спецификации

Проверка непротиворечивости технических требований — ещё одна задача того же типа. Когда в спецификации сотни пунктов, и нужно понять, не противоречат ли они друг другу, и что из них следует для конкретного сценария. Модель читает, движок проверяет, ответ приходит с цитатами.

Образование

Разбор задач с пошаговым объяснением — область, где проверяемость особенно ценна. Система не просто даёт ответ, а показывает вывод: вот посылки, вот правило, вот следствие. Студент видит не «правильный ответ», а почему он правильный. И может проверить каждый шаг.

Научные исследования

Проверка логической структуры статей и теорий, поиск противоречий, проверка совместности гипотез. Здесь система работает не как «помощник в написании», а как инструмент проверки: она не предлагает содержание, она проверяет то, что уже сформулировано.

Заключение

Во всех перечисленных областях работает один и тот же принцип: модель предлагает, движок решает, человек выбирает. Система не заменяет специалиста — она даёт ему инструмент, который не врёт. Может не решить. Может воздержаться. Но если решает — можно проверить, на чём.

Код, документация и все проверки — на GitHub:

https://github.com/merfill/ankyra

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