Логика в верификации и AI

2024: DeepMind AlphaProof получает серебро на IMO, используя формальные доказательства в Lean. В том же году Boeing сертифицирует автопилот через formal methods. А npm при каждом `npm install` запускает SAT-солвер - ту же технологию, что верифицирует процессоры Intel.

• npm/yarn dependency resolution - SAT под капотом каждого `npm install`
• AWS S2N TLS: Z3 нашёл реальные баги до деплоя в продакшн
• AlphaProof (DeepMind 2024) - серебряная медаль IMO через Lean + LLM

SAT-солверы: NP-полнота в продакшне

SAT (Boolean Satisfiability) - первая NP-полная задача (Cook 1971): дана формула в КНФ, существует ли присваивание переменных, делающее её истинной? Долгое время считалось, что NP-полнота делает SAT практически непригодным. **DPLL** (Davis-Putnam-Logemann-Loveland, 1962) изменил это: поиск с возвратом плюс два правила упрощения.

**Unit propagation:** если клауза содержит ровно один незначенный литерал, его значение вынуждено. **Pure literal elimination:** если литерал встречается только с одним знаком, можно сразу присвоить значение. Эти два правила резко сокращают пространство поиска.

**MiniSAT** (Een & Sorenson, 2003) - 600 строк C++, перевернул SAT-соревнования. Показал, что простая реализация CDCL бьёт сложные эвристики. Kissat (2020, Biere et al.) - современный чемпион SAT Race, прямой наследник MiniSAT.

**ML-применение:** npm/yarn dependency resolution - это SAT-задача. Каждый `npm install` запускает minisat-подобный солвер: зависимости пакетов кодируются как клаузы, solver ищет совместимое присваивание версий. Intel использует SAT для верификации чип-дизайна (Cadence Formal). AWS использует SAT в инструментах синтеза аппаратуры.

SMT: SAT плюс арифметика

SAT работает с булевыми переменными. Реальные программы используют целые числа, массивы, указатели. **SMT** (Satisfiability Modulo Theories) расширяет SAT теориями: линейная арифметика, битовые векторы, массивы, неинтерпретированные функции. Формула $x + y > 5 \land x < 3 \land y < 3$ - типичный SMT-запрос.

**Архитектура DPLL(T):** SAT-ядро работает с абстрактными булевыми переменными, представляющими атомарные формулы теории. При каждом частичном присваивании T-solver проверяет совместность с теорией. При T-конфликте генерируется объяснение - новая клауза для SAT-ядра. SAT управляет комбинаторикой, T-solver - теорией.

**Z3** (Leonardo de Moura & Nikolaj Bjorner, Microsoft Research, 2008) - стандарт индустрии. Открытый исходный код, Python/C++/Java/C# bindings. Выиграл множество SMT-соревнований (SMT-COMP). **CVC5** (Stanford/Iowa/NYU) - основной конкурент, особенно силён в теории строк.

**ML-применение:** AWS формально верифицировала библиотеку S2N TLS с помощью Z3 - солвер нашёл реальные баги до деплоя в продакшн. Ethereum Certora Prover использует SMT для верификации смарт-контрактов (миллиарды долларов под защитой формальных методов). Python mypy использует SMT-подобные рассуждения в type narrowing.

Автоматическое доказательство теорем

SMT решает вопрос выполнимости. Иногда требуется доказать теорему - построить формальное доказательство, проверяемое машиной. **Интерактивные пруверы** (proof assistants): Lean 4, Coq, Isabelle/HOL. Математик пишет доказательство, система верифицирует каждый шаг. Программа и доказательство - одно и то же.

**Соответствие Карри-Говарда:** доказательство = программа, утверждение = тип. Если тип `A -> B` населён (существует программа этого типа), то из A доказуемо B. Это не метафора - буквальный изоморфизм. В Coq одна запись является одновременно функцией и доказательством теоремы. В Lean 4: `theorem add_comm (n m : Nat) : n + m = m + n`

**AlphaProof** (DeepMind, 2024): LLM генерирует кандидаты доказательств в Lean 4, формальный верификатор отбрасывает неверные. Результат: серебряная медаль на IMO 2024 - решены 4 из 6 задач. Первое автоматическое решение задач олимпийского уровня с формальными гарантиями.

**ML-применение:** Lean Copilot (Stanford) - GitHub Copilot для формальных доказательств, использует LLM для подсказок тактик. Microsoft верифицирует драйверы Windows устройств с помощью Dafny (язык с встроенным SMT-верификатором). Проект Mathlib содержит 100,000+ формально верифицированных теорем в Lean 4.

Верификация нейросетей

Формальные методы верифицируют программы относительно спецификации. **Верификация нейросетей** - новая область: проверяем свойства типа $\epsilon$-робастности формально. Дано: сеть $f$, входная область $D$, свойство $P$. Задача: верно ли, что для всех $x \in D$ выполняется $P(f(x))$?

**Reluplex** (Katz et al., 2017) - первый SMT-солвер для нейросетей с ReLU-активациями. Расширяет симплекс-метод правилом обработки ReLU. Применён к ACAS Xu (бортовая система предотвращения столкновений): нашёл реальное нарушение safety-свойства в одном из 45 нейросетей-советников.

**Marabou** (NeuralNetworkVerification.com) - открытый наследник Reluplex, поддерживает свёрточные сети. alpha-beta-CROWN - современный чемпион (VNN-COMP 2021-2023), комбинирует branch-and-bound с LP-релаксациями. Certification gap: разрыв между тем, что можно верифицировать, и тем, что реально деплоится в safety-critical системы.

Формальная верификация гарантирует, что **модель соответствует спецификации** - но не что сама спецификация правильна. ACAS Xu: нашли нарушение safety property, но сама property была написана инженерами и могла не охватить все сценарии. Верификация переносит риск с реализации на спецификацию.

**ML-применение:** автопилот Boeing 787 сертифицирован с использованием formal methods (DO-178C Level A - высший уровень критичности ПО). Tesla FSD использует bounded model checking для safety-свойств. FAA требует формальную верификацию для DO-178C Level A ПО. Стандарт ISO 26262 (automotive) требует formal analysis для ASIL-D систем.

Ключевые идеи

• SAT - NP-полная задача, но CDCL (нехронологический откат + clause learning) делает её практически решаемой для задач с миллионами переменных
• SMT расширяет SAT теориями арифметики и структур данных: DPLL(T) = SAT-ядро + T-солвер. Z3 - стандарт индустрии
• Соответствие Карри-Говарда: доказательство = программа, утверждение = тип. AlphaProof (2024) использует LLM + Lean для IMO-уровня
• Верификация NN (Reluplex, Marabou) проверяет safety/robustness формально, но верифицирует соответствие спецификации - не её корректность

Связанные темы

Формальная логика связывает несколько разделов математики и CS:

• Модальная логика — Темпоральная логика LTL/CTL - основа model checking в верификации программ
• Дискретная математика — Графы импликаций в CDCL, комбинаторика пространства поиска SAT

Вопросы для размышления

• SAT является NP-полной задачей, но CDCL-солверы решают промышленные экземпляры с миллионами переменных. Что это говорит о структуре практических SAT-задач по сравнению с worst-case?
• Формальная верификация Boeing 787 гарантирует соответствие спецификации DO-178C. Кто и как верифицирует саму спецификацию?
• AlphaProof генерирует доказательства в Lean, которые затем проверяет формальный верификатор. Чем это принципиально отличается от генерации доказательств без формальной проверки?

Связанные уроки

• ml-12 — Темпоральная логика LTL/CTL из модальной логики - основа model checking в верификации программ
• dm-01 — Дискретная математика - основа SAT и графовых алгоритмов в CDCL
• lt-01-pac-intro — Формальная верификация ML-моделей требует PAC-гарантий как спецификаций
• it-01 — Информационно-теоретические рассуждения параллельны логическим доказательствам
• prob-04-bayes — Вероятностные модели верифицируются через вероятностный SMT
• fl-33-formal-verification