Нейросимволический ИИ

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

Зачем их объединять

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

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

Паттерн на практике

Типичная архитектура: нейросетевая модель работает как фронтенд, который интерпретирует вопрос пользователя и переводит его в формальный запрос, а символьный солвер выполняет этот запрос и возвращает гарантированно корректный результат. LLM вообще не касается вычислений - она лишь переводит и презентует результат.

Наглядный пример - chiasmus. LLM определяет: "пользователь хочет узнать, может ли пользовательский ввод дойти до этого SQL-запроса", формулирует запрос достижимости и вызывает MCP-инструмент. Tree-sitter разбирает код в AST, факты Prolog кодируют граф вызовов, а поиск с возвратом (backtracking) в Prolog находит все пути (или доказывает, что их нет). Ответ выдаёт солвер, а не модель.

Где это применяется

• Анализ кода - chiasmus использует tree-sitter + Prolog для анализа достижимости, поиска мёртвого кода и анализа влияния изменений
• Математические рассуждения - LLM переводят текстовые задачи на язык символьной математики, а затем вызывают CAS (Wolfram, SymPy) для решения
• Планирование - LLM генерируют описания доменов на PDDL, после чего классические планировщики находят оптимальные последовательности действий. Проверка результата важна не меньше: в llm-self-verification-limits самокритика планов в Blocksworld дала GPT-4 гораздо меньше пользы, чем валидатор планов VAL, а в остальных протестированных доменах самокритика и вовсе снизила точность
• Запросы к базам данных - text-to-SQL, где LLM генерирует запрос, а движок базы данных гарантирует корректное исполнение
• Формальная верификация - LLM генерируют наброски доказательств, а интерактивные доказатели теорем (Lean, Coq) их проверяют
• Головоломки с ограничениями - судоку кодируется как 9-раскраска графа или полиномиальный идеал, после чего передаётся солверу с возвратом или решателю на базисах Грёбнера (chalkdust-sudoku-secrets)

Экономика токенов

Помимо корректности, здесь есть и чисто прагматический аргумент стоимости. Символьные солверы работают локально и вообще не тратят токены. LLM, которая делает пять итераций поиска через grep и рассуждений для трассировки цепочки вызовов, потратит ~2500 токенов и всё равно может упустить какие-то пути. Один вызов символьного солвера как инструмента обходится в ~200 токенов и даёт исчерпывающий результат. Чем больше вычислений удаётся вынести в детерминированные локальные инструменты, тем дешевле и надёжнее становится система.

Противоречие с end-to-end подходом

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