Skip to content

ADR 006: Neuro‑Symbolic Governance (Нейро-символьное управление)

Дата: 2026-04-23
Статус: Принято
Автор: Black Swan Core Architecture Team

1. Контекст

До версии 0.9 проверка изменений L3.1-инвариантов (производных правил) выполнялась вручную через Constitutional Debate Loop: LLM-дебаты между Red‑Team и Blue‑Team с последующей проверкой контрпримеров.

Этот подход имел критические недостатки:

  1. Тривиальные тавтологии. LLM (особенно GLM‑5.1) склонна генерировать инварианты, которые истинны по определению (например, «i ≥ 0» для цикла, где переменная всегда неотрицательна). Z3 быстро доказывал их, создавая иллюзию корректной верификации.
  2. Неполные спецификации. LLM могла упустить граничные условия или неявные предположения, делая доказательство неполным.
  3. Человеческий фактор. Дебаты требовали ручной интерпретации результатов, что несовместимо с полностью автономной системой Фазы 4+.

С переходом на DeepSeek‑V4 (ADR‑001) и её улучшенными reasoning-способностями появилась возможность автоматизировать полный цикл: от генерации формальной спецификации до её верификации.

2. Решение

Реализовать Neuro‑Symbolic Governance Layer — полностью автоматический конвейер генерации, фильтрации и верификации формальных доказательств для изменений L3.1.

Компоненты конвейера:

  1. LLM‑генератор формальной спецификации. Architectus (DeepSeek‑V4, 60% экспертов) получает структурированный промпт, содержащий:

    • Полный набор L3.0‑аксиом в SMT‑LIB2.
    • Текущие L3.1‑инварианты.
    • Предлагаемое изменение на естественном языке.
    • Few‑shot примеры корректных спецификаций. На выходе — строго валидный SMT‑LIB2 или TLA+ код с определением нового предиката и утверждением его совместимости с L3.0.

  2. Concolic Filtering. Кастомная обёртка над angr выполняет символьное выполнение спецификации. Цели:

    • Отсеять тривиальные тавтологии: если инвариант выполняется на всех путях без сужения пространства состояний → trivial → отклонение.
    • Найти контрпример до тяжёлого SMT-солвера: если найден путь с нарушением → invalid → отклонение. Это снижает нагрузку на следующий этап на 30–40%.

  3. Multi‑Solver Verification. Спецификация проверяется тремя независимыми SMT‑солверами: Z3, CVC4, Yices. Решение принимается единогласно: все три должны вернуть unsat (отсутствие контрпримера). Если хотя бы один находит модель → предложение отклоняется.

  4. Сохранение доказательства. Успешная спецификация сохраняется в IPFS, её CID записывается в ConstitutionalPrinciple в Mem0g L2. Это позволяет перепроверить доказательство в будущем при изменении других L3.1.

Интеграция с Constitutional Evolution 2.0 (ADR‑004): В популяционном алгоритме NSGA‑II этот конвейер выполняет роль Z3‑Anchor — обязательного фильтра, через который проходят все мутации политик.

3. Последствия

Положительные

  • Математическая строгость. Каждая поправка к L3.1 имеет формальное доказательство совместимости с L3.0, проверяемое тремя независимыми солверами.
  • Устранение тривиальных доказательств. Concolic Filtering гарантирует, что Z3 проверяет содержательные инварианты.
  • Полная автоматизация. Цикл от предложения до верификации занимает ≤ 5 минут без участия человека.
  • Воспроизводимость. Proof Tree и CID доказательства позволяют повторить проверку в любой момент.

Отрицательные

  • Высокие требования к LLM. Генерация корректного SMT‑LIB2 требует полной мощности Architectus (60% экспертов). На ранних фазах (до Hardware Transition) это может создавать задержки.
  • Ложные отклонения. Concolic Filtering может отбрасывать валидные, но сложные инварианты, которые не укладываются в лимит времени символьного выполнения.
  • Зависимость от трёх солверов. При расхождении их результатов требуется дополнительный анализ.

Нейтральные

  • Необходимость поддержки актуальных версий Z3, CVC4, Yices и angr в изолированном sandbox.

4. Связь с другими документами