AIが難解な数学の証明を検証する未来に一歩近づきました。
500ページ超えの大学院レベルの数学教科書を約3万体ものAIエージェントで1週間かけて「機械が検証できる形（Lean）」に書き直した、という報告。
Metaなどの研究チームが約10万ドルかけて実施しました。
そもそもなぜこんなことをするのか。
背景には、数学の査読が抱えてきた悩みがあります。
論文の証明は年々長く複雑になり、査読者がすみずみまで検証しきれないまま世に出ることも珍しくありません。
証明をコンピュータが読める形に書き直しておけば、正しさは機械が保証してくれます。ただしこれを人手でやるのはあまりに大変なので、AIの群れで一気に肩代わりできるかもしれない、という方向性が今回示されています。
作り方が面白く、AIエージェントたちは人間のソフトウェア開発チームと同じようにGitでコードを共有し、互いのプルリクエストをレビューし合いながら進めました。
書き手、証明係、レビュー係、雑務係といった役割分担を行っています。
今回できあがったのは約13万行、5900件の定理や定義からなるコードで、本に出てくる340個の主要な定理・定義はすべて証明まで通っているそうです。
費用の約10万ドルは高いと思うかもしれませんが、人間の専門家チームを雇って同じことをやるのと同等か、むしろ安いくらいで、研究チームは今後さらに3〜10倍の効率化が見込めるとしています。
