Twitch: Learning Abstractions for Equational Theorem Proving

O artigo apresenta o Twitch, uma ferramenta que descobre automaticamente abstrações (padrões de termos recorrentes) a partir de provas parciais ou bem-sucedidas para auxiliar o provador de teoremas equacionais Twee, resultando na prova de problemas de dificuldade rating-1 e em acelerações significativas em outros.

O essencial

Imagine que você está tentando resolver um quebra-cabeça gigante e complexo, como um labirinto sem fim. Você tem um robô muito inteligente (o provador de teoremas) que pode encontrar a saída, mas ele tem um problema: ele é muito inteligente, mas também muito distraído.

Ele tenta milhões de caminhos diferentes. A maioria deles são becos sem saída, mas ele gasta tempo e energia explorando cada um deles antes de perceber que não leva a lugar nenhum. O robô sabe que precisa ser rápido, então ele usa regras simples: "Escolha o caminho mais curto" ou "Escolha o caminho com menos curvas". Mas, às vezes, o caminho mais curto não é o que leva à saída; o caminho certo tem uma curva específica que o robô ignora porque parece "estranho" no início.

Aqui entra o Twitch, a ferramenta apresentada neste artigo.

O Problema: O Robô Perdido

Pense no robô (chamado Twee) como um explorador em uma floresta densa. Ele precisa provar uma matemática difícil. Ele gera milhões de "pistas" (equações) para seguir. A maioria é inútil. O robô precisa de ajuda para saber quais pistas são importantes. Normalmente, um humano teria que apontar: "Ei, preste atenção em formas de árvore que se parecem com isso aqui!". Mas humanos são lentos e não podem estar em todos os lugares.

A Solução: O "Twitch" e o "Stitch"

Os autores criaram um sistema chamado Twitch que ensina o robô a aprender sozinho quais formas são importantes. Para fazer isso, eles usam uma ferramenta chamada Stitch (que significa "ponto de costura" em inglês).

A Analogia da Costura:
Imagine que você tem um monte de roupas velhas e cheias de manchas. Se você tentar lavar cada peça individualmente, vai gastar muita água e sabão. Mas, se você notar que todas as manchas têm o mesmo formato, você pode criar um "molde" especial para limpar apenas aquele formato.

O Stitch faz exatamente isso com as provas matemáticas:

1. Ele olha para provas que já foram resolvidas (ou tentativas falhas de provar algo difícil).
2. Ele procura por padrões que se repetem muito. "Olha, essa forma de equação aparece 50 vezes aqui!"
3. Ele cria um molde (uma abstração) para essa forma. Em vez de escrever a equação longa e complicada toda vez, ele diz: "Vamos chamar essa parte complicada de 'X'".

Isso é como criar uma atalho mental. Em vez de o robô pensar "Vou resolver essa equação gigante", ele pensa "Vou resolver o 'X'". Isso torna o processo muito mais rápido.

Como o Twitch Aprende?

O Twitch tem duas maneiras de aprender esses "moldes":

1. Aprendendo com o Fracasso (Abstrações de Prova Parcial):
   Imagine que o robô tentou resolver um problema difícil e falhou depois de 5 minutos. Ele não desistiu; ele deixou um rastro de "pistas" (equações) no chão. O Twitch olha para esse rastro, encontra os padrões mais interessantes que apareceram durante a tentativa e cria moldes a partir deles. Depois, ele dá esses moldes ao robô e diz: "Tente de novo, mas preste atenção nessas formas". Muitas vezes, o robô consegue resolver o problema agora!

2. Aprendendo com os "Irmãos" (Abstrações de Domínio):
   Imagine que você está tentando resolver um problema de Lógica. O Twitch olha para outros problemas de Lógica que já foram resolvidos com sucesso. Ele diz: "Olha, em todos esses problemas de Lógica, as pessoas sempre usam essa mesma estrutura de pensamento. Vamos criar um molde para isso e usar no problema difícil que você tem agora". É como um aluno que estuda exercícios fáceis de uma matéria para aprender as dicas que vão ajudar a resolver a prova difícil.

O Resultado: Mais Rápido e Mais Inteligente

Quando os autores testaram isso, o robô ficou muito mais eficiente:

• Velocidade: Ele resolveu problemas 10 vezes mais rápido em alguns casos.
• Sucesso: Ele conseguiu resolver 12 problemas que eram considerados "impossíveis" ou muito difíceis para ele antes (problemas com nota 1, os mais difíceis).
• Inteligência: O robô não apenas ficou mais rápido; ele começou a "pensar" de forma mais estruturada, focando nas partes da equação que realmente importam, ignorando o ruído.

Resumo em uma Frase

O Twitch é como um professor particular que olha para os erros e acertos passados de um aluno, descobre quais "atalhos" funcionam melhor, e ensina o aluno a usar esses atalhos para resolver problemas novos e difíceis muito mais rápido, sem precisar de um humano apontando o caminho o tempo todo.

É uma forma de ensinar a máquina a reconhecer padrões e criar atalhos sozinha, transformando um processo de tentativa e erro cego em uma busca inteligente e direcionada.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "Twitch: Learning Abstractions for Equational Theorem Proving", apresentado em português:

1. O Problema

Os provadores de teoremas automatizados baseados em saturação (como o Twee, um provador de teoremas equacionais) enfrentam um espaço de busca massivo. Eles geram milhões de "pares críticos" (inferências possíveis), mas apenas uma fração mínima é útil para a prova final.

• Desafio: Identificar quais pares críticos são "interessantes" rapidamente. As heurísticas atuais do Twee são simples e baseadas principalmente no tamanho (peso) do par crítico.
• Limitação das abordagens existentes: Estratégias que usam orientação humana (como a estratégia de resonance ou hint) exigem que o usuário especifique manualmente quais formas de termos ou cláusulas são importantes. Isso é trabalhoso e não escala bem para domínios desconhecidos.
• Objetivo: Descobrir automaticamente "formas de termos interessantes" (padrões recorrentes) que aparecem em provas relevantes e usá-los para guiar a busca, sem intervenção humana direta.

2. Metodologia

O artigo apresenta o Twitch, uma ferramenta que descobre automaticamente abstrações (padrões de termos que ocorrem repetidamente) e integra essas abstrações ao provador Twee. O sistema utiliza uma ferramenta chamada Stitch, originalmente desenvolvida para síntese de programas, para comprimir conjuntos de termos encontrando definições de funções auxiliares que reduzem o tamanho total dos termos.

O Twitch opera em dois modos principais para gerar abstrações:

A. Abstrações de Prova Parcial (Partial Proof Abstractions)

• Cenário: Quando não há provas anteriores de problemas relacionados no mesmo domínio.
• Processo:
  1. O Twee tenta provar um problema difícil ($P_h$) até um limite de tempo. Se falhar, ele gera uma grande coleção de regras de reescrita e lemas intermediários.
  2. O sistema classifica esses lemas por uma métrica de "interessante": $s(l=r) = \frac{|T(l=r)|}{|l=r|^2}$, onde $|T|$ é o tamanho total dos termos na prova do lema e $|l=r|$ é o tamanho do lema. Lemas simples que exigem provas longas recebem pontuação alta.
  3. O Stitch é executado sobre os termos dos lemas mais bem classificados para encontrar padrões de compressão (abstrações).
  4. O Twee é reexecutado com essas abstrações.

B. Abstrações de Domínio (Domain Abstractions)

• Cenário: Quando há um conjunto de problemas mais fáceis já resolvidos no mesmo domínio.
• Processo (inspirado em Curriculum Learning):
  1. O Twitch executa o Twee em problemas "fáceis" do domínio.
  2. Para cada prova bem-sucedida, o Stitch gera abstrações locais.
  3. Essas abstrações locais são testadas: se acelerarem a re-prova do problema original, elas são consideradas "boas".
  4. O Stitch é executado novamente sobre o conjunto de todas as "boas abstrações locais" para encontrar padrões comuns de nível superior (abstrações de domínio).
  5. Essas abstrações de domínio são aplicadas a problemas difíceis do mesmo domínio.

C. Integração no Twee (Mecanismo de Abstração)

Diferente de adicionar as abstrações como novos axiomas (o que expandiria o espaço de busca e poderia causar lentidão), o Twitch estende o Twee para suportar abstrações nativamente na função heurística:

• Redução de Peso: Quando um par crítico contém um termo que corresponde a uma abstração, o peso (custo) desse termo é reduzido na heurística de seleção.
• Fórmula de Peso: O peso de uma abstração $A$ aplicada a uma substituição $\sigma$ é calculado como $w(A\sigma) = w_A + \sum w(x\sigma)$. Isso permite que termos repetidos dentro da abstração sejam contados apenas uma vez (comportamento de "atalho"), incentivando o provador a selecionar inferências que utilizam esses padrões.

3. Principais Contribuições

1. Método de Geração Automática: Uma abordagem para extrair abstrações de tentativas de prova falhas (lemas intermediários) e de provas bem-sucedidas de problemas relacionados.
2. Uso do Stitch para Provas: Adaptação da ferramenta Stitch (síntese de programas) para o domínio da prova de teoremas equacionais, tratando termos de prova como entrada para compressão.
3. Implementação no Twee: Extensão do provador equacional Twee para aceitar abstrações como guias heurísticos (redução de peso) em vez de apenas axiomas, permitindo o uso de muitas abstrações sem explodir o espaço de busca.
4. Validação Empírica: Demonstração de que o aprendizado de estrutura sintática pode superar heurísticas baseadas apenas em tamanho.

4. Resultados Experimentais

Os experimentos foram realizados em um conjunto de 1041 problemas de igualdade unitária (UEQ) do TPTP v9.2.1.

• Problemas Difíceis (Rating $\ge$ 0.9): O Twitch conseguiu provar 18 problemas difíceis que o Twee padrão não conseguia resolver dentro de 1000 segundos.
  • Exemplo Notável: O problema LAT075-1 (Rating 1.00, sobre o operador Sheffer/NAND) foi resolvido em 32 segundos (vs. tempo anterior de ~250s ou falha) usando abstrações de domínio como $f(x, x)$ (negação) e padrões de auto-distributividade.
• Melhoria de Desempenho Geral:
  • O uso de abstrações de domínio combinado com a estratégia de "goal flattening" reduziu o tempo de execução pela metade para problemas que o Twee já resolvia, e aumentou o número de problemas resolvidos em 300 segundos em cerca de 25.
  • As abstrações de prova parcial também trouxeram melhorias, embora menos consistentes que as de domínio, sendo úteis quando não há dados de treinamento disponíveis.
• Abstrações vs. Axiomas Definicionais: O estudo comparativo mostrou que usar abstrações como guias heurísticos (redução de peso) é mais robusto do que adicioná-las como axiomas. Adicionar muitos axiomas tende a causar timeouts devido à expansão do espaço de busca, enquanto as abstrações nativas oferecem aceleração com menor risco.

5. Significado e Conclusão

O trabalho demonstra que a descoberta automática de abstrações baseadas em estrutura é uma estratégia promissora para a prova de teoremas equacionais.

• Impacto: Permite que provadores automatizados "aprendam" padrões matemáticos significativos (como negação, conjunção ou leis de distributividade) a partir de provas existentes e os apliquem a novos problemas difíceis.
• Interpretabilidade: Diferente de modelos de aprendizado de máquina "caixa preta" (como redes neurais usadas em ENIGMA), as abstrações geradas são padrões sintáticos explícitos e interpretáveis por humanos.
• Futuro: O artigo sugere que a curadoria de domínios de treinamento e o refinamento das heurísticas de seleção de lemas são caminhos para melhorar ainda mais a qualidade das abstrações. A combinação de abstrações de domínio e de prova parcial mostrou-se particularmente eficaz para casos extremos.

Em resumo, o Twitch preenche a lacuna entre a busca cega baseada em tamanho e a orientação humana manual, automatizando a identificação de "atalhos" estruturais cruciais para provar teoremas complexos.