Los investigadores presentan EasyProver, un sistema que usa agentes de IA para demostrar o refutar enunciados en Lean, un lenguaje para escribir pruebas que pueden verificarse automáticamente. También presentan Aegis, un benchmark que convierte problemas de programación competitiva en tareas de verificación vinculadas a implementaciones en Rust.
En la evaluación de los investigadores, EasyProver demostró 1.054 de los 2.000 enunciados de Aegis seleccionados, con un límite de 30 minutos por enunciado. El artículo también informa de puntuaciones altas en benchmarks consolidados de demostración de teoremas, que, según los investigadores, están cerca de alcanzar su techo.
Por qué importa
Para los equipos de software que estén considerando aplicar verificaciones formales a código Rust, Aegis ofrece tareas que incluyen detalles como las conversiones de enteros y el comportamiento ante fallos. Aún no se sabe si EasyProver puede verificar su propio código de forma eficiente.
