研究とモデル 2026年10月23日

今日 · 研究記事 10 月 22 日

Claude、OSS がクラッシュしないと証明——前提あり

Anthropic によれば、Claude は 123 のオープンソースライブラリの 239 のファジングのエントリポイントで、64 MB 以内のどんな入力でもクラッシュしないことを証明した。対象は RISC-V の機械語にコンパイルした実行ファイルで、証明には前提条件がある。 ファジングは、大量のランダムな入力をプログラムに当て、クラッシュを起こす入力を探す試験の方法である。Anthropic と提携先の Theorem は、これらの試験を証明すべき命題に書き換えた。どんな入力を与えてもクラッシュは起きない、という命題だ。証明は数学の推論ですべての入力を覆う。試験が示せるのは、試した入力で誤りが出なかったことまでである。Anthropic の記事の該当箇所はこうだ。「Claude successfully patched the bugs it found and then proved that there are no crashes on any input (up to 64 MB) for 239 entry points across 123 different OSS-Fuzz libraries.」（Anthropic、2026-10-22）。

前提は三つある。プログラムがシングルスレッドの静的実行ファイルであること。メモリ予算が決まっていること。RISC-V の Linux 上で動くこと。

証明は約 1.8 億行である。証明検査器 Rocq が機械で検査し、人の審査には頼らない。Anthropic によれば、信頼すべきものとして残るのは、RISC-V と Linux のプロセスの形式モデル、命題そのもの、Rocq だけである。これらのライブラリにバグがないという意味ではないと、Anthropic は明記している。証明の過程で数百のバグが見つかり、Claude は先に修正してから証明した。

費用の面では、証明に数億トークンを使う。数字はすべて Anthropic の自己申告で、Anthropic は独立の検証のために証明の一部を公開した。この種の証明では、どの部品を信頼すればよいかがはっきりする。証明する性質はクラッシュしないことで、プログラムが正しく動くことではない。広く使われるかどうかは数億トークンの費用次第だと、本紙は読む。 どう確かめたか →