Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

O artigo apresenta o Strat2Rocq, uma abordagem que extrai estratégias de prova de modelos de linguagem para formalizá-las como lemas no Rocq, aumentando assim a taxa de sucesso dos provadores simbólicos e dos agentes de prova baseados em LLM.

O essencial

Imagine que você tem um gênio matemático (o Modelo de Linguagem ou LLM) que é incrivelmente rápido, criativo e consegue resolver problemas complexos de lógica quase instantaneamente. No entanto, esse gênio tem dois grandes problemas:

1. Ele é caro de manter (precisa de supercomputadores).
2. Ele é inseguro para empresas que não podem revelar seus segredos industriais (códigos confidenciais) para uma nuvem externa.

Por outro lado, você tem um robô lógico (o Provedor Simbólico, como o CoqHammer). Ele é barato, roda no seu computador pessoal, é super seguro e não comete erros de "alucinação". Mas ele é lento e, às vezes, trava porque não consegue ver o "pulo do gato" para resolver um problema.

A pergunta que os autores deste trabalho fizeram foi: "E se pudéssemos pegar as 'dicas de estratégia' do gênio e ensinar o robô a usá-las, sem precisar que o gênio esteja lá na hora?"

A resposta é o Strat2Rocq.

A Metáfora: O Mestre e o Estagiário

Pense no Gênio (LLM) como um Mestre de Xadrez experiente e no Robô (Provedor Simbólico) como um estagiário muito inteligente, mas inexperiente.

1. O Problema: O estagiário tenta resolver um tabuleiro complexo, mas fica preso em movimentos óbvios e demorados. O Mestre, se estivesse lá, daria um conselho rápido: "Não pense em cada passo, lembre-se que neste cenário, a peça X sempre se move para o canto Y". Mas você não pode ter o Mestre no escritório o tempo todo (é caro e arriscado).

2. A Solução (Strat2Rocq):

   • Fase 1 (Aprendizado Offline): Você pede ao Mestre para resolver uma pilha de problemas antigos. Enquanto ele resolve, você observa como ele pensa. Você percebe que ele usa atalhos inteligentes. Em vez de copiar o Mestre para o escritório, você escreve um manual de regras (chamado de "Lemas") baseado nas estratégias que ele usou.
   • Fase 2 (O Trabalho Real): Agora, quando o estagiário (o Robô) recebe um novo problema, você entrega a ele esse manual de regras que você criou. O estagiário não precisa do Mestre ao lado. Ele apenas consulta o manual, vê o atalho que o Mestre usaria e resolve o problema sozinho, rápido e seguro.

Como funciona na prática?

O sistema faz isso em duas etapas principais:

• Mineração de Estratégias (Offline): O sistema usa o LLM para provar milhares de teoremas. Ele olha para a "pista" que o LLM deixou (a prova em linguagem natural) e transforma os "pulos de fé" inteligentes do LLM em regras formais e verificáveis. É como transformar a intuição do gênio em uma lei escrita.
• Prova Online: Quando chega um novo teorema para ser provado, o sistema pega essas regras novas e as entrega ao provedor simbólico (CoqHammer). O provedor, agora com esse "superpoder" extra, consegue resolver coisas que antes eram impossíveis para ele.

Os Resultados (O que aconteceu?)

Os autores testaram isso em projetos reais de software (como compiladores e sistemas operacionais verificados). O resultado foi impressionante:

• O Robô ficou 13,41% mais eficiente: Com as dicas do manual, o provedor simbólico conseguiu provar muito mais teoremas do que conseguia sozinho.
• Segurança e Custo: Como o LLM só é usado uma vez para criar o manual (offline), o processo final é barato e seguro. Você não precisa enviar dados confidenciais para a nuvem toda vez que quiser provar algo.
• Efeito Colateral Surpreendente: O manual também ajudou o próprio LLM a trabalhar melhor quando usado como um agente autônomo, provando que as regras extraídas são realmente úteis.

Resumo em uma frase

O Strat2Rocq é como um tradutor que pega a "intuição mágica" de uma inteligência artificial cara e a transforma em um "manual de instruções" barato e seguro, permitindo que computadores comuns resolvam problemas de lógica complexa com a mesma eficiência de um gênio, sem precisar que o gênio esteja presente.

Resumo técnico

Título: Extração de Estratégia de Prova de LLMs para Aprimorar Provedores Simbólicos

Autores: Jian Fang, Yican Sun e Yingfei Xiong (Universidade de Pequim, China).

---

1. Problema e Motivação

A verificação de software, particularmente através de Prova de Teoremas Interativa (ITP), é crucial para garantir a segurança de sistemas críticos. No entanto, a escrita de provas formais exige um esforço humano substancial (ex: no kernel seL4, o esforço de prova é 10x maior que a implementação do código).

Embora os Grandes Modelos de Linguagem (LLMs) tenham demonstrado capacidades notáveis na automação de provas, eles apresentam limitações significativas para o uso em ambientes de produção:

• Custo Computacional: Requerem recursos intensivos, inviáveis para empresas menores.
• Segurança: O envio de códigos proprietários para serviços externos de LLMs representa riscos de vazamento de dados confidenciais.
• Dependência: Provedores puramente simbólicos (como o CoqHammer no ecossistema Rocq/Coq) permanecem essenciais por serem seguros, baratos e executáveis localmente, mas muitas vezes têm desempenho inferior ao dos agentes híbridos (LLM + Provedor).

Questão de Pesquisa: É possível extrair as estratégias de prova internas dos LLMs e convertê-las em um formato que aprimore a capacidade dos provedores simbólicos, mantendo a segurança e a eficiência?

---

2. Metodologia: O Framework Strat2Rocq

Os autores propõem o Strat2Rocq, um framework que opera em duas etapas distintas: uma fase offline (mineração) e uma fase online (prova). O objetivo é transformar o conhecimento tácito do LLM em lemas formais verificáveis no Rocq.

Fase 1: Mineração de Lemas Offline

Nesta etapa, o sistema extrai estratégias de um conjunto de treinamento (teoremas existentes) sem envolver o LLM durante a prova do usuário final.

1. Geração de Prova em Linguagem Natural (NL): Para cada teorema do conjunto de treinamento, um LLM é solicitado a gerar uma prova passo a passo em linguagem natural. Isso é feito porque os LLMs tendem a raciocinar melhor em NL do que em código formal direto, e a prova em NL reflete melhor o processo de raciocínio interno.
   • Prompt: Inclui definições de tipos, funções e o contexto do script atual.
2. Generalização e Formalização: O LLM é solicitado a:
   • Generalizar os passos da prova em NL para criar lemas gerais (estratégias reutilizáveis).
   • Formalizar esses lemas e suas provas no Rocq.
3. Agente de Reparo: Como a autoformalização é propensa a erros, um agente de prova iterativo é utilizado. Ele tenta compilar e provar os lemas gerados; se falhar, usa um módulo de reparo baseado em LLM para corrigir erros específicos até que o lema seja válido ou o limite de tentativas seja atingido.

Fase 2: Prova de Teoremas Online

Uma vez extraídos e validados os lemas:

1. Inserção no Contexto: Ao tentar provar um novo teorema pelo usuário, os lemas extraídos são inseridos no contexto de prova.
2. Prova Simbólica Pura: O provedor simbólico (CoqHammer) utiliza esses novos lemas como conhecimento prévio.
   • Diferencial: Diferente de agentes híbridos que chamam o LLM em tempo real, aqui o LLM não é consultado durante a prova do usuário. O sistema é puramente simbólico, mas "instruído" com o conhecimento distilado do LLM.

---

3. Contribuições Principais

1. Novo Problema de Pesquisa: Propõe a extração offline de estratégias de prova de LLMs para enriquecer provedores simbólicos, evitando a dependência online de LLMs.
2. Abordagem de Extração: Desenvolveu um método para analisar provas em linguagem natural geradas por LLMs, generalizá-las e formalizá-las como lemas reutilizáveis.
3. Implementação e Validação: Implementou o Strat2Rocq no ecossistema Rocq (Coq) e validou empiricamente sua eficácia em projetos de verificação de software de código aberto.

---

4. Resultados Experimentais

O sistema foi avaliado em um conjunto de dados de 2.394 teoremas provenientes de projetos como CompCert, Coq-Art, Ext-Lib e Vfa.

• Eficácia na Extração (RQ1): O Strat2Rocq conseguiu extrair, em média, 1,91 novos lemas para cada teorema original do conjunto de treinamento, demonstrando capacidade de capturar estratégias internas dos LLMs.
• Melhoria no Provedor Simbólico (RQ2):
  • A taxa de sucesso do CoqHammer aumentou em 13,41% em média ao utilizar os lemas extraídos.
  • Em projetos específicos como CompCert (um compilador C certificado), a melhoria foi de 17,75%.
  • Mecanismo de Melhoria: Os lemas extraídos permitiram que o provedor simbólico evitasse a necessidade de indução (um ponto fraco do CoqHammer) e melhoraram a seleção de lemas relevantes, permitindo provar teoremas que antes falhavam.
• Generalização (RQ3): O método funcionou bem com diferentes LLMs de back-end (Claude 3.7 Sonnet e o3-mini), e a combinação de lemas de ambos os modelos resultou em ainda mais teoremas provados, indicando que as estratégias são complementares.
• Impacto em Agentes LLM (RQ5): Curiosamente, os lemas extraídos também beneficiaram agentes de prova baseados em LLM (com aumento de 4,00% na taxa de sucesso), reduzindo o consumo de tokens ao permitir que o CoqHammer resolva mais teoremas independentemente.
• Ablação (RQ4): A etapa de geração de prova em linguagem natural foi crucial. Removê-la e pedir formalização direta resultou em uma queda de 63,56% no número de lemas extraídos e 6,21% na performance final.

---

5. Significado e Conclusão

O trabalho demonstra que é possível distilar o conhecimento de LLMs para sistemas simbólicos tradicionais, criando um híbrido que mantém a segurança e a eficiência dos provedores simbólicos (executáveis localmente, sem vazamento de dados) enquanto incorpora a inteligência heurística dos LLMs.

• Segurança e Custo: Permite que empresas com orçamentos limitados ou dados confidenciais utilizem o "cérebro" dos LLMs sem depender de chamadas de API em tempo real.
• Interpretabilidade: O trabalho oferece uma nova perspectiva sobre como os LLMs realizam provas formais. Ao converter suas estratégias em lemas simbólicos verificáveis, os autores criam um modelo simbólico aproximado do comportamento do LLM, ajudando a responder a questões fundamentais sobre o funcionamento interno desses modelos.

Em suma, o Strat2Rocq fecha a lacuna entre a flexibilidade dos LLMs e a robustez dos provadores formais, elevando o estado da arte na automação de provas em verificação de software.