Resumo Técnico: MATHCONSTRAINT

Declaração do Problema

O avanço rápido dos Modelos de Linguagem de Grande Escala (LLMs) no raciocínio matemático e algorítmico tornou os benchmarks estáticos cada vez mais obsoletos. Conjuntos de dados fixos sofrem de saturação, onde os modelos alcançam rapidamente pontuações altas, e de contaminação, onde dados de treinamento se sobrepõem aos conjuntos de teste. Isso é particularmente agudo para tarefas de raciocínio combinatório, que exigem verificação rigorosa e frequentemente envolvem problemas NP-difíceis, onde uma única violação de restrição invalida uma solução. Os benchmarks existentes dependem ou de coleções de instâncias fixas que envelhecem rapidamente, utilizam verificação heurística "LLM-como-julgador", ou carecem da capacidade de escalar continuamente a dificuldade em sincronia com as melhorias dos modelos.

O artigo identifica a necessidade de uma infraestrutura de avaliação que possa gerar instâncias frescas, difíceis e automaticamente verificáveis sob demanda, em vez de um lançamento único de conjunto de dados.

Metodologia

Os autores apresentam o MATHCONSTRAINT, um gerador de benchmark adaptativo e uma estrutura de avaliação projetada para testar sob estresse as capacidades de raciocínio combinatório dos LLMs.

1. Estrutura de Geração Adaptativa

O MATHCONSTRAINT opera como um loop gerador-verificador, e não como um conjunto de dados estático.

• Famílias de Problemas: O sistema recorre a um registro de 39 tipos de problemas parametrizados que abrangem programação por restrições (por exemplo, BIBD, quadrados latinos, n-rainhas) e construção de grafos (por exemplo, grafos de Ramsey, coloração de cliques, k-colorabilidade).
• Verdade Terrena Apoiada por Solucionador: Cada instância é codificada usando solucionadores de back-end (pycsp3 para programação por restrições e pysms para SAT/simetrias módulo). Um solucionador de referência determina a polaridade correta (SAT/UNSAT) e, para instâncias satisfatíveis, gera uma testemunha verificada.
• Dificuldade Adaptativa: A dificuldade é controlada por meio de intervalos de parâmetros (por exemplo, tamanho do grafo, contagem de restrições) e não por conjuntos de teste fixos. A estrutura inclui um "filtro de admissão de falha na fronteira": uma instância candidata só é admitida no benchmark se pelo menos um modelo de fronteira falhar em resolvê-la. Isso garante que o benchmark permaneça discriminativo à medida que os modelos melhoram.
• Verificação: A avaliação baseia-se em contratos formais. Para alegações de SAT, a solução submetida pelo modelo é injetada como restrições unitárias rígidas na codificação original e re-solucionada. Para alegações de UNSAT, apenas a polaridade é verificada. Isso evita a dependência de LLMs para julgar suas próprias saídas.

2. Interface de Avaliação e Uso de Ferramentas

A estrutura avalia os modelos sob duas condições:

• NO_TOOLS (SEM_FERRAMENTAS): O modelo deve emitir uma resposta JSON final diretamente.
• TOOLS (FERRAMENTAS): O modelo opera em um ambiente Python isolado com acesso a solucionadores genéricos SAT/SMT (pysat, z3, pycosat). O modelo pode intercalar raciocínio com chamadas execute_python (até um orçamento de 8 rodadas) antes de chamar submit_answer.

3. Métricas

• Precisão: Definida como a porcentagem de instâncias onde a saída do modelo (polaridade e testemunha, se aplicável) passa pelo verificador baseado em solucionador.
• Precisão SAT: A precisão de identificar corretamente a satisfatibilidade (polaridade), independentemente de a testemunha ser válida.
• SIM@k: Uma métrica de replay que truncar as trilhas registradas de uso de ferramentas para um máximo de $k$ rodadas para medir a sensibilidade aos orçamentos de ferramentas.

Principais Contribuições

1. Estrutura MATHCONSTRAINT: Um gerador de benchmark adaptativo que produz problemas parametrizados de programação por restrições e estilo grafo/SAT com rótulos certificados por solucionador e testemunhas verificadas por verificador.
2. Conjuntos de Dados Adaptativos: O lançamento de dois conjuntos de dados demonstrando a eficácia da estrutura:
   • MATHCONSTRAINT-EASY: 266 instâncias (25 tipos) onde modelos de fronteira alcançam 72,6%–87,6% de precisão sem ferramentas.
   • MATHCONSTRAINT: 329 instâncias (39 tipos) com parâmetros mais difíceis, onde os mesmos modelos caem para 18,5%–66,9% de precisão, demonstrando resistência à saturação.
3. Avaliação de Uso de Ferramentas: Uma avaliação abrangente de 12 modelos de fronteira e de peso aberto em configurações sem ferramentas e com ferramentas habilitadas. O estudo destaca que o acesso a ferramentas não é meramente um detalhe de implementação, mas uma capacidade distinta, elevando a precisão média em 28 pontos percentuais no benchmark difícil.
4. Métrica SIM@k: A introdução de uma métrica de replay de orçamento de ferramentas mostrando que reduzir o orçamento de ferramentas de 8 para 4 rodadas pode eliminar até 37 pontos percentuais de precisão, revelando que a orquestração eficaz de computação externa é uma dimensão crítica da capacidade de raciocínio.

Resultados

• Resistência à Saturação: A transição de MATHCONSTRAINT-EASY para MATHCONSTRAINT restaurou com sucesso a separação de desempenho entre modelos de fronteira. No benchmark difícil, apenas 3 dos 12 modelos ultrapassaram 50% de precisão sem ferramentas, comparado a 11 dos 12 no conjunto fácil.
• Impacto das Ferramentas: O acesso a um ambiente Python isolado com solucionadores SAT/SMT melhorou significativamente o desempenho.
  • GPT-5.5: Aumentou de 66,9% para 80,9%.
  • CLAUDE-4.6-SONNET: Mostrou o maior ganho, subindo de 18,5% para 70,5% (+52 pontos).
  • Melhoria Média: O acesso a ferramentas elevou a precisão média da coorte de fronteira em 28 pontos percentuais.
• Lacuna da Testemunha: Uma discrepância significativa foi observada entre "Precisão SAT" (identificar corretamente a existência) e "Precisão" total (fornecer uma testemunha válida). Para modelos como CLAUDE-4.6-SONNET, a lacuna foi de 53,5 pontos, indicando que os modelos frequentemente identificam corretamente que uma solução existe, mas falham em construir uma testemunha válida sem assistência de ferramentas.
• Sensibilidade ao Orçamento: A análise SIM@k revelou que o desempenho é altamente sensível ao número de rodadas de ferramentas. Modelos como CLAUDE-4.6-SONNET e GEMINI-3.1-FLASH-LITE mostraram perfis de "ganho tardio", onde a maioria de suas respostas corretas foi alcançada apenas após múltiplas rodadas de uso de ferramentas.

Significado e Alegações

O artigo posiciona o MATHCONSTRAINT não como um ranking estático, mas como infraestrutura de avaliação. Seu significado principal reside em sua capacidade de:

• Escalar com a Capacidade: Ao gerar instâncias dinamicamente com base nas taxas de falha dos modelos, o benchmark evita o problema do "alvo móvel" onde conjuntos de dados estáticos tornam-se triviais.
• Desacoplar Raciocínio do Uso de Ferramentas: A estrutura isola a capacidade de raciocinar sobre restrições combinatórias da capacidade de codificar e executar essas restrições em um solucionador, revelando que os modelos de fronteira frequentemente carecem desta última sem orquestração explícita de ferramentas.
• Quantificar a Eficiência de Ferramentas: O estudo argumenta que o "uso de ferramentas orçado" é uma capacidade de primeira classe. A alta sensibilidade da precisão aos orçamentos de ferramentas (por exemplo, a queda de 37 pontos ao reduzir as rodadas de 8 para 4) sugere que as avaliações futuras devem medir não apenas se um modelo pode resolver um problema, mas quão eficientemente ele coordena a computação externa.

Os autores concluem que, à medida que os modelos dependem cada vez mais de computação externa, as avaliações devem mudar de medir apenas o raciocínio abstrato para medir a coordenação eficaz de busca, verificação e uso de ferramentas sob restrições.