Resumo Técnico: Lean como Juiz Controlado por Risco para Raciocínio Matemático em Linguagem Natural

1. Declaração do Problema

O artigo aborda o desafio de utilizar assistentes de prova formais (especificamente Lean) como juízes para o raciocínio matemático em linguagem natural gerado por Modelos de Linguagem de Grande Escala (LLMs). Embora uma prova Lean bem-sucedida forneça forte evidência positiva para uma afirmação formal, a ausência de uma prova é um sinal ambíguo. Uma prova falha pode indicar uma resposta matematicamente incorreta, mas também pode resultar igualmente de uma formalização mal tipada, fatos de biblioteca ausentes ou expiração de tempo na busca por provas.

As abordagens atuais frequentemente tratam a falha de prova como um sinal negativo de correção, arriscando a confusão entre incorreção matemática e falta de cobertura formal. Os autores identificam um "penhasco de cobertura": a confiabilidade da seleção formal depende agudamente da proporção de respostas candidatas que podem ser formalizadas e provadas com sucesso. Quando a cobertura é alta, a seleção formal é altamente precisa; quando a cobertura é baixa, o sinal torna-se pouco confiável.

O problema central é determinar quando um sistema downstream deve confiar em um sinal formal Lean e quando deve tratar o sinal como fora de cobertura (ou seja, não resolvido) em vez de incorreto, ao mesmo tempo que fornece uma garantia de risco de amostra finita para as respostas aceitas.

2. Metodologia: COVCAL

Os autores propõem o COVCAL (Lean Calibrado por Cobertura), um wrapper seletivo controlado por risco que decide se deve aceitar uma resposta formal ou abster-se com base em diagnósticos de cobertura.

2.1 Framework de Observação Parcial

O sistema trata o pipeline formal como um mecanismo de observação parcial. Ele não observa a verdade de cada resposta candidata, mas observa apenas:

1. Quais classes de respostas normalizadas atingem uma afirmação Lean bem-formada (Cobertura Tipada).
2. Quais dessas classes são provadas com sucesso (Cobertura Provada).
3. O peso da classe provada de maior peso versus o rival não resolvido de maior peso (Margem Formal).

Uma classe de resposta é definida como um grupo de strings candidatas que denotam a mesma resposta final (por exemplo, $1/2$, $0.5$, $2/4$). Classes que não são formalizadas ou não são provadas são consideradas não resolvidas, não automaticamente erradas.

2.2 Diagnósticos de Cobertura

O COVCAL calcula quatro métricas-chave para um problema dado $x$:

• Cobertura Tipada ($C_{typ}$): O peso total das classes candidatas que atingiram uma afirmação Lean bem-formada (status: proved, typechecked ou timeout).
• Cobertura Provada ($C_{prf}$): O peso total das classes candidatas que receberam uma prova verificada pelo kernel.
• Massa de Rival Não Resolvido ($R_{unres}$): O peso da classe de resposta de maior peso que não foi provada.
• Margem Formal ($M$): A diferença entre o peso da classe provada de maior peso e a massa do rival não resolvido.

2.3 Seleção e Certificação

O COVCAL aceita a classe provada de maior peso apenas se uma regra pré-declarada baseada em limiares $(\tau_{typ}, \tau_{prf}, \tau_M)$ for satisfeita. Se a regra não for atendida, o sistema se abstém (ou recua para um método não formal, como consistência própria).

Para garantir a confiabilidade, o COVCAL emprega certificação de risco seletivo de amostra finita. Ele garante que, com probabilidade $1-\delta$, o risco seletivo (taxa de erro) das respostas aceitas seja no máximo $\epsilon$. Dois regimes de certificação são propostos:

1. Regime de Bonferroni: Busca sobre uma grade de limiares em uma divisão de calibração e aplica uma correção de limite de união ($\delta/|T|$) para contabilizar as múltiplas comparações. Isso é conservador e requer alta densidade de sinal para ser viável.
2. Regime Dev-then-Cal: Seleciona o limiar em uma divisão de desenvolvimento independente e o certifica uma vez na divisão de calibração usando um único limite de Clopper-Pearson ($\delta$). Isso é mais eficiente em termos de amostra, mas requer separação estrita entre os dados de desenvolvimento e calibração.

2.4 Limites Teóricos

O artigo prova que, sem diagnósticos de cobertura (ou seja, confiando apenas na existência de uma prova), nenhum certificado de correção pontual não-vazio pode ser derivado se existir uma classe rival não resolvida e inequivalente. A falta de evidência formal não é evidência de falsidade matemática; é evidência de status não resolvido.

3. Contribuições Principais

1. Caracterização do Penhasco de Cobertura: No conjunto de dados MATH-500, os autores demonstram que a resposta "vencedora da prova" está correta em 96% das vezes em alta cobertura provada, mas apenas em 20% em baixa cobertura. Isso estabelece que as provas Lean são confiáveis apenas quando a cobertura e a margem são altas.
2. Esparsidade e Fidedignidade do Sinal: O sinal formal é esparso e imperfeito. Um auto-formalizador de 7B prova uma classe para apenas 28% dos problemas. Além disso, uma auditoria manual revela que apenas $\approx 43\%$ dessas provas são fidedignas ao problema original (o restante são identidades triviais ou afirmações verdadeiras, mas irrelevantes).
3. Método COVCAL: Um framework de previsão seletiva que certifica o risco sob observação parcial. Ele lida explicitamente com a assimetria da falha de prova e fornece garantias de amostra finita para previsões aceitas.
4. Viabilidade Dependente do Formalizador: O artigo demonstra que a viabilidade do certificado é governada pela cobertura de auto-formalização. Um formalizador de 7B gera um sinal muito esparso para o regime conservador de Bonferroni (rejeitando todas as 20 partições bootstrap), enquanto um formalizador especializado em provadores (Goedel-Prover-V2-8B) alcançando 79% de cobertura torna o método viável em 17/20 partições.

4. Resultados Experimentais

Os experimentos foram conduzidos em um subconjunto filtrado do MATH-500 (378 exemplos) usando Qwen2.5-Math-7B para geração e vários formalizadores para auto-formalização.

• Desempenho de Linha de Base: A consistência própria sozinha alcança 91% de precisão sem abstenção.
• Desempenho do COVCAL:
  • Sob o regime de Bonferroni com um formalizador de 7B, o método rejeita todas as entradas (0/20 partições) porque o sinal é muito esparso para satisfazer o limite de união estrito.
  • Sob o regime dev-then-cal com o formalizador de 7B, 12/20 partições são certificadas. A fração aceita é $\approx 21\%$, com uma precisão aceita de 0,93.
  • Com o Goedel-Prover-V2-8B (formalizador especializado), a cobertura provada sobe para 79%. O Bonferroni torna-se viável em 17/20 partições, aceitando $\approx 48\%$ dos problemas com 0,98 de precisão aceita.
• Auditoria de Fidedignidade: Uma auditoria manual de 45 exemplos estratificados mostrou que, embora 73,6% das afirmações provadas fossem não triviais e corretas, apenas 43% eram fidedignas à afirmação do problema. Muitas afirmações "provadas" eram fatos secundários verdadeiros ou identidades triviais que não capturavam as restrições do problema.

5. Significado e Alegações

O artigo alega que sua contribuição principal é uma conta precisa de quando e com qual formalizador um sinal formal parcial pode ser confiável sob controle de risco, em vez de simplesmente melhorar a precisão bruta.

• Controle de Risco sobre Precisão Bruta: Como a consistência própria já é 91% precisa, o valor do COVCAL reside em sua capacidade de fornecer um certificado para o subconjunto de respostas que aceita, distinguindo entre "verificado" e "não resolvido" em vez de "correto" e "incorreto".
• Tratamento de Observações Parciais: O trabalho reformula a verificação formal como um problema de previsão seletiva onde provas ausentes são tratadas como candidatos não resolvidos, prevenindo a rotulagem incorreta de raciocínio correto como incorreto devido a falhas de formalização.
• Dependência de Especialização: Os resultados destacam que a escala bruta do modelo não é um substituto para a especialização. Um formalizador especializado em provadores supera significativamente um modelo generalista maior em termos de cobertura de prova, que é a restrição vinculativa para o controle de risco certificável.

Os autores concluem que o COVCAL serve como uma interface conservadora para usar o Lean como juiz: é viável e informativo apenas quando o auto-formalizador cobre massa de resposta suficiente para suportar um certificado de risco, mas não garante que todas as respostas sejam verificadas.