Forschende stellen EasyProver vor, ein System, das mithilfe von KI-Agenten Aussagen in Lean beweist oder widerlegt. Lean ist eine Sprache für maschinell überprüfbare Beweise. Außerdem präsentieren sie Aegis, einen Benchmark, der Programmierwettbewerbsaufgaben in Verifikationsaufgaben zu Rust-Implementierungen überführt.
In ihrer Evaluation bewies EasyProver 1.054 von 2.000 zufällig ausgewählten Aegis-Aussagen innerhalb eines Zeitlimits von 30 Minuten pro Aussage. Die Arbeit berichtet zudem von hohen Ergebnissen bei etablierten Benchmarks zum automatischen Beweisen von Theoremen. Laut den Forschenden sind diese Ergebnisse nahe an der Sättigungsgrenze.
Warum es wichtig ist
Für Softwareteams, die formale Prüfungen für Rust-Code erwägen, bietet Aegis Aufgaben, die auch Details wie Integer-Konvertierungen und Fehlerverhalten berücksichtigen. Ob EasyProver den eigenen Code effizient verifizieren kann, ist jedoch noch offen.
