Forskarna presenterar EasyProver, ett system som använder AI-agenter för att bevisa eller motbevisa påståenden i Lean, ett språk för att skriva maskinkontrollerbara bevis. De presenterar också Aegis, ett benchmark som omvandlar problem från tävlingsprogrammering till verifieringsuppgifter kopplade till Rust-implementationer.
I forskarnas utvärdering bevisade EasyProver 1 054 av 2 000 utvalda Aegis-påståenden inom en tidsgräns på 30 minuter per påstående. Artikeln rapporterar även höga resultat på etablerade benchmark för teorembevisning, som forskarna säger närmar sig mättnad.
Varför det spelar roll
För mjukvaruteam som överväger formella kontroller av Rust-kod erbjuder Aegis uppgifter som omfattar detaljer som heltalskonverteringar och felbeteende. Det är fortfarande oklart om EasyProver effektivt kan verifiera deras egen kod.
