形式手法とプログラミングの未来
(blog.janestreet.com)- 形式手法は、ソフトウェアが意図した性質を満たしているかを証明するための手法であり、エージェントコーディングの普及によってコストと効用の判断が変わりつつある
- Jane Streetはこれまで、形式手法は一部の特殊なケースを除けばコストに見合う価値が低いと見ていたが、現在は専任チームを立ち上げつつある
- seL4では8,700行のCコードの検証に25人年を要し、コード1行あたり約23行の証明と0.5人日ほどの検証作業が必要だった
- エージェントが生成したコードには、実際にリリース可能な品質との隔たりがあり、検証のボトルネックを減らし、エージェントに強いフィードバックを与える手段として形式手法の重要性が高まっている
- Jane Streetは、言語を深く制御でき、準備の整ったプログラマコミュニティもあるため、OxCamlと証明志向の手法をあわせて発展させる余地があると見ている
形式手法とプログラミングの未来
- Jane Streetはこの25年間、組織として形式手法には関心がないと言ってきたが、もはやその立場を維持していない
- より良いコード、より信頼できるコードを書くための道具の力は以前から重視しており、型システムは大きな恩恵をもたらす軽量な形式手法だと考えてきた
- 特殊なケース、とりわけハードウェア合成を除けば、形式手法はコストが高すぎて大半のソフトウェアには適さないと判断してきた
- seL4は形式検証されたマイクロカーネルであり重要な成果だったが、8,700行のCコードの検証に25人年を要した
- コード1行ごとに約23行の証明が必要で、1行を検証するのに約0.5人日を要した
- セキュリティが重要なマイクロカーネルのように、リスクが高く仕様が比較的明確な場合には、このアプローチには価値がありうる
- しかし大半のソフトウェアには適しておらず、Jane Streetの最も重要なソフトウェアにも当てはまらないと感じていた
- エージェントコーディングの登場によって判断は変わり、形式手法の可能性に対する懐疑は期待へと変わった
- Jane Streetは形式手法チームを立ち上げつつあり、洗練された型システムと同じくらい広く有用なソフトウェア構築ツールにしたいと期待している
なぜ考えが変わったのか
- エージェントコーディングは、いくつもの面で形式手法の従来のコスト・効用構図を揺さぶっている
- だからといって、エージェントが難しい証明を独力で好き勝手に構成できるという意味ではないが、モデルは大きな助けになり、より多くの人が道具を生産的に使えるようにする
- 形式手法の利用は以前より容易になっており、過去の費用対効果の計算を見直す価値が出てきた
-
検証のボトルネックがより重要になっている
- モデルは有用なコードを書くのがますます上手くなっているが、モデルが生成したコードと実際にリリースできるコードの間には大きな隔たりがある
- モデルは与えられた目標を達成することには驚くほど優れている一方、その過程でコードベースの品質を維持または改善するには十分に強くない
- エージェントが作るコードは良くなっているものの、過度に複雑で奇妙なバグや境界ケースが多く、コードベースの中核的な不変条件に従わない傾向がある
- 人間は、エージェントが作ったコードが十分な品質に達しているかを検証するために多くの時間を費やさなければならない
- 形式手法はこの検証負担を減らし、レビュー工程をより効率的にできる
-
エージェントはフィードバックに強い
- エージェントは、強化学習で訓練されるときにも、コーディングに使われるときにも、フィードバックから恩恵を受ける
- 形式手法は、エージェントが難しい問題を解く能力を高める強力なフィードバックの形になりうる
- テストも非常に価値があり、プロパティベーステストやファジングを活用すればさらに良くなる
- ただしテストだけでは十分ではなく、プログラムが取りうる状態空間を網羅するには本質的な限界がある
- OxCamlでのプログラミング経験では、エージェントは型システムが与える普遍的保証から大きな利益を得る
- 型システムがデータレースを防げるなら、データレースを排除できる
- 型をうまく構成してクロスサイトスクリプティング脆弱性を不可能にできれば、単純なテストでは難しい形で脆弱性をなくせる
- 型は、エージェントと一緒にプログラミングするとき、検証のボトルネックを緩和し、より良いフィードバックを提供する
- より強力な証明手法を活用すれば、さらに改善できる余地があるかもしれない
なぜここでやるのか
- 世界中が、エージェントがプログラミングの未来に何を意味するのかを考えており、形式手法とエージェントを組み合わせようとするスタートアップも多い
- Jane Streetは、使っている言語を深く制御できるため、証明志向の手法により適するよう言語を調整できる
- 考えられる方向性はいくつもある
- 性質のモジュール式仕様を型システムに統合できる
- 所有権や可変性のような要素に型レベルの制約を加え、特定の証明を容易にできる
- 証明手法を言語に直接組み込める
-
準備の整ったプログラマコミュニティ
- Jane Streetには、こうした手法を受け入れる準備ができたプログラマコミュニティがある
- プログラミング言語に携わる人にとっては、より良いプログラミングのアイデアを作ることよりも、そのアイデアを実務で使ってもらうことの方が難しい
- Jane Streetでは、約束された新しく見慣れない型システム機能が十分に早く出てこないという理由で、ユーザーが不満を述べることがよくある
- こうした手法を活用できる背景を持つ人が多く、正しい結果と高品質なソフトウェアを作ることへの関心もすでに根付いている
- 積極的で期待の大きいユーザーベースがあることで、短期的な改善と長期的なビジョンの両方を試す自由が得られる
- 短期的な改善は比較的すぐに影響を与えられる
- 長期的なビジョンは、数年がかりで到達するより野心的な目標になる
- 短期的な試みから学びつつ、長期目標に向けて積み上げていける
-
外部ツールとの関係
参加案内
- Jane Streetは London と New York で形式手法関連の人材を募集している
- 現在、そのポジションの面接とチーム作りは初期段階にある
- 今後やるべきことは非常に多く、チームに加わる人を探している
補足
- モデルは複雑な証明を扱う際、依然として人間の助けと指導を必要とする
- 人間のプログラマは、システムがなぜ動くのか、そして高いレベルでどのように証明するかについてのアイデアを持てる
- しかし大半のプログラマは、特定の証明システムを満たす形で証明のアイデアをエンコードする方法を知らない
- モデルは、証明を書く際の技術的な細部に関する多くの反復作業を自動化し、専門性を提供できる
Obj.magicのような抜け道は、型レベルの制約を回避できてしまう- 大半のコードでこうした例外を追跡して禁止すれば、普遍的保証にかなり近い状態を得られる
- 形式手法は、このような抜け道の使用が実際になぜ安全なのかを明示的にできる
1件のコメント
Hacker Newsの意見
数十年前に正しさの証明に取り組んでいて、当時のシステムはその後の多くのシステムよりも証明自動化が進んでいた
易しい部分は最初のSATソルバーであるOppen-Nelson簡約器が解決し、難しい部分はヒューリスティクスと以前の補題を使うBoyer-Moore証明器が担っていた。人間の難しい仕事は、証明器に試させたうえで、その後の証明に使える補題を提案することだった
その後のシステムは自動化が減ったように見え、形式手法が外れた理由は、実務より形式主義にのめり込みすぎたからだと思う。商用プロジェクトでバグのないコードを求めていた立場からすると、学術系プロジェクトは論文向けの簡潔な記法や少ないケース分析を好む数学者バイアスに陥っているように感じられた
実際には大量の自動化された力仕事が必要で、必要な洞察は少ないほうがよい。賢い人たちが紙と鉛筆の証明の冗長さを避けようとして、様相論理や時間論理のような新しい論理を作り続けたが、あまり役に立たなかった。この分野の基本的な真実は、ほとんどの定理はかなり平凡だということだ
Jane Streetの人たちが言うように、言語を制御できることが大きな利点だ。検証文はプログラミング言語の中に統合されるべきで、コメントや別の構文、別ファイルに埋め込まれていると不要な仕事が増える。Jane Streetがこの方向を推し進めているのはよさそうだ
40年以上も前にあまりに早くこの仕事をやっていて、当時はBoyer-Moore証明器で数論をゼロから積み上げるのに計算時間が45分ほどかかったが、今では1秒もかからない
https://archive.org/details/manualzilla-id-5928072/page/n3/m...
論理はコンピュータサイエンスとソフトウェア工学において、物理学・機械工学・土木工学における微積分のような位置にある。LTLや近年の分離論理のようなものは途方もないブレークスルーだった
かなりの人気を得たTLA+ がその証拠で、モデル検査は非常に実用的だ。今おもしろいのは、より重い形式手法、特に定理証明が一般的なシステムソフトウェアでも使えるほど安価になるかもしれないという点だ
関数に対する形式仕様を書き、SAT/SMT、定理証明器、LLMのハイブリッドで合成し、正しさを証明してもらう方式が、そう遠くないうちに標準になるかもしれない
On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf
心配なのは、解読しにくい数学が生まれ、それを少数の信奉者集団が守る状況だ。異なる難解な記法同士は互換性がなく、ひとつを理解しても別のものを理解するのにほとんど役立たないかもしれない。大半の人は、きちんと検証できない英語の文だけを書くことになるだろう
さらに悪いことに、機械に自分の文を形式化させ、その形式主義や証明は理解しないまま検証ごっこに加わり、すべてが破綻したときに驚いたふりをするかもしれない
型システムがすばやく扱えない部分にこうした能力を統合しようと、少しずつ作業を進めているので、この道を先に進んだ人たちの視点に関心がある
よい。ここ数か月、Scala 3で表現力の高い型を使って、型がますます多くのコンパイル時証明を担うように移してきた。マクロは使わないが、いくつかは使える
このやり方は、エージェント型テストが広がっていく問題を減らすのに役立つだけでなく、エージェントが低品質な作業方式に落ちるのも防いでいるようだ。特に、エージェントがある程度一般化すべき場面でも、何にでも新しい単一事例型を作ろうとする名詞の積み上げを防いでいる
良質なエージェントコーディングを加速する方向は、形式手法に似たツール群、強い型システムを持つ言語まで含めた側だと思う
ここで言う表現力の高い型とは、チームがすでに型レベルプログラミングに慣れていないなら、一般的なコードベースには入れたくないような技法を意味する。つまり、高階カインド型や型関数が奇妙な代物ではなく基本ブロックであるチームであるべきだ
エージェントは知識面では大半の開発者より「数学」が得意で、圏論に染まった開発者よりも優れていることすら多い。しかも会話に対して「無限の」忍耐力があると考えれば、教育もかなりうまい
個人的には、Codexに趣味の証明をいくつかLean風に変換させたが、とても簡単だった。100%「正しい」と言うつもりはなく、もっと厳密に確認するにはLean 4をさらに学ぶ必要があるが、基本的には古典的な証明の落とし穴も点検しているようだ。形式手法の未来には大いに期待している
Gen AIが大量のコードを生成するので、人間の価値を検証の側へ移そうという話に見える。プログラミングとは本当に何なのか、ときどき考える。
英語が母語でない立場では、プログラミングを学ぶこと自体が大きな挑戦だ。翻訳されていない英語の文書を理解するには機械翻訳に頼らなければならず、自分の言語の資料は5〜6年ほど遅れている。
いまやAIが作った何万行ものコードをコードレビューするのは不可能なので、数学的証明のような絶対的なルールを立てようという議論が見られる。この記事を読んでRustのborrow checkerを思い出した。実際にRustを何度か使ってみると、人はborrow checkerを避けるために抜け道を使うような悪い癖につながりがちだ。
数学的厳密さが行き過ぎると、人は回避策を探すようになる。私のように教育が十分でないプログラマーは、特にそうなりやすい。
こうした試みは結局、特定の形式化された答えのためだけのコードを書く結果になる気がする。そうして標準化されたとき、人間の要求に対応できるのか確信が持てない。
こうした防御的プログラミングの試みは悪くないが、私の表現で言うなら攻撃的プログラミングをしたい。リスクを取るが、素早く直してデプロイし、時間がたてば十分によくなると信じるやり方だ。
もちろんJane Streetのように正確さが重要で、業務範囲がよく定義された既存産業では、この記事のアプローチが合っている。市場の要求を適切にモデリングできるだけのデータが十分あるからだ。
しかし金を稼ぐために金鉱を探して移動し続ける私のような社会的敗残者にとっては、こうした方法論はぜいたくに見える。成熟したモデリングを備えた既存事業は、高学歴の専門人材が継続的に最適化しなければならないが、現実的にその需要には追いつけないと分かっている。だからモデリングが構造化されていない場所を探すが、そこでもこのアプローチを使えるのかは分からない。
そこでは「直せばいい」は通用しない。何が間違っていたのか理解する頃には、すでに数十億を失っているかもしれない。
だから攻撃的なやり方は、非中核領域では通用しうる。
参考までに、すでにあちこちで防御的なやり方は使われている。PythonやJavaなどにはガベージコレクタがあり、コードが意図通り実行されることがある程度検証されているとも言える。
いつ形式検証が見え始めるのかと思っていたが、実装の詳細を心配する段階から、問題を科学的・数学的に記述する段階へ進むのは自然なことだ。
Gen AIのせいで防御的プログラミングのコストは大きく下がり、人間による検証のコストは大きく上がった。一方で形式手法は検証を安くするが、仕様・型・証明を書き、実装を堅い枠組みに合わせて曲げるなど、実装オーバーヘッドが大きい。
ところがGen AIはその面倒な作業を自動化できる。両者はまさに相性抜群だ。
少し努力は必要だが、継続的な翻訳オーバーヘッドをなくせれば非常に大きな助けになる。
ただ、自分を「社会的敗残者」と呼ぶことや、キャリアの中でこうした実践に従っていないことが、この論点とどう関係するのかはよく分からない。
最近この関連のアイデアをいじっているのだが、驚いたのは最前線のモデル、特にChatGPT-5.5がRoqc、以前のCoq証明支援系で、特定の手動証明をどれだけうまく完成させるかだった。
証明がいつも美しいわけではないが、ChatGPTは、限られてはいるがゼロではない証明支援系の経験と、証明される補題の分野についてかなり大きなドメイン知識を持つ私ならずっと長くかかる作業を、数分、10〜100回の反復以内で証明してしまうことが多い。
この短い文章の文脈でこれが興味深いのは、特定の形式手法ツールが動作する基本前提を揺るがすからだ。Frama-CやAda/SPARKなどは、CVC5やZ3のようなツールが自動的に解消できる証明義務を生成することに集中しており、失敗するとRoqcで手動証明するという、かなり苦痛な代替手段に移る。
よくある流れは、ある義務が「難しい」、つまり自動で解消されないと分かったあと、コードの義務生成地点で見える補題やアサーションの集合を組み替えて「易しく」するか、場合によってはコード自体を変えることだ。
Roqc証明が2倍高価な世界では、それは理にかなっている。人間にとって書くのが難しく、コードや周辺の証明が変わったときの保守のばらつきも大きいからだ。
しかしRoqc証明が「AIをループに入れた自動解消」になるなら、このコスト差は消える。そうなれば証明をコードのように書けるし、人が読みやすい明快さを第一にして、コンパイラや証明器の最適化はずっと後回しにできる。その含意はまだ完全には咀嚼できていないが、かなり興味深い。
証明は扱ったことがないが、「変更後にこのテストが失敗した」と言うと、AIが私の意図どおり既存テストと新しいテストの両方を通るようにコードを直す代わりに、テスト自体を変えてしまうのは時々見たことがある。
これからが楽しみだ。
形式仕様の話を読むたびに、「同じテストを別のやり方で書いている」ように見えるし、もっと悪くすると「同じ実装を別のやり方で書いている」ようにも見える。
二重に書けばエラーを見つける助けにはなるかもしれないが、形式仕様もテストや実装とまったく同じバグを持ちうるのなら、何が特別なのかよく分からない。
根本的な問題は、プログラムが何かをすることを形式的に証明するには、その「何か」を非常に具体的に定義しなければならない点にある。そうなると、実質的にはテストや実装を書き直しているのと同じに見える。
ここ数年、この話題を断続的に追ってきたが、何かを見落としている気がずっとしていて、それが何なのか分からない。誰か説明してくれないだろうか。
テストの欠点は、問題になりうると思った動作しかテストできないことだ。何がまずいか分かっていなかった動作まで先回りして修正するには、道具箱の中でももっと変わった道具が必要になる。ファズテストはその方向への一つの出発点であり、形式検証もまた別の出発点だ。
もちろん、こうした道具の品質は、望ましい動作を許容し望ましくない動作を禁止する包括的な形式モデルをどれだけうまく書けるかにかかっており、多くの分野で私たちはいまだに驚くほどその地点から遠い
たとえば単体テストでは、「foo('abc') は末尾に空白のない文字列を返す」と書ける。
しかし形式手法なら、「任意の入力 x に対して foo(x) は末尾に空白のない文字列を返す」と証明できる。
ささいな例ではあるが、「任意のプログラム P に対して compile(P) は P と同じ動作をする」といった、もっと複雑なものも想像できる。
もちろん、「同じ動作」が何を意味するかは定義しなければならない
設計の性質を指定すると、ツールがさまざまな方法で設計をテストし、その性質に違反しうるかを確認する。
たとえば交通信号を制御するシステムなら、交差する車線が同時に、あるいは一定時間内に両方とも青信号になることはない、という性質を指定できる。
ツールはこれを 完全探索 で確認し、違反するコードトレースを示せる
静的に証明される型システムは、各コンポーネントが他のすべてのコンポーネントと事前に整合するよう検査してくれる。単に「このテストが通る」ではなく、組み合わせたときに「これらすべてのテストが妥当で一貫した全体を成す」ことを保証し、矛盾したモデルがコードに実装されるのを防ぐ。
Rust の
matchが考えうるすべての分岐を完全に扱うことを要求するのを、コードベース全体の規模に拡張したようなものに近い。根本的なロジックや理論の誤りまでは防げないのは確かだ。しかし、たとえば Haskell の型システムと、その場しのぎの関数型テストやプロパティテストを組み合わせたものより、はるかに堅牢であることに驚くかもしれない。これら全体も強力な体系ではあるが、形式的に証明された暗号はさらに高い基準にある
とくに並行性・分散・マルチスレッドの状況で価値が大きい。競合状態やデッドロックはテストも推論も非常に難しく、「A、B、C が A、C、B の順で起こりうるか」のような問題がまさにそうだ。
この分野の成熟は、おおむね次のように進む気がする。第一に、LLM は最初は「二度目に試す」ような事後検証にとどまるとしても、形式手法の学習と利用をはるかに速くするだろう。
第二に、「実装コードが変わったが、モデルを壊したように見えるか？」を LLM が確認する自動化へ移っていくだろう。依然として決定的ではないにせよ、たまにしか変わらない何かを人間がレビューしなければならない状態よりは、ずっとましである可能性が高い。
第三に、本当の飛躍は「形式仕様だけを書き、実装は生成せよ」というツールを次の段階に引き上げることにあるだろう。こうしたコード生成プロジェクトはすでにいくつもあるが、たいていの企業が望む水準にはまだ十分成熟していない。LLM ツールが、そのうちの一つをニーズに合わせるために必要な 1〜2 年の手作業を加速できるとしたらどうだろう
Kleppmann の以前の記事 https://martin.kleppmann.com/2025/12/08/ai-formal-verificati... も参考になりそうで、型システムやリンターに入れられるものは当然そうするかどうかを検討すべきだ。
もっと書きやすい方法が出てきてほしい。記事に出てきたツールの中では、dafny と iris が産業用途に最も近いように思える。Amazon S3 も内部で TLA を使ってきた経緯があると認識している。
ただ、この分野の TypeScript のような存在、既存のツールに自然に入り込み、ゼロコスト抽象化のように機能し、人々が心から以前のやり方より好むようなものは、まだ見たことがない気がする。
カスタムリンターを使うのも、依然としてかなりつらい。golangci-lint はつらいコードベースだし、semgrep は使ったことがないが、ルールエンジンが威圧的に見えた。気に入る AST API にもまだ出会っていない
演繹的推論、つまり「形式手法」へのこうした賛歌は、常にその根本的な限界を見落としている。公理と定義が対象ドメインにどれだけ適合しているかという問題だ。
「理論上、理論と実践に違いはない。実際には……」という言葉と同じことだ。Jane Street は、コードの目的が決定的アルゴリズムを実装することであり、対応関係が 1:1 の大規模コードベースを維持するだろうと推測している。多くの開発者はそうした領域で働いているが、何百万人もの開発者はそうではない。ほとんどの UI や、ほとんどの探索的作業などがそうだ。
形式手法と並行して、論理・数学的な方法ではないが、受け入れ基準を高解像度で定義しようとする流れもある。この流れは少なくともマッピングの問題とは格闘しているが、地図が領土ではない大半の場面では解決できていない。
Google の検索結果ページには極度に進化した内部最適化フレームワークがあるが、本当に最適点に到達したのだろうか。ぼんやりしたアイデアをつかむために急いで作ったプロトタイプのほうが、よりうまく示せたのではないか。こうした問いは、システム内部ではなく、そのシステムが奉仕する外側を見ることで最もよく答えられる。
論理回路、形式検証が多く入る CPU コンポーネント、カーネル、プロトコル、パーサー、コンパイラ、暗号、セキュリティフレームワーク、並行性の基本要素などは、検証から大きな利益を得る。
さらに学ぶなら、Hillel Wayne の記事がよい出発点になる: https://www.hillelwayne.com/formally-specifying-uis/
そして場合によっては、結果がよく定義されていなくても学習できるので、何が妥当かを座って考えるだけの問題ではない。
プログラミング言語の設計と実装に少し関心がある立場からすると、この一文は本当に興味深かった。「プログラミング言語を扱う人のほとんどにとって、簡単な部分はプログラミングをより良くする新しくて優れたアイデアを出すことだ。難しい部分は、誰かを説得してそのアイデアを実際の仕事に使わせることだ」
完全に同意する。たとえ利点があっても、新しい言語に持ち込める見慣れなさの量には限界がある。
しかし AI エージェントは、プログラミング言語設計における急進的に新しいアイデアに大きな抵抗を示さないだろう。エージェント型 AI の後で、プログラミング言語設計がどう進化するかについて、しばらく考えてきた。
採用への懸念をはるかに小さくできるとき、プログラミング言語を改善するためにどんな新しいアイデアを生み出せるかを見るのは、非常に興味深いことになりそうだ。
https://steveklabnik.com/writing/the-language-strangeness-bu...
アプリケーションセキュリティテストの分野で形式手法を適用する方向で取り組んでおり、同じアプローチをビジネスロジックの検証にも適用できると考えている。
そのために taint analysis を使っている。かなり確立された形式手法のアプローチだが、実際のコードベースにおけるデータフローの複雑さのため、現場ではまだ広く適用されていない。
形式手法を AST パターンマッチングや単純な型検査を超えて拡張するのは、本当に難しい作業だ。taint analysis で実際のコードベースの手続き間データフローを数分以内に追跡し、深く隠れた脆弱性を見つけるレベルに到達するまでに、何年もの研究開発がかかった。
興味があればプロジェクトを見てほしい: https://github.com/seqra/opentaint
約 18 か月前に LLM と一緒に型を使うことに夢中になり、
lean4に本気になったのは 6〜8 か月前くらいだ。今では、実用的な C/C++ FFI、したがって事実上あらゆるものと接続できるCIC証明基盤なしに、ソフトウェア作業に AI 支援を使うことは考えられない。JSON から Python まで全部禁止し、
nixもコンパイラを持つように書き直した。私たちが使うほぼすべてのものは、プロパティテストや複数のファズテストを限界までかけるだけでなく、少なくとも.olean連携を通じてプロパティテストを駆動するlean4証明を持っている。余裕があれば、ドメイン全体の完全性まで証明し、その性質もテストする。高速な部分はすべて
lean4から生成されるので、C++/Rust 論争はスキップしている。C++ のバグが実際にはlean4コードのバグだった場合に利点はあるが、どちらにも転びうる。これは大きな変化であり、「JSON と Python を禁止するだって？」と懐疑的な人を責めるつもりはない。しかし私たちはこのやり方で数百万行を検査してきており、AI + 形式システムは、AI なしから AI と Python へ移ることよりも、はるかに大きな飛躍だ。後者は私たちの経験では進歩が単調ではないが、前者はほぼ常に単調に前進する。
かなり大胆なこともできる。これは ISL や CuTe のようなものがモデル化する多面体テンソル計算の形式証明で、これを使えば C++23 の
mdspanでデバイス上の swizzling と tiling を行い、それが正しいことまで証明できる。ただしこの例は、カバレッジに関する L'Hopital 的な議論をうまく示してはいない: https://github.com/b7r6/mdspan-cuteその結果は本当に高速で、最初の試みから速い。
https://straylight.software/assets/lambda-hierarchy.svg