Sistema de IA Inovador Mostra Promessa na Verificação de Software sem Bugs

Tradicionalmente, a verificação de código de software tem sido um processo trabalhoso que envolve revisões manuais de código ou a execução do código para identificar anomalias. Embora valiosas, esses métodos são suscetíveis a erros humanos e impraticáveis para sistemas complexos.

Entre em cena o Baldur, uma solução meticulosamente projetada que aproveita o poder dos Modelos de Linguagem Grande (LLMs) para gerar provas matemáticas automaticamente. Ao ajustar LLMs em conteúdo matemático extenso e na linguagem Isabelle/HOL usada para provas, o Baldur dá um salto gigante em direção à automação do que antes era uma tarefa árdua. O resultado? Um sistema que trabalha em conjunto com provadores de teoremas para verificar a correção do código, reduzindo significativamente a margem de erro.

No coração do sucesso do Baldur está a parceria com o Thor, a ferramenta responsável por gerar provas automaticamente. O Thor possui uma taxa de sucesso de 57%, mas quando combinado com o Baldur, os dois alcançam uma notável precisão de 65,7% na geração de provas. Esta dupla dinâmica, inspirada na mitologia nórdica, demonstra o potencial da verificação de software impulsionada por IA.

Desafios nos LLMs

Um dos principais desafios encontrados ao trabalhar com LLMs, como o ChatGPT, é sua falta ocasional de correção. Em vez de levantar bandeiras vermelhas, eles podem "falhar silenciosamente", fornecendo resultados errôneos que parecem válidos. Abordar essa questão é crucial para garantir a confiabilidade das provas geradas por IA.

O desenvolvimento do Baldur não foi uma pequena façanha, levando vários meses e um esforço colaborativo com o Google. Emily First, autora principal do projeto, empregou o Minerva, um LLM treinado em um vasto corpus de texto em linguagem natural. Posteriormente, o Minerva foi ajustado em um conjunto de dados substancial de 118 GB de artigos matemáticos e científicos e conteúdo da web contendo expressões matemáticas. No entanto, o diferencial chave foi o ajuste fino adicional da linguagem Isabelle/HOL, preparando o cenário para a geração de provas matemáticas abrangentes.

A abordagem do Baldur para a correção de erros é engenhosa. Quando o provador de teoremas identifica um erro em uma prova gerada, ele alimenta essa informação de volta ao Baldur, permitindo que o sistema aprenda com seus erros. Este processo iterativo melhora a precisão e a confiabilidade das provas, tornando-o uma ferramenta altamente eficaz para a verificação de código.

Um futuro promissor para o software sem bugs

Embora haja espaço para melhorias, o Baldur representa uma via promissora para a verificação formal de software. Os engenheiros ainda são responsáveis pelo desenvolvimento do software, mas agora eles têm um poderoso aliado na forma do Baldur, capaz de automatizar a criação de provas matemáticas.

Yuriy Brun, professor do Manning College of Information and Computer Sciences da UMass Amherst, observou: "Nosso trabalho foca em tentar automatizar a escrita dessas provas. O Baldur usa grandes modelos de linguagem para, dada uma teorema matemática, gerar automaticamente uma prova desse teorema que um provador de teoremas pode então verificar."

O sucesso do Baldur é atribuído à equipe dedicada que trabalhou incansavelmente neste projeto. Juntamente com Emily First, Markus Rabe, que o Google empregou na época, e Talia Ringer, professora assistente na Universidade de Illinois—Urbana Champaign, contribuíram significativamente. A Agência de Projetos de Pesquisa Avançada de Defesa (DARPA) e a Fundação Nacional de Ciências (NSF) apoiaram o projeto.

Soluções inovadoras como o Baldur oferecem esperança enquanto a indústria de tecnologia lida com a complexidade crescente dos sistemas de software. Com as capacidades da IA continuando a evoluir e amadurecer, o potencial do Baldur para elevar a correção do software a novos patamares permanece promissor.