Математическая логика
Логика и AI
AlphaProof решает задачи Международной Математической Олимпиады на уровне серебряной медали. Это не просто паттерн-матчинг - это формальные доказательства, проверенные Lean4. Граница между нейронным и символьным AI исчезает.
- **AlphaProof (2024):** DeepMind решил 4/6 задач IMO-2024, объединив LLM с поиском по пространству доказательств Lean4
- **Certified Neural Networks:** верификация свойств нейросетей (робастность, fairness) с помощью формальных методов в Marabou, α,β-CROWN
- **DeepProbLog в производстве:** комбинирование нейросетей и вероятностной логики в медицинской диагностике и автономных системах
Предварительные знания
Разрыв между нейронным и символьным
AlphaGeometry (2024) решил 25 из 30 задач IMO по геометрии, объединив нейросеть с символьным движком дедукции. Нейронные сети обучаются на данных, но не умеют систематически рассуждать. Символьный AI рассуждает точно, но хрупок и не обобщается. **Нейро-символьная интеграция** (neuro-symbolic AI) пытается объединить оба мира: нейронная гибкость + логическая строгость.
1) Loose coupling: нейросеть для восприятия, логика для рассуждения. 2) Tight coupling: логические ограничения в функции потерь. 3) Full integration: дифференцируемая логика - градиентный спуск прямо через логические операции.
Почему нейронные сети плохо справляются с задачами систематической композиции (systematic generalization)?
Дифференцируемая логика
Дифференцируемая логика делает логические операции **дифференцируемыми**: заменяет булевы AND/OR/NOT на непрерывные функции. Это позволяет обучать нейросети с логическими ограничениями через градиентный спуск.
T-норма - обобщение AND на [0,1]: t(a,b) где t(1,1)=1, монотонность, коммутативность, ассоциативность. Примеры: min(a,b), ab (product), max(0,a+b-1) (Łukasiewicz). T-конорма - обобщение OR: s(a,b) = 1-t(1-a,1-b).
Зачем в дифференцируемой логике используется product t-норма p·q вместо min(p,q)?
Logic Tensor Networks
Logic Tensor Networks (LTN, Donadello et al., 2017) - фреймворк, объединяющий логику первого порядка с тензорными операциями. Константы, переменные и предикаты представляются векторами; кванторы ∀ и ∃ - агрегациями по тензорам.
В LTN используется «Real Logic»: замена символов на вещественные тензоры. Предикат P(x) → нейросеть из ℝⁿ в [0,1]. Константы → обучаемые эмбеддинги. Функции → нейросети. Кванторы → mean/min агрегации.
Как квантор ∀x. P(x) реализуется в Logic Tensor Networks?
Будущее: AlphaProof и LLM + Logic
Новейшие системы объединяют мощь LLM с формальными доказательными ассистентами. **AlphaProof** (DeepMind, 2024) решил задачи IMO уровня, комбинируя AlphaZero-поиск с Lean4. Это указывает на конвергенцию нейронного и символьного AI.
LLM умеют генерировать Lean/Coq код - перевод математики на формальный язык. Формальный верификатор проверяет корректность. LLM генерирует много вариантов → верификатор фильтрует → правильные используются для дообучения LLM. Цикл самоулучшения.
Какое ключевое преимущество комбинации LLM + формального верификатора над чистым LLM?
Ключевые идеи
- **NeSy разрыв** - нейронное: гибко, но непрозрачно; символьное: точно, но хрупко; интеграция - объединить оба
- **Дифференцируемая логика** - AND/OR/NOT как T-нормы на [0,1]; логические правила = soft constraints в функции потерь
- **LTN** - предикаты = нейросети; константы = эмбеддинги; кванторы = агрегации; обучение через удовлетворение аксиом
- **LLM + formal verifier** - LLM генерирует кандидаты доказательств, верификатор гарантирует корректность; AlphaProof = IMO silver
Связанные темы
Нейро-символьный AI синтезирует весь курс математической логики:
- Логика в верификации и AI — Формальная верификация нейросетей - применение методов логики к ML-системам
- Вероятностная логика и логика знаний — DeepProbLog = нейросети + вероятностная логика; эпистемическое планирование в NeSy-агентах
- MLTT и Coq/Agda — AlphaProof использует Lean4 (основан на зависимых типах); формальное доказательство = MLTT-терм
Вопросы для размышления
- LLM (GPT-4, Claude) иногда рассуждают правильно, иногда «галлюцинируют». Что им не хватает до настоящего логического вывода? Это вопрос архитектуры или данных?
- Если нейросеть обучается на логических ограничениях - является ли она в каком-то смысле «понимающей» логику? Или только имитирует?
- AlphaProof решает IMO-задачи, но не умеет сформулировать новую нетривиальную теорему. Что нужно для «настоящего» математического творчества в AI?