OEIS Open: How many conjectures can language models turn into theorems?

Resumo Técnico: OEIS OPEN

Enunciado do Problema
O artigo aborda a falta de benchmarks sistemáticos para avaliar as capacidades de sistemas de IA na resolução de problemas de pesquisa abertos em matemática. Os benchmarks existentes, como o HorizonMath e o FrontierMath: Open Problems (FM:OP), dependem de lacunas "gerador–verificador", onde as soluções são objetos concretos (ex: grafos, polinômios) que são difíceis de encontrar, mas baratos de verificar. O autor argumenta que essas abordagens falham em cobrir a maior parte da pesquisa matemática, que frequentemente exige a prova de afirmações gerais em vez da exibição de objetos. Além disso, os benchmarks existentes frequentemente aceitam evidências numéricas em vez de provas formais, dependem de código de verificação feito à mão propenso a erros e incluem problemas que podem ser insolúveis.

O autor propõe o OEIS OPEN, um benchmark projetado para testar se Modelos de Linguagem (LMs) podem resolver autonomamente conjecturas matemáticas abertas produzindo provas formais (ou refutações) dentro do assistente de prova Lean.

Metodologia

• Construção do Dataset: O benchmark consiste em 492 conjecturas abertas extraídas da Online Encyclopedia of Integer Sequences (OEIS). Essas conjecturas foram originalmente coletadas e formalizadas em Lean por Tsoukalas et al. [6]. O processo de seleção envolveu a filtragem de 2.649 conjecturas da OEIS para encontrar problemas não triviais, matematicamente interessantes, porém não famosos, adequados para a prova de teoremas automatizada. O foco em sequências de inteiros minimiza o risco de má formalização, pois esses problemas geralmente envolvem operações elementares em vez de definições complexas que exigem longas cadeias de dependências de bibliotecas.
• Estrutura de Avaliação: Diferente de tentativas anteriores que utilizaram agentes complexos e sob medida (ex: AlphaProof Nexus usando busca evolutiva), esta avaliação utiliza um harness de agente simples e de código aberto construído sobre a biblioteca Inspect. O agente base utiliza um loop estilo ReAct com três ferramentas: um shell bash, um editor de texto e um monitor de recursos. O ambiente inclui Lean 4 com Mathlib, SageMath e bibliotecas Python (sympy, mpmath, numpy).
• Segurança e Verificação: Para evitar "modificações não autorizadas" (ex: injeção de axiomas, adulteração do ambiente), a avaliação divide cada tentativa em três contêineres Docker isolados:
  1. Contêiner do Agente: Onde o modelo gera a prova.
  2. Contêiner de Compilação: Um ambiente limpo onde a fonte submetida é compilada para um artefato binário (.olean).
  3. Contêiner do Pontuador (Scorer): Executa o SafeVerify (uma adaptação do lean4checker) para verificar o binário contra o teorema alvo.
  • O SafeVerify garante que a submissão prove exatamente a afirmação alvo sem introduzir axiomas extras além dos três padrão (propext, Quot.sound, Classical.choice) e sem depender de truques de metaprogramação não verificados.
• Variantes Experimentais: O estudo avalia modelos sob diferentes condições:
  • Orçamentos: Um limite de \50 por conjectura para o conjunto completo (492 problemas) e um limite de \200 para um subconjunto aleatório de 100 problemas (OEIS OPEN LITE).
  • Complexidade do Agente: Comparando o agente base simples contra uma variante "DeepAgent" (apresentando delegação, memória persistente e listas de tarefas) e uma variante com acesso a um snapshot offline de 476.000 artigos matemáticos do arXiv.

Principais Resultados

• Desempenho:
  • No conjunto OEIS OPEN completo ($50 de orçamento), o Claude Opus 4.8 resolveu 30% (147/492) das conjecturas. O GPT-5.5 resolveu 26%, e o Gemini 3.5 Flash resolveu 22%.
  • Estes resultados superam significativamente o estado da arte anterior, o sistema AlphaProof Nexus (Tsoukalas et al.), que resolveu apenas 9% (44/492) das mesmas conjecturas com um custo semelhante.
  • No subconjunto OEIS OPEN LITE ($200 de orçamento), o desempenho melhorou, com o Claude Fable 5 alcançando uma taxa de sucesso de 44% e o GPT-5.6 Sol atingindo 43%.
• Eficiência de Custo: O custo médio por conjectura resolvida foi modesto, variando de \6 (GPT-5.5) a \10 (Claude Opus 4.8), com um máximo de $47.
• Impacto da Complexidade e Dados:
  • Fornecer aos agentes acesso à literatura matemática (476k artigos do arXiv) não melhorou o desempenho no conjunto LITE.
  • O uso da arquitetura mais complexa DeepAgent não melhorou o desempenho em relação ao agente base simples.
• Escalabilidade: As taxas de resolução parecem subir log-linearmente com o orçamento de gastos. O autor estima que, com um orçamento de \200, os melhores modelos atuais poderiam resolver aproximadamente 216 das 492 conjecturas (acima das 147 a \50), sugerindo que o escalonamento adicional do computacional de inferência renderia mais resultados, embora com custo exponencial.

Significância e Alegações

O artigo alega que o OEIS OPEN demonstra que os modelos de linguagem atuais podem resolver autonomamente conjecturas de pesquisa abertas a um custo modesto, sem a necessidade de arquiteturas de agentes altamente especializadas e sob medida.

• Autonomia: Os resultados sugerem que os LMs podem expandir a fronteira da pesquisa matemática de forma independente, resolvendo problemas que anteriormente só eram tentados por sistemas customizados e complexos.
• Simplicidade: O sucesso do agente "ReAct" minimal apoia a "lição amarga" (bitter lesson) na IA: fornecer aos modelos ferramentas simples e gerais frequentemente supera a prescrição de estruturas complexas e específicas para o problema.
• Utilidade do Benchmark: O trabalho estabelece as provas formais como um padrão viável e rigoroso para benchmarking de IA em matemática, evitando as armadilhas de evidências numéricas e verificadores feitos à mão.
• Natureza das Conjecturas: O autor é modesto quanto à significância matemática das conjecturas específicas resolvidas. Eles observam que, embora estas sejam problemas propostos por matemáticos, a maioria provavelmente recebeu pouca atenção prévia. O dataset serve como um proxy para "pesquisa aberta" em vez de um teste para resolver problemas famosos e de alto perfil (como a Hipótese de Riemann).

Limitações
O autor reconhece diversas limitações:

1. Risco de Má Formalização: Embora as sequências de inteiros reduzam este risco, algumas conjecturas no dataset podem estar mal formalizadas em Lean, potencialmente tornando-as mais fáceis de resolver do que o pretendido.
2. Escopo: O benchmark é limitado a problemas formalizáveis em Mathlib; ele não pode cobrir toda a pesquisa matemática.
3. Vazamento de Dados (Data Leakage): Uma vez que uma conjectura é resolvida, sua prova pode entrar nos dados de treinamento de futuros modelos, potencialmente inflando as métricas de desempenho futuro.
4. Reduções: O benchmark aceita apenas provas da conjectura ou de sua negação, não reduções a outros problemas famosos abertos, o que matemáticos poderiam valorizar muito.

Em conclusão, o artigo apresenta o OEIS OPEN como um benchmark robusto, seguro e escalável que revela a crescente capacidade de modelos de linguagem de propósito geral para realizar pesquisa matemática autônoma, resolvendo uma parte significativa de conjecturas abertas com complexidade mínima de agente.