Constraint Learning for Non-confluent Proof Search

Este artigo apresenta uma abordagem de aprendizado de restrições para reduzir o excesso de retrocesso na busca de provas no cálculo de conexão de primeira ordem, mantendo a completude em calculistas de tabela não confluentes.

O essencial

Imagine que você está tentando resolver um labirinto gigante para encontrar uma saída (que, neste caso, é uma prova matemática).

A maioria dos sistemas de prova matemática funciona como um explorador muito teimoso: ele escolhe um caminho, anda até o fim e, se bater numa parede (um "beco sem saída"), volta um passo, tenta outro caminho, e assim por diante. Isso se chama backtracking (retrocesso).

O problema é que, em alguns tipos de labirintos (chamados de "não confluentes"), esse explorador pode ficar preso em um ciclo infinito de erros. Ele pode voltar, tentar o mesmo caminho errado de novo, bater na parede de novo, voltar de novo... gastando uma energia enorme para não chegar a lugar nenhum.

O Problema: O Explorador que Esquece

No mundo da lógica matemática (especificamente no cálculo de "tableau de conexão"), o sistema precisa fazer escolhas. Às vezes, ele escolhe fechar uma porta (uma parte da prova) que parece boa, mas que, mais tarde, impede que ele feche outra porta essencial. Quando ele percebe o erro, ele tem que desfazer tudo e tentar de novo.

Se ele fizer isso muitas vezes, o computador trava.

A Solução: O "Diário de Viagem" (Constraint Learning)

Os autores deste paper, Michael, Clemens e Laura, tiveram uma ideia brilhante: e se o explorador aprendesse com seus erros?

Eles criaram um sistema chamado Constraint Learning (Aprendizado de Restrições). Funciona assim:

1. O Erro: O explorador chega a um beco sem saída. Ele não consegue avançar.
2. A Investigação: Em vez de apenas voltar e tentar de novo, o sistema para e pergunta: "Por que eu estou preso aqui?"
3. A Lição: Ele descobre que o problema foi uma combinação específica de decisões anteriores. Por exemplo: "Eu fechei a porta A e, ao mesmo tempo, escolhi o caminho B. Juntos, A e B me prenderam."
4. O Diário: O sistema escreve uma regra no seu "diário de viagem" (um banco de dados de restrições): "Nunca, em hipótese alguma, tente fazer A e B juntos novamente."
5. O Pulo do Gato (Backjumping): Agora, quando o sistema estiver explorando e perceber que está prestes a fazer A e B juntos, ele não precisa voltar passo a passo. Ele dá um "pulo" direto para trás, ignorando todas as decisões inúteis que o levariam a esse erro, e tenta um caminho totalmente diferente.

A Analogia do Quebra-Cabeça

Pense em montar um quebra-cabeça gigante:

• Sem aprendizado: Você tenta encaixar uma peça azul no canto. Não serve. Tira. Tenta encaixar no meio. Não serve. Tira. Tenta em outro lugar. Você gasta horas testando a mesma peça em lugares onde ela claramente não cabe, porque esqueceu que já tentou ali antes.
• Com aprendizado: Você tenta encaixar a peça azul no canto. Não serve. Você pensa: "Ah, essa peça azul é muito grande para o canto esquerdo. Nunca mais vou tentar encaixá-la lá." Da próxima vez que pegar a peça azul, você sabe imediatamente para onde ela não deve ir. Você economiza tempo e evita frustração.

O Que Eles Conseguiram?

Os autores criaram um protótipo chamado hopCoP para testar essa ideia.

• Eles compararam o hopCoP (que aprende com os erros) com um sistema antigo chamado meanCoP (que apenas tenta e erra, ou corta o caminho de forma aleatória).
• O Resultado: O hopCoP conseguiu resolver muito mais problemas em menos tempo. Ele evitou milhões de passos inúteis que o sistema antigo teria feito.

Por que isso é importante?

Antes, para evitar que o sistema travasse, as pessoas usavam "gambiarras" (regras rígidas) que faziam o sistema ser mais rápido, mas que às vezes falhavam em encontrar a prova (eram incompletas).
Com essa nova técnica, eles conseguiram acelerar o sistema sem perder a capacidade de encontrar a resposta. É como ter um GPS que não só te mostra o caminho, mas aprende com os engarrafamentos e te avisa: "Ei, não entre naquela rua, vai dar trânsito!", antes mesmo de você entrar.

Resumo da Ópera:
O papel ensina como ensinar computadores a lembrar de seus erros na busca por provas matemáticas. Em vez de repetir o mesmo erro infinitamente, eles criam uma "lista de proibições" inteligente que os faz pular direto para soluções melhores, economizando tempo e energia computacional.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "Constraint Learning for Non-Confluent Proof Search" (Aprendizagem de Restrições para Busca de Provas Não Confluentes), apresentado em português.

1. Problema Identificado

O artigo aborda um desafio fundamental na busca automática de teoremas utilizando cálculos de tableaux não confluentes, especificamente o cálculo de tableaux de conexão (connection tableau calculus).

• Natureza do Problema: Em calculi não confluentes, a ordem em que as escolhas de extensão e redução são feitas importa. Uma escolha incorreta pode levar a um "beco sem saída" (dead end) onde o tableau não pode ser fechado, exigindo backtracking (retrocesso).
• Limitações Atuais:
  • O backtracking excessivo é ineficiente, pois o sistema pode tentar fechar o mesmo objetivo repetidamente, mesmo quando a causa raiz do impasse (ex: uma substituição de variável específica) não mudou.
  • Restrições simples de backtracking (como cortes em Prolog, usados no sistema leanCoP) reduzem o tempo de execução, mas tornam o sistema incompleto, ou seja, podem falhar em encontrar uma prova que existe.
  • Métodos de backtracking padrão (como em SAT solvers modernos) não são diretamente aplicáveis sem perda de completude neste contexto.

2. Metodologia Proposta

Os autores propõem adaptar a técnica de Aprendizagem de Restrições (Constraint Learning), amplamente utilizada em SAT solvers (CDCL) e SMT, para o domínio da busca de provas em tableaux de conexão.

A. Linguagem de Restrições

O núcleo da metodologia é a definição de uma linguagem para explicar por que uma inferência falhou ou por que um tableau ficou "preso" (stuck).

• Definição de "Motivo" (Reason): Quando uma inferência $j$ não pode ser aplicada, o sistema identifica um conjunto mínimo de inferências anteriores que, se aplicadas, impedem $j$.
• Linguagem Simplificada (Definição 1): Inicialmente, as restrições são conjuntos de átomos representando:
  1. Início do tableau com uma cláusula $C$ ($SC$).
  2. Redução de uma posição $p$ para um ancestral $q$ ($R^q_p$).
  3. Extensão de uma posição $p$ conectando à $i$-ésima literal de uma cláusula $C$ ($E^i_{p/C}$).
• Linguagem Refinada (Seção 5): Para maior eficiência e generalidade, a linguagem é decomposta em:
  • Posicionamento de Literais: $L@p$ (o literal $L$ está na posição $p$).
  • Vinculação de Variáveis: $x \mapsto t$ (a variável $x$ está ligada ao termo $t$).
  • Não-Conexão: $p \not\sim q$ (nenhuma conexão pode ser feita entre as posições $p$ e $q$, independentemente da substituição).
  • Disequações: $s \neq t$ para suportar refinamentos como regularidade.

B. Algoritmo de Busca (Algoritmo 1)

O algoritmo de busca foi redesenhado para integrar o aprendizado de restrições:

1. Manutenção de Rastros (Trail): Mantém-se um rastro de átomos (inferências aplicadas) que são verdadeiros no estado atual.
2. Detecção de Impasse: Se todas as inferências possíveis em uma ramificação aberta falharem (ou violarem uma restrição aprendida), o tableau está "preso".
3. Aprendizado: O sistema calcula a "razão" do impasse (o conjunto de inferências que causaram o problema) e gera uma nova cláusula de restrição (constraint clause) que proíbe a combinação específica de decisões que levou a esse estado.
4. Backjumping: Em vez de retroceder passo a passo, o sistema usa a nova restrição para retroceder diretamente para o ponto onde a decisão conflitante foi tomada, pulando níveis desnecessários.
5. Completude: Diferente de métodos com cortes, este sistema mantém a completude. Se um tableau fechado existir dentro do limite de profundidade, o algoritmo o encontrará.

3. Contribuições Chave

1. Primeira Aplicação de Constraint Learning em Tableaux de Conexão: Adaptação bem-sucedida de técnicas de CDCL para um cálculo de tableaux não confluentes, mantendo a completude teórica.
2. Linguagem de Restrições Específica: Desenvolvimento de uma linguagem formal para explicar falhas de inferência em tableaux de primeira ordem, lidando com substituições globais e ligações de variáveis.
3. Sistema Protótipo (hopCoP): Implementação de um provador de teoremas (hopCoP) que incorpora essa lógica, comparável ao meanCoP (uma variante incompleta do leanCoP otimizada).
4. Análise de Trade-off: Demonstração de que a redução drástica no número de passos de backtracking compensa o custo computacional de gerenciar as restrições aprendidas.

4. Resultados Experimentais

Os autores compararam o hopCoP (com aprendizado de restrições) contra o meanCoP (com cortes, incompleto) e o !meanCoP (com cortes agressivos) em vários conjuntos de benchmarks (TPTP, MPTP, Miz40).

• Redução de Backtracking: Em problemas onde a prova existe em profundidades maiores (ex: PUZ005-1), o hopCoP reduziu drasticamente o número de passos de extensão tentados em comparação com o meanCoP. Enquanto o meanCoP tentou mais de 6 milhões de passos na profundidade 7, o hopCoP tentou apenas ~48 mil.
• Desempenho Geral:
  • No conjunto M2k, o hopCoP provou 1.050 teoremas em 10 segundos, superando o meanCoP (795) e o !meanCoP (878).
  • No conjunto Miz40, o hopCoP provou 13.040 teoremas, superando significativamente os outros dois (7.592 e 9.748).
  • No conjunto TPTP, o hopCoP provou 4.026 teoremas, superando o meanCoP (3.578).
• Conclusão dos Dados: A sobrecarga de manter as restrições aprendidas não prejudicou o desempenho; pelo contrário, a eliminação de caminhos de busca inúteis resultou em um sistema mais rápido e robusto, mesmo sendo completo.

5. Significância e Impacto

• Viabilidade Prática: O trabalho demonstra que é possível melhorar o comportamento de sistemas de prova não confluentes sem sacrificar a completude, algo que métodos anteriores (como cortes) não conseguiam fazer.
• Ponte entre Áreas: Une conceitos de satisfação de restrições (CSP) e SAT/SMT com a prova de teoremas clássica de primeira ordem.
• Futuro: Os autores sugerem que essa abordagem pode ser aplicada a outros calculi de tableaux não confluentes e explorar a interseção com aprendizado de máquina (usando heurísticas aprendidas para guiar a geração de restrições e vice-versa).
• Limitações e Melhorias: O uso de posições explícitas na linguagem de restrições limita a reutilização de restrições entre diferentes estruturas de tableau. Futuras implementações poderiam buscar detectar conflitos modulo posições estruturalmente equivalentes para tornar o sistema ainda mais eficiente.

Em resumo, o artigo apresenta uma solução elegante e eficaz para o problema do backtracking excessivo em provadores de teoremas, transformando falhas de busca em conhecimento útil (restrições) que guia o sistema diretamente para soluções viáveis, mantendo a garantia teórica de encontrar uma prova se ela existir.