Resumo Técnico: Avaliando Agentes de LLM Aumentados por SageMath para Matemática Computacional e Experimental

Definição do Problema

Os avanços recentes em IA para matemática concentraram-se predominantemente na autoformalização (tradução de linguagem natural para linguagens de prova formal como Lean ou Coq) e na prova de teoremas automatizada. Embora essas abordagens tenham alcançado desempenho de medalha de ouro em competições e resolvido problemas abertos específicos, elas negligenciam amplamente o papel dos Sistemas de Álgebra Computacional (CAS) no fluxo de trabalho mais amplo da pesquisa matemática.

Na matemática computacional e experimental (ex: álgebra comutativa combinatória, teoria dos grafos, teoria de grupos finitos), pesquisadores utilizam rotineiramente ferramentas CAS como o SageMath para explorar hipóteses, validar candidatos e buscar contraexemplos. No entanto, a integração desses motores simbólicos em fluxos de trabalho de agentes de Large Language Models (LLM) permanece subexplorada. A questão central deste trabalho é: Até que ponto o feedback simbólico verificável de um CAS melhora o desempenho de LLMs de fronteira em matemática de nível de pesquisa, e como isso molda seu comportamento em uma configuração de agente?

Metodologia

Configuração Experimental

Os autores propõem uma configuração de agente do tipo ReAct onde os LLMs interagem iterativamente com duas ferramentas:

1. SageMath: Um CAS de código aberto que fornece uma interface Python unificada para sistemas como GAP, Singular e PARI/GP. O agente gera código, executa-o em um ambiente isolado (sandbox) e recebe saída verificável.
2. Context7: Uma ferramenta que fornece documentação atualizada e exemplos de código para mitigar alucinações em relação a assinaturas de API e caminhos de módulos.

O estudo avalia 15 modelos de fronteira (incluindo GPT-5.5, Claude Opus 4.7/4.8, Qwen 3.7-Max, variantes do DeepSeek e outros) em um subconjunto curado de 133 problemas de nível de pesquisa derivados do benchmark RealMath. O conjunto de dados foi refinado para incluir apenas problemas com soluções algoritmicamente verificáveis (numéricas ou expressões simbólicas) adequadas para o SageMath.

Protocolo de Avaliação

A avaliação compara duas condições para cada modelo:

1. Baseline Sem Ferramentas (Tool-Free): Raciocínio direto sem ferramentas externas.
2. Configuração de Agente Aumentada por Ferramentas: Raciocínio iterativo com acesso ao SageMath e Context7 (limitado a 15 chamadas de ferramenta por problema).

Pipeline de Validação:
Para lidar com a complexidade da equivalência simbólica, um pipeline de validação híbrido é empregado:

• Validador Simbólico: Compara a saída do modelo com a verdade fundamental (ground truth) usando SymPy. Se a diferença simplificar para zero, a resposta é aceita.
• LLM-as-a-Judge (LLM como Juiz): Casos rejeitados pelo validador simbólico são reavaliados por três LLMs de fronteira (Claude Opus 4.7, GPT-5.5, Gemini 3.5 Flash) via votação majoritária para capturar expressões matematicamente equivalentes, mas estruturalmente diferentes.

Principais Contribuições

1. Avaliação de Uso de Ferramentas em Agentes: Um estudo empírico demonstrando que o acesso a um CAS melhora significativamente o desempenho em problemas de nível de pesquisa. O estudo isola o efeito do feedback simbólico verificável através de ablação controlada.
2. Refinamento de Benchmark: Um refinamento do benchmark RealMath, introduzindo um pipeline de pós-processamento de múltiplos estágios para filtrar problemas computáveis e um processo de normalização assistido por LLM para verificação simbólica executável.
3. Análise de Erro e Comportamento: Uma análise granular de falhas de execução, dinâmicas de recuperação e rastreios de chamadas de ferramentas, revelando padrões comportamentais distintos entre agentes eficazes e ineficazes.

Resultados

Ganhos de Desempenho

• Melhoria Geral: O acesso às ferramentas melhorou a taxa de resolução de todos os modelos avaliados, com um ganho médio de +9,7 pontos percentuais (pp).
• Amplitude de Ganhos: Os ganhos variaram significativamente, de +1,5 pp (Kimi K2.7) a +27,8 pp (Qwen 3.7-Max, subindo de 42,1% para 69,9%).
• Modelos Abertos vs. Fechados: Modelos de pesos abertos ganharam significativamente mais em média (+15,3 pp) comparados aos modelos fechados de fronteira (+6,5 pp), em grande parte devido a baselines sem ferramentas mais fracas. No entanto, o acesso ao CAS reduziu a lacuna de desempenho entre modelos abertos e fechados.
• Melhores Desempenhos: GPT-5.5 alcançou a maior taxa de resolução de 75,2% com o menor uso de tokens entre as configurações habilitadas para ferramentas. Opus 4.8 seguiu com 73,7%.

Eficiência e Uso de Tokens

• Ineficiência de Tokens: Um maior gasto de tokens não correlacionou com maior precisão. As configurações habilitadas para ferramentas variaram de ~34k a ~556k tokens por problema.
• Inversão de Eficiência: Em problemas solucionáveis por todos os modelos na configuração sem ferramentas, os modelos de pesos abertos foram os mais eficientes em termos de tokens. No entanto, em problemas solucionáveis apenas com ferramentas, modelos fechados (GPT-5.5, Opus 4.7/4.8) tornaram-se os mais eficientes, enquanto os modelos de pesos abertos caíram para o último lugar do ranking.

Padrões Comportamentais

• Comprimentos de Rastro Bimodais: As execções dos agentes são fortemente bimodais. Modelos fortes (Opus 4.7, GPT-5.5) tipicamente resolvem problemas dentro das primeiras 3 a 4 interações de ferramenta, usando ferramentas primariamente para verificação. Modelos mais fracos frequentemente esgotam o orçamento total de 15 chamadas, buscando soluções através da computação.
• Dinâmicas de Recuperação: A capacidade de recuperar de falhas de chamada de ferramenta variou mais do que as taxas de falha brutas. Modelos fortes recuperaram-se de falhas 69–77% das vezes, enquanto modelos mais fracos (ex: Sonnet 5) recuperaram-se apenas 16% das vezes.
• Tipos de Erro: O modo de falha dominante foi TypeError (786 instâncias), refletindo o tratamento incorreto do sistema de objetos do Sage, em vez de erros de sintaxe. NameError foi comum em modelos que falharam em manter o estado do interpretador entre as chamadas.

Achados Específicos de Domínio

• Combinatória: Apresentou o maior ganho médio (+18,7 pp), consistente com o suporte maduro do SageMath.
• Teoria de Grupos: Permaneceu como a categoria mais difícil; embora ganhos tenham sido observados, nenhum modelo excedeu uma taxa de resolução de 44%, e o acesso às ferramentas às vezes reduziu as pontuações para modelos específicos (ex: GPT-5.5).
• Tipos de Resposta: Modelos geralmente performaram melhor em problemas numéricos do que em expressões simbólicas. O acesso às ferramentas reduziu significativamente essa lacuna para modelos fracos em manipulação simbólica (ex: Qwen ganhou +36 pp em expressões).

Significância e Alegações

Os autores alegam que agentes aumentados por CAS representam uma direção promissora para auxiliar matemáticos na exploração computacional. O estudo demonstra que:

1. Feedback Verificável é Crítico: O acesso a um CAS permite que os agentes refinem o raciocínio através de experimentação iterativa, emulando efetivamente um ciclo de pesquisa em matemática computacional.
2. Descoberta de Conjecturas: O estudo de caso de um problema de nó de toro torcido ilustra que os agentes podem reproduzir elementos chave do fluxo de trabalho de um matemático: computar objetos intermediários, identificar padrões, formular conjecturas e validá-las através de parâmetros.
3. Passo para a Automação: Este trabalho é apresentado como um passo para a descoberta automatizada de conjecturas, sugerindo que a computação simbólica executável pode estender substancialmente as capacidades de raciocínio prático dos modelos de fronteira além da prova pura de teoremas.

O artigo conclui que, embora os sistemas atuais sejam limitados em problemas que exigem profundo insight teórico ou conhecimento contemporâneo especializado, os ganhos observados indicam que integrar LLMs com motores simbólicos é um caminho viável para avançar a matemática experimental.