Исследователи представили EasyProver — систему, в которой ИИ-агенты доказывают или опровергают утверждения на языке Lean, предназначенном для написания доказательств, проверяемых компьютером. Они также разработали Aegis — набор тестов, преобразующий задачи по конкурентному программированию в задания на проверку реализаций на Rust.
В ходе оценки EasyProver доказала 1 054 из 2 000 выбранных утверждений Aegis, уложившись в лимит 30 минут на каждое. В статье также сообщается о высоких результатах на известных тестах для систем автоматического доказательства теорем. По словам исследователей, эти результаты близки к предельным.
Почему это важно
Командам разработчиков, которые рассматривают возможность формальной проверки кода на Rust, Aegis предлагает задания, учитывающие такие нюансы, как преобразование типов целых чисел и поведение при сбоях. При этом пока неизвестно, насколько эффективно EasyProver сможет проверять их собственный код.
