Зеленые доказательства, пустые обещания: когда агенты ИИ пишут свои собственные спецификации

Я попросил агентов по кодированию ИИ написать формально проверенный код. Каждое решение прошло верификатор. Затем я проверил, что на самом деле обещали доказательства. Что касается меньшей модели, то 5 из 8 спецификаций практически ничего не говорят. Один из методы были неправильными, и их доказательство было зеленым. Этот пост посвящен этому пробелу, дешевому способу его обнаружения и небольшому инструменту с открытым исходным кодом, который это делает. для любого файла Дафни. Эксперимент Я разрабатываю язык программирования, который будет писаться агентами и проверяться машинами. (подробнее об этом в конце). Прежде чем что-либо проектировать, мне нужны были данные: когда агент должен доказать его код, меньше ли ошибок проскакивает? Настройка (VerifBench): 8 коротких алгоритмических задач, выбранных потому, что студенты LLM классически на них натыкаются: григорианский подсчет дней (високосные столетия), строгая проверка UTF-8 (длинные значения, суррогаты), сопоставление glob с экранированием, кэшем LRU, лексикографически наименьшей топологической сортировкой, выравниванием текста, сложение больших чисел (заимствования, -0), нормализация пути Unix. Та же спецификация естественного языка, два варианта: простой Python (агент может запускать собственные тесты) или Дафни, где агент должен написать требования/гарантии/инварианты и получить дафни подтвердите, чтобы пройти. Читы типа «предполагать» или