Исследователи выпустили TorchLean — первый фреймворк, который объединяет привычный PyTorch API с математически строгой верификацией нейросетей в системе доказательств Lean 4.
Раньше модель обучалась в PyTorch, а анализировалась в другой системе. Между ними — семантический разрыв: различия в операторах, форматах тензоров или обработке чисел с плавающей точкой могли нарушить гарантии безопасности.
Как это работает
TorchLean строится на трёх компонентах:
• Верифицированный API в стиле PyTorch с eager и compiled режимами — оба компилируются в единое промежуточное представление
• Точная семантика Float32 через исполняемое ядро IEEE-754 и модели округления
• Верификация через алгоритмы IBP и CROWN/LiRPA с проверкой сертификатов
(Для справки: Lean 4 — система интерактивных доказательств, где математические утверждения формализуют и проверяют компьютером.)
Что протестировали
Авторы проверили систему на сертифицированной робастности, физически-информированных нейросетях (PINNs) и верификации нейроконтроллеров. Дополнительно механизировали теоретические результаты — включая универсальную теорему аппроксимации.
И что мне с этого?
Для разработчиков ИИ-систем в критических областях — от беспилотников до медтеха — TorchLean открывает возможность получить математические гарантии безопасности без смены привычного инструментария.
Следующий этап — расширение поддержки операторов и интеграция с популярными библиотеками верификации.