ハクソク

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

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

2026年3月4日原文(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を使って実装を生成するってわけ。でも、製品として使えるようにするには、その仕様書がすべてのユースケースやエッジケース、エラーハンドリング、パフォーマンス目標、セキュリティやプライバシーの管理などをカバーしてないといけない。これって、実際の実装にかなり近い気がするんだけど、ただ別の言語で書いてるだけじゃない？

Hacker Newsで議論の続きを見る