研究者らは、機械検証可能な証明を書くための言語Leanで、命題を証明または反証するAIエージェントシステム「EasyProver」を発表した。また、競技プログラミングの問題を、Rust実装にひもづく検証タスクに変換するベンチマーク「Aegis」も紹介している。
研究者らの評価では、EasyProverはAegisの命題から抽出した2,000件のうち1,054件を、各命題30分の制限時間内に証明した。論文では、既存の定理証明ベンチマークでも高いスコアを記録したと報告しており、研究者らはそれらのベンチマークは飽和に近いとしている。
なぜ重要か
Rustコードに形式的な検証を導入しようとするソフトウェアチームにとって、Aegisには整数の型変換や失敗時の挙動といった細部を含むタスクが用意されている。ただし、EasyProverが各チームのコードを効率よく検証できるかは、まだ分かっていない。
