革新的なAIシステム、バグなしのソフトウェア検証で有望

従来、ソフトウェアコードの検証は、手動のコードレビューや異常を特定するためのコード実行を伴う、労働集約的なプロセスでした。これらの方法は価値がありますが、人間の誤りに対して脆弱であり、複雑なシステムには非現実的です。

Baldurが登場しました。これは、大規模言語モデル（LLM）の力を活用して数学的証明を自動的に生成するように綿密に設計されたソリューションです。広範な数学的内容および証明に使用されるIsabelle/HOL言語でLLMをファインチューニングすることで、Baldurはかつて困難であったタスクの自動化に向けて大きな一歩を踏み出します。その結果？ 定理証明器と連携してコードの正しさを検証し、エラーマージンを大幅に削減するシステムが誕生しました。

Baldurの成功の核心には、証明の自動生成を担当するツール「Thor」とのパートナーシップがあります。Thorは57%の成功率を誇りますが、Baldurと組み合わせることで、両者は証明の生成において驚異的な65.7%の精度を達成します。北欧神話にインスパイアされたこのダイナミックなデュオは、AI駆動のソフトウェア検証の可能性を示しています。

LLMにおける課題

ChatGPTなどのLLMを扱う際に遭遇する主な課題の一つは、その正しさが時折欠如していることです。警告を発するのではなく、「静かに失敗」し、有効に見える誤った結果を提供することがあります。AI生成の証明の信頼性を確保するには、この問題に対処することが不可欠です。

Baldurの開発は簡単な作業ではなく、数ヶ月とGoogleとの共同作業を要しました。プロジェクトの筆頭著者であるEmily Firstは、Minerva、膨大な自然言語テキストのコーパスで訓練されたLLMを使用しました。その後、Minervaは、数学的および科学的な論文、および数学的表現を含むウェブコンテンツからなる118GBの大幅なデータセットでファインチューニングされました。しかし、重要な違いは、Isabelle/HOL言語をさらにファインチューニングし、包括的な数学的証明の生成の基盤を整えた点にあります。

Baldurのエラー修正へのアプローチは巧妙です。定理証明器が生成された証明内のエラーを特定すると、この情報をBaldurにフィードバックし、システムがミスから学習できるようにします。この反復プロセスは証明の精度と信頼性を高め、コード検証において非常に効果的なツールとなります。

バグなしのソフトウェアへの有望な未来

改善の余地はありますが、Baldurは形式化されたソフトウェア検証にとって有望な道筋を表しています。エンジニアは依然としてソフトウェアの開発を担当しますが、今や彼らには、数学的証明の作成を自動化できる強力な味方、Baldurがいます。

UMass AmherstのManning College of Information and Computer Sciencesの教授であるYuriy Brun氏は、「私たちの仕事は、これらの証明の作成を自動化することを目指しています。Baldurは大規模言語モデルを使用して、数学的定理が与えられた場合、その定理の証明を自動的に生成し、それを定理証明器が検証できるようにします」と述べました。

Baldurの成功は、このプロジェクトのために休むことなく努力した dedicated なチームに起因します。Emily Firstに加え、当時Googleに雇われていたMarkus Rabe、およびイリノイ大学アーバナ・シャンペーン校の助教であるTalia Ringerが大幅に貢献しました。このプロジェクトは、高度研究計画局（DARPA）および国立科学財団（NSF）の支援を受けました。

Baldurのような革新的なソリューションは、テクノロジー業界がソフトウェアシステムの絶え間なく増大する複雑さと格闘する中で希望を提供します。AIの能力が進化し成熟し続ける中で、Baldurがソフトウェアの正しさを新たな高みへ導く可能性は有望です。