Проблема, которую все игнорируют: LLM врёт красиво, но непредсказуемо
Вы доверяете ИИ заполнить налоговую декларацию? Составить юридический договор? Проверить соответствие проекта строительным нормам? Ответ - нет. Потому что даже самая продвинутая модель в любой момент может сгенерировать юридически некорректную фразу, пропустить критичный пункт или "придумать" несуществующий нормативный акт. Это не баг, это фича - статистическая природа языковых моделей. Но в некоторых областях эта фича стоит денег, репутации и свободы.
Галлюцинации - не ошибка, а фундаментальное свойство генеративных моделей. Бороться с ними внутри архитектуры LLM - всё равно что пытаться заставить вероятностный процесс стать детерминированным. Безнадёжно.
Нейро-символический мост: когда нейросеть думает, а логика проверяет
CausaNova не пытается исправить LLM. Вместо этого она ставит над ней надзорный орган - SMT-солвер (Satisfiability Modulo Theories). Это инструмент формальной верификации, который доказывает или опровергает логические утверждения. Архитектура превращает процесс обработки документа в диалог между творцом и критиком.
1 Abstract Intent: LLM формулирует "что нужно сделать"
Первая фаза - перевод человеческого запроса на язык намерений. Не "заполни форму 3-НДФЛ", а "документ должен содержать: 1) ФИО плательщика, 2) ИНН, 3) сумму дохода за год X, 4) применяемый налоговый вычет по статье Y...". LLM (в реализации используют Qwen) генерирует абстрактную спецификацию требований. Здесь модель может ошибаться - пропустить пункт, добавить лишнее. Это нормально.
2 Guard Resolver: превращение намерений в логические ограничения
Критическая часть. Спецификация из первого шага транслируется в набор логических формул - guards (ограничений). Например: "сумма дохода ≥ 0", "ИНН состоит ровно из 12 цифр", "дата подачи ≤ текущая дата", "если применён вычет А, то не может быть применён вычет Б". Эти формулы пишутся на языке, понятном SMT-солверу (обычно SMT-LIB).
Guard Resolver - это по сути компилятор с естественного языка на язык формальной логики. Самая сложная часть системы, потому что ошибка трансляции сведёт на нет всю верификацию.
3 Документ как модель: извлечение фактов
Параллельно исходный документ (или заполненная форма) анализируется для извлечения структурированных данных. Имя, даты, числа, флаги. Эти данные также представляются как переменные в логической системе. Если в документе написано "Иванов Иван Иванович", система создаёт переменную taxpayer_name со значением "Иванов Иван Иванович".
4 SMT-солвер: формальная проверка выполнимости
Момент истины. SMT-солвер (Z3, CVC5 или аналоги) получает на вход: 1) ограничения из Guard Resolver, 2) факты из документа. Задача: доказать, что существует интерпретация переменных (значения из документа), удовлетворяющая всем ограничениям. Если доказательство найдено - документ корректен. Если нет - солвер возвращает контрпример: какие именно условия нарушены.
Пример из жизни: почему это работает там, где падают чистые LLM
Представьте систему проверки строительных планов. Человек говорит: "Проверь, соответствует ли план нормам пожарной безопасности".
- Обычная LLM: прочитает план, "вспомнит" общие принципы из обучающих данных, сгенерирует текст вроде "План в целом соответствует нормам, однако рекомендуется проверить ширину эвакуационных выходов". Расплывчато, неубедительно, потенциально опасно.
- CausaNova:
- Abstract Intent: LLM выделяет конкретные требования - "расстояние от любой точки помещения до выхода ≤ 30м", "ширина главного эвакуационного выхода ≥ 1.2м", "количество выходов ≥ 2 для помещений вместимостью > 50 человек".
- Guard Resolver: превращает это в формулы: (max_distance ≤ 30), (main_exit_width ≥ 1.2), (if capacity > 50 then exit_count ≥ 2).
- Из документа извлекаются факты: max_distance=35, main_exit_width=1.5, capacity=60, exit_count=1.
- SMT-солвер проверяет систему формул. Результат: "НЕВЫПОЛНИМО". Контрпример: нарушены условия max_distance ≤ 30 и (capacity > 50 → exit_count ≥ 2).
С чем сравнивать? Альтернативы, которые не дотягивают
| Подход | Как работает | Проблема |
|---|---|---|
| Чистые LLM с промптингом | "Будь внимателен, проверь всё тщательно" в промпте | Нулевые гарантии. Модель может искренне думать, что всё проверила, и всё равно ошибиться. |
| RAG (Retrieval-Augmented Generation) | Подкладывает в контекст нормативные документы | Уменьшает галлюцинации, но не устраняет. Модель может неправильно интерпретировать или проигнорировать часть контекста. Как в статье про LLM, которые понимают цель, но игнорируют её. |
| Простые rule-based системы | Жёсткие правила типа "если поле X, то проверь Y" | Хрупкость. Не справляются со сложными логическими зависимостями и контекстом. Требуют ручного поддержания тысяч правил. |
| Fine-tuning под конкретную задачу | Дообучение модели на примерах проверок | Улучшает среднюю точность, но не даёт 100% гарантии на новых данных. Ошибки всё равно будут, просто реже. |
| CausaNova (нейро-символический) | LLM генерирует гипотезы, SMT-солвер их доказывает/опровергает | Даёт формальные гарантии для проверяемой логики. Но требует описания домена на языке ограничений. |
Где это взять и как попробовать
Проект открыт на GitHub. Основа - Python, использует трансформерные модели (оригинальная работа тестировалась на Qwen, но подойдёт любая), SMT-солвер Z3 через API. Архитектура модульная: можно заменить LLM-компонент, можно использовать другой солвер.
Сложность не в запуске кода, а в определении доменных ограничений для вашей задачи. Нужно формально описать, что значит "корректный документ" в вашей области. Это требует экспертизы - юриста, бухгалтера, инженера. Но сделайте это один раз, и система будет проверять документы с математической точностью.
CausaNova не заменяет эксперта. Она формализует его знания в логические правила, а затем применяет эти правила с машиночитаемой строгостью. Эксперт всё равно нужен - но теперь его знания масштабируются.
Кому это нужно прямо сейчас
- Юридические технологии: проверка договоров на соответствие законодательству, выявление внутренних противоречий.
- Финансовый сектор: верификация отчётности, налоговых деклараций, заявок на кредит.
- Государственные услуги: автоматическая проверка заявлений граждан на полноту и соответствие требованиям.
- Инжиниринг и строительство: контроль проектной документации на соответствие нормам (СНиПы, ГОСТы).
- Медицина: проверка назначений на противоречия (несовместимые лекарства, нарушение протоколов).
Если ваша задача - не просто "сгенерировать текст похожий на документ", а гарантировать, что документ семантически корректен, CausaNova предлагает архитектурный ответ. Это не очередной wrapper над API OpenAI, а принципиально другой подход, где нейросеть отвечает за понимание естественного языка, а символьная система - за безошибочность логики.
Пока одни пытаются дообучить LLM "меньше галлюцинировать", другие строят мост между вероятностным и детерминированным мирами. Второй путь сложнее, но он единственный, который приводит к гарантиям. В мире, где ИИ начинает принимать решения с реальными последствиями, математическая проверка перестаёт быть академической роскошью. Она становится необходимостью.
Интересно, что подобный гибридный подход начинает появляться и в других областях - например, в Text-to-SQL системах с guardrails или в документ-ориентированных SLM. Но CausaNova идёт дальше - до формальных доказательств.
Попробуйте запустить демо. И когда в следующий раз услышите "ИИ заменит юристов", спросите: "А этот ИИ может доказать, что его вывод логически непротиворечив?" С CausaNova - может.
