Resumo Técnico: Danus – Orquestrando Agentes de Raciocínio Matemático com Memória de Grafo de Fatos

Declaração do Problema

Recentes agentes baseados em Grandes Modelos de Linguagem (LLMs) demonstraram a capacidade de enfrentar problemas matemáticos de nível de pesquisa, por vezes resolvendo questões em aberto. No entanto, escalar esses sistemas para lidar com tarefas de pesquisa de longo horizonte permanece um desafio significativo. Sistemas multiagentes existentes frequentemente dependem de um ciclo de "gerar–verificar–revisar" com papéis especializados, mas eles têm dificuldade em coordenar buscas de provas paralelas de forma eficaz. Quando múltiplos agentes tentam contribuir para uma única prova sem um gerenciamento de memória robusto, os contextos compartilhados podem tornar-se confusos, e artefatos intermediários irrelevantes ou errôneos podem se propagar, degradando o desempenho. O problema central é como orquestrar um enxame de agentes para construir colaborativamente provas matemáticas longas, detalhadas e corretas, mantendo um estado de verdade confiável.

Metodologia

O artigo propõe o Danus, um sistema de orquestração projetado para escalar o raciocínio matemático através de um Grafo de Fatos compartilhado que serve como um mecanismo global de gerenciamento de memória. A arquitetura do sistema impõe uma separação rigorosa de poderes entre três tipos distintos de agentes:

1. O Agente Principal:

   • Papel: Realiza o planejamento global, coordenação e interação estratégica com matemáticos humanos. Ele não realiza derivações detalhadas.
   • Função: Interpreta o problema, consulta modelos de estratégia de alto nível (ex: GPT-5.5-pro) quando necessário, decompõe o problema e atribui direções aos agentes trabalhadores.
   • Gerenciamento de Estado: Lê periodicamente o Grafo de Fatos e os logs de memória global para resumir o estado atual da prova, identificar becos sem saída e reatribuir trabalhadores para direções promissoras. Ele atua como a interface para a orientação humana.

2. Agentes Trabalhadores (Enxame):

   • Papel: Executam a busca de provas detalhadas em paralelo.
   • Função: Com base nos agentes de geração Rethlas, os trabalhadores exploram o problema a partir de múltiplos ângulos (construtivos e refutacionais) simultaneamente. Cada trabalhador foca em afirmações específicas (lemas, contraexemplos, exemplos didáticos) em vez da prova inteira.
   • Interação: Os trabalhadores propõem enunciados com provas de suporte ao verificador. Eles recuperam fatos relevantes do Grafo de Fatos para sustentar suas afirmações atuais, mas não editam o grafo diretamente.

3. O Verificador Sem Estado (Stateless):

   • Papel: A única autoridade sobre a correção.
   • Função: Um serviço sem estado que verifica as afirmações matemáticas propostas antes que elas sejam admitidas no Grafo de Fatos. Ele lê o Grafo de Fatos para verificar dependências e referências citadas.
   • Confiabilidade: Projetado para produzir essencialmente zero falsos positivos; ele rejeita provas com etapas omitidas ou referências errôneas.

O Grafo de Fatos (Inovação Central)

O Grafo de Fatos é um Grafo Acíclico Dirigido (DAG) que serve como a fonte única de verdade do sistema.

• Estrutura: Os nós representam fatos verificados (um enunciado matemático + uma prova verificada pelo verificador). As arestas representam dependências lógicas (ou seja, o Fato B depende do Fato A).
• Vantagens sobre Blueprints Únicos: Diferente de sistemas anteriores que utilizavam um único arquivo Markdown (que força todos os trabalhadores a carregar todo o contexto acumulado), o Grafo de Fatos permite que os trabalhadores recuperem apenas os fatos específicos relevantes para sua tarefa atual. Isso mantém a janela de contexto pequena e focada, reduzindo alucinações e interferências.
• Paralelismo: Múltiplos trabalhadores podem contribuir para o grafo simultaneamente sem conflitos de bloqueio de arquivo.
• Revogação: Se um fato for posteriormente considerado incorreto (por exemplo, devido a uma referência falha), ele e todos os fatos que dele dependem são removidos do grafo, garantindo a integridade da estrutura restante.

Arquitetura de Memória

• Grafo de Fatos: Armazena apenas verdades verificadas.
• Memória Global: Um contexto compartilhado para o Agente Principal e para os trabalhadores, contendo produtos intermediários (planos, becos sem saída, direções promissoras, exemplos construídos) e logs de consultas com modelos externos.
• Memória Local: Logs privados para cada trabalhador individual para rastrear seu próprio histórico de raciocínio.

Fluxo de Trabalho

1. Inicialização: Um humano fornece um problema. O Agente Principal formula um plano e atribui tarefas ao enxame de trabalhadores.
2. Busca Paralela: Trabalhadores geram afirmações e provas, enviando-as ao Verificador. Fatos verificados são adicionados ao Grafo de Fatos.
3. Orquestração: O Agente Principal resume periodicamente o estado, consulta modelos externos para estratégia e redireciona os trabalhadores com base no progresso ou estagnação.
4. Terminação: O ciclo continua até que o teorema alvo (ou sua refutação) apareça como um fato verificado no grafo.
5. Síntese: O Agente Principal converte o Grafo de Fatos em um manuscrito em estilo de artigo acadêmico. Este rascunho passa por uma passagem final de verificação para corrigir erros introduzidos durante a compressão dos fatos em prosa linear.

Principais Contribuições

1. Orquestração por Grafo de Fatos: Introduz um mecanismo de memória baseado em DAG que permite a busca de provas paralela e escalável ao desacoplar o contexto do trabalhador do estado global da prova, evitando o "inchaço de contexto" e a interferência vistos em abordagens de arquivo único.
2. Separação de Poderes: Estabelece uma arquitetura rigorosa onde o planejamento, a execução e a verificação são estritamente separados, impedindo que o orquestrador introduza matemática não verificada.
3. Design com Humano no Ciclo (Human-in-the-Loop): Facilita a interação onde humanos fornecem orientação de alto nível e revisão final, enquanto o sistema lida com o trabalho pesado de busca, decomposição e síntese.
4. Pipeline de Verificação Robusto: Demonstra um sistema onde um verificador sem estado garante que o Grafo de Fatos permaneça uma fonte confiável de verdade, permitindo a acumulação segura de longas cadeias de dependência (até 54 níveis de profundidade em experimentos).

Resultados

O sistema foi avaliado em seis estudos de caso de nível de pesquisa em geometria algébrica, teoria de singularidades e combinatória. Em todos os casos, uma interface web do GPT-5.5-pro baseline falhou em produzir resultados significativos.

• Optimal Bend-and-Break para Foliações: O Danus sintetizou técnicas de diferentes referências para provar que a constante ótima é $r+1$. Ele identificou de forma independente referências insatisfatórias e buscou melhores.
• Conjectura do Índice Global de Shokurov (3D): O Danus decompôs autonomamente o problema em cinco classes e descobriu uma solução de teoria de Lie para três classes. Foi necessária apenas uma dica de alto nível (programa de modelo mínimo foliado) para resolver as duas restantes.
• Índices de Cartier Totais em Famílias: O Danus uniu geometria algébrica, álgebra comutativa e geometria algébrica real para provar a limitação. Ele corrigiu uma hipótese mal interpretada de uma fonte em PDF após intervenção humana.
• Assintótica de Números Matryoshka: O Danus resolveu este problema combinatório inteiramente de forma autônoma, desde o enunciado do problema até o manuscrito final, com zero orientação matemática humana.
• Homogeneidade Ponderada via Campos Vetoriais Logarítmicos: O Danus produziu uma prova através de uma rota não antecipada por especialistas humanos. Quando uma referência falha foi identificada por humanos, o Danus conseguiu revogar os fatos dependentes e reconstruir a prova.
• Classes Tangentes de Matroides: Em uma comparação controlada contra seu predecessor (Rethlas), o Danus resolveu um problema complexo que o Rethlas falhou em resolver em três tentativas. O Grafo de Fatos permitiu que o sistema gerenciasse 3.157 fatos verificados e cadeias de dependência de até 54 níveis de profundidade, enquanto o Rethlas confundiu conceitos matemáticos distintos.

Significância e Alegações

O artigo alega que a orquestração baseada em grafos de fatos fornece uma rota eficaz para escalar agentes de raciocínio matemático para problemas de pesquisa de longo horizonte.

• Escalabilidade: O sistema escala com sucesso o cálculo de tempo de execução (test-time computation) tanto em largura (exploração paralela de muitas direções) quanto em profundidade (acumulação de longas cadeias de raciocínio verificado).
• Confiabilidade: O protocolo de verificação estrito garante que o Grafo de Fatos permaneça uma fonte confiável de verdade, permitindo a construção de provas que são longas e complexas demais para uma única passagem de modelo.
• Colaboração: O Danus demonstra que agentes de IA podem contribuir substancialmente para a construção de provas, lidando com decomposição, síntese e reparo de erros, enquanto matemáticos humanos permanecem essenciais para a seleção de problemas, fornecimento de ideias de alto nível ausentes e revisão especializada final.
• Limitações: Os autores observam modestamente que o sistema ainda requer intervenção humana para os saltos conceituais mais difíceis e que a geração do manuscrito final, embora verificada, ainda pode exigir ajustes humanos para convenções de notação e citação. O sistema não cria novas ideias matemáticas ex nihilo, mas se destaca em encontrar caminhos para soluções quando elas existem.

O artigo conclui que o Danus representa um passo em direção a sistemas de pesquisa matemática colaborativa, onde agentes de IA são integrados ao julgamento humano para resolver problemas de pesquisa abertos.