本文へ
ハクソク

世界を動かす技術を、日本語で。

形式的手法とプログラミングの未来

元記事: 原文(blog.janestreet.com)

概要

  • Jane Street は長年、 フォーマルメソッド に消極的だったが、現在は積極的に取り組み始めている。
  • エージェント型コーディング の登場により、フォーマルメソッドのコストとメリットのバランスが大きく変化。
  • 型システム の有効性を実感しており、より強力な証明技術への期待が高まっている。
  • 独自言語 OxCaml とプログラマーコミュニティの強みを活かし、内部での開発体制を強化中。
  • 新たなチームメンバーを ロンドン と ニューヨーク で募集中。

Jane Streetにおけるフォーマルメソッドへの転換

  • 過去25年間、Jane Streetはフォーマルメソッドに興味がないと公言してきた歴史。
  • 型システム は「軽量フォーマルメソッド」として多大な恩恵を受けてきた実績。
  • 一般的なフォーマルメソッドはコストが非常に高く、 seL4 マイクロカーネルの事例では8,700行のCコードに25人年、1行あたり23行の証明が必要。
  • セキュリティクリティカル なソフトウェアには価値があるが、通常のソフトウェアには費用対効果が合わない認識。

エージェント型コーディングによる状況の変化

  • エージェント型コーディング の出現で、フォーマルメソッド導入コストが劇的に低下。
  • モデル（AI/エージェント）が証明作業を支援し、より多くの開発者が活用可能な環境。
  • 従来のコスト/ベネフィット計算を再考する価値が生まれた。

フォーマルメソッドの新たなメリット

  • 検証ボトルネック の重要性が増大。
  • モデル生成コードは実用的だが、品質やコードベースの一貫性維持が難しい現状。
  • エージェント生成コードの品質確認・検証負担を フォーマルメソッド で効率化可能。
  • フィードバック源としてのフォーマルメソッドの有用性。
    • エージェントの学習やコーディング時にさらなる問題解決力向上。
  • テスト も重要だが、テストだけではカバーできない状態空間や保証が存在。
    • 型システムによる 普遍的保証（∀） の有効性。

Jane Streetがこの分野に適している理由

  • OxCaml など自社言語への深いコントロールにより、証明指向機能の組み込みが可能。
  • 型システムの拡張や所有権・ミュータビリティ制約など、証明を容易にする設計が可能。
  • プログラマーコミュニティ の成熟度が高く、新機能への期待と受容性が高い。
  • ユーザーからのフィードバックを活かし、短期的・長期的な改善を並行して推進可能。

外部コミュニティとの連携と今後の展望

  • Lean, Dafny, Rocq, Agda, Iris など外部のPLコミュニティやツールにも関心。
  • OxCaml と外部ツールとの統合による相乗効果を模索。
  • 言語と証明技術を同時に進化させることで、独自の優位性を発揮。

チームメンバー募集

  • ロンドン と ニューヨーク で新チームを構築中。
  • 初期段階のため、幅広い知見と情熱を持つ人材を歓迎。
  • 興味がある場合はぜひ応募を検討。

補足・脚注

  • モデル（AI/エージェント）は複雑な証明においても人間の支援が必要なケースが多い。
  • 型システムにも例外（Obj.magic等）は存在するが、追跡・制限によりほぼ普遍的な保証が可能。
  • Yaron Minskyは2002年にJane Streetに参加し、OCaml導入の立役者。

提供: ハクソク · 要約更新:

AIによる日本語要約です。内容は原文とあわせてご確認ください。

Hacker Newsの議論を読む

Hackerたちの意見

つまり、GEN AIがたくさんのコードを生成するから、人間の価値を検証にシフトさせるってことだよね。プログラミングって本当に何なのか、時々考えるんだ。実際、英語が苦手な私にとって、プログラミングを学ぶのは大きな挑戦なんだよね。翻訳がない英語の文書を理解するためには機械翻訳に頼るしかないし、私の言語の教材は5年から6年遅れてる。今、AIが生成する何万行ものコードをレビューするのは不可能だから、数学的証明のような絶対的なルールを確立しようとする議論をよく見る。これを読むと、Rustの借用チェッカーを思い出す。実際、Rustで何度か書いた後、借用チェッカーを避けるためにトリックを使う悪い習慣に陥ることが多いんだ。数学的な厳密さが行き過ぎると、人間はそれを回避する方法を見つけがちだよね。私みたいな教育を受けていないプログラマーは特にそう。こういう試みを振り返ると、特定の形式化された答えのためだけにコードを書く結果になりそう。もしそれが標準化されちゃったら、人間のニーズに応えられるかどうかはわからない。こういう防御的なプログラミングの試みはいいと思うけど、私は攻撃的なプログラミングをしたい（この言葉は私が作った）。リスクを取るけど、すぐに修正して出荷する。時間が経てば、十分に良くなると信じてる。もちろん、精度が重要で作業範囲が明確な確立された業界、例えばJane Streetでは、この記事のアプローチは正しいと思う。つまり、市場の需要を適切にモデル化するのに十分なデータがあるから。でも、私みたいな社会的に負け組の人間が金を稼ごうとすると、常に金鉱を探してあちこち移動するから、こういう方法論は贅沢に思える。成熟したモデリングを持つ確立されたビジネスは、継続的に最適化するために高度に教育された専門家が必要なんだ。でも、現実的にはその需要についていけないってわかってる。だから、構造化されていないモデリングの場所を探してるけど、それでもこのアプローチが使えるかどうかはわからない。

└

こういう方法論は贅沢に思えるよね。 その通り！この記事でもその点を認めてる。Jane Streetはこの恩恵を受けるのに特に恵まれてるよね。

└

「攻撃的プログラミングがしたい（この言葉は俺が作った）」リスクを取るけど、すぐに修正して出荷する。いいね、その言葉も好きだ。だけど、このパラダイムは業界では完全に現状維持だよね。問題は、Gen AIのおかげで「防御的プログラミング」のコストが大幅に下がった一方で、（人間の）検証のコストが上がったことなんだ。逆に、形式的手法は検証を安くするけど、実装には大きなオーバーヘッドがかかる（仕様、型、証明を書くこと、そして一般的に実装を厳格なフレームワークに曲げること）。でもGen AIはその面倒な作業を自動化できる。まさに天の配剤だね。

└

janestreetの視点から見る必要があるよ。彼らはHFTで、何百万、下手したら何千万の株や金融商品を高頻度で取引してる。だから「修正」はない。何が間違っているか理解する頃には、もう数十億を失ってる。だから、オフェンシブな手法は重要でない領域では機能するかもしれない。ちなみに、君はすでにどこでもディフェンシブな手法を使ってるよ。PythonやJavaなんかはガーベジコレクタが付いてるし、コードが君の意図通りに実行されていることが確認されてる。正式な検証がいつ始まるのか気になってたんだ。実装の詳細を心配するところから、問題の科学的・数学的な説明に移行するのは自然な流れだよね。

前のkleppmannの投稿を見てね https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...。そう、明らかに、型システムやリンターに入れられるものは、入れるべきだと思う。もっと使いやすい方法が増えるといいな。投稿に挙げられているツールの中では、dafny + irisが工業的に近いと思う。あと、amzn S3は社内でTLAを使ってた歴史があると思う。でも、この分野ではまだtypescriptを見たことがないと思う。既存のツールに落とし込めるゼロコストの抽象化で、人々が古いやり方よりも本当に好むものがあればいいんだけど。（カスタムリンターを書くのはまだまだ大変だし。golangci-lintは痛いコードベースだし、semgrepは試してないけどルールエンジンが怖そうだった。好きなAST APIはまだ使ったことがない。）

いつものことだけど、この演繹的推論への賛歌（「形式的手法」）は、その根本的な限界を見落としてる。「公理や定義が、マッピングしようとしている領域にどれだけフィットするのか？」ってことだよね。（「理論的には、理論と実践に違いはない。実践では…」）私の推測では、Jane Streetはマッピングが1:1の大きなコードベースを維持してると思う。なぜなら、そのコードの目的は決定論的アルゴリズムを実装することだから。多くの他のコーダーもそういう分野で働いてる。でも、私たちの大多数はそうじゃない。ほとんどのUIや探索的な作業など。形式的手法に並行して、高解像度で受け入れ基準を定義する動きがあるけど、論理的・数学的ではない。これは少なくともマッピング問題に取り組んでいるけど、地図が領域でないところでは解決できない。Googleの結果ページは、非常に進化した内部最適化フレームワークで本当に最適に達したのか？あなたが曖昧なアイデアを捉えるために作ったプロトタイプは、それをよりよく示すことができたのか？こういう質問は、システムの外に目を向けて、システムが何を提供しているのかを見ることで最もよく答えられる。

└

フォーマルメソッドは、セマンティクスが明確に定義されている領域にこそ必要なんだよね。論理回路（多くのCPUコンポーネントがフォーマル検証を受けてる）、カーネル、プロトコル、パーサー、コンパイラ、暗号、セキュリティフレームワーク、並行性プリミティブなど、検証から大きな恩恵を受けてる。

└

Googleの結果ページはあまり明確じゃないね。でも、その下のコードの90％以上は明確に定義されてると思う。結果が明確でない場合でも、学習できることがあるから、何が意味を成すかを考えるだけじゃないんだよね。

└

実際のほとんどのUIは状態機械に集約されていて、これは形式的検証に非常に適している。Hillel Wayneの著作は、もっと学ぶための良い出発点だよ: https://www.hillelwayne.com/formally-specifying-uis/

形式的な仕様について読むたびに、「同じテストを違う方法で書くだけ」か、もっと悪いことに「同じ実装を違う方法で書くだけ」って感じがするんだ。二度やることでエラーを見つけるのに役立つかもしれないけど、形式的な仕様がテストや実装と同じバグに悩まされるなら、何が特別なのかわからない。問題の根本は、プログラムが何かを正式に証明したいなら、その「何か」が何なのかを非常に具体的にしなきゃいけないってことだよね。そうなると、結局またテストや実装を書いてることになる。これについては何年も考えてきたけど、何かを見逃している気がするんだ。でも、それが何なのかわからない。誰か教えてくれない？

└

いつも形式的な仕様について読むと、「同じテストを違う方法で書くだけ」か、もっと悪いことに「同じ実装を違う方法で書くだけ」って感じがする。 [...] 誰か教えてくれない？ 大きな違いは、形式的手法を使うことで「すべての」量化子を使えることだよ。例えば、「foo('abc')は末尾に空白がない文字列を返す」という単体テストを書くことができる。でも、形式的手法を使うと、「任意の入力xに対して、foo(x)は末尾に空白がない文字列を返す」と証明できる。これは簡単な例だけど、「任意のプログラムPに対して、compile(P)はPと同じ動作をする」といったもっと複雑なことも想像できる。当然、「同じ動作をする」という意味を定義しなきゃいけないけどね！

└

私はソフトウェアを書かないけど、ASICやFPGA設計では、形式的手法の仕様がSATソルバーのようなものを使って、基礎となるテスト記事が仕様を満たしているかどうかを判断できるようにするんだ。設計の特性を指定して、ツールがさまざまな方法で設計をテストして、その特性を侵害できるかどうかを確認する。例えば、ターンシグナルを制御するシステムがあるとする。交差する車線が同時に緑の信号を持つことができない、あるいはその間に時間がないという特性を指定できる。ツールはこれを徹底的にチェックして、それを侵害するコードのトレースを浮き彫りにすることができる。

Hacker Newsで議論の続きを見る

同じ出典の記事