プログラミングの未来を変える？「形式手法（Formal Methods）」の現在地

ソフトウェアのバグをゼロに近づけるための強力な武器として注目されている「形式手法（Formal Methods）」。プログラムの正しさを数学的に証明するこのアプローチは、今後の開発現場のスタンダードになるのでしょうか？その可能性と現実的な課題について掘り下げていきます。

言い換えれば、生成AIが大量のコードを吐き出すようになったからこそ、人間の価値を検証（verification）にシフトさせるべきだという考え方だよね。プログラミングとは一体何なのか、時々考えるよ。実際、英語話者じゃない自分にとって、プログラミングを学ぶこと自体がものすごくハードルが高い。翻訳のない英語ドキュメントを理解するには機械翻訳に頼るしかないし、母国語の資料は5〜6年遅れているような状態だからね。

で、AIが生成する数万行のコードを人間がレビューするのは不可能だから、数学的証明のように絶対的なルールを確立する議論が出てくるのもわかる。Rustのボローチェッカーの話を思い出すね。実際、Rustを何度か書いていると、ボローチェッカーを回避するために小細工を使うという悪習に陥ることがよくあるんだ。

数学的な厳密さが度を越すと、人間はどうにかして抜け道を探そうとするものだ。自分みたいな勉強不足のプログラマーは特にそうなりがち。

こういう試みを振り返ってみると、おそらく特定の定型化された答えのためだけにコードを書く結果になるんじゃないかな。そこまで標準化されてしまうと、人間のニーズに応えられるのか疑問だね。

こういう守りのプログラミング（defensive programming）の試みはいいと思うけど、自分は攻めのプログラミング（ offensive programming：勝手に命名した）がしたいんだ。リスクは取るけど、素早く修正して出荷する。時間をかけて改善していけば十分良くなるはず、と信じるスタイルさ。もちろん、Jane Streetのように精度が重要で、業務範囲が明確に定義されている確立された業界では、この記事のアプローチは正しい。要は、市場の要求を適切にモデル化できるだけのデータが揃っているからね。

でも、自分みたいな金脈を探してあちこち動き回っている社会の負け犬からすると、こうした手法は贅沢品に見える。成熟したモデルを持つ大企業は、最適化を継続するために高度に教育された専門家が必要だろうけど、現実的にそんな要求についていけないのはわかっている。だから、モデル化されていない場所を探しているんだけど、それでも今回のアプローチが使えるのかは自信がないな。

前回のkleppmannの投稿を見てみて。タイプシステムやリンターでチェックできることは、何であれやるべきだというのはその通りだね。

もっと使いやすい方法が出てくるといいんだけど。投稿に挙げられたツールの中だと、DafnyとIrisが一番産業レベルに近いかな。Amazon S3は内部でTLA+を使ってきた歴史があるはず。でも、TypeScriptみたいな「既存のツールに統合できる、コストゼロの抽象化」のような、みんなが自然と昔の方法より好んで使うようなものは、まだこの分野には出てきていない気がする。

（あと、カスタムリンターを書くのも相変わらず結構大変。golangci-lintのコードベースは苦痛だし、semgrepは試してないけどルールエンジンが難しそうだった。今のところ、好きになれるAST APIに出会えていないんだよね）

いつものことだけど、演繹的推論（「形式手法」）を称賛するこの議論は、その根本的な限界を見落としている。前提条件や定義が、対象とするドメインにどれだけ正確に合致しているのか？という点だ（「理論上、理論と実践に違いはない。だが、実践では…」）。Jane Streetが1対1で対応する大規模なコードベースを維持できているのは、そのコードの目的が決定論的なアルゴリズムを実装することだからだろう。他のプログラマーもそういう分野で働いている人は多い。でも、UIや探索的な作業など、多くの仕事はそうじゃない。

形式手法とは別に、論理数学的にではなく、高解像度で受け入れ基準を定義しようとする動きもある。これはマッピングの問題に取り組んではいるけど、「地図は領域そのものではない」という大前提がある以上、完全に解決できるわけじゃない。Googleの検索結果ページは、非常に進化した内部最適化フレームワークで、本当に最適解に到達したと言えるんだろうか？ ぼんやりしたアイデアを形にするために適当に作ったプロトタイプの方が、本質をうまく捉えていたんじゃないか？ こういう問いに対する答えは、システムの外側を見て、そのシステムが何に貢献しているのかを確認しないと見えてこないものさ。

形式仕様（formal specs）の話を読むたびに、「ただ別の方法で同じテストを書いているだけ」あるいはもっと悪いことに「別の方法で同じ実装を書いているだけ」のように思えて仕方ない。

二重に作業をすればミスは減るかもしれないけど、結局はテストや実装と同じバグを抱える可能性があるなら、形式仕様に一体何がそんなに特別なんだろう？

結局の問題の根本は、プログラムが「何をするか」を形式的に証明したければ、その「何」を極めて具体的に定義しなきゃいけない点にあるんじゃないか。そうなったら、結局また一からテストや実装を書いているのと変わらないよね。

もう何年も断続的にこの分野を調べているけど、何か大事なところを見落としているような気がしてならない。でも何が欠けているのかわからないんだ。

誰か教えてくれないか？

18ヶ月ほど前にLLMと型を組み合わせることに目覚めて、6〜8ヶ月前からはlean4に本格的に取り組んでいる。今となっては、実用的なC/C++（つまり何でもできる）FFIを持つCIC証明基盤がない環境で、ソフトウェア開発のAI支援を使うことなんて考えられないな。

JSONからPythonまで全て禁止して、nixを書き換えてコンパイラまで組み込んだ。書くコードのほとんどはプロパティベーステストと徹底的なファジングを繰り返しているだけでなく、最低限.oleanリンクを通じてプロパティテストを動かすための証明をlean4で記述している。余裕があるときは、ドメイン全体を網羅する証明まで行い、それをプロパティテストにかけるんだ。

C++/Rustの面倒な部分は全部スキップしている。なぜなら、高速な処理は全てlean4から生成されるから。C++にバグがあるとしても、それは実際にはlean4コードのバグということになるので、結局どちらでも関係ないんだ。

これはかなりの転換だし、「JSONとPythonを禁止だと！？ありえない！」と懐疑的になる人がいるのも分かる。でも、我々は数百万行規模でこの手法を実践してきた。AIと形式手法の組み合わせは、「AIなし」から「AIとPython」へ移行するよりも、遥かに大きな飛躍だよ。後者は進捗が停滞することもあるが、前者はほぼ確実に進捗が右肩上がりだ。

しかも、かなりエグいこともできる。例えば、ISLやCuTeでモデル化される多面体テンソル計算の形式証明もその一つ。これを使えば、C++23のmdspanを使ってデバイス上でswizzlingやtilingを行い、その正しさを証明できる（カバレッジに関するロピタルの定理的議論はここでは深く触れないけどね: https://github.com/b7r6/mdspan-cute ）。

結果として、まあ、めちゃくちゃ速い。最初の一発目でね。
https://straylight.software/assets/lambda-hierarchy.svg

Jane Streetの貢献もあって、現在の数学の研究にOCamlを採用しようかかなり迷った。結局はLean 4を選んだけどね。LLMがLeanのコーディングをサポートしてくれるようになったから。パフォーマンスは半分ほど犠牲にしたけれど（それもそのうち埋まるだろうし）、各アルゴリズムが最も明確に表現できるのはLeanだと感じている。Leanは美しい言語で、それと比べるとOCamlは古英語のように見えてしまうよ。

Leanはオプションで検証できるように設計されていて、証明が主たる（唯一ではないけど）アプリケーションだ。Jane StreetがLean 4に移行せずにこの方向性を模索し続けるのは、インピーダンス・ミスマッチのように思えるな。

もう何十年も前の話だけど、当時は正当性証明の仕事をしていたんだ[1]。当時のシステムの方が、後年のシステムより証明の自動化が進んでいた側面もあったよ。簡単なものは最初のSATソルバーであるOppen-Nelsonシンプライファーで解けたし、難しいものはBoyer-Moore証明器を使っていた。これはヒューリスティクスと過去の補題を使って定理証明器をガイドする仕組みだ。Boyer-Moore証明器は人間が補題を提案して助けてやる必要があって、それがその後の証明に使われる。ここが人間にとってのきつい仕事だったね。

後のシステムは自動化の度合いが下がったように感じる。形式手法でよく失敗するのは、携わる人たちが形式主義にのめり込みすぎることだ。私は当時、学術的ではなく、バグのないコードを求める商用プロジェクトで働いていたんだけど、学術的なプロジェクトはどうしても小難しくなりがちだった。数学者特有のバイアスで、簡潔な記法を求めてケース分析を疎かにするんだ。あれはいい解決策じゃない。機械的な反復作業を自動化しまくって、人間の洞察に頼る部分を減らすべきなんだよ。頭のいい人たちは、紙と鉛筆での証明の冗長さを避けるために、様相論理や時相論理といった新しい論理を作り続けようとしたけど、実際にはあまり役に立たなかった。
この分野の基本的な真実は、定理のほとんどが極めてありふれたものだということだ。

Jane Streetの連中が指摘するように、言語そのものをコントロールできることには大きなメリットがある。検証の記述はプログラミング言語に統合されているべきだ。多くのシステムではコメントの中に埋め込まれていたり、言語とは別の構文だったり、ひどい場合は完全に別のファイルになっていたりする。これは無駄な労力だ。彼らがこの方向に突き進んでいるのは良いことだと思う。

40年以上前、私たちは既にこの取り組みをしていた。当時、Boyer-Moore証明器を使ってゼロから数論を構築するのに45分くらいの計算時間が必要だったが、今なら1秒もかからないだろうね。
[1] https://archive.org/details/manualzilla-id-5928072/page/n3/mode/2up

最近関連するアイデアをいろいろ試していて語り出したら止まらないんだけど、一つ驚いたのは、フロンティアモデル（特にChatGPT-5.5）が、Roqc（Coq）証明アシスタントでの手動証明の補完に驚くほど効果的だということだ。

証明自体は必ずしも綺麗じゃないけど、私のような証明アシスタントの経験が限られていて、かつ証明対象の補題に関しては一定のドメイン知識があるという人間がやるよりも、ChatGPTなら数分で、しかも10〜100回の反復で証明できることがよくある。

なぜこれが興味深いかというと、従来の形式手法ツールのツールチェーンの前提を覆すからだよ。Frama-CやAda/SPARKなどは、CVC5やZ3で自動的に解消できる証明義務の生成に注力していて、手動証明という苦痛な手段が残されているのが現状だ。一般的なワークフローは、「証明義務が『難しい』（自動解消できない）と判明したら、コード内の見える補題やアサーションを再構成して『簡単』にしようとする」、あるいはコード自体をいじってしまう、というもの。Roqcでの証明はコストが二重にかかる（人間が書くのが難しい上に、コードの進化に合わせてメンテナンスが必要）から、これは合理的だった。でも、もしRoqcの証明が「AIをループに組み込んで自動的に解消」できるなら、コストの差分は消える。人間が読みやすく、明確であることを第一の目標にして、最適化は二の次にするという、普段のプログラミングと同じ感覚で証明を書く未来が見えてくるんだ。

まだその影響を完全に消化しきれてはいないけど、すごくワクワクしているよ。

最高だね。ここ数ヶ月、Scala 3の高度な型システムを使って、コンパイル時に型がより多くの証明を保持するようにシフトしている（マクロを使わずにね）。

エージェントによる「テストの肥大化」を防ぐだけでなく、エージェントが低品質な動作モードに陥るのを防ぐ効果があるみたいだ。最近防いでいる面倒なことの一つに「名詞の増殖」と呼んでいる現象がある。エージェントが、適切にジェネリックにすべきところで、すべてに対して新しい単相的な型を作ろうとすることだ。

私の予想では、堅牢な型システムを持つ言語を含め、形式手法に近いツール群が「まともな品質」のエージェント・コーディングを加速させることになるだろう。

「高度に表現力豊かな型」と言うのは、チームがすでに型レベルプログラミングのトレンドに乗っていない限り、通常のコードベースには入れたくないような手法のことだ（HKTや型関数が基本的な構成要素になっているような環境なら別だけど）。AIエージェントは、知識面ではほとんどの開発者（圏論かぶれの人たちでさえも）よりも「数学」に強い。さらに良いことに、彼らは「無限」の忍耐力があるから、対話を通じて教えるのがすごく得意なんだ。

個人的なことだけど、Codexに趣味の証明をいくつかLeanに書き換えさせたら、めちゃくちゃ簡単だったよ。まあ、それが100%「正解」かは保証できない（もっとLean 4を学んでしっかりチェックしないと）けど、デフォルトで古典的な証明の落とし穴をチェックしてくれているようにも見える。

形式手法の未来にはすごく期待しているよ。

彼はseL4マイクロカーネルに触れているね。仕様書はIsabelleで書かれていて、かなり複雑だ：https://sel4.systems/Info/Docs/seL4-spec.pdf

ボトルネックは、仕様が正しいことを確信することが極めて重要だという点だね。

カーネルのようなものには適さないかもしれないけど、暗号アルゴリズムなんかには用途があるんじゃないか？