Melhorando a Autoformalização com Filtragem de Verificação de Tipo

Modelos de linguagem grandes (LLMs) mostraram potencial em converter linguagem natural em linguagens formais, um processo conhecido como Autoformalização. Apesar dessa promessa, os métodos atuais enfrentam desafios. Por exemplo, a performance passada no benchmark de formalização ProofNet para o assistente de provas Lean mostrou que apenas 16,1% das declarações informais puderam ser convertidas com Precisão. Da mesma forma, nossos testes com o modelo mais recente, GPT-4o, alcançaram uma taxa de sucesso de apenas 34,9%.

Um problema chave com esses modelos é a falha frequente em produzir declarações formais que passem a Verificação de tipos corretamente. A verificação de tipos garante que as declarações não só sejam sintaticamente corretas, mas também consistentes com os tipos definidos. Um impressionante 86,6% dos erros do GPT-4o vieram de falhas na verificação de tipos.

Para resolver esse problema, propomos um novo método que incorpora filtragem por verificação de tipos. Nosso processo começa gerando um conjunto diversificado de Formalizações para uma determinada declaração informal. Em seguida, usamos o assistente de provas Lean para eliminar quaisquer candidatos que não passem pela verificação de tipos. Combinando esse método com técnicas de autorreferência, aumentamos a precisão das formalizações do GPT-4o em 18,3%, alcançando um novo recorde de 53,2% no benchmark da ProofNet.

#A Importância da Autoformalização

A verificação automática do raciocínio lógico é importante para várias áreas, incluindo matemática, verificação de software, hardware e inteligência artificial. Os assistentes de prova ajudam a expressar claramente as declarações matemáticas e checar suas provas mecanicamente. No entanto, essas ferramentas exigem formalização, ou seja, precisam que declarações matemáticas informais sejam convertidas em linguagem formal.

A autoformalização não é um processo simples, o que levou a uma pesquisa contínua para melhorar os métodos de automação dessa conversão. As soluções mais avançadas atualmente dependem principalmente das capacidades de aprendizado com poucas amostras dos grandes modelos de linguagem ou de tradução reversa destilada. No entanto, essas técnicas mostraram sucesso limitado. Por exemplo, o melhor resultado com Lean 3 no benchmark ProofNet foi alcançado usando o modelo Codex, com apenas 16,1% de taxa de sucesso.

Modelos mais recentes têm melhor desempenho, mas ainda assim carecem de confiabilidade na produção de formalizações corretas. Nossa avaliação do GPT-4o indicou que, embora ele tenha se saído melhor entre os modelos testados, ainda conseguiu converter apenas 34,9% das declarações com precisão para Lean 4.

#Desafios com a Verificação de Tipos

Através da nossa análise, identificamos uma razão comum para a falha entre esses modelos: a incapacidade de passar pela verificação de tipos. A verificação de tipos é crucial, pois avalia se uma formalização usa a gramática e as definições corretamente. Embora a verificação de tipos não garanta uma tradução correta, é um passo necessário e pode ser facilmente automatizado. Descobrimos que a taxa de sucesso da verificação de tipos variou entre 4% e 45,2%, dependendo do modelo e da linguagem formal usada.

Notavelmente, descobrimos que melhorias nas taxas de verificação de tipos correlacionam com uma melhor precisão na tradução de declarações informais. Portanto, nosso objetivo era utilizar o sinal de verificação de tipos dos provadores automáticos de teoremas para aprimorar os métodos existentes de autoformalização.

#Metodologia Proposta

Nossa abordagem inclui três etapas principais: amostragem, filtragem e seleção. Para cada declaração informal e sua correspondente linguagem formal-alvo, geramos primeiro múltiplas formalizações potenciais. O assistente de provas Lean então realiza a verificação de tipos dessas declarações, filtrando aquelas que não passam. A partir dos candidatos restantes, aplicamos heurísticas de seleção para escolher uma única tradução final.

Esse método foi implementado em quatro modelos diferentes usando o benchmark ProofNet com Lean 4. Nossa avaliação manual mostrou que essa abordagem aumentou significativamente a precisão da autoformalização, especialmente com o modelo de melhor desempenho, GPT-4o, que melhorou de 34,9% para 53,2%.

#Avaliação das Técnicas de Formalização

Os métodos de autoformalização devem avaliar rigorosamente seu desempenho. Em nossos experimentos, usamos o benchmark ProofNet, que consiste em diversos exercícios matemáticos de graduação que emparelham declarações informais com suas formalizações correspondentes em Lean 3. Em seguida, fizemos a transição para uma versão Lean 4 do benchmark criada por uma equipe de pesquisa independente.

Testamos vários modelos, incluindo Llemma-7B, Llemma-34B, Llama3-8B-Instruct, GPT-4-turbo e GPT-4o. Cada modelo passou por duas estratégias de adaptação: ajuste fino usando tradução reversa destilada e aprendizado com poucas amostras.

Embora a avaliação manual seja a maneira mais precisa de medir o sucesso, apresenta desafios em escalabilidade. Portanto, também exploramos a correlação entre as taxas de verificação de tipos e a correção, mesmo que isso não possa determinar exclusivamente a validade das declarações formais.

#Principais Descobertas dos Experimentos

Nossos resultados de avaliação revelaram insights significativos sobre a eficácia do nosso método proposto. Notamos que modelos que utilizam filtragem por verificação de tipos, combinados com técnicas de autorreferência, consistentemente superaram métodos de linha de base.

Por exemplo, ao comparar o desempenho de diferentes modelos sob condições idênticas, descobrimos que a filtragem por verificação de tipos não só melhora o desempenho, mas é vital para o sucesso.

#O Papel do Comprimento das Declarações

Uma observação notável foi como o comprimento das declarações formais afeta a precisão. Nossa análise indicou que os modelos tendem a ter dificuldades com formalizações mais longas ao traduzir a entrada informal. As descobertas confirmaram que, embora nosso método tenha melhorado o desempenho em todos os comprimentos, as melhorias foram particularmente notáveis com declarações mais longas.

#Conclusão

Em resumo, desenvolvemos um novo método de autoformalização que se integra com abordagens existentes e melhora significativamente os resultados. Ao focar na verificação de tipos e na seleção de candidatos, nossa técnica provou ser eficaz em aumentar a precisão das formalizações derivadas de LLMs.

Trabalhos futuros podem refinar ainda mais esses modelos aumentando o tamanho das amostras, ajustando o processo de seleção e aprimorando a estrutura geral para uma melhor formalização. Embora este estudo demonstre o potencial para uma autoformalização eficaz, aplicar esses métodos em cenários do mundo real continua a ser um passo importante.

Ao melhorar como os matemáticos podem formalizar sua pesquisa, esperamos contribuir positivamente para os campos de verificação e raciocínio formal, fornecendo ferramentas que aumentem a produtividade sem sacrificar a precisão.