Automated conjecturing with \emph{TxGraffiti}

Resumo Técnico de "Conjecturação Automatizada com TxGraffiti"

Declaração do Problema
O artigo aborda o desafio da conjecturação automatizada: a geração de desigualdades matematicamente úteis, não redundantes e interpretáveis entre invariantes numéricos de objetos matemáticos (especificamente grafos). Embora a prova automática de teoremas seja um campo maduro, a geração automatizada de conjecturas historicamente lutou com o problema de "demasiadas afirmações", onde a enumeração sistemática produz vastos números de afirmações verdadeiras em banco de dados, mas triviais ou redundantes. O objetivo é filtrar essas afirmações para identificar aquelas que oferecem novas informações genuínas (informatividade) e são adequadas para escrutínio e prova humana.

Metodologia
O artigo introduz o TxGraffiti (Texas Graffiti), um sistema baseado em heurísticas e otimização que opera sobre uma tabela de instantâneo versionado e finito de objetos matemáticos. Diferentemente de seus predecessores (Graffiti e Graffiti.pc), que calculam invariantes dinamicamente durante a busca, o TxGraffiti trata a base de evidências como um artefato estático.

O pipeline de conjecturação consiste nas seguintes etapas:

1. Curadoria de Dados (Tabela de Instantâneo):

   • Uma tabela é construída onde as linhas representam objetos (grafos) e as colunas representam invariantes numéricos pré-calculados (por exemplo, número de independência $\alpha$, número de emparelhamento $\mu$) e predicados booleanos (por exemplo, "é conexo", "é regular").
   • A estratégia de curadoria prioriza a cobertura em vez da aleatoriedade, incluindo especificamente construções extremas, testemunhas de igualdade (casos agudos) e contraexemplos para garantir que a tabela seja diagnosticamente rica.

2. Geração de Candidatos via Otimização:

   • Para um invariante alvo escolhido $\alpha$ e um predicado booleano $P$ (hipótese), o sistema busca limites afins da forma $\alpha \le mx + b$ ou $\alpha \ge mx + b$, onde $x$ é um invariante preditor.
   • Em vez de enumerar árvores de expressão complexas, o TxGraffiti fixa uma classe de hipóteses paramétrica simples (limites afins univariados) e ajusta coeficientes resolvendo Programas Lineares (PLs).
   • PL de Limite Superior: Minimiza o slack total $\sum (mx_i + b - \alpha_i)$ sujeito a $\alpha_i \le mx_i + b$ para todas as linhas que satisfazem $P$.
   • PL de Limite Inferior: Maximiza o slack total (ou minimiza o slack negativo) sujeito a $\alpha_i \ge mx_i + b$.
   • O sistema também suporta limites multivariados e relações não lineares expandindo o esquema com colunas derivadas (por exemplo, $n-\mu$, $\Delta^2$), embora a interface web padrão priorize modelos de preditor único para interpretabilidade.

3. Filtragem (Heurística Estática-Dalmata):

   • Para gerenciar a redundância, o TxGraffiti emprega uma heurística estática-dalmata.
   • Número de Toque: Definido como a contagem de objetos no instantâneo onde a desigualdade se mantém com igualdade (instâncias agudas).
   • Lógica de Seleção: Os candidatos são classificados pelo número de toque. Um candidato é aceito como um "representante" se tocar pelo menos um objeto ainda não coberto pelos conjuntos agudos de representantes previamente aceitos. Se o conjunto agudo de um candidato for idêntico ao de um representante aceito, ele é retido como um "alias" (uma forma sintética diferente do mesmo locus de igualdade). Candidatos que não adicionam novas instâncias agudas são descartados.

Principais Contribuições

• Arquitetura do Sistema: O TxGraffiti é apresentado como um sistema modular disponível como uma aplicação web interativa e um pacote Python de código aberto (txgraffiti). Ele desacopla o cálculo de invariantes da geração de conjecturas, permitindo iteração rápida em conjuntos de dados fixos.
• Ajuste Baseado em Otimização: O artigo muda o paradigma da enumeração baseada em gramática (gerar fórmulas e testá-las) para ajuste baseado em otimização (resolver PLs para encontrar os limites mais apertados para preditores específicos). Isso garante que os candidatos gerados sejam "verdadeiros na tabela" por construção e otimizados para apertamento.
• Filtragem Estática-Dalmata: A adaptação da heurística dalmata para um instantâneo fixo permite um processo de filtragem determinístico de passagem única que prioriza limites com alto "toque" (muitas testemunhas agudas) enquanto elimina redundância.
• Interpretabilidade: Ao restringir a classe de hipóteses a modelos afins simples e racionalizar coeficientes, o sistema produz conjecturas que são concisas e legíveis por humanos.

Resultados
O artigo demonstra a eficácia do sistema através de vários exemplos:

• Ilustração do Fluxo de Trabalho: Usando o número de dominação total $\gamma_t$, o sistema gerou um limite $\gamma_t(G) \ge \frac{2}{3}R(G)$ para grafos com $\Delta(G) \le 3$. Isso foi rapidamente generalizado para um teorema envolvendo $\Delta(G)$ e provado usando estimativas padrão.
• Publicações Estimuladas: O artigo cataloga vários resultados da teoria dos grafos que originaram como conjecturas do TxGraffiti e foram subsequentemente provados:
  • Independência vs. Emparelhamento: A conjectura de que $\alpha(G) \le \mu(G)$ para grafos $r$-regulares foi provada em [51].
  • Limites de Forçamento Zero: Várias desigualdades relacionando números de forçamento zero ($Z, Z_t, Z_+$) a parâmetros de dominação e independência foram conjecturadas e provadas, incluindo $Z(G) \le \beta(G)$ para grafos sem garra e limites para grafos cúbicos.
  • Problemas Abertos: O sistema identificou a conjectura $Z(G) \le \alpha(G) + 1$ para grafos conexos com $\Delta \le 3$, que permanece um problema aberto central, embora existam resultados parciais.

Significado e Alegações
O artigo posiciona o TxGraffiti não como uma ferramenta para descobrir teoremas profundos autonomamente, mas como um gerador de evidências estruturado que facilita a investigação matemática humana.

• Validade Empírica: O sistema produz afirmações "verdadeiras na tabela", o que significa que elas se mantêm para todas as instâncias no instantâneo curado. Os autores reservam explicitamente o termo "teorema" para afirmações estabelecidas por prova formal, distinguindo a saída do sistema como conjecturas.
• Postura Filosófica: Ecoando a perspectiva empírica de Fajtlowicz (que projetou o Graffiti), o artigo argumenta que a capacidade de máquinas produzirem conjecturas plausíveis e profundas é um fato empírico que apoia a visão de máquinas como participantes significativos na descoberta matemática aberta.
• Escalabilidade e Reprodutibilidade: Ao tratar a tabela de instantâneo como um artefato versionado e auditável, o TxGraffiti aborda questões de robustez de corrupção de dados e garante que as conjecturas possam ser reproduzidas e refinadas à medida que a base de evidências cresce.

Os autores concluem que, embora a implementação atual se concentre em invariantes de grafos, o "paradigma da tabela de instantâneo" e o pipeline de otimização e filtragem são amplamente aplicáveis a qualquer domínio onde objetos admitam características e predicados computáveis.