マサチューセッツ大学アマースト校が率いるコンピューター科学者のチームは最近、ソフトウェアのバグを防ぎ、基礎となるコードが正しいことを検証するために使用できる全体証明を自動的に生成する新しい方法を発表しました。

Baldur と呼ばれるこの新しい方法は、大規模言語モデル (LLM) の人工知能の力を活用しており、最先端のツールである Thor と組み合わせると、66% 近くという前例のない有効性が得られます。このチームは最近、ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering で優秀論文賞を受賞しました。

「残念なことに、私たちはソフトウェアがどこにでもあり、私たち全員が毎日それを使っているにもかかわらず、ソフトウェアにはバグがあると予想するようになりました」と、マサチューセッツ州アマースト校マニング情報コンピュータ科学大学の教授であり、この論文の先輩でもあるユーリー・ブラン氏は言う。著者。

バグのあるソフトウェアの影響は、迷惑なフォーマットの不具合や突然のクラッシュから、重大な問題を引き起こす可能性のあるものまで多岐にわたります。セキュリティ侵害または使用される高精度ソフトウェア宇宙探査またはヘルスケア機器の制御用。

もちろん、ソフトウェアが存在する限り、ソフトウェアをチェックする方法はありました。よく使われる方法の 1 つは最も単純です。人間にコードを 1 行ずつ調べてもらい、エラーがないことを手動で確認してもらいます。または、コードを実行して、期待される動作と照らし合わせてチェックすることもできます。たとえば、ワードプロセッサ ソフトウェアが「Return」キーを押すたびに改行することを期待していても、代わりに疑問符、コード内の何かが間違っていることがわかります。

どちらの方法にも問題はあります。人的ミスそして、考えられるすべての不具合をチェックすることは、非常に時間と費用がかかり、些細なシステム以外では実行不可能です。

より完全ではありますが、より困難な方法は、数学的証明コードが期待どおりに動作することを示し、定理証明器を使用して証明も正しいことを確認します。この方法はマシンチェックと呼ばれます。

しかし、これらの証明を手動で書くのは信じられないほど時間がかかり、広範な専門知識が必要です。「これらの証明は、ソフトウェア コード自体よりも何倍も長くなる可能性があります」と、マサチューセッツ州アマースト大学の博士論文の一部としてこの研究を完了した論文の筆頭著者であるエミリー ファースト氏は言います。

ChatGPT が最も有名な例である LLM の台頭により、考えられる解決策は、そのような証明を自動的に生成することを試みることです。ただし、「LLM の最大の課題の 1 つは、LLM が常に正しいとは限らないことです」と Brun 氏は言います。「クラッシュして何かが間違っていることを知らせる代わりに、彼らは『黙って失敗する』傾向があり、不正確な答えを導き出しながらも、それが正しいかのように提示します。そして、多くの場合、黙って失敗するのが最悪のことです。」

ここでバルドルが登場します。

まず、そのチームは Google で作業を行い、自然言語テキストの大規模なコーパスでトレーニングされた LLM である Minerva を使用し、それを 118 GB の数理科学論文と数式を含むウェブページで微調整しました。

次に、数学的証明が記述される Isabelle/HOL と呼ばれる言語で LLM をさらに微調整しました。次に、Baldur は証明全体を生成し、定理証明者と連携してその動作をチェックしました。定理証明者がエラーを検出すると、その証明とエラーに関する情報を LLM に送り返し、その間違いから学習して、できればエラーのない新しい証明を生成できるようにします。

このプロセスにより、精度が大幅に向上します。プルーフを自動的に生成する最先端のツールは Thor と呼ばれ、57% の確率でプルーフを生成できます。Baldur (北欧神話によれば、Thor の兄弟) が Thor とペアになると、2 人は 65.7% の確率で証拠を生成できます。

まだかなりの程度の誤差はあるものの、Baldur はソフトウェアの正しさを検証するために考案されたこれまでで最も効果的かつ効率的な方法であり、AI の機能がますます拡張され洗練されるにつれて、Baldur の有効性も高まるはずです。

紙は出版されたの一環として第 31 回 ACM 欧州合同ソフトウェア エンジニアリング会議およびソフトウェア エンジニアリングの基礎に関するシンポジウムの議事録。

詳細情報:Emily First 他、Baldur: 大規模な言語モデルを使用した完全証明の生成と修復、第 31 回 ACM 欧州合同ソフトウェア エンジニアリング会議およびソフトウェア エンジニアリングの基礎に関するシンポジウムの議事録（2023年）。DOI: 10.1145/3611643.3616243