Resumo Técnico: Mask-Proof

Declaração do Problema

Embora os Grandes Modelos de Linguagem (LLMs) sejam cada vez mais capazes de resolução de problemas matemáticos e demonstrações de nível de pesquisa, há uma carência crítica de instrumentos escaláveis e reproduzíveis para medir o raciocínio ao nível de passo em demonstrações longas através de diversas fontes. Os métodos de avaliação existentes sofrem de três limitações primárias:

1. Viés Centrado na Resposta: Benchmarks como GSM8K e MATH focam em respostas finais, falhando em avaliar o rigor do processo de raciocínio intermediário.
2. Graduação por Especialistas de Alto Custo: Avaliar a qualidade de uma demonstração frequentemente exige especialistas humanos, o que não escala e é difícil de reproduzir entre diferentes domínios.
3. Lacunas de Contexto e Dependência: Demonstrações de pesquisa do mundo real dependem de lemas externos, macros e fatos de base não declarados. Mascarar passos sem recuperar essas dependências leva a tarefas subdeterminadas onde as falhas são interpretáveis de forma ambígua (confundindo a capacidade de raciocínio com a falta de informação).
4. Dificuldade de Verificação: A verificação automatizada é dificultada pela diversidade notacional e reformulações equivalentes, tornando a correspondência de strings inadequada e ferramentas simbólicas insuficientes para garantias gerais.

Metodologia: O Pipeline Mask-Proof

Os autores introduzem o Mask-of-Proof, um pipeline de curadoria de dados baseado em LLM projetado para transformar demonstrações de pesquisa heterogêneas em problemas de avaliação de nível de passo, verificáveis e autocontidos. O pipeline opera através de três estágios principais:

1. Coleta de Artigos e Extração de Demonstrações

• Fonte: O pipeline faz a curadoria de submissões recentes do arXiv (agosto–outubro de 2025) para minimizar a contaminação de pré-treinamento.
• Filtragem: Ele extrai fontes LaTeX e filtra demonstrações triviais (ex: puramente definicionais ou completáveis por padrão) para garantir que o raciocínio não trivial seja exigido.
• Auditoria Humana: Todas as instâncias finais passam por auditoria manual por especialistas de domínio para verificar a correção matemática, a suficiência de contexto e a ausência de pistas de atalhos.

2. Curadoria Automatizada de Dados

O pipeline utiliza o Codex CLI para realizar duas tarefas críticas:

• Recuperação Autocontida: O sistema resolve dependências percorrendo referências internas (ex: \ref, \eqref) e expandindo macros definidas pelo usuário. Para dependências implícitas (símbolos definidos em outro lugar), ele busca a declaração de definição na fonte LaTeX e a anexa como "Informação Adicional". Isso garante que o passo mascarado seja solucionável usando apenas o contexto fornecido.
• Mascaramento Agêntico: Em vez de mascaramento aleatório, o pipeline usa um agente para selecionar passos de fórmulas críticas para a inferência. Esses passos são substituídos por um token [MASK]. A rubrica de seleção garante que o passo mascarado não possa ser resolvido por pistas superficiais locais ou correspondência de padrões rasa, forçando o modelo a sintetizar definições globais com variáveis locais.
• Fidelidade: O pipeline desacopla a seleção de passos da aplicação da máscara para evitar a reescrita indesejada da demonstração, garantindo que o texto restante permaneça idêntico ao original.

3. Avaliação Automatizada (Mask-ProofJudge)

• Tarefa: Os modelos são incumbidos de reconstruir o passo da fórmula mascarada.
• Juiz: Um avaliador baseado em LLM (GPT-OSS-120B High) assessa a equivalência semântica entre a saída do modelo e a verdade fundamental (ground truth).
• Redução de Variância: Para lidar com a estocasticidade da geração, o sistema amostra quatro soluções por problema e agrega os julgamentos via votação majoritária.
• Métrica: A métrica primária é o Avg@4, representando a média de correção sobre quatro tentativas independentes.

Principais Contribuições

1. Pipeline Mask-Proof: Um framework reprodutível e automatizado que converte demonstrações de pesquisa do mundo real em tarefas de passo mascarado verificáveis, abordando os desafios do "o que medir" e "como pontuar" na avaliação de nível de passo.
2. Mask-ProofJudge: Um framework de avaliação automática calibrado contra julgamentos de especialistas, alcançando 96,8% de concordância com anotadores humanos através de votação com redução de variância.
3. Mask-ProofBench: Um benchmark composto por 292 problemas curados em diversas áreas de pesquisa (ex: geometria algébrica, topologia, EDPs). Todas as instâncias são auditadas manualmente e projetadas para serem autocontidas.

Resultados Experimentais

Os autores avaliaram 17 LLMs de última geração (padrão e com reforço de raciocínio) no Mask-ProofBench e em um subconjunto de dados cruzados derivado do IMO-ProofBench.

• Fronteira de Capacidade de Raciocínio: Uma fronteira clara de desempenho surgiu em aproximadamente 32% de precisão. Todos os modelos com reforço de raciocínio (ex: GPT-5.2, DeepSeek-R1) excederam esse limiar, enquanto os modelos padrão ficaram abaixo dele. Modelos com reforço de raciocínio superaram seus equivalentes padrão em 12% a 27%.
• Ablação sobre Autocontenção: A remoção do módulo de recuperação de dependência causou uma degradação de desempenho de 11% a 23%, confirmando que a completude do contexto é essencial para uma avaliação válida.
• Ablação sobre Estratégia de Mascaramento: O mascaramento aleatório inflou os escores significativamente (ex: modelos padrão saltando de ~8% para ~50%), eliminando efetivamente a lacuna de desempenho entre modelos de raciocínio e modelos padrão. O mascaramento agêntico mostrou-se necessário para evitar a exploração de atalhos e manter o poder discriminativo.
• Correlação com Especialistas: Quando aplicado ao IMO-ProofBench, o pipeline Mask-Proof alcançou uma correlação de ranking de Spearman de 0,79 com a graduação de especialistas humanos, apesar de não utilizar humanos no loop de pontuação ou rubricas customizadas.
• Reprodutibilidade: Execuções independentes do pipeline mostraram alta consistência na recuperação de dependências (97,2% de recall) e na seleção de máscaras (89,3% de consistência ao contar máscaras semanticamente próximas).

Significância e Alegações

O artigo afirma que o Mask-Proof aborda a "lacuna de medição" na IA para a Ciência ao fornecer um método fiel, reprodutível e comparável para avaliar o raciocínio matemático em nível de passo.

• Escalabilidade: Oferece uma alternativa de baixo custo à graduação por especialistas, permitindo a avaliação de demonstrações de pesquisa em ambiente real.
• Validade: Ao impor contextos autocontidos e mascaramento agêntico, o benchmark mede a inferência genuína em vez da exploração de atalhos ou cópia de contexto.
• Generalização: O pipeline generaliza-se com sucesso para conjuntos de dados externos (IMO-ProofBench), produzindo rankings de modelos que se alinham ao consenso de especialistas sem exigir o design de rubricas específicas de domínio.

Os autores concluem que, embora existam limitações relativas a fontes não-LaTeX e possível vazamento residual, o Mask-Proof estabelece uma fundação para estudar o raciocínio de nível de passo como um fenômeno científico reprodutível, indo além da precisão da resposta final para avaliar o rigor do próprio processo de demonstração.