Исследователи разработали VERINA — новый стандарт проверки кода и формальных доказательств ИИ

<p><strong>Исследователи из Калифорнийского университета и Meta FAIR представили VERINA — новый бенчмарк для комплексной оценки генерации кода, спецификаций и формальных доказательств с помощью языковых моделей искусственного интеллекта.</strong></p> <p>Современные языковые модели ИИ активно используются для программирования и уже внедряются в инструменты вроде Cursor и GitHub Copilot. Однако, как отмечают эксперты, такие системы не способны гарантировать абсолютную корректность создаваемого кода: ошибки и баги становятся серьезным препятствием для продуктивности разработчиков. «Проблема в том, что существующие бенчмарки не охватывают все этапы — генерацию кода, спецификаций и доказательств — в едином комплексе», — отмечают авторы исследования.</p> <p>VERINA (Verifiable Code Generation Arena) — первый в своем роде бенчмарк, который включает 189 задач разного уровня сложности с подробными описаниями, кодом, спецификациями, формальными доказательствами и тестами, оформленными в системе Lean. Все примеры прошли ручную проверку и доработку для обеспечения качества, а тесты обеспечивают 100% покрытие строк кода и гарантируют корректность решений.</p> <p>Набор данных разделен на две части: VERINA-BASIC (108 задач, переведенных из Dafny) и VERINA-ADV (81 более сложная задача, взятая из студенческих работ по теоремному доказательству). Такой подход позволяет оценивать ИИ на задачах разной сложности и выявлять, как увеличивается сложность генерации формальных доказательств.</p> <p>В ходе тестирования девяти современных языковых моделей было установлено: лучше всего ИИ справляется с генерацией кода, хуже — со спецификациями, и наиболее сложной остается задача генерации формальных доказательств (успех менее 3,6% для всех моделей). Особенно заметно падение результатов на сложных задачах VERINA-ADV. При этом предоставление готовых спецификаций значительно улучшает качество кода, а итеративная доработка доказательств позволяет повысить успешность на простых задачах.</p> <p>Эксперты отмечают, что VERINA задает новый стандарт для оценки ИИ в программировании, но пока остается относительно небольшим по объему и требует дальнейшего масштабирования. В будущем планируется расширение набора задач и совершенствование метрик с использованием более мощных автоматических доказателей.</p>