В статье, опубликованной на arXiv 5 ноября, рассматривается, что означает «верифицированный» код, сгенерированный большими языковыми моделями. Авторы разделяют три проверки: принимает ли верификатор код, связано ли доказательство со спецификацией и отражает ли эта спецификация исходное требование.
В одном из тестов авторы сообщают, что верификатор принял 99.1% решений на HumanEval, но лишь для 1.9% примеров сертификат был связан с предикатом или функцией, заданными спецификацией. В отдельном конвейере на Rust, разработанном для обеспечения такой связи, скрытые тесты не прошли 11.48% структурно верифицированных примеров MBPP-Rust и 14.82% примеров из части VeriContest.
Почему это важно
Для команд, которые используют проверку доказательств при оценке сгенерированного кода, результаты показывают: одного лишь принятия кода верификатором может быть недостаточно, чтобы установить его содержательную связь с требованиями или корректность при прохождении скрытых тестов.
