Resumo Técnico: BlueprintRepair: Edições Locais Tipadas para Blueprints de Provas Lean Falhas

Declaração do Problema

Os modernos provadores de teoremas baseados em LLM para Lean utilizam cada vez mais blueprints: grafos de dependência estruturados onde os nós representam enunciados formais e as arestas representam dependências de prova. Embora esses sistemas consigam gerar planos de prova, eles frequentemente encontram falhas. Essas falhas manifestam-se tipicamente como:

1. Defeitos Localizados no Grafo: Enunciados incorretos, dependências ausentes ou redundantes, ou lemas intermediários falsos dentro de uma estrutura de grafo que, de outra forma, estaria correta.
2. Falhas de Autoria de Prova: A estrutura do grafo está correta, mas o provador falha em gerar o conteúdo da prova necessário para um nó específico.
3. Falhas Compostas: Uma combinação de defeitos interligados.

As estratégias de reparo tradicionais envolvem frequentemente a regeneração de arquivos inteiros ou o uso de geração de texto livre para aplicar patches no código. Este artigo investiga se edições locais tipadas e com verificação de esquema no grafo do blueprint são suficientes para o reparo, e como elas se comparam às alternativas de texto livre em termos de cobertura, eficiência e custo. Um desafio crítico identificado é que um reparo de prova pode compilar com sucesso enquanto viola as dependências declaradas pelo blueprint (por exemplo, usando um lema não declarado), tornando o blueprint incorreto mesmo que o teorema alvo seja provado.

Metodologia

A Interface BLUEPRINTREPAIR

Os autores propõem a BLUEPRINTREPAIR, uma interface de reparo que restringe o modelo a um conjunto de dez operações locais com verificação de esquema. Estas operações permitem ao modelo:

• Modificar Enunciados: Enfraquecer um nó, fortalecer hipóteses ou reescrever um enunciado.
• Alterar a Estrutura do Grafo: Dividir um nó, adicionar uma dependência ou remover uma dependência.
• Remover Nós: Eliminar nós falsos ou nós mortos (não utilizados).
• Escrever Provas: Fornecer o conteúdo da prova para um nó específico.
• Terminar: Parar se o estado for considerado irreparável.

Crucialmente, o enunciado do teorema alvo não pode ser alterado por estas operações. Cada operação é aplicada mecanicamente por um harness, que executa então o compilador Lean e um provador de nós fixo.

Critério de Aceitação Consciente do Grafo

Uma contribuição inovadora é o critério de aceitação. Um módulo reparado é aceito apenas se:

1. O módulo completo elabora (compila).
2. Cada nó no fechamento alvo é provado.
3. O enunciado alvo permanece inalterado.
4. Consistência de Dependência: Os termos de prova compilados não devem usar nenhum lema do blueprint que não esteja explicitamente declarado nas arestas de dependência do grafo. O sistema extrai Actual(v) (lemas usados na prova do nó v) e verifica se Actual(v) ⊆ Declared(v).

Benchmark: BLUEPRINTTRACE

Os autores construíram o BLUEPRINTTRACE, um benchmark de 142 estados de falha controlados derivados de 141 teoremas distintos do miniF2F.

• Construção: Partindo de blueprints corretos, construídos por autores, defeitos específicos foram injetados (ex: remover uma hipótese, adicionar um lema falso, remover uma dependência).
• Estratos: O conjunto de dados inclui 91 falhas de "forma de edição" (defeitos localizados), 39 falhas de "autoria de prova" (grafo intacto, prova ausente) e 12 estados "compostos".
• Dados: O artefato inclui trajetórias completas de ações aceitas e rejeitadas, feedback do Lean, uso de tokens e registros de custo.

Protocolo Experimental

O estudo compara três interfaces de reparo sob condições equivalentes (mesma origem, feedback, modelo e orçamento):

1. Reparo Tipado: As operações locais com verificação de esquema propostas.
2. Patching Local: Blocos de busca e substituição exata de texto livre aplicados à fonte.
3. Reescrita de Módulo: Geração de texto livre do módulo completo.

Os experimentos foram conduzidos utilizando DeepSeek-V4-Flash e Qwen3.6-Flash, com um orçamento de até 8 passos (12 para estados compostos) por tarefa.

Resultados Principais

Cobertura

• Falhas de Forma de Edição: Nas 91 falhas localizadas, o Reparo Tipado resolveu 79 estados com o DeepSeek-V4-Flash, comparado a 81 para ambos o Patching e a Reescrita. As diferenças foram estatisticamente insignificantes (McNemar p = 0,63).
• Falhas de Autoria de Prova: O Patching liderou com 18 resoluções, seguido pelo Reparo Tipado (16) e pela Reescrita (13).
• Estados Compostos: O Patching e a Reescrita resolveram 10 de 12 estados, enquanto o Reparo Tipado resolveu 9.
• Cobertura Total: O Patching alcançou o total mais alto (109/142), com o Reparo Tipado e a Reescrita empatados em 104/142. As três interfaces combinadas resolveram 118 estados, indicando que cada interface captura um subconjunto único de falhas.

Eficiência e Custo

• Eficiência de Tokens: O reparo tipado atingiu quase a sua cobertura final (103/104 resoluções) dentro de 10.000 tokens de conclusão por tarefa. Em contraste, o Patching atingiu 90 resoluções e a Reescrita 87 resoluções com o mesmo orçamento de tokens. O Patching só ultrapassou o Reparo Tipado após ~34.000 tokens.
• Custo: O reparo tipado foi o mais custo-efetivo. Em relação ao Reparo Tipado, o Patching foi 1,30× mais caro, e a Reescrita foi 2,06× mais cara (DeepSeek-V4-Flash).
• Segundo Modelo: O Qwen3.6-Flash resolveu menos estados no total, mas manteve a mesma ordem de eficiência, sendo o Reparo Tipado o mais barato por resolução.

Controle e Comportamento

• Segurança do Alvo: As operações tipadas impedem alterações no enunciado alvo por design (recusadas antes da aplicação). As interfaces de texto livre (Patching/Reescrita) são verificadas após a geração; a Reescrita falhou 12 vezes ao alterar a assinatura do alvo.
• Alcance: Os autores demonstraram que os 11 estados resolvidos pelo Patching, mas não pelo Reparo Tipado, poderiam ser expressos usando as operações tipadas (exigindo até 6 chamadas). Isso sugere que a lacuna reside na seleção de ações pelo modelo, e não na expressividade da interface.

Significância e Alegações

O artigo afirma que para blueprints majoritariamente corretos com defeitos localizados, o reparo tipado local é uma estratégia de reparo altamente eficiente.

• Custo-Eficiência: O reparo tipado recupera a maior parte da cobertura alcançável com o menor custo de tokens e financeiro, atingindo o seu platô muito mais rápido do que a geração de texto livre.
• Integridade do Grafo: A interface com verificação de esquema e o invariante Actual ⊆ Declared garantem que os reparos de prova permaneçam consistentes com a estrutura do blueprint, evitando erros de dependência "silenciosos".
• Design de Sistema: Os resultados apoiam uma visão de sistemas híbridos: utilizar edições locais tipadas para a maior parte do reparo (baixo custo, alta velocidade) e reservar a geração de texto livre para os casos restantes, mais difíceis, onde a própria estrutura do grafo pode precisar de uma reformulação mais radical.

Os autores enfatizam que este é um benchmark de diagnóstico controlado. Embora as edições tipadas funcionem bem em defeitos localizados, o artigo não afirma que sejam superiores para falhas de formalização arbitrárias de grande escala ou que o conjunto específico de dez operações seja exaustivo. O trabalho fornece um conjunto de dados de trajetória (BLUEPRINTTRACE) para permitir pesquisas futuras sobre melhores políticas de reparo utilizando edições estruturais bem-sucedidas e rejeitadas.