I ricercatori presentano EasyProver, un sistema che usa agenti di IA per dimostrare o confutare enunciati in Lean, un linguaggio per scrivere dimostrazioni verificabili automaticamente. Presentano anche Aegis, un benchmark che trasforma problemi di programmazione competitiva in verifiche legate a implementazioni in Rust.
Nella valutazione dei ricercatori, EasyProver ha dimostrato 1.054 dei 2.000 enunciati di Aegis selezionati, entro il limite di 30 minuti per ciascuno. L’articolo riporta inoltre risultati elevati nei benchmark consolidati per la dimostrazione automatica di teoremi, che secondo i ricercatori sono vicini al massimo raggiungibile.
Perché conta
Per i team software che valutano controlli formali sul codice Rust, Aegis propone verifiche che includono dettagli come le conversioni tra interi e il comportamento in caso di errore. Non è ancora chiaro se EasyProver riuscirà a verificare con efficienza il loro codice.
