Resumo Técnico: Iteris: Loops de Pesquisa Agênticos para Matemática Computacional

1. Declaração do Problema

O artigo aborda o desafio de aplicar IA a problemas abertos em matemática computacional. Diferente de problemas de competição ou tarefas de otimização de objetivo único, a pesquisa neste domínio exige uma interação complexa entre experimentação numérica, construção adversarial e desenvolvimento de provas formais. Os sistemas de IA atuais frequentemente têm dificuldade em coordenar esses distintos modos de pesquisa ou em manter trajetórias de pesquisa de longo horizonte, onde fatos precisam ser separados, verificados e reorganizados.

Os autores aplicam seu sistema proposto, Iteris, a dois problemas específicos da coleção Simons Workshop [3]:

1. Problema 2.4: Uma comparação assintótica entre Gradiente Conjugado (CG) e Descida de Coordenadas Aleatorizada (RCD) em sistemas lineares com espectros de lei de potência. O objetivo é determinar um diagrama de fase para a razão de custo normalizada entre os dois métodos.
2. Problema 4.3: Uma questão sobre se a fatoração QR com pivoteamento de coluna (QRCP) seleciona de forma confiável submatrizes bem condicionadas de uma matriz com linhas ortonormais, especificamente sob condições de baixa coerência.

2. Metodologia: O Sistema Iteris

O Iteris é um sistema de pesquisa agêntico organizado como um loop de explorar–planejar–executar. Ele coordena distintos modos de pesquisa através de um sistema de memória baseado em arquivos que serve tanto como armazenamento de estado de longo prazo quanto como mensagens estruturadas entre agentes.

2.1 O Protocolo Agêntico

Cada iteração do sistema segue três fases distintas:

1. Exploração (Explore): Um Agente de Exploração realiza uma "sondagem leve ao nível do repositório". Ele lê os arquivos do projeto, inspeciona iterações recentes e redige raciocínios de rascunho sobre rotas plausíveis. Crucialmente, ele não escreve o plano oficial, mas produz um aconselhamento registrando formas de tarefas recomendadas, verificações de mínimos locais e avaliações de risco para evitar que o sistema se comprometa excessivamente com um ramo estagnado.
2. Planejamento (Plan): Um Agente de Planejamento lê o estado global do projeto (declaração do problema, roteiro, memória, status da rota) e o aconselhamento de exploração. Ele decide o pool de tarefas para a próxima iteração, gerando um TASK_POOL.json estruturado que define categorias de tarefas, objetivos, entradas e requisitos de verificação.
3. Execução (Execute): Agentes de Execução especializados recebem tarefas atribuídas e realizam ações de pesquisa específicas, escrevendo arquivos de resultados estruturados de volta na memória do projeto.

2.2 Agentes de Execução

O sistema emprega quatro categorias de agentes de execução, cada um com habilidades de tarefas específicas definidas por especificações de capacidade baseadas em Markdown:

• Agente de Fundação (Foundation Agent): Audita fontes, congela definições, redige cartões de conjectura e mantém a disciplina de alegações.
• Agente de Experimento (Experiment Agent): Executa trabalhos numéricos (harnesses de teste, diagnósticos, buscas de contraexemplos). A evidência é tratada como orientação, não como prova.
• Agente de Prova (Proof Agent): Constrói e verifica artefatos de prova para afirmações estáveis, casos especiais ou lemas.
• Agente de Revisão (Review Agent): Avalia evidências, lacunas de prova e o valor da rota, recomendando se deve aprofundar, reformular ou aposentar um ramo de pesquisa.

2.3 Separação de Preocupações

Uma característica de design fundamental é a separação do Agente de Exploração do Agente de Planejamento. Enquanto o Agente de Planejamento mantém a coerência global, o Agente de Exploração realiza sondagens agressivas para detectar "inércia local" (ex: trabalho de acompanhamento incremental) e sugere direções alternativas antes que uma tarefa seja oficialmente comprometida. Isso permite que o sistema busque além de seu caminho atual enquanto mantém o planejamento globalmente coerente.

3. Contribuições Principais e Resultados

3.1 Resultado I: Diagrama de Fase CG vs. RCD

O Iteris foi aplicado à comparação de CG e RCD em espectros de lei de potência ($A_n = U_n \text{diag}(1^{-p}, \dots, n^{-p})U_n^*$).

• Teorema 1: O sistema estabeleceu um diagrama de fase de parâmetros fixos para o comportamento assintótico da razão $\rho_n(\epsilon, p)$ (épocas de RCD vs. passos de CG) conforme $n \to \infty$.
• Principais Descobertas:
  • Para $p > 1$ (espectro somável), o RCD converge em $O(1)$ épocas enquanto o CG leva $O(n)$ passos, portanto $\rho_n \to 0$.
  • Para $p = 1$, $\rho_n \to 0$ com um limite logarítmico.
  • Para $0 < p < 1$, o comportamento é governado por um piso de CG limitante $F(p)$, derivado de um problema de momento de dimensão finita envolvendo a medida de cauda $\nu_p$.
  • Se o limiar de erro $\epsilon < F(p)$, o CG requer graus crescentes para convergir, enquanto o RCD permanece limitado, fazendo com que $\rho_n \to 0$.
  • Se $\epsilon > F(p)$, o CG converge em $O(1)$ passos enquanto o RCD requer uma fração positiva de uma época, fazendo com que $\rho_n$ seja afastado de zero.
• Interação Humano-IA: O sistema identificou a estrutura de fase e o mecanismo do "piso de Hankel". No entanto, um rascunho inicial de prova dependia de uma suposição mais forte e injustificada para a análise de taxa no regime $p < 1$. Especialistas humanos detectaram essa lacuna, e o argumento foi reparado através de interação para fornecer limites de taxa conservadores e verificados.

3.2 Resultado II: Contraexemplo de QRCP

O Iteris abordou se o QRCP garante submatrizes bem condicionadas para matrizes com linhas ortonormais e coerência limitada.

• Teorema 2: O sistema construiu uma família de contraexemplos de baixa coerência mostrando que o QRCP pode falhar em selecionar submatrizes bem condicionadas, mesmo quando as energias das linhas são controladas uniformemente.
• Principais Descobertas: Para qualquer $H^* > 1$ (limite de coerência) e $B > 0$, existe uma matriz $Q$ com linhas ortonormais e coerência $\mu(Q) < H^*$ tal que o número de condição da submatriz selecionada excede $B k^e$.
• Mecanismo: O contraexemplo explora uma pressão de "retrosubstituição triangular". O sistema projetou um bloco central selecionado que satisfaz as condições de pivô local, mas cria uma norma inversa grande. Colunas adicionais foram inseridas para restaurar a ortonormalidade global sem serem selecionadas pela regra de pivoteamento.
• Interação Humano-IA: O Iteris identificou o obstáculo e gerou a construção. A trajetória da prova foi inicialmente circuitária; especialistas humanos reorganizaram o argumento em uma prova legível e alinharam o teorema informal com uma verificação formal em Lean 4.

4. Significância e Alegações

O artigo afirma que sistemas de IA agênticos podem participar significativamente de fluxos de trabalho de pesquisa para problemas abertos em matemática computacional, mas enfatiza que a validação humana permanece essencial.

• Além de Benchmarks: O Iteris demonstra que a IA pode ir além da resolução de exercícios isolados para participar de pesquisa genuína, gerando artefatos exploratórios de longo horizonte e rascunhos de provas.
• Integração de Fluxo de Trabalho: O sistema coordena com sucesso a experimentação numérica (para identificar características estruturais como o piso de Hankel ou a pressão de retrosubstituição) com a construção de provas formais.
• Papel da Intervenção Humana: Os autores afirmam explicitamente que o Iteris desloca, em vez de remover, o esforço humano.
  • No caso do CG, o sistema encontrou a estrutura, mas os humanos repararam a análise de taxa.
  • No caso do QRCP, o sistema encontrou o contraexemplo, mas os humanos reorganizaram a prova e verificaram a consistência semântica.
• Comparação com LLMs Diretos: Consultas diretas a modelos avançados (ex: GPT-Pro) produziram heurísticas plausíveis ou esboços de alto nível, mas falharam em fechar provas, muitas vezes confundindo distinções entre limites esperados e de alta probabilidade ou tratando passos plausíveis como obrigações cumpridas. O Iteris, por outro lado, decompõe heurísticas em obrigações de prova auditáveis e usa agentes de revisão para bloquear atalhos injustificados.

O artigo conclui que, embora a IA possa ampliar o espaço de busca e produzir argumentos de rascunho, o julgamento matemático final, a verificação de pressupostos, a detecção de lacunas e a exposição permanecem responsabilidades humanas críticas.