Resumo Técnico: FormInv: Um Protocolo de Medição para Invariância Semântica em Benchmarks de Raciocínio Matemático

1. Declaração do Problema

Os benchmarks atuais para raciocínio matemático em Modelos de Linguagem de Grande Escala (LLMs) dependem fortemente de métricas de precisão agregada calculadas em formulações canônicas de problemas. Este artigo argumenta que tais métricas são insuficientes porque assumem que o desempenho do modelo é independente de como uma pergunta é formulada. Os autores identificam uma "lacuna de medição" crítica: os modelos frequentemente exibem alta precisão em benchmarks padrão, mas falham em manter a invariância semântica—a capacidade de produzir respostas consistentes através de paráfrases logicamente equivalentes.

O artigo destaca que os benchmarks padrão (por exemplo, GSM8K, MATH, MathCheck) carecem de verificação rigorosa da equivalência semântica das paráfrases. Consequentemente, os rankings de benchmarks podem ser artefatos de formulações específicas, em vez de medidas verdadeiras da capacidade de raciocínio. Os autores recorrem à teoria psicométrica, especificamente ao Funcionamento Diferencial de Itens (DIF) e à Teoria da Generalizabilidade, para formalizar essa questão. Eles postulam que, se a resposta de um modelo muda com base em reescritas semanticamente equivalentes, isso indica uma falha na compreensão matemática genuína, dependendo, em vez disso, do reconhecimento de padrões superficiais.

2. Metodologia

2.1 O Protocolo FormInv

Os autores propõem o FormInv, um protocolo de medição projetado para auditar e quantificar a invariância semântica. O protocolo consiste em três componentes principais:

1. A Lacuna de Invariância (IG) e a Taxa de Consistência Semântica (SCR):

   • IG: Definida formalmente como o desvio padrão das respostas binárias de um modelo através de uma classe de equivalência de paráfrases. Matematicamente, $IG(f, [x]_\sim) = \sqrt{p(1-p)}$, onde $p$ é a probabilidade de uma resposta correta dentro da classe de equivalência. Uma IG de 0 implica invariância perfeita.
   • SCR: A proporção de teoremas para os quais o modelo responde corretamente em todas as formas de paráfrase. Diferentemente da IG, que mede a variância, a SCR mede a interseção entre correção e invariância.
   • Q de Cochran: Utilizado como teste estatístico para homogeneidade marginal entre $k > 2$ famílias de paráfrases para determinar se a taxa de falha de um modelo varia significativamente por família.

2. A Taxonomia de Paráfrase de 8 Famílias:
   O benchmark avalia modelos através de oito famílias distintas de transformação, categorizadas por seu rigor de verificação:

   • T1 (Certificável Formalmente): Famílias F4 (notação), F6 (ordem), F7 (descompactação) e F8 (equivalência). Estas dependem de regras Lean4/FOL ou verificação via Sistema de Álgebra Computacional (CAS) (por exemplo, SymPy).
   • T2 (Validade Condicional): Famílias F1 (sintática), F2 (quantificador) e F3 (voz passiva). Estas dependem do contexto de tipo e são verificadas via modelos ou CAS quando aplicável.
   • T3 (Heurística): Família F5 (variação de conectivos). Estas dependem de heurísticas de linguagem natural e exigem revisão por especialistas do domínio.

3. Auditoria de Unanimidade Inter-Modelo:
   Um mecanismo de controle de qualidade inovador onde uma paráfrase é sinalizada como semanticamente incorreta se uma supermaioria de modelos (por exemplo, $\ge 6/9$) falhar na paráfrase enquanto passa na versão canônica. Isso aproveita a suposição de que erros sistemáticos na própria paráfrase, e não no raciocínio do modelo, causam falha universal.

2.2 Construção do Benchmark

• Substrato: A avaliação utiliza 103 teoremas curados do Mathlib4 (verificados em Lean4), abrangendo domínios como teoria dos números, álgebra e análise real.
• Conjunto de Dados: O conjunto de dados principal (FormInv v1) contém 760 itens (103 teoremas $\times$ ~7,4 paráfrases). Uma avaliação estendida "Track B" utiliza 100 teoremas mais difíceis do ntp-mathlib (811 itens).
• Verificação: As paráfrases são geradas via GPT-4o e verificadas por meio de um protocolo multiestágio: CAS para famílias algébricas, garantias de modelo para famílias superficiais e revisão 100% por especialistas humanos para famílias definicionais (F7/F8).

2.3 Configuração Experimental

O estudo avalia 9 modelos de ponta (incluindo GPT-4o, Claude Sonnet/Haiku, DeepSeek V3/R1, Gemini 2.5 Flash e Llama 3.3 70B) através de 366–811 itens. Os modelos são avaliados no modo zero-shot com restrições estritas de VERDADEIRO/FALSO.

3. Resultados Principais

3.1 A Lacuna de Invariância vs. Precisão

A descoberta mais significativa é a desconexão entre precisão agregada e consistência semântica.

• Claude Haiku 4.5 alcança 86% de precisão, mas apenas 50% de SCR, o que significa que metade de suas respostas corretas é inconsistente através das paráfrases.
• DeepSeek V3 alcança 96,4% de precisão e 82% de SCR.
• Uma lacuna de 10 pontos na precisão oculta uma lacuna de 32 pontos na SCR. O artigo observa que a precisão, por si só, é "constitucionalmente cega" a essa falha estrutural.
• Há uma forte correlação negativa ($r = -0,965$) entre precisão e IG Média, sugerindo que modelos mais precisos são geralmente mais invariantes, mas essa correlação é algebricamente impulsionada pela definição de IG e não garante invariância para famílias específicas.

3.2 Reversões de Ranking e Complementaridade

Os rankings dos modelos não são estáveis; eles se invertem dependendo da família de paráfrase:

• F6 (Ordem de Comparação): O GPT-4o falha em 0,0% dos itens, enquanto o Claude Sonnet falha em 16,7%.
• F7 (Descompactação Definicional): O Claude Sonnet falha em ~6%, enquanto o GPT-4o falha em 10,0%.
• Este padrão de falha complementar implica que nenhum modelo único domina Pareto todas as famílias. Consequentemente, os designers de benchmarks escolhem implicitamente uma ponderação de famílias que determina o vencedor. O artigo formaliza isso como o corolário "No-Free-Benchmark": para qualquer ranking alvo, existe uma ponderação $\lambda$ sobre as famílias de paráfrase que a realiza.

3.3 Achados da Auditoria de Qualidade

O protocolo de unanimidade inter-modelo identificou com sucesso paráfrases semanticamente incorretas em benchmarks existentes:

• Auditoria MathCheck: Aplicada a 129 grupos no MathCheck, o protocolo sinalizou 4 paráfrases semanticamente incorretas (3,1%). A remoção desses erros deslocou o GPT-4o do rank 2 para o rank 4, elevando o Claude Haiku e o DeepSeek V3.
• Auditoria FormInv v1: O protocolo identificou 11 erros em itens gerados pelo GPT-4o, incluindo excessos de bicondicional, inversões de voz passiva e remoção de contexto de tipo. Esses erros eram invisíveis para avaliação de modelo único, mas expostos pela unanimidade.

3.4 Dependência do Regime de Dificuldade

Na avaliação "Track B" usando teoremas mais difíceis:

• A correlação entre precisão e invariância enfraqueceu ($r = -0,415$, não significativa).
• A dificuldade específica da F5 (variação de conectivos) dissolveu-se; todas as famílias agruparam-se em taxas de falha semelhantes (28–35%).
• Modelos de raciocínio (DeepSeek R1, o4-mini) mostraram a menor IG em teoremas difíceis, sugerindo que a deliberação via Cadeia de Pensamento reduz a sensibilidade superficial apenas quando os teoremas exigem raciocínio de alto nível.

4. Contribuições

1. Framework de Invariância: Formaliza a SCR e a IG como métricas primárias para invariância semântica, fundamentadas no teorema da expectativa condicional de Doob e na teoria DIF. Classifica famílias de paráfrase em níveis T1, T2 e T3 com base no rigor de verificação.
2. Benchmark FormInv: Um conjunto de dados de 760+ itens derivados de teoremas verificados em Lean4, avaliado em 9 modelos com uma auditoria rigorosa de unanimidade inter-modelo.
3. FormInvSelector: Um algoritmo que utiliza perfis de SCR por família para recomendar o modelo com a menor taxa de falha esperada para regimes de tarefa específicos (por exemplo, selecionar um modelo para raciocínio definicional versus tarefas de comparação).
4. Auditoria de Qualidade de Paráfrase: Demonstra que a unanimidade inter-modelo ($\ge 6/9$ modelos falhando em uma paráfrase) é um método automatizado e de baixo custo para detectar itens de benchmark semanticamente incorretos, separando efetivamente erros de benchmark de erros de modelo.

5. Significado e Alegações

O artigo afirma que o FormInv é o primeiro protocolo a aplicar a teoria da invariância de medição e métricas fundamentadas em DIF ao raciocínio matemático formal. Seu significado reside em três áreas:

• Revelando Falhas Ocultas: Expõe que as métricas padrão de precisão podem ser enganosas, escondendo uma "lacuna de 32 pontos" entre o desempenho superficial e a compreensão semântica genuína.
• Integridade do Benchmark: Fornece uma ferramenta para construtores de benchmarks auditar seus próprios conjuntos de dados antes da publicação, impedindo que rankings sejam artefatos de paráfrases falhas. Os autores afirmam que "se você gera paráfrases programaticamente, você não sabe quantas estão erradas".
• Avaliação Consciente do Regime: Desafia a noção de um único "melhor" modelo, demonstrando que os rankings são dependentes do regime (variando por família de paráfrase e dificuldade). O artigo conclui que os designers de benchmarks escolhem implicitamente os vencedores ao selecionar quais famílias incluir, e o FormInv torna essa escolha explícita e auditável.

Os autores permanecem modestos quanto às limitações, observando que a certificação em escala total de todas as paráfrases via Lean4 é trabalho futuro, e que o estudo atual depende de um conjunto curado de 103 teoremas (embora estendido para 100 mais difíceis no Track B). Eles enfatizam que o FormInv é uma métrica suplementar destinada a complementar, não substituir, as avaliações existentes baseadas em precisão.