Исследователи Caltech выпустили TorchLean — фреймворк для формальной верификации нейронных сетей в системе доказательств Lean 4. Инструмент решает критическую проблему: разрыв между кодом, который выполняет модель, и математическими гарантиями её корректности.
Сейчас верификация ИИ-моделей происходит отдельно от их исполнения. Это создаёт семантический разрыв — гарантии могут нарушиться из-за различий в обработке данных, округлении чисел или интерпретации операций. В критически важных системах — медицине, автопилотах, финансах — такие расхождения недопустимы.
Как работает TorchLean
Фреймворк объединяет три компонента:
- PyTorch-совместимый API с режимами выполнения
- Точная семантика чисел Float32 по стандарту IEEE-754
- Верификация через методы IBP и CROWN/LiRPA с проверкой сертификатов
Команда протестировала решение на задачах сертифицированной робастности, физически-информированных нейросетях (PINNs) и верификации нейронных контроллеров. Также формализовала теорему универсальной аппроксимации — фундаментальный результат теории нейросетей.
Практическое применение
Для создателей критически важных ИИ-систем это означает возможность получить математические гарантии корректности без отрыва от привычного PyTorch-workflow.
Особенно актуально для стартапов в области автономного транспорта, медтеха и финтеха, где регуляторы требуют формальных доказательств безопасности.
Проект доступен с открытым исходным кодом на leandojo.org.
