Математика может стать ремнём безопасности для вайбкодинга

Математика может стать ремнём безопасности для вайбкодинга

Исследовательница Стэнфорда Чуюэ Сун и её коллеги применили ИИ для формальной проверки части кода, шифрующего переписку в Signal. Проект занял менее половины дня и стоил меньше 500 долларов; вручную та же работа потребовала пяти месяцев трёх квалифицированных специалистов.

Формальная проверка не просто прогоняет тесты, а превращает требования и код в формулы, чтобы математически подтвердить нужные свойства программы. Раньше это было слишком долго и дорого. Теперь стартапы пытаются сделать подход практичным: Сун присоединилась к &Truth, а Anthropic и Theorem сообщили, что с помощью ИИ нашли ошибки в открытом коде, которые не обнаружили триллионы тестов.

Для вайбкодера вывод простой: генерировать быстрее уже мало — следующий полезный слой продукта может доказывать, что критичный код ведёт себя именно так, как задумано.

Какой модуль вашего проекта вы бы первым отправили на математическую проверку?

«У меня работает» получает строгое доказательство.

🔗 Источник:: https://www.wired.com/story/software-verification-is-the-hot-new-answer-to-the-ai-safety-crisis/