宇宙船のバグも逃さない！1000行超えの巨大プログラムをAIで守る新技術

いや、全然違うよ。LoCは『Lines of Code』、つまりプログラムの行数のことだ。これは大規模なプログラムにバグがないか、AIを使ってどうやって数学的に証明するか、っていう硬い論文だよ。

それが意外と難しいんだ。プログラムが大きくなると、AIも一度に全部を理解できなくなるし、関数同士の複雑なやり取りを正確に把握して『仕様』を作るのは、今のLLMでも限界があるんだよ。

そうだね。形式検証では『この入力のときは、こう動かなきゃダメ』っていう厳密なルール（仕様）が必要なんだけど、これを人間が書くのはめちゃくちゃ大変なんだ。そこでこの論文が提案しているのが『Preguss』っていうフレームワークだよ。

名前の由来はともかく、中身は『分割統治』っていう賢いやり方なんだ。まず、静的解析っていうツールを使って、プログラムの中で『ゼロで割り算しそう』とか『メモリが溢れそう』っていう危ない場所（実行時エラー、RTE）を先に見つけるんだ。

その通り。それが第一段階の『Divide（分割）』。次に、その危ない場所ごとに、LLMを使って『ここがエラーにならないための条件』をピンポイントで作らせるんだ。これが第二段階の『Conquer（攻略）』だね。

そう。しかも、ただ仕様を作るだけじゃなくて、静的解析の結果をヒントにLLMに指示を出すから、精度がすごく高いんだ。実験では、人間が手作業で検証する手間を8割以上も減らせたらしいよ。

実際に使われている宇宙機の制御システムを調べたら、プロでも気づかなかったバグを6つも見つけたんだって。宇宙でエラーが起きたら大変だから、この成果はかなり大きいよ。

いや、まだ課題はあるよ。今は主に実行時エラーを防ぐのがメインだし、もっと複雑な『意図通りの機能か』っていう検証には、さらに高度な仕様生成が必要になる。それに、LLMが間違った仕様を作っちゃう可能性もゼロじゃないからね。

そこまで行くとSFだけど、ソフトウェアの信頼性を高めるための大きな一歩なのは間違いないね。これからは、もっと巨大なシステムにも対応できるように研究が進むはずだよ。

それはただの『賞味期限切れチェック』だろ。さっさと片付けなさい。