Microsoft показала PDD Kit для проверки кода, написанного ИИ-агентами
PDD Kit доказывает, что код соответствует заданным требованиям, а там, где доказательство неприменимо, использует тесты; пока инструмент проверяет только код на языке программирования Rust.
Microsoft Research представила PDD Kit — исследовательский прототип для проверки кода, написанного ИИ-агентами. Он превращает требования разработчика в формальные условия и математически доказывает, что программа им соответствует.
Почему это важно: Тесты агента могут подтверждать работу написанной им программы, даже если она расходится с заказанным поведением. Доказательство охватывает все входные данные в рамках заданной модели и её допущений. Человек при этом проверяет сами требования и границы доказательства.
Повод: Исследователи испытали PDD Kit на Pet Store — интернет-магазине примерно из 5 000 строк кода на языке Rust. Формальная проверка охватила логику входа. По словам Microsoft Research, она выявила существовавшие ошибки, а разработчику не потребовалось читать весь сгенерированный код построчно.
Детали: Исходное требование разрешало выдавать токен — цифровое подтверждение входа — только при правильном пароле. Программа, которая отказывает всем, тоже выполнила бы это условие. Поэтому разработчик подтвердил и обратное: верный пароль должен давать токен, если поиск учётной записи и подпись токена прошли без ошибок. Доказательство также связывает пароль и токен с одной учётной записью: оно исключает сценарий, когда проверяют пароль Боба, а доступ выдают от имени Алисы.
Как это работает: Сначала PDD Kit читает код, задаёт уточняющие вопросы и фиксирует ответы в понятном команде плане. Затем агент составляет спецификацию — точные условия, которым должна отвечать программа, — пишет реализацию и доказательство. Доказательство принимает или отвергает Verus, инструмент формальной проверки программ на Rust. Это механическая проверка: языковая модель не решает, пройден ли этот этап.
Проверка требований: Два дополнительных агента проверяют, правильно ли спецификация передаёт намерения разработчика. Чтобы выявить слишком слабые условия, PDD Kit намеренно вносит ошибки в отдельные копии кода — например, заставляет программу отказывать всем пользователям. Verus должен отвергнуть каждую такую версию по соответствующему условию. Пропущенную ошибку система считает пробелом и отправляет работу на доработку.
Но: Функции, которые обращаются к базе данных, проверяют пароль или подписывают токен, остаются за границей доказательства. Их поведение разработчик принимает как допущение, а PDD Kit проверяет тестами. Спецификация также не гарантирует, что запрос когда-либо завершится, и не ограничивает частоту попыток входа. Пока прототип формально проверяет только код на Rust.
В примере доказанную логику встроили в действующий обработчик входа. PDD Kit добавляет Verus к автоматическим проверкам проекта: последующие правки человека или агента тоже должны соответствовать утверждённой спецификации. Нарушение доказательства останавливает сборку программы.