Jane Street、形式手法チーム設立へ
原題: Formal methods and the future of programming
なぜ重要か
大手金融技術企業が形式手法への投資を決定したことで、AI時代のソフトウェア開発における品質保証手法の新たな方向性を示している。
金融サービス企業Jane Streetは25年間形式手法に懐疑的だったが、AI エージェントコーディングの登場により方針転換し、形式手法専門チームの構築を発表した。同社はCTOのYaron Minsky氏が型システムと同様に形式手法を広く活用できるツールにしたいと述べた。
Jane StreetのCTO Yaron Minsky氏は、同社が過去25年間形式手法に興味を示さなかったが、現在は専門チームを構築中だと発表した。従来、形式手法はコストが高すぎると判断していた。例として挙げたseL4マイクロカーネルでは、8700行のCコードを検証するのに25人年の労力と、各行につき23行の証明と半人日が必要だった。
しかし、AIエージェントコーディングの登場により状況が変化した。第一に、モデルが形式手法の使用コストを劇的に削減し、より多くの人が生産的に活用できるようになった。第二に、検証ボトルネックの重要性が増している。AIモデルは有用なコードを生成するが、実際にリリースできる品質との間には大きなギャップがある。エージェントが生成するコードは複雑で、バグや隅の事例が多く、コードベースの重要な不変条件に従わない傾向がある。
形式手法により、この検証負担を軽減し、レビュープロセスをより効率的にできると同社は考えている。また、エージェントはフィードバックで向上するため、形式手法が提供する構造化されたフィードバックが有益だとしている。同社の目標は、現在の高度な型システムと同様に、形式手法をソフトウェア構築の広く有用なツールにすることだ。