Onderzoekers presenteren EasyProver, een systeem dat AI-agenten inzet om stellingen in Lean te bewijzen of te weerleggen. Lean is een taal voor het schrijven van bewijzen die machinaal kunnen worden gecontroleerd. Ook introduceren ze Aegis, een benchmark die opgaven uit programmeerwedstrijden omzet in verificatietaken die gekoppeld zijn aan Rust-implementaties.
In de evaluatie van de onderzoekers bewees EasyProver 1.054 van de 2.000 geselecteerde Aegis-stellingen binnen een limiet van 30 minuten per stelling. Het artikel meldt ook hoge scores op bestaande benchmarks voor het bewijzen van stellingen. Volgens de onderzoekers liggen die scores dicht bij het maximaal haalbare.
Waarom het ertoe doet
Voor softwareteams die formele controles van Rust-code overwegen, bevat Aegis taken met details als conversies tussen integer-typen en gedrag bij fouten. Of EasyProver hun eigen code efficiënt kan verifiëren, is nog niet bekend.
