A lacuna entre código correto e um programa verificado

LLMs conseguem escrever Rust que compila e até passa em cargo test. O que não conseguem fazer de forma confiável é escrever uma prova formal de que o código está correto para todas as entradas possíveis.

O problema não é a sintaxe de Rust. A verificação formal exige declarar o que você quer provar, encontrar a invariante que faz a prova funcionar, e expressar ambos em uma linguagem que o verificador aceite. LLMs são treinados em código-fonte, não no ato de provar. Eles veem teoremas, mas raramente veem as vinte tentativas fracassadas que precederam a prova bem-sucedida.

Se você colar uma busca binária recursiva no GPT-4 e pedir para “provar que isso está correto”, receberá algo que parece uma prova. Mencionará invariantes de loop e pré-condições. Também provavelmente usará sintaxe de Dafny, referenciará lemas que não existem, e afirmará invariantes que são fracas demais para estabelecer a pós-condição. Parece certo até você tentar verificá-lo.

Como a verificação formal de Rust realmente se parece

Rust tem várias ferramentas de verificação. Kani é um model checker que explora exaustivamente todos os estados possíveis de uma função até certo limite. Prusti e Creusot são verificadores dedutivos que traduzem Rust para lógica e pedem a um SMT solver que prove propriedades. Cada um exige anotações em uma sintaxe específica.

Aqui está uma função simples e como uma prova dedutiva real se parece em 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 verifica que a pré-condição a.len() > 0 garante a pós-condição result == a[0]. Isso é trivial porque a lógica é simples. Agora vamos dificultar:

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
}

As invariantes são a parte difícil. Um humano as escreve pensando no que permanece verdadeiro a cada iteração. Um LLM pode chutar s == i * (i - 1) / 2 porque esse padrão aparece nos dados de treinamento, ou pode omitir a invariante inteiramente e deixar o solver falhar.

O que acontece quando você pede uma prova a um LLM

Testei isso com vários modelos. O prompt foi: “Escreva uma função Rust verificada que calcula o fatorial de n usando Creusot, com pré-condições, pós-condições e invariantes de loop completas.”

As respostas caíram em três categorias.

Primeiro, alguns modelos produziram anotações plausíveis que usavam a sintaxe errada. Eles escreveram #[precondition(...)] em vez de #[requires(...)], ou misturaram sintaxe de Prusti com sintaxe de Creusot. O código nem sequer fazia o parsing.

Segundo, alguns modelos produziram anotações sintaticamente corretas com invariantes que eram fracas demais. A função fatorial precisa de uma invariante como res == fact(i). Os modelos frequentemente escreveram res >= i, que é verdadeiro mas inútil para provar a pós-condição. Creusot relataria que não conseguia estabelecer o objetivo, e o LLM não tinha mecanismo para corrigir isso.

Terceiro, algumas respostas acertaram a invariante mas alucinaram um lema auxiliar. Elas referenciavam uma função math::fact que não existe na biblioteca padrão de Creusot. A prova só funciona se você construir aquela definição lógica você mesmo.

Nenhum dos modelos produziu uma prova que passasse na primeira tentativa.

Onde os LLMs realmente ajudam no fluxo de verificação

Isso não significa que LLMs são inúteis para verificação formal. Significa que você deve usá-los para as tarefas certas.

Eles são bons em gerar boilerplate. Dada uma assinatura de função, um LLM geralmente consegue produzir as cláusulas #[requires] e #[ensures] que capturam os contratos óbvios. Para uma função fn divide(a: i32, b: i32) -> i32, ele corretamente sugerirá #[requires(b != 0)] e #[ensures(result * b == a)]. Isso não são insights profundos, mas economizam digitação.

Eles são razoáveis em explicar erros do verificador. Se Creusot reportar “cannot prove loop invariant”, colar o erro em um LLM frequentemente produz uma explicação útil do que a invariante deveria fazer. Não sugerirá a invariante exata que você precisa, mas reduzirá o espaço de busca.

Eles são úteis para traduzir entre linguagens de verificação. Se você tem uma prova em Dafny e quer portá-la para Prusti, um LLM pode lidar com grande parte do mapeamento sintático. A lógica subjacente é a mesma. Esse é exatamente o tipo de tarefa de reconhecimento de padrões em que LLMs se destacam.

A limitação fundamental: provar é busca, não completude

Escrever uma prova não é como escrever um servidor web. Quando você escreve um servidor web, há muitas respostas corretas. Quando você escreve uma prova, há exatamente uma resposta, ou uma pequena família de respostas, e todo o resto está errado.

LLMs são preditores de próximo token. Eles geram a continuação mais provável dado o contexto. Um passo de prova não é a continuação mais provável. É o passo que fecha a obrigação de prova, que pode ser a vigésima opção mais provável ou a duas-milésima.

Considere provar que uma função de ordenação retorna uma permutação de sua entrada. A ideia chave geralmente é definir um multiset ou contar ocorrências. Um LLM pode sugerir comparar comprimentos, que é necessário mas não suficiente. É preciso um humano para reconhecer que igualdade de comprimentos não implica permutação, e introduzir a invariante de contagem.

Model checking com Kani evita parte disso porque não requer invariantes. LLMs conseguem gerar harnesses kani::proof de forma mais confiável porque parecem unit tests. Mas Kani só funciona para verificação limitada. Se você precisa de uma prova ilimitada, ainda precisa do humano.

Um fluxo de trabalho prático que usa ambos

Se você quer verificar Rust hoje, aqui está um fluxo de trabalho que realmente funciona.

Comece escrevendo o código normalmente. Execute cargo test. Depois adicione contratos. Use um LLM para gerar as cláusulas #[requires] e #[ensures] a partir da assinatura da função. Revise-as cuidadosamente. O modelo acertará as fáceis e errará sutilmente as difíceis.

Execute o verificador. Ele falhará em pelo menos um loop. Pegue a mensagem de erro e peça ao LLM para explicar qual invariante está faltando. Use sua explicação como ponto de partida, não como resposta. Escreva a invariante você mesmo.

Itere. O verificador lhe dirá se sua invariante é forte o suficiente. O LLM não fará isso. Trate o modelo como um programador par que conhece a sintaxe mas nunca terminou uma prova.

A resposta honesta para a pergunta

LLMs conseguem escrever provas formais para Rust? Não. Ainda não. Não sem um humano que entenda a lógica.

Eles conseguem escrever o scaffolding, explicar erros e traduzir entre ferramentas. Mas encontrar a invariante, o lema ou a hipótese de indução que faz a prova funcionar ainda é uma habilidade humana.

Se você está procurando uma ferramenta que permita pular o aprendizado de separation logic ou Hoare triples, um LLM não é isso. Se você está procurando uma ferramenta que torna a curva de aprendizado menos íngreme lidando com a sintaxe e o boilerplate enquanto você foca na lógica, um LLM vale a pena tentar.

Comece com Kani se você quer verificações limitadas sem invariantes. Mude para Creusot ou Prusti quando precisar de provas ilimitadas. Use o LLM para acertar a sintaxe, mas espere escrever a prova você mesmo.

Perguntas frequentes

O que é verificação formal em Rust?

A verificação formal usa lógica matemática para provar que um programa satisfaz uma especificação para todas as entradas possíveis. Em Rust, ferramentas como Kani, Prusti e Creusot adicionam anotações às funções que descrevem pré-condições, pós-condições e invariantes. Um verificador então checa se essas propriedades valem.

ChatGPT consegue escrever provas para Kani?

ChatGPT consegue escrever harnesses de prova Kani, que parecem unit tests com atributos #[kani::proof]. Esses harnesses são mais fáceis de gerar do que provas dedutivas porque não requerem invariantes de loop. No entanto, harnesses complexos com assumptions e assertions ainda precisam de revisão humana.

Qual é a diferença entre Kani e Creusot?

Kani é um bounded model checker. Ele explora todos os caminhos de execução possíveis até um limite e checa por panics ou falhas de assertion. Creusot é um verificador dedutivo. Ele traduz Rust para fórmulas lógicas e usa um SMT solver para provar propriedades para todas as entradas, incluindo loops ilimitados, mas requer invariantes fornecidas pelo usuário.

Por que LLMs têm dificuldade com invariantes de loop?

Invariantes de loop exigem raciocinar sobre o que permanece verdadeiro através de iterações, o que é uma forma de raciocínio indutivo. LLMs são treinados para prever continuações de texto prováveis, não para buscar a declaração lógica exata que fecha uma obrigação de prova. A invariante correta frequentemente não é o próximo token mais provável.