Resumo Técnico: Nem Todas as Provas são Iguais: Avaliando a Qualidade de Provas de LLM Além da Correção

Declaração do Problema

Embora os Grandes Modelos de Linguagem (LLMs) tenham demonstrado uma capacidade significativa de gerar provas matemáticas corretas, os atuais benchmarks de avaliação focam quase exclusivamente na correção. Esse foco singular negligencia dimensões críticas da qualidade de uma prova que são essenciais para a utilidade matemática, como clareza, concisão, insight e transferibilidade. Uma prova pode ser formalmente correta, mas ser excessivamente verbosa, depender de cálculos exaustivos e tediosos, utilizar técnicas obscuras inacessíveis ao público pretendido ou falhar em se adaptar a restrições metodológicas específicas. Além disso, os benchmarks existentes frequentemente tratam todas as provas corretas como igualmente valiosas, falhando em capturar as substanciais variações estilísticas e estruturais entre elas. O desafio reside em definir e medir essas qualidades subjetivas de uma maneira escalável e automatizada, sem depender de uma avaliação humana cara ou inconsistente.

Metodologia: PROOFRANK

Para abordar essas lacunas, os autores introduzem o PROOFRANK, o primeiro benchmark projetado especificamente para avaliar proxies escaláveis da qualidade de provas em matemática gerada por LLMs. O benchmark consiste em 382 problemas de competição desafiadores de resposta final, abrangendo álgebra, geometria, combinatória, cálculo e teoria dos números. O uso de problemas de resposta final permite a verificação escalável da correção, mantendo, ao mesmo tempo, a exigência de provas escritas rigorosas.

O framework de avaliação baseia-se em comparações pareadas de soluções corretas para evitar a dificuldade de atribuir pontuações absolutas através de diversos problemas. A correção é tratada como um pré-requisito; os modelos são comparados apenas em problemas onde ambos produzem soluções válidas. O PROOFRANK avalia cinco métricas complementares, categorizadas em dois tipos:

1. Métricas de Nível de Prova (Comparando provas individuais)

• Concisão: Medida via compressibilidade. Um modelo de raciocínio forte tenta encurtar uma prova enquanto preserva a equivalência lógica. A métrica é a razão entre o comprimento do texto original e o comprimento do texto encurtado. Razões menores indicam maior concisão (mais texto redundante removido).
• Facilidade Computacional: Avalia o quanto uma prova depende de álgebra tediosa, enumeração ou verificação de casos. Um juiz LLM compara pares de provas para determinar qual exige menos "tempo de acompanhamento" devido à densidade de notação e ao cálculo explícito.
• Simplicidade Cognitiva: Mede a acessibilidade das técnicas de prova utilizadas. Avalia a complexidade das ideias centrais, a sofisticação das ferramentas (ex: teoremas de nicho vs. métodos padrão) e a dificuldade de integrar múltiplos conceitos.

2. Métricas de Nível de Problema (Comparando o comportamento do modelo em múltiplas tentativas)

• Diversidade: Quantifica a habilidade de um modelo de produzir abordagens válidas distintas para o mesmo problema. As soluções são agrupadas por técnica (usando resumos gerados por LLM), e a diversidade é medida pela entropia da distribuição do modelo sobre esses agrupamentos.
• Adaptabilidade: Avalia se um modelo consegue produzir uma prova correta enquanto adere a uma técnica especificada solicitada no prompt. Isso testa a habilidade do modelo de seguir restrições e explorar caminhos matemáticos específicos.

Sistema de Classificação: Os resultados pareados são agregados em classificações de nível de modelo usando um modelo de Bradley-Terry, produzindo pontuações estilo Elo. Esta abordagem mitiga os vieses inerentes à pontuação absoluta e lida com grafos de comparação incompletos onde os modelos não resolvem todos os problemas.

Principais Contribuições

1. Métricas de Estilo de Prova Escaláveis: Os autores definem e implementam um conjunto de cinco métricas (concisão, facilidade computacional, simplicidade cognitiva, diversidade, adaptabilidade) que servem como proxies concretos e mensuráveis para a qualidade subjetiva da prova.
2. Benchmark PROOFRANK: A introdução de um benchmark abrangente composto por 382 problemas de nível de competição, curados para avaliar LLMs além da mera correção.
3. Avaliação Empírica de Modelos de Fronteira: Uma avaliação sistemática de 10 modelos de última geração (incluindo GPT-5.4, Gemini-3.1-Pro, Kimi-K2.5, etc.), revelando distinções claras de forças e fraquezas que são invisíveis para benchmarks de correção pura.

Resultados Experimentais

A avaliação revela diferenças substanciais na qualidade das provas entre os modelos que não são capturadas apenas pela precisão:

• Dominância do GPT-5.4: O GPT-5.4 lidera o benchmark, alcançando a maior precisão (86,4%) e o desempenho superior em três das cinco métricas de qualidade (Facilidade Computacional, Simplicidade Cognitiva e Adaptabilidade).
• Trade-offs e Divergência: Existe uma baixa correlação entre precisão e métricas de qualidade. Por exemplo, o GLM-5 alcança uma precisão razoável (49,1%), mas apresenta desempenho abaixo da média em todas as métricas de qualidade. Inversamente, o QWEN3.5-397B pontua alto em Facilidade Computacional (evitando métodos de força bruta), mas tem a menor precisão entre os modelos avaliados, destacando um trade-off entre elegância e correção.
• Fraquezas Específicas de Modelos: O GEMINI-3.1-PRO performa particularmente mal em concisão, com soluções que são, em média, 3,5 vezes mais verbosas do que o necessário. O KIMI-K2.5-THINK é o modelo mais conciso, mas ocupa o último lugar em Simplicidade Cognitiva.
• Efeitos de Prompting: Experimentos mostram que a concisão é parcialmente controlável via prompting. No entanto, forçar a concisão frequentemente leva a quedas significativas na precisão (ex: queda de ~15% para Kimi e DeepSeek), sugerindo que a otimização de estilo não é uma melhoria "gratuita" e requer um equilíbrio cuidadoso.
• Necessidade de Filtragem de Correção: Quando a filtragem de correção é removida, as classificações mudam drasticamente. Modelos que produzem argumentos simples, porém incorretos (ex: STEP-3.5-FLASH), inflam artificialmente suas pontuações de qualidade, sublinhando que a avaliação de qualidade deve ser pautada pela correção.

Significância e Alegações

O artigo afirma que o PROOFRANK fornece uma expansão necessária do cenário de avaliação para o raciocínio matemático em LLMs. Ao ir além da correção binária, o benchmark revela que os modelos possuem "personalidades de prova" distintas — alguns são rigorosos, mas verbosos, outros são elegantes, mas propensos a erros, e alguns são adaptáveis enquanto outros são rígidos.

Os autores argumentam que estas descobertas são críticas para aplicações práticas:

• Utilidade Educacional e de Pesquisa: Em contextos educacionais, a clareza e o insight de uma prova são tão importantes quanto sua correção. Na pesquisa, a habilidade de gerar provas diversas ou adaptáveis pode auxiliar na exploração de novos caminhos matemáticos.
• Seleção de Modelos: Os trade-offs não triviais entre precisão e métricas de qualidade sugerem que os usuários devem selecionar modelos com base em necessidades específicas (ex: priorizar facilidade computacional para verificação ou diversidade para brainstorming) em vez de confiar apenas em pontuações de precisão.
• Direções Futuras: O trabalho sugere que as avaliações futuras do raciocínio matemático devem medir a utilidade das provas geradas, reconhecendo que uma prova correta não é inerentemente uma boa prova se ela falha em comunicar insight ou transferir para outros contextos.

O artigo permanece modesto quanto às suas limitações, reconhecendo que a qualidade da prova é inerentemente subjetiva e que suas métricas são proxies, não medidas absolutas. Depende de juízes LLM, o que introduz potenciais vieses, embora experimentos de validação extensos sugiram que esses proxies são robustos e alinham-se razoavelmente bem com julgamentos humanos em dimensões específicas como facilidade computacional e simplicidade cognitiva.