AIを使ってDafnyプログラムの検証を改善する

コーディングの世界では、バグって夏のピクニックでうざい蚊みたいなもんだよね。チクチクして良い日を台無しにしちゃう。フォーマル・バリフィケーションはソフトウェアがちゃんと動くことを確実にするためのカッコイイ方法で、バグに悩まされる可能性を減らしてくれるんだけど、そのバリフィケーションを受けるのは結構お金がかかるから、多くの人が古いやり方を続けちゃうんだ。たとえバグの危険があってもね。

Dafnyはそんなカッコイイバグキャッチャーみたいなもんだ。プログラムのバリフィケーションを楽にするよ。でも、これを最大限に活かすには、アノテーションっていう追加情報を入れる必要がある。アノテーションは、Dafnyキャッチャーにコードについて教える小さなメモみたいなもんだ。残念ながらほとんどのプログラマーは、これらのメモを作るためのフォーマルロジックや戦略の専門家じゃない。そこで、私たちの頼もしいAI、いわば「コーディングのフェアリーゴッドマザー」が登場するってわけ。

#フェアリーゴッドマザー：AIとDafny

私たちは、スーパー賢いチャットボットみたいな大規模言語モデル(LLM)の頭脳と、いくつかの賢い検索技術を組み合わせて「Dafnyアノテーター」っていうツールを作ろうとしてる。このツールは、Dafnyプログラムにアノテーションを振りまいて、すべてが問題ないか確認するんだ。まるで魔法の助手が君の仕事を見て、「あ、ここにこれを追加して！」って言ってくれるみたいな感じ。

私たちのちょっとした実験では、この魔法のツールをDafnyプログラムのコレクションに試してみた。初めの結果はちょっと期待外れで、成功率はわずか15.7%。まるで猫に「持ってこい」って教えるみたいに、時間がかかるんだ。でも安心して！改善する計画があるから。

#データが多ければ楽しい

フェアリーゴッドマザーのパフォーマンスがうまくいかなかった理由の一つは、Dafnyプログラムの例が足りなかったから。音楽を聞かずに鳥に歌わせようとするようなもんだ。だから、自分たちでプログラムを作ることにしたんだ。それをDafnySynthって名付けた。

DafnySynthは、私たちのLLMが遊んで新しいDafnyプログラムを生成できる遊び場みたいなもんだ。たくさんの遊び心あふれる例を作ることで、AIがもっといい学習ができるようにする。ロボットが実際には動かないおかしなプログラムを作るのを想像するのは楽しいけど、私たちはちゃんとしたコードで、バリフィケーションテストに合格するものを作ってるよ。

#成功のための微調整

合成例を集めた後は、AIのスキルを微調整する時間だ。これはフェアリーゴッドマザーにちょっと追加のトレーニングを与えるようなもんだ。新しいデータセットと古いデータセットを使ってトレーニングしたら、モデルの成功率が50.6%に上がった。前よりもずっと多くのサムズアップだね！

#アノテーションを探して

論理的なアノテーションを追加するために、私たちのツールは3つのプロセスを経て動く。まず、LLMを使って新しいアノテーションを提案する。「これいいメモだ！」って叫んで、次にそれをどこに入れるか考える。もしその提案がうまくいかなかったら、勝つ組み合わせを見つけるまでやり続ける。頑固な瓶を開けようとする友達みたいにね。

このプロセスがどう機能するか詳しく見てみよう。

1. アノテーション提案：AIが候補アノテーションを作成する。まるで子供がシャレードでいろんな推測をしてるみたいだ。

2. 挿入：いろんな場所に各候補アノテーションを試す。まるでスパゲッティを壁に投げて、くっつくかどうかを見てるみたいだ。

3. 貪欲選択：成功した組み合わせが見つかれば、それを選んで次に進む。ダメなら、元のプログラムをバックアップとして残す。

この体系的なアプローチがAIに何がうまくいくか、何がいかないかを学ばせて、正しいアノテーションを与えるチャンスを増やすんだ。

#失敗から学ぶ

さらに改善するために、既存のアノテーション付きプログラムを集める。これは、自転車の乗り方を他の人を見て学ぶのに似てる。何がうまくいくか、何がダメかをメモするみたいなね。AIがアノテーションの提案をした時、既存のアノテーションを取り除いてトレーニングデータセットを作る。この作業がAIに何を追加する必要があるかを理解させるんだ。

#編集グラフで遊び場を作成する

さあ、ここからちょっとワクワクする。子供たちがレゴの城を一つずつブロックを積み上げて作るように、プログラムも一連の小さな編集を通じて作られるべきだと私たちは思ってる。AIは、Dafnyバリファイアの助けを借りて、初期コードを取り、それに徐々に変更を加えていく。これを「編集グラフ」と呼んでる。

このグラフのノードは、さまざまな編集やコンセプトを示し、エッジはあるアイデアが別のアイデアにどうつながるかを示してる。たとえば、最初は「数字が完全平方数かどうかをチェックするプログラム」って簡単なアイデアから始まって、そこから一歩ずつ外側に広がって、最終的には完全なDafnyメソッドに至るんだ。

このプロセスのエディターたちは、小さな助手の役割を果たす。あるエディターが高レベルのアイデアを提案したり、別のエディターがそれをシンプルで動くプログラムに変えたりするんだ。そして、プログラムがバリフィケーションテストに合格しなかったら、アノテーターが登場してアノテーションを適用し、ゴールに達成しようとする。

#トレーニングデイ：成功率

こんなに頑張った後、私たちはツールをテストにかけた。いろんなモデルとトレーニングセットを使って、その効果を確かめたよ。最初のLLMは苦戦して、成功率はわずか15.7%だった。でも、微調整や合成データの追加を重ねるごとに成功率が上がっていった。

たとえば、合成データだけで微調整した後、成功率は27.7%に上がった。両方のデータセットを組み合わせたら、成功率はなんと50.6%に到達。まるでシャイな友達がダンスフロアに出てきてバックフリップを決めたみたいだ！

#LLMと伝統的な言語

さて、どうして私たちがLLMに注目してるか疑問に思うかもしれない。LLMは次の大きなものとして注目されてるけど、例が豊富じゃない言語には魔法をもたらさないこともあるんだ。ほとんどのLLMはPythonみたいな人気のある言語でトレーニングされてるから、たくさんの例がある。でも、Dafnyみたいな新しい言語やあまり人気のない言語にはそれが少ない。

実際、私たちが求めるアノテーションは、大きな言語には存在しないんだ。でも、実際のコーディングと私たちが生成した合成データを組み合わせることで、LLMが学べる良い例を作ることができた。まるで友達に初めて自分のお気に入りの料理を紹介するかのように、ちょっとした体験が必要なんだ！

#支援の未来

全体の流れとして、私たちの作業はプログラマーがDafnyや似たような言語でバリファイされたプログラムを書くのを楽にすることを目指してる。LLMとバリフィケーションツールの組み合わせが、バグを遠ざけてコーディングを少し楽にする未来への道を開くかもしれない。

自分のプログラムを書いて、ちょっとしたAIの魔法で自動的にバリファイされて、デバッグの時間を節約できる世界を想像してみて。私たちは、正しいツールとトレーニングがあれば、これが現実になると信じてるよ。

#結論：前進するバズ

結論として、バグはいつも私たちを悩ませるけど、DafnyアノテーターみたいなAIツールを使えばそれを抑える手助けになる。論理的なアノテーションを自動化することで、バリファイされたプログラミングを楽にしようとしてるんだ。

旅はまだ終わってない。もっと学ぶことがあって、改善も必要だけど、一歩一歩進むことで、コーディングとバリフィケーションが手を取り合って、より信頼できるソフトウェアの景観を作る未来に近づいていける。もしかしたら、いつか猫に「持ってこい」を教えることができるかもしれないね！