Pesquisadores apresentam o EasyProver, um sistema que usa agentes de IA para provar ou refutar afirmações em Lean, uma linguagem para escrever provas que podem ser verificadas por máquinas. Eles também apresentam o Aegis, um benchmark que transforma problemas de programação competitiva em tarefas de verificação vinculadas a implementações em Rust.
Na avaliação dos pesquisadores, o EasyProver provou 1.054 das 2.000 afirmações do Aegis selecionadas, com um limite de 30 minutos por afirmação. O artigo também relata pontuações altas em benchmarks consolidados de demonstração de teoremas, que, segundo os pesquisadores, estão perto da saturação.
Por que importa
Para equipes de software que consideram usar verificações formais em código Rust, o Aegis oferece tarefas que incluem detalhes como conversões de inteiros e comportamento em caso de falha; ainda não se sabe se o EasyProver consegue verificar o próprio código dessas equipes com eficiência.
