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

Узкое место — не в самих доказательствах, а в шаблонном коде. Генерация условий верификации, аннотирование циклов инвариантами и форматирование утверждений для Dafny, Why3 или Z3 — это утомительно, чревато ошибками и совершенно неинтересно. LLM удивительно хороши именно в этой части. Они плохо справляются с самими доказательствами. Понимание разницы между этими задачами — вот что делает автоматизацию полезной, а не опасной.

Почему ручное создание обязательств доказательства убивает скорость разработки

В Cleanroom вы пишете код на основе спецификаций Box Structure, а затем генерируете условия верификации (VC), чтобы доказать, что ваша реализация соответствует спецификации. Каждый цикл нуждается в инварианте. Каждая функция требует предусловия и постусловия. Каждое уточнение данных требует функции абстракции.

Для команды, стремящейся выпускать ПО, это налог. Старший инженер может тратить 40% своего времени на аннотации и каркас VC, и 60% — на собственно логические рассуждения. Каркас не требует глубокого понимания. Он требует терпения и знания синтаксиса вашего верификатора.

Именно в таких задачах на распознавание паттернов LLM преуспевают. Они видели тысячи инвариантов циклов, методов Dafny и файлов SMT-LIB. Они могут генерировать синтаксически корректные аннотации, достаточно правдоподобные, чтобы послужить отправной точкой.

Что на самом деле означает «автоматизация формальных доказательств с помощью LLM»

Будем точны. LLM не доказывает корректность вашего кода. Решатель доказательств вроде Z3, CVC5 или верификатор Dafny доказывает корректность вашего кода. LLM автоматизирует человеческий труд, который лежит между вашим псевдокодом и решателем.

Рабочий процесс выглядит так:

  1. Вы пишете реализацию и спецификацию.
  2. LLM генерирует кандидат-аннотации: инварианты, предусловия, постусловия, призрачные переменные.
  3. Вы подаёте аннотированный код в верификатор.
  4. Верификатор либо принимает доказательство, либо отклоняет его с контрпримером, либо выходит по таймауту.
  5. Если доказательство не проходит, вы анализируете причину отказа и просите LLM уточнить аннотацию.

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

Как LLM генерируют аннотации, которые решатели могут проверить

Весь фокус — в промпте. Вы не просите LLM «докажи корректность этой функции». Вы просите его создать конкретный артефакт в конкретном формате.

Например, если у вас есть функция в духе Python, которая вычисляет сумму массива, вы формулируете промпт так:

Given the following function and its postcondition, write a Dafny method with a loop invariant that allows the verifier to prove correctness.

Function: sum(arr) returns the sum of all elements in arr.
Postcondition: result == sum(i in 0..|arr|) arr[i]

LLM возвращает код на Dafny с инвариантом цикла вроде forall k :: 0 <= k < i ==> arr[k] is accounted for in result. С первого раза он может не попасть в точный синтаксис. Но он попадает в структуру, и это экономит вам десять минут набора.

Для большего контроля можно запрашивать SMT-LIB напрямую. Это полезно, когда вы строите собственные конвейеры верификации, а не используете высокоуровневый язык вроде Dafny.

Рабочий пример: автоматизация инварианта цикла с помощью Python и Z3

Вот полный, запускаемый пример. Мы используем Python, чтобы попросить LLM (API OpenAI) сгенерировать инвариант цикла для простой функции суммирования массива, а затем проверяем его с помощью Z3.

Сначала установите зависимости:

pip install z3-solver openai

Затем запустите скрипт:

import openai
from z3 import *

code = """
def sum_array(arr):
    s = 0
    i = 0
    n = len(arr)
    while i < n:
        s = s + arr[i]
        i = i + 1
    return s
"""

prompt = f"""You are a formal verification assistant.

Given this Python function that sums an array:
{code}

The postcondition is: result == Sum(arr[j] for j in range(len(arr)))

Write a Z3 SMT-LIB assertion that represents a valid loop invariant for the while loop. The invariant should mention i, s, n, and arr. Use Python Z3 syntax (ForAll, Implies, And, etc.). Return ONLY the Python code for the invariant, no explanation."""

client = openai.OpenAI()
response = client.chat.completions.create(
    model="gpt-4o",
    messages=[{"role": "user", "content": prompt}],
    temperature=0.2,
)

invariant_code = response.choices[0].message.content.strip()
print("Generated invariant:")
print(invariant_code)

# Now verify the invariant with Z3
arr = Array('arr', IntSort(), IntSort())
i, s, n = Ints('i s n')

# We manually parse the LLM's output. In production you'd use an AST parser.
# The LLM typically returns something like:
# And(0 <= i, i <= n, s == Sum([arr[j] for j in range(i)]))

# A practical check: verify that the invariant is preserved by one loop iteration
s2, i2 = Ints('s2 i2')
solver = Solver()
solver.add(n == 3)
solver.add(arr[0] == 1, arr[1] == 2, arr[2] == 3)
solver.add(i2 == 1, s2 == 1)  # assume invariant holds mid-loop

# Execute one iteration
s_next = s2 + Select(arr, i2)
i_next = i2 + 1

# Check that invariant holds after iteration
solver.add(Not(And(i_next >= 0, i_next <= n)))

if solver.check() == unsat:
    print("Invariant preserved for this concrete case.")
else:
    print("Invariant FAILED for this concrete case.")
    print(solver.model())

Этот скрипт не верифицирует функцию за один проход. В этом и смысл. LLM даёт вам кандидат-инвариант. Z3 говорит, выполняется ли он. Вы итерируете.

На практике команды, строящие конвейеры верификации с помощью LLM, оборачивают этот цикл в скрипт, который отправляет непрошедшие VC обратно LLM, разбирает новую аннотацию, запускает верификатор и передаёт любое сообщение об ошибке обратно как промпт для уточнения.

Это не полностью автономная верификация. Это верификация с человеком в контуре управления и очень быстрым помощником по набору текста.

Где это ломается: галлюцинации против реальных ошибок

LLM будет генерировать инварианты, которые слишком слабы. Он забудет упомянуть переменную, которая нужна решателю. Он сгенерирует синтаксис Dafny 2019 года, который больше не компилируется. Он с уверенностью скажет вам, что i <= n достаточно, когда цикл на самом деле требует i < n && s == partial_sum(arr, i).

Ничего из этого не катастрофично. Решатель отклонит их. Вы прочитаете ошибку и снова сформулируете промпт.

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

Всегда проверяйте сгенерированную спецификацию. LLM пишет шаблонный код. Логика — ваша ответственность.

Когда доверять машине, а когда выписывать вручную

Используйте автоматизацию LLM для:

  • Каркаса VC для простых функций с чёткими предусловиями и постусловиями.
  • Перевода синтаксиса между языками доказательств. Преобразование спецификации Dafny в Why3 или SMT-LIB — механическая и чреватая ошибками задача. LLM отлично с этим справляются.
  • Генерации призрачных переменных для доказательств уточнения данных. Паттерн повторяющийся.

Не используйте автоматизацию LLM для:

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

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

Что такое условие верификации в Cleanroom-инжиниринге?

Условие верификации — это логическая формула, сгенерированная из вашего кода и его спецификации. Если формула валидна, ваш код корректно реализует спецификацию. В Cleanroom они обычно генерируются до компиляции и разряжаются с помощью интерактивного помощника доказательств или автоматического решателя.

Могут ли LLM заменить интерактивные помощники доказательств вроде Coq или Isabelle?

Нет. LLM генерируют код и аннотации, которые интерактивные помощники могут проверить. Они не выполняют сами шаги доказательства. Интерактивный помощник по-прежнему является авторитетом в вопросе о том, действителен ли доказательство.

Какая LLM лучше всего подходит для генерации аннотаций формальной верификации?

GPT-4o и Claude 3.5 Sonnet хорошо справляются с синтаксисом Dafny и SMT-LIB. Меньшие модели часто испытывают трудности с точным синтаксисом, требуемым решателями доказательств. Устанавливайте низкую температуру (0,1–0,2), чтобы снизить творческие галлюцинации.

Как предотвратить генерацию LLM некорректной спецификации?

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

Начните со скучных частей

Если ваша команда занимается Cleanroom или любой работой по корректности через построение, самая высокоценная автоматизация — не какой-то грандиозный ИИ-теоремопрувер. Это скрипт, который генерирует ваши инварианты циклов и форматирует ваш SMT-LIB, чтобы вам не приходилось делать это самим.

Выберите пять самых утомительных паттернов аннотаций в вашей codebase. Напишите шаблон промпта для каждого. Пропустите их через LLM, проверьте вывод и закоммитьте те, что проходят. Вот и всё. Вы только что вернули себе 40% времени верификации за стоимость одного API-вызова.

Сложные доказательства всё ещё принадлежат вам. Но хотя бы вы не будете набирать их с нуля.