ハクソク

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

AIがソフトウェアを書くとき、誰がそれを検証するのか？

45日前原文(leodemoura.github.io)

概要

  • AIによるソフトウェアコードの自動生成が急速に進行中
  • コードの大部分がAIで生成される時代が目前
  • セキュリティや品質保証の課題が拡大
  • 数学的証明による検証が重要性を増す
  • 検証プラットフォームの要件と今後の展望

AIが世界のソフトウェアコードを書き換える現実

  • Metal社が防衛産業向けコードのAI書き換えで1億2500万ドル調達
  • GoogleやMicrosoftでは新規コードの25～30%がAI生成
  • AWSはToyotaのCOBOL 4000万行をAIで近代化
  • MicrosoftのCTOは2030年までに95%がAI生成コードと予測
  • AnthropicはAIエージェントで10万行のCコンパイラを2週間・2万ドル未満で構築
    • Linuxの起動やSQLite、PostgreSQL、Redis、Luaのコンパイルに成功
  • AIによる大規模ソフトウェアの高速生成が現実化

コード品質と検証のギャップ

  • AI生成コードの約半数が基本的なセキュリティテストに不合格
  • 最新の大規模モデルでもセキュリティ向上は限定的
  • Andrej Karpathyは「Accept All」で人間のコードレビューが形骸化する現象を指摘
  • HeartbleedのようなバグがAIの速度で拡散するリスク
  • Harvard Business ReviewはAI生成の「workslop」現象を報告
    • メモなら迷惑、暗号ライブラリなら壊滅的被害

新たなサプライチェーンリスク

  • AIが生成するコードがサプライチェーン攻撃の新たな標的に
  • トレーニングデータやAPIの改ざんによる脆弱性の大量注入リスク
  • 従来のコードレビューやテストでは巧妙な脆弱性発見が困難
  • **形式的仕様（Formal Specification）**の導入が不可欠

数学的証明の重要性

  • テストは信頼性、証明は保証を提供
  • AIが証明コストを削減すれば、全入力・全ケースを網羅する保証が現実に
  • 例：TLSライブラリの定数時間実行要件
    • テストやレビューでは見逃すタイミングサイドチャネルも、証明なら即座に検出
  • AIによるテスト最適化は過学習を招く危険性
  • 証明は騙せない—全入力を網羅

検証による開発加速

  • 検証は「コスト」から「触媒」へ
  • AIが証明付きソフトウェアを容易に生成できれば、検証は開発のボトルネックではなくなる
  • MLカーネルやハードウェア設計の納期短縮
  • 航空・自動車・医療機器など認証の効率化
  • 仕様（Specification）がエンジニアリングの中心に
    • シンプルな正しいモデルをAIと共同作成→効率的な実装と等価性証明をAIが担当

AI時代の検証プラットフォーム要件

  • 小規模かつ信頼性の高いカーネル（数千行）による機械的証明チェック
    • LeanやRustなど複数言語で独立実装し、相互検証
  • AIと検証レイヤーの分離が不可欠
    • ベンダーロックイン防止、セキュリティアーキテクチャの観点からオープンソース必須
  • プログラミング言語と定理証明器の統合
    • コードと証明を一元管理、翻訳ギャップなし
  • AIが逐次的な証明探索を制御できるフレームワーク
    • ブラックボックス型ソルバーではなく、学習・フィードバック可能な仕組み
  • 大規模な形式知識ライブラリ
    • 数学者とエンジニアが共用できるプラットフォーム
  • 深い拡張性
    • ユーザーやAIが独自のツールや証明戦略を内部から拡張可能

LeanとAIコミュニティの動向

  • AlphaProof（Google DeepMind）、Aristotle（Harmonic）、SEED Prover（ByteDance）、Axiom、Aleph（Logical Intelligence）、Mistral AIなどがLeanを採用
  • 国際数学オリンピックでのAI推論システムもLeanを利用
  • Lean + Mathlibによる未来の拡張性と応用範囲の拡大

Hackerたちの意見

問題は検証よりももっと深いところにあると思う。技術的には検証は可能だよね。理論的にはCコンパイラやブラウザを作って、既存のテストを使って動作確認ができる。でも、もっと難しいのは発見の部分。全く新しいものをどうやって作るか、既存のテストスイートがないものをどうやって検証するかってこと。検証ができるのは、誰かが「正しい」っていう定義をしているからなんだ。仕様書やリファレンス実装、期待される動作のセットがあって、それにシステムが合致すればいい。でも、本当に新しいものを作るときは、比較するための基準がないし、事前に決められたゴールもない。単に問題を解決するだけじゃなくて、その問題が何なのかを見極める必要があるんだ。
└
それはソフトウェア業界が何十年も自ら作り上げてきた問題だよね。少なくとも「アジャイル」が普及してから、仕様に基づいて作ることを拒否する文化ができてしまったし、顧客から仕様を引き出すのは不可能だって主張するようになった。
└
テストについて考える方法は2つある。A) 実装が仕様を満たしているかどうかを確認できる。B) システムの動作を（信頼できる）説明として示してくれるので、システムをよりよく理解できる。
記事にはAWSのCedar認可ポリシーエンジンがLeanで書かれているってあるけど、実際にはDafnyで書かれてるんだ。Dafnyを書くのは、Leanで見るような証明を書くよりも「普通」のコードを書くことに近い。数学者じゃないから、Leanのチュートリアルでは早々に諦めちゃったけど、最近のプロトタイプではDafnyを少し学んで、ClaudeのDafnyコードを半日でレビューできるくらいには自信がついた。Dafnyコードはサービスのコアにセキュリティカーネルを形成していて、ミューテーション操作が行われる前に監査ログが必ず書かれるような不変条件を強制してた。もちろん、バグもあったけど、主に仕様の問題（仕様が不十分だったり、デザインが悪かったり）や、Claudeが証明を十分に進めなかったことから来てた（関連する型の一つだけを証明して、私の方でも仕様の問題があったかもしれない）。結局、私はI/Oバウンドのグルーコードを書いてるだけで、普通のテスト駆動開発で十分だったって気づいた。PythonのコードはDafnyよりも早く正確にレビューできるから、また人間に最適化する方向に戻ったよ。
└
Cedarは以前Dafnyで書かれていたけど、AWSはその実装を放棄してLeanで書き直したんだ。 https://aws.amazon.com/blogs/opensource/lean-into-verified-s...
└
LLMはDafnyを書くのがLeanより簡単だって。研究「A benchmark for vericoding: formally verified program synthesis」では、次のように報告してるよ： > 「我々は、形式的仕様から形式的に検証されたコードを生成するためのLLM生成の最大のベンチマークを提示し、テストした… Leanでは成功率が27%、Verus/Rustでは44%、Dafnyでは82%だとわかった。」 https://arxiv.org/html/2509.22908v1
みんなにRTFA（記事をちゃんと読め）を勧めるよ。見出しにだけ反応するんじゃなくてね。これは未来がどこに向かっているのかの一端を垣間見ることができる。私は「自動化される最後の仕事はQAになる」って言ってるけど、日々その実感が強くなってる。今の時代にプロダクトエンジニアでいるのは一つのことだけど、著者がいるレベルでコードが検証可能である必要があるのはまた別の話だよね。でも、人々がアプリを楽しむのをやめてカーネルを楽しむようになったら、本当にゲームが根本から変わると思う。もう一つの言葉もあるんだ。「十分に進化したエージェントはDSLと区別がつかない」って。Leanをこの方程式に入れることは考えてなかったけど、この二つのアイデアを組み合わせてみると、Leanがエージェントフレームワーク全体を飲み込んで、オペレーティングシステムが消える世界に近づいている気がする。もし今日、10年後にも relevancy があるものを作ろうと思っているなら、これは洞察に富んでるよ。
└
> 「十分に進化したエージェントはDSLと区別がつかない。」よくわからないけど、もっと詳しく聞きたいな。
└
私も形式的手法には熱心だけど、LLMベースの技術がLeanでアプリケーションソフトウェアのかなりの部分を書くのを経済的に可能にするとは思えない。LLMは、良いトレーニングデータがある分野で証明を持つコードを探すのに強力なヒューリスティックな役割を果たすことができるけど、残念ながらそういう分野は少ないんだ。それに、たとえ厳密に証明されたコードでも、人間はパフォーマンスの問題を見極めるために読む必要があるし、Leanを読めるように人を育てるのはコストがかかる。とはいえ、OPが言うように、証明可能な正しいシステムプログラミングを開発するにはとてもエキサイティングな時期だよ。
└
まだ成功した便利なバイブコードアプリはないね。カーネルはまだ遠いと思う。
└
> みんなにRTFAをして、見出しだけに反応しないように勧めるよ。これは「リードを埋める」記事の一例だね。新しいzlibの自動形式化の発表から始めるべきだった！それで興奮させてから、残りの話をすればよかったのに。AIに関するトピックについて、読者にとってはすでにうんざりするほど馴染みのある、あまりにも無骨で醜いLLMが書いた一般的な文章から始まるなんて、ちょっと残念だよね。† つまり、私の言葉で言うと「あなたに関心を持たせることに失敗している」ってことだね。
なんか見落としてるかもしれないけど、これってコードを書くのと同じじゃない？ただ手順が増えただけって感じ。今はエンジニアが緩い仕様書を使って、それをコードに変換してるけど、提案されたアプローチだと、まずその仕様書を正式に検証可能な形に変えなきゃいけないんだよね。それからLLMを使って実装を生成するってわけ。でも、製品として使えるようにするには、その仕様書がすべてのユースケースやエッジケース、エラーハンドリング、パフォーマンス目標、セキュリティやプライバシーの管理などをカバーしてないといけない。これって、実際の実装にかなり近い気がするんだけど、ただ別の言語で書いてるだけじゃない？
└
重要なのは、仕様書は「明らかに計算可能」である必要はないから、実装するコードよりもずっとシンプルにできるってこと。たとえば「ある関数が値への参照を持っている場合、その値はその関数が明示的に変更しない限り変わらない」という性質を考えてみて。表現は簡単だけど、Rustで実装するには借用チェッカーが必要で、これはかなり重いエンジニアリングなんだよね。そして、その実装が実際にその性質を保証することを証明するのも簡単じゃない！
└
フォーマルな仕様は、コードを書くよりも簡単に書けることがあるよ。例えば、Dafnyのリファインメントタイプなんかはそう。高レベルだから、面倒な実装の詳細に悩まされることもないし。手動でコーディングするのではなく、フォーマルな仕様に焦点を当てることで、ソフトウェアをより早く開発できるだけでなく、より高い保証を得られる可能性もある。もちろん、今のところはほとんど理論的な話だけど、ワクワクする可能性だよね。高レベルの仕様はパフォーマンスの問題を見落としがちだけど、ほとんどのシナリオには十分だと思う。それに、1990年代から問題を任意の粒度で分解できるフォーマルな開発手法があるし、正しさを保ちながらね。これらのアイデアは、近いうちに再評価される可能性が高いと思う。
> Claude C Compilerは別の側面を示してるね：テストを通すことを最適化してて、正しさにはこだわってない。テストスイートを満たすために値をハードコーディングしてる。一般化はしない。これが、職場で俺が苦しんでるポイントの一つなんだ。作業者がコーディングエージェントにコードを生成させて、そのコードのテストカバレッジを生成させるんだ。LLMは喜んでユニットテストを作り出すけど、それは既存のコードの挙動を強化するだけなんだよね。誰も「生成されたコードがシステムの望ましい機能的挙動を実装してるのか？」って聞かない。さらに厄介なのは、LLMが大量のコードを生み出すから、人間はそれをただ承認するだけになってる。マージしてビルドに行くって感じ。建設的な提案はないけど、業界は何か大惨事が起こるまでアクセルを踏み続けると思う。
└
> 誰も「生成されたコードがシステムの望ましい機能的挙動を実装してるのか？」って聞かない。明らかな疑問だけど、なんでなんだろう？有能な開発者がいると仮定して、もしかしたら十分なQAの時間がないからかも？多くの場所は機能工場みたいになってるし。個人的なプロジェクトでは、実装よりもテストのためのコード行が多いんだよね。
└
次のレビューでは、別のエージェントが元の問題と生成されたコードを分析して、コードが問題の意図に合っていれば承認するってのはどう？手動作業をオフロードできるように、しっかり説明できるものを見逃さないようにするのが原則。エージェントの成功率に応じて、複数の基準を検証するエージェントを一つ使うか、異なるレビュー基準のために別々のエージェントを使うことができるよ。
└
テスト生成ループが本当の罠なんだ。エージェントにコードを書かせて、そのコードのテストを書くように頼む。もちろんテストは通るよ。コードが何をするかをテストしてるだけで、何をすべきかをテストしてるわけじゃないからね。タスクマネージャーを作ってるときにこれにぶつかった。PUTエンドポイントはcompleted=trueを設定したけど、完了タイムスタンプは設定しなかった。エージェントが書いたテストは「completedをtrueに設定するか」をテストしてたから、すべて通過したんだ。「いつ完了したかを記録するか」はテストしてなかった。生産環境には59件のnullタイムスタンプのタスクがあったけど、下流のレポートでそれが発覚した。修正は簡単だったけど、確認のギャップは大きかった。
└
これ、響くね。仕事でめちゃくちゃ雑なものを受け取ってるから、レビューにあまり気を使わなくなっちゃった。
└
えっと、テストは先に書くべきだよね。エージェントはこれができないの？
└
だから、テストを先に書いてからコードを書くんだよ。特にバグを修正するときは、バグがあるときにテストがちゃんと失敗することが確実だからね。
└
そう、これがまさに私が気づいた馬鹿げたことなんだ。LLMから出てくるものは、正しいことじゃなくて、聞きたいことを聞かせるように最適化されてる。
└
> 誰も生成されたコードがシステムの望ましい機能的動作（「ビジネスロジック」）を実装しているかどうかを確認することはない。LLMを使うのは楽しいけど、テストがただの形式的なものになっていることがよくわかる。人々は、本当にテストが意味のあることをチェックしているのか？
└
僕の職場では100%のテストカバレッジが求められてるから、みんなAIを使って1万行のユニットテストファイルを生成して、誰も何も確認できてない。
└
> LLMは単にコードの既存の動作を強化するユニットテストをどんどん生成している。誰も生成されたコードがシステムの望ましい機能的動作（「ビジネスロジック」）を実装しているかどうかを確認することはない。仕様駆動開発やTDDを使えるよ。まずテストを書いて、失敗するコードを書いて、それからテストに合格するようにコードを修正する。
確認の複雑さの壁があると思う。システムにコンポーネントを追加するにつれて、それらが一緒に機能することを確認するのにかかる時間が超線形的に増えていく。ある時点で、確認の複雑さが急上昇するんだ。文字通り、すべてを確認する時間がなくなる。AIコーディングエージェントは、コンポーネントを生成するのが早すぎて、この壁に直面するのが以前よりも早い。複雑さの管理が下手だからね。今や確認はエージェント的なソフトウェア工学の問題だと思う。形式的手法は役立つと思うけど、エンドツーエンドのUIテストやシステムと現実世界の相互作用のような複雑な状況にどう適用できるかは見えない。もっと詳しい考えをXに投稿したよ。 https://x.com/i/status/2027771813346820349
└
投稿ありがとう。いい読み物だった。僕もn-LLMのガバナンス/バリデーションレイヤーに取り組んでいて、観測可能にしているから、君の言う暴走AIの話に共感した。僕の研究は、推論前または実行前のバリデーションレイヤーとして、評判やステークコンセンサスメカニズムに向かっている。十分な「意思決定流動性」があれば、決定を確認する時間をスキップできるんだ。
根本的な問題は、平均的な開発者の検証ループがテストではなく、結果に基づいていることだよね。コードを書いて、ブラウザをリロードして、出力を確認する。これで自分の思い通りに動く？よし、これで終わり。テストを書くとか、すべてのテストケースをカバーするなんてことはしない。そんな不安定な基盤の上に、さらに未テストのコードが積み上げられるとどうなるか。質の悪いソフトウェアが生まれるんだ（大規模な書き直しなしには修正できないことが多い）。それに、大半の「バイブコーダー」はAIが生成したコードの何が悪いのかを見極めるだけの経験や知識が足りてない。そういうのを理解するには、AI以上の知識が必要だし、自分が取り組んでいる分野にしっかりした基盤が求められる。例えば、AIにコメントフォームのコードを書いてもらうとする。バックエンドとフロントエンドのコードを生成してくれる（ReactやSvelte、Vueなど）。バイブコーダーはUIを見て、「わー、すごくいい感じ！」って思って承認する。でも、経験豊富な人はそのフォームにCSRF保護がないことに気づくかもしれない。バイブコーダーはCSRFの概念すら知らないかもしれないし（OSWAPのトップ10のセキュリティリスクなんてなおさら）。だから、根本的な問題は、AIよりもその分野について知識がないから、欠陥を見抜けないことなんだ。この根本的な問題が解決されない限り、解決策は見えないと思う。最近は誰でもコードやUIを生成できるから、すぐには解決しないだろうしね。でも、コンサルタントやその手の人にはいいニュースだよ。なぜなら、後でバイブコーディングの混乱を修正する仕事が増えるから。次の日にハッキングされることもあるし、急ぎの料金も取れるしね。だから、そんなに悪くはないよ。
└
フロントエンドのテストについての印象だけど、2つのタイプがあると思う。実用的じゃないくらい書くのが難しいか、無駄か。ほとんどの組織は後者を選んで、最終的にレンダリングされたDOMのような簡単にテストできるものをテストして、人間のQAに頼ることが多い。「ページは本当に想定通りに見えるのか？UI要素とのインタラクションは正しく動くのか？フローは実際に機能するのか？」みたいな難しい部分はね。結局、テストはエンドユーザーのようにページを意味的に見ることも、インタラクトすることもできないから、こうなるんだよね。
僕は、形式的手法や数学的証明がテストのようにLLMにフィードバックを得るために役立つと思うけど、「毒されたトレーニングデータが特定のバグや脆弱性を引き起こす」という問題を解決するとは全く思わない。バグは形式的な仕様にも導入されるし、人々はそれを見逃すだろう。速い対応と修正時間、つまりアンチエントロピーが、活性化エネルギーを増やそうとする試みよりも勝ると思う。問題を最初から防ぐのではなく、クリーンアップ方法が必要だ。
> 誰も結果を正式に検証していない これは趣味のプロジェクトや急いで作られたスタートアップのMVPには当てはまるかもしれないけど、実際には考慮すべきいくつかのポイントがある。1. 僕が関わっているソフトウェアチームは、通常のレビュー慣行を維持している。AIが完全に作成した機能でも、通常のPRレビューを通る。開発者は「すべて受け入れる」を選ぶかもしれないけど、これは良いプラクティスとは言えない。変更は人間によってレビューされる。2. コードとセキュリティレビューを目的としたサブエージェントは良い仕事をしている。別のモデルを使ってコードをレビューすることもできて、異なる視点を提供できる。3. 1年前、AIが書いたコードは初回で動作しないことが多くて、痛い思いをしながら共同トラブルシューティングが必要だった。今は95%の確率で動くけど、最適ではないかもしれない。改善のスピードを考えると、6〜9ヶ月後には、動くだけでなく、質も良くなると期待しても安全だ。
> AIがソフトウェアを書くとき、誰がそれを検証するの？ ああ、それは簡単だよ：責任を問われるのは検証する人だ。