Разрыв между корректным кодом и верифицированной программой

LLM могут писать Rust, который компилируется и даже проходит cargo test. Что они не могут делать надёжно — так это писать формальное доказательство того, что код корректен для всех возможных входных данных.

Проблема не в синтаксисе Rust. Формальная верификация требует, чтобы вы сформулировали, что хотите доказать, нашли инвариант, который позволяет доказательству пройти, и выразили оба утверждения на языке, который принимает верификатор. LLM обучаются на исходном коде, а не на самом акте доказательства. Они видят теоремы, но редко видят двадцать неудачных попыток, предшествовавших успешному доказательству.

Если вы вставите рекурсивный бинарный поиск в GPT-4 и попросите «докажи, что это верно», вы получите нечто, похожее на доказательство. В нём будут упоминаться инварианты циклов и предусловия. Но, скорее всего, в нём будет синтаксис из Dafny, ссылки на леммы, которых не существует, и утверждения об инвариантах, слишком слабых для установки постусловия. Это выглядит правильно, пока вы не попытаетесь это проверить.

Как на самом деле выглядит формальная верификация Rust

В Rust есть несколько инструментов верификации. Kani — это верификатор моделей (model checker), который исчерпывающе исследует все возможные состояния функции в определённых границах. Prusti и Creusot — дедуктивные верификаторы, которые переводят Rust в логику и просят SMT-solver доказать свойства. Каждый требует аннотаций в конкретном синтаксисе.

Вот простая функция и как выглядит настоящее дедуктивное доказательство в Creusot:

// Requires creusot-contracts crate
use creusot_contracts::*;

#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
    &a[0]
}

Creusot проверяет, что предусловие a.len() > 0 гарантирует постусловие result == a[0]. Это тривиально, потому что логика простая. Теперь усложним:

use creusot_contracts::*;

#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
    let mut i = 0;
    let mut s = 0;
    #[invariant(i <= n)]
    #[invariant(s == i * (i + 1) / 2)]
    while i < n {
        i += 1;
        s += i;
    }
    s
}

Инварианты — это сложная часть. Человек пишет их, размышляя о том, что остаётся истинным на каждой итерации. LLM может угадать s == i * (i - 1) / 2, потому что этот шаблон встречается в обучающих данных, или полностью опустить инвариант и дать solver-у потерпеть неудачу.

Что происходит, когда вы просите LLM о доказательстве

Я тестировал это на нескольких моделях. Промпт был: «Напиши верифицированную Rust-функцию, вычисляющую факториал n с помощью Creusot, с полными предусловиями, постусловиями и инвариантами цикла.»

Ответы разделились на три категории.

Во-первых, некоторые модели выдали правдоподобно выглядящие аннотации с неправильным синтаксисом. Они написали #[precondition(...)] вместо #[requires(...)] или смешали синтаксис Prusti с синтаксисом Creusot. Код даже не парсился.

Во-вторых, некоторые модели выдали синтаксически корректные аннотации со слишком слабыми инвариантами. Для функции факториала нужен инвариант вроде res == fact(i). Модели часто писали res >= i, что истинно, но бесполезно для доказательства постусловия. Creusot сообщал, что не может установить цель, и у LLM не было механизма это исправить.

В-третьих, в нескольких ответах инвариант был верным, но галлюцинировала вспомогательная лемма. Они ссылались на функцию math::fact, которой нет в стандартной библиотеке Creusot. Доказательство работает только если вы построите это логическое определение самостоятельно.

Ни одна из моделей не выдала доказательство, прошедшее проверку с первого раза.

Где LLM реально помогают в рабочем процессе верификации

Это не значит, что LLM бесполезны для формальной верификации. Это значит, что их нужно использовать для правильных задач.

Они хорошо генерируют шаблонный код (boilerplate). Зная сигнатуру функции, LLM обычно может выдать пункты #[requires] и #[ensures], захватывающие очевидные контракты. Для функции fn divide(a: i32, b: i32) -> i32 он корректно предложит #[requires(b != 0)] и #[ensures(result * b == a)]. Это не глубокие озарения, но экономят нажатия клавиш.

Они сносно объясняют ошибки верификатора. Если Creusot сообщает «cannot prove loop invariant», вставка ошибки в LLM часто даёт полезное объяснение того, что должен делать инвариант. Он не предложит точный нужный инвариант, но сузит пространство поиска.

Они полезны для перевода между языками верификации. Если у вас есть доказательство в Dafny, и вы хотите портировать его в Prusti, LLM может взять на себя большую часть синтаксического отображения. Базовая логика одна и та же. Это именно тот вид задач на распознавание шаблонов, в которых LLM превосходны.

Фундаментальное ограничение: доказательство — это поиск, а не дополнение

Писать доказательство — не то же самое, что писать веб-сервер. Когда вы пишете веб-сервер, правильных ответов много. Когда вы пишете доказательство, правильный ответ ровно один, или небольшое семейство ответов, и всё остальное неверно.

LLM — предсказатели следующего токена. Они генерируют наиболее вероятное продолжение в данном контексте. Шаг доказательства — это не наиболее вероятное продолжение. Это шаг, который закрывает обязательство доказательства, который может быть двадцатым по вероятности или двухтысячным.

Представьте доказательство того, что функция сортировки возвращает перестановку своего входа. Ключевой инсайт обычно — определить мультимножество или подсчитать вхождения. LLM может предложить сравнивать длины, что необходимо, но недостаточно. Нужен человек, чтобы понять, что равенство длин не влечёт перестановку, и ввести инвариант подсчёта.

Model checking с Kani избегает части этого, потому что не требует инвариантов. LLM могут более надёжно генерировать kani::proof-harness-ы, потому что они выглядят как unit tests. Но Kani работает только для ограниченной верификации. Если нужно неограниченное доказательство, человек всё ещё необходим.

Практический рабочий процесс, использующий оба подхода

Если вы хотите верифицировать Rust сегодня, вот рабочий процесс, который реально работает.

Начните с написания кода как обычно. Запустите cargo test. Затем добавьте контракты. Используйте LLM для генерации пунктов #[requires] и #[ensures] из сигнатуры функции. Внимательно проверьте их. Модель верно справится с простыми и тонко ошибётся со сложными.

Запустите верификатор. Он потерпит неудачу хотя бы на одном цикле. Возьмите сообщение об ошибке и попросите LLM объяснить, какого инварианта не хватает. Используйте его объяснение как отправную точку, а не как ответ. Напишите инвариант сами.

Итерируйтесь. Верификатор скажет, достаточно ли силён ваш инвариант. LLM — нет. Воспринимайте модель как напарника по парному программированию, который знает синтаксис, но никогда не заканчивал доказательство.

Честный ответ на вопрос

Могут ли LLM писать формальные доказательства для Rust? Нет. Пока нет. Не без человека, который понимает логику.

Они могут писать каркас, объяснять ошибки и переводить между инструментами. Но нахождение инварианта, леммы или индукционной гипотезы, которая позволяет доказательству пройти, — это всё ещё человеческое умение.

Если вы ищете инструмент, позволяющий пропустить изучение separation logic или Hoare triples, LLM — не он. Если вы ищете инструмент, который делает кривую обучения менее крутой, беря на себя синтаксис и шаблонный код, пока вы сосредоточены на логике, LLM стоит попробовать.

Начните с Kani, если хотите ограниченные проверки без инвариантов. Переходите на Creusot или Prusti, когда нужны неограниченные доказательства. Используйте LLM, чтобы получить правильный синтаксис, но будьте готовы писать доказательство сами.

Часто задаваемые вопросы

Что такое формальная верификация в Rust?

Формальная верификация использует математическую логику для доказательства того, что программа удовлетворяет спецификации для всех возможных входных данных. В Rust инструменты вроде Kani, Prusti и Creusot добавляют к функциям аннотации, описывающие предусловия, постусловия и инварианты. Верификатор затем проверяет, выполняются ли эти свойства.

Может ли ChatGPT писать доказательства для Kani?

ChatGPT может писать Kani proof harness-ы, которые выглядят как unit tests с атрибутами #[kani::proof]. Эти harness-ы проще генерировать, чем дедуктивные доказательства, потому что они не требуют инвариантов циклов. Однако сложные harness-ы с предположениями и утверждениями всё ещё нуждаются в человеческой проверке.

В чём разница между Kani и Creusot?

Kani — bounded model checker. Он исследует все возможные пути выполнения в определённых границах и проверяет наличие panic или assertion failures. Creusot — дедуктивный верификатор. Он переводит Rust в логические формулы и использует SMT-solver для доказательства свойств для всех входов, включая неограниченные циклы, но требует инвариантов, предоставленных пользователем.

Почему LLM испытывают трудности с инвариантами циклов?

Инварианты циклов требуют рассуждений о том, что остаётся истинным на протяжении итераций, что является формой индуктивного рассуждения. LLM обучаются предсказывать вероятные продолжения текста, а не искать точное логическое утверждение, которое закрывает обязательство доказательства. Правильный инвариант часто не является наиболее вероятным следующим токеном.