Claudeが123のOSSライブラリでアセンブリレベルの形式検証を完遂
LLMs are making formal software verification feasible at a much larger scale
AnthropicはTheoremとの共同研究で、Claudeを使い123の実世界のオープンソースライブラリについてRISC-Vのアセンブリコードレベルでセキュリティ特性を証明した。既存のファズテストを仕様に変換し、任意の64MB未満の入力でクラッシュしないことを約1億8000万行のRocq証明で示した。証明の過程でClaudeは数年にわたり検出されなかったバグを発見し、自ら修正している。
Linuxカーネルは、今日最もよくテストされたソフトウェアの一つであり、世界中の数十億台のデバイスに展開されているにもかかわらず、最近1,000件以上の脆弱性が開示された。
HNでの議論
232- yazaddaruvala
むしろ逆のことが起きると思う。LLMはLLMが生成した命令型スタイルのコードを形式的に検証したりはしないだろう。我々（エージェント開発を含む）は命令型言語から離れ、関数型を飛ばして決定論的宣言型言語へと移行する。おそらく、SQLのためのTypescriptに似た実験的言語が多数出現し、命令型言語と同じ結果を簡潔に表現するための、はるかに微妙な演算子を備えるだろう。それらはゲーム開発やLinuxカーネル（Linusが同意するわけないけど笑）で高性能に動作するようにコンパイルされ、さらに分散実行エンジン上で実質的に共有メモリ空間を持って実行できるようになる。これにより、はるかに簡潔な成果物が可能になる。ハルシネーションの可能性が低減し、出力トークンが減り、思考ループの反復が減り、人間がレビューするのに十分簡潔になる（必要な領域では）。さらに、関数の能力を大幅に制限する定理のような構文、おそらく検証のための高レベルなエフェクトシステムのようなものが追加される。これは「暗号関数の定数時間コンパイル」や、ローカルコンテキストでの読み書きに対する「ACID準拠の保証」、分散実行エンジン上の関数に対する「ちょうど一度だけの配信の保証」など、多くのことに使われる。その時点で、すべてのプログラムはデフォルトで形式的に検証されるようになる。AdaErlangSQL+++とでも考えればいい。
- jaykru
付録[0]から：「エージェントが書いた証明は、同じ定理の他の証明と同様に『優れて』いる。つまり、等価性定理を証明している。しかし、エージェントがこの冗長な証明スタイルをより複雑なプログラムに直接スケールできるかはまだわからない。MachCSLのような他のエージェントベースの検証プロジェクトの経験は、答えはノーかもしれないことを示唆している。エージェントは冗長な証明スタイルで複雑さの壁にぶつかり、スケールアップするには証明をより良いモジュール抽象化と推論原則の周りに構造化する必要がある。もしそうなら、エージェントが正しい抽象化を発見し導入してこの複雑さを軽減するのをどう支援できるか？これには専門の証明エンジニアの入力が必要か、それともスケーラブルな証明を可能にする良い抽象化をエージェントが発見するのを導く共通原則を抽出できるか？」最近のLLMの証明の公開で数学者の中には同様のパターンを観察し、LLMは人間の数学の凸包を超えたところで数学的能力の壁にぶつかると示唆している。形式的検証で行われる種類の証明は、LLMの推論にとってかなり興味深いリトマス試験紙だ。なぜなら、考慮されるシステムは必ずしも分布内にあるわけではないからだ（数学では、扱う「システム」や構造、それらに関する証明が何千もの個別の書籍に登場するのと比較して）。そのため、広範なドメイン知識で事前学習されたLLMが人間に対して持つ優位性は、それほど大きなものを買わない。私の意見では、この観察は[…]
- malisper
懐疑的な人向けに言うと、私はPostgresのRust書き換えで形式的検証を使ってかなりの成功を収めている。RustとCのコードをLeanに変換できるコンパイラを書いた。両方の関数がLeanに入ったら、LLMにそれらが同一に動作するというLeanの証明を書かせる。これまでに、コードの約12%がシングルスレッドで実行されたときに同じ動作をすることを証明した。これはおよそ7万行のCコードに相当する。これにより、プラットフォーム間で浮動小数点演算が異なる結果を生む可能性があるなど、非常に軽微な動作の違いが見つかった。これをスケールアップする方法を模索中だが、これ以上スケールできない根本的な制限は見当たらない。
- fedupnow
私は35歳で、彼らが思い通りにしたら終わりだ。私は職人にはならない。27歳で建設業を辞めたのは、プログラミングが大好きだったからだ。建設業で働くのは毎日ほとんど自殺したい気分だった。あまりにひどかったので20代を酒で潰した。今は何年も禁酒しているが、それは完全にプログラミングのおかげで、自分のやっていることを本当に愛しているからだ。しかしこの会社は、いろいろな意味でそれを私から奪おうとしている。私は人生の多くと全貯蓄をこの転身に投資した。今は毎日、Anthropicが回りくどい方法で停止問題を解決すると主張しているから電気技師になれと怒鳴られている。彼らは主張することを実際にやる必要すらない。業界の20%を説得すればいいだけで、私のような人間は引退できるほど長く働く機会を永遠に得られない。彼らが成功するとは本当に思わないが、もし成功したら、私は公共図書館でコーディングするホームレスになるだろう。もう一からやり直すつもりはない。
- sestep
ここ数週間、仕事でこれをやっている。エージェントがSIMDやCUDAを使ってある関数を高速化する実験を示すPRを開き、そのPRに元の実装と動作が等価であるというRocqの証明が含まれているので、自信を持ってマージできるのは非常に強力だ。
- pinevale
何に対して形式的検証するのか？意図された入力も意図されない入力も、すべてのステークホルダーの利益も、考えうるすべてのユーザー行動もカバーする、あの捉えどころのない100%カバレッジの形式的仕様に対して？バイブコーディング時代に？いや、このページはそれが存在しないことを認める良識がある。結局、彼らは従来のファザーでクラッシュを見つけ、クラッシュを修正し、そして…クラッシュが修正されたという形式的証明を書くことに落ち着くのか？それは…かなり無意味に思える？何か見落としているのだろうか？
- Olscore
家を建てるには3つの層がある：
1. ビジョン：何が欲しいか（我々の意図）
2. 設計図：書いた仕様（我々の設計）
3. 検査：建てたものを設計図と照合する（証明）
この研究は検査をほぼ完璧にする。しかし検査は設計図だけをチェックし、我々のビジョンはチェックしないので、間違った設計図から建てられた家でも完璧な検査に合格できる。残りの半分は、設計図が我々の意図と一致し、エージェントが建てている間もそうであり続けることを保証することだ。私はそれに取り組んでいるので、これは補完的だと思う：
- passive
これは高い可能性のように思えたが、これまでのソフトウェアへのLLMの採用は主にベストプラクティスを捨てるためだったので、検証の拡大につながるとは懐疑的だ。ベゾスが、従業員にボトルに小便をさせながら、週3日労働になると語るようなものだ。