ハクソク

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

私たちは今、証明の自動化を実現しました

2026年7月27日原文(imperialviolet.org)

概要

  • 依存型言語 （Coq Rocq、Leanなど）の魅力と課題を解説
  • 証明自動化（LLMやSMTソルバー）の現状と限界
  • Zstandard （zstd）圧縮アルゴリズムの特徴と実装体験
  • FSEエントロピー符号化法 の仕組みを詳細に説明
  • Lean での実装例と依存型の利点を紹介

依存型言語と証明の現状

  • Coq Rocq や Lean などの依存型言語は、極めて細かな 不変条件 を型システムで表現・保証可能
  • 通常の言語ではコメントや設計文書に留まる情報も、機械的に 検証 可能
  • チーム規模拡大に伴う 誤解 や コンポーネント間の不整合 防止に寄与
  • ただし、強力な型システムの代償として、 証明作業 に膨大な労力が必要
    • 例：seL4プロジェクトでは、設計・実装よりも10倍の時間を証明に費やし、証明コードはCコードの20倍以上に
  • 証明工学 （proof engineering）の重要性
    • 証明の再利用性や保守性向上のための構造化
  • SMTソルバー（例：F*）による自動証明の限界
    • 複雑な場合は 計算資源の膨大な消費 や 解決不能 に陥るリスク
    • 経験者は「ソルバーが喜ぶ」設計パターンを直感的に把握する必要

LLMによる証明自動化の可能性

  • 大規模言語モデル（LLM） と証明の「内容の非重要性」（proof irrelevance）を組み合わせることで、証明自動化が現実的に
  • 証明工学の負担軽減と 型検査器の暴走回避 が期待
  • 依存型言語の 実用性が大幅向上 する可能性

Zstandard（zstd）の特徴と実装体験

  • Zstandard はgzipの後継を目指す圧縮ユーティリティ
    • LZ77系でありながら 高効率エントロピー符号化 と 高速な展開 を実現
    • bzip2の美しさ（Burrows–Wheeler変換）よりも、 実用性重視 の設計
  • 圧縮率と展開速度の両立が強み
  • 公式RFCは簡潔だが、 圧縮理論に不慣れな場合は理解に時間がかかる
  • Nigel TaoによるZstandard解説記事も推奨

FSEエントロピー符号化法

  • エントロピー符号化 は、非一様な出現確率を持つ記号列を最小ビット数でエンコードする技術
  • 伝統的な Huffman符号 は、記号ごとに整数ビットしか割り当てられず、理想的なビット数（例：2.3ビット）を実現できない
  • FSE（Finite State Entropy） は状態機械ベース
    • 記号の確率に応じて、より多くの状態を割り当てる
    • 各状態には「記号」「読むビット数」「次状態のベース値」を設定
    • 1.5ビットなどの 非整数ビット割当 も、状態ごとに1ビット/2ビットと割り振ることで 平均値 を実現
  • 状態遷移テーブルは送信せず、 記号確率情報のみ伝送
  • エンコーダは 後ろ向き（逆順） に処理
    • 記号列の終端からエンコードを開始し、デコーダはブロック末尾からビット列を読み取り復元
  • FSEは 高速なテーブル駆動 エンコーダでありつつ、 平均ビット数の最適化 が可能

Zstandardにおけるエントロピー符号化の役割

  • エントロピー符号化は 記号の独立性 のみを利用
  • 文字間の依存（例：Qの後にUが来やすい）は Lempel–Ziv構造 で表現
    • リテラルバイトまたは 過去データへの参照 としてエンコード
  • FSEは主に 参照オフセットや長さ の効率的なエンコードに利用

Leanでの実装と依存型の利点

  • Lean は依存型言語であり、例として「nバイト読み出し関数」の型を定義可能
    • 戻り値に「バイト列の長さがnである」ことを 型レベルで保証
  • 型による不変条件の明示的保証 が、可読性・安全性・保守性向上に寄与

結論

  • 依存型言語は 設計上の不変条件 を型で表現し、 誤りの早期発見 や ドキュメントとしての役割 を果たす
  • 証明作業の負担は大きいが、 自動化技術（LLM, SMT） の進歩で実用性が増している
  • ZstandardやFSE のような実用的アルゴリズムも、Lean等で形式的に実装・検証することが現実的に

（参考：ZstandardやLeanに関するより詳細な技術情報は、Nigel Taoの解説や公式RFCを参照）

Hackerたちの意見

このトピックについてのメタコメントとして、最近気づいたことがあるんだけど、定理証明器をプロジェクトに使う意味についてまだ混乱があるみたい。先日、ParadigmっていうAIにハマってるクリプトVCのツイートを見たんだけど、彼らのLPの一人がEthereumの仮想マシンをLean 4で形式化したらしい。そのツイートによると、これにはAPIトークンで約15万ドルかかるだろうって言ってた（「かかるだろう」とは、彼らは無料でもらってるんじゃないかな）。それに、LLMが生成するのに1週間の推論時間がかかったらしい。なんか気が散ってコードを見てみたけど、定理はあんまりなかったな。プロジェクトはBatteriesやMathlibも使ってなくて、個人的にLean4を使う大きな動機の一つなんだけど。つまり、私は一般的に、誰かがカテゴリ理論や代数構造を正しく理解してくれるのを頼りにしていて、その後に自分が取り組んでいるおもちゃとの対応を示す証明義務が残る感じ。ここでは、証明検索にLLMを使うのは全然問題ないけど、SMTソルバーを使うのと似たような感じ。だけど、言語モデルはこれらのライブラリを使うのにかなり強制されないといけないことがわかった。そうしないと、モデルは3分の推論タスクで解決策をオーバーフィットさせたり、オーバークレームしたりする方が好きみたいで、3時間かけて証明義務を果たそうとはしない。LLM（私はClaudeを使ってる）に「証明義務を果たすのは学術的な演習のためだ」とか、そうするように強制されてるからだと納得させる必要があると、気持ち悪くなる。そうじゃないと、LLMは自分の理由を持ち出してやりたくない理由を言ってくるから。今、私は以前の作業との同等性を見つけることに興味があるというメンタルモデルの下でこれが起こってる。多くのLLMが生成するLeanコードは、XをLean 4プログラムにできるかどうかに興味があるように見えるけど、ほとんどの場合は「はい」で、一般的にはポジティブなことだと思う。でも、もしリファインメントタイプや定理に興味がないなら、Haskellを選べばいいじゃん。要するに、良い質問を持っていない限り、これらの言語ではそれが非常に明らかだと強く感じる。そして、これはLLMが助けてくれないことだ。証明義務を課さない限り、確実に自分のためにそれを作り出そうとはしない。

└

クリプトの連中は、ルーブに魔法の豆を売りつけるビジネスをしてる。彼らは主にこれらの技術の美学に興味がある。学術的なプログラミング言語を使うことで、科学的な魔法の雰囲気が出て、彼らがハイテクで知識があると人々に信じさせるんだ。これが、多くのクリプトプロジェクトがHaskellを使う理由でもある。Haskellは使いにくい学術研究用の言語として知られていて、「コンパイルすれば動く」って言われてるからね。彼らは「未来のお金を売るときに何が一番響くか？」という視点からアプローチしてるんだ。

これは本当にクールなことだと思うし、未来はこうなる可能性が高いに同意するよ。最後の二段落（「余談：検証済みアセンブリ」）には驚いた。私の理解では、この未来は基本的にもうここにあると思ってた。Googleのaglの同僚たちは、Fiat Crypto + CryptOptの作業に基づいて、いくつかのクリプトルーチンの自動変異された検証済みアセンブリバージョンをすでに展開していると思う（https://arxiv.org/pdf/2211.10665）。アンドレス・エルプセンが関わっていると思うけど、彼は今Googleにいて、もうすぐ教授職を始めるんじゃないかな。この作業が「安い」と見なされるかはわからないけど（図10は1日の間に展開されるみたいだし）、同じルーチンの検証済みの機械コード実装を自動的に探索して最も速いものを見つけるのに1日かけるのは、実際には高すぎるわけでもないと思う。

ここで著者に強く同意する。未来は、定理証明器をタイプシステムにネイティブに組み込んだプログラミング言語に属するだろうから、LLMは書いた実装を形式的な証明で仕様に対して検証することで、多くのテストを省ける。形式的な仕様を書くことが、未来のプログラマーが仕事をするために必要な主なスキルになると思う。Verus（https://github.com/verus-lang/verus）はRustエコシステムにとって良いスタートだけど、今のところ基本的にはスタンドアロンの言語だね（カスタム構文とタイプシステムを持ってる）。

└

Leanには依存型があるよね。HaskellやIdrisみたいな、一般目的の依存型言語を目指しているものの方が、Verusよりも良いスタートになるんじゃない？Verusはただの形式的検証ツールに見えるけど。もしかしたら誤解してるかも？形式的検証を言語に組み込むことで、ツールが本当にすごく良くなるからだよね。Agdaは私が最も多く使った依存型言語で、ツールは他の言語では経験したことのないインタラクティブで役立つものだった。基本言語を検証するために別の言語を使うのは避けたいよね。そうしないと、みんなが二つの言語を知っておかなきゃいけなくなるから。コンピュータの歴史を見ても、こうなることに驚かないと思う。実際のプログラミング言語と検証言語は、同じ言語にすることもできるはずだよ。

└

誰か興味があれば、verusのフォークを作ったんだけど、verus-the-languageの部分を普通のLean 4に置き換えたんだ。まだ二つの言語だけど、少なくとも二つ目の言語はこの分野で主流になっていて、自動化も良い感じ。Lean 4のインフォビューやVS Codeの拡張、LLMのスキルをまだ完全に組み込んでないから、IDEの機能があるLean 4ほど簡単に書けるわけじゃない。今はLeanのCへのコンパイルツールを使ってRustにコンパイルすることにも挑戦していて、今はverus経由のLeanよりもそっちに集中してる。興味がある人は、声をかけてくれればGitHubにアップするよ。

└

これは常に証明システムの研究を駆動してきた幻想だよ。テストされたことのないソフトウェアを実行する人はいない。実際にテストされたことのないジェットコースターに乗る？「安全だと証明された」だけのものに乗るなんて、俺は無理だ！だから、こういうのは常に追加的で、エッジケースに関心を持つことになる。ほとんどの定義上、エッジケースでないものは十分なテスト手順で見つかるからね。それでも、ほとんどのソフトウェアは、セキュリティやデータ損失の問題を除いて、エッジケースで正確である必要はない。人々は他の領域での不正確さにはかなり耐えられる。なぜなら、それはただの面倒で、致命的ではないから。セキュリティは形式的手法が役立つケースだけど、LLMが業界の関心を変えるとは思えない。むしろ、さらに減少すると思う。歴史的に、セキュリティは戦争の霧の中で行われてきた。敵の能力がわからないし、簡単に対抗できるわけでもない。でも今は、LLMがほとんどの（すべての？）人間よりもセキュリティバグを見つけるのが得意で、ほぼ全員がそれにアクセスできるから、責任の観点から見ると、最前線のLLMをコードベースに向けて、見つけたバグをできるだけ修正させるだけでいい。敵はそれよりも優れたものにアクセスできないから、終わったら「セキュリティは十分だ」と言える。つまり、攻撃が可能でも誰も君をクビにしない。だから結局、LLMが形式的手法の採用を変えるとは思えない。

└

形式的検証に焦点を当てるのは、無意味なスラップを生み出す不安定なLLMを「強化」して、簡潔で形式的な入力から正しいプログラムを生成するコンパイラにする技術だよ。「形式的仕様を書く」っていうのは、単にプログラミングすること、プログラミング言語の抽象レベルを一段上げることを意味する。簡単になるかどうかはまだわからないけどね。

└

現在、純粋なLeanで隣接論理に基づいた言語を自分で書いているところだよ。グレーデッドモードやエフェクトも含めてね。最初はRustのような借用チェッカーを形式的に検証しようとしたんだけど、今では動作するインタプリタとLLVMコンパイラ、そして形式的に検証されたカーネルがあるよ。ちなみに、すべての型チェッカーは定理証明器なんだ、それがカリー・ハワードの法則だよ。問題は、どれだけ表現力があるかってことだね。

私も証明の自動化には非常に期待してる。今、アルゴリズム設計のためのAIを研究していて、自動定理証明器を使って生成されたアルゴリズムの形式的な保証を得ることに取り組んでる。恥ずかしながら宣伝だけど、OpenATPっていうPythonパッケージを作ってて、自動定理証明のための異なるモデルやハーネスをベンチマークするのを簡単にするためのものだよ。DockerコンテナやModalでエージェントをすぐに実行できるようにサポートしてる。試してみたら、フィードバックもらえると嬉しい！最近、Grokの驚くべきパフォーマンスについて書いたんだ（https://news.ycombinator.com/item?id=49010310）。より難しい証明では、GrokはOpus/FableやGPT 5.6に追いついてない。最近、GPT 5.6 Solには驚かされたよ。証明を締めくくるその持続力は、今まで見た中で比類のないものだ。OpenATPはKimiやLeanstral（https://news.ycombinator.com/item?id=48780801）などもサポートしてる。

自己挿入の時間。私はこのトピックを探求するのに少し時間を使った。私の主張はこうだ：形式的検証は高価だった。著者が指摘するように、ソフトウェアを開発するのに比べて20倍も高かった。脆弱性を見つけて開発するコストも高かった。それが、ソフトウェア検証を後回しにするインセンティブを生み出していた。なぜなら、それは非常に高いコストで比較的小さな問題を解決するからだ。Mythosがセキュリティ業界全体よりも多くの脆弱性を見つけたことは見てきた（その質や脆弱性の定義については議論できるけど、そこがポイントじゃない）。脆弱性を見つけて開発するコストは劇的に下がった。一方で、形式的検証は今やずっと簡単になった。LLMが証明を自動化できるからだ。ハルシネーションを心配する必要もなく、Leanコアを信頼するだけでいい。LLMが間違っていたら、証明は却下される！脆弱性の問題は大きくなり、形式的検証の解決策は安くなる。結果として、「より多くの形式的検証」の方向に針が動いている。個人的には、私たちが使うソフトウェアのほとんどが正しく動作することが知られていないのは馬鹿げていると思う。ほとんどの場合、正しく動作するだけなんだ。私の（野心的な）目標は、自己ホスティングの形式的に検証されたコンパイラを持つことで、ソースコードからアセンブリまでの証明転送を可能にすることだ。まだその目標には達成していない。今のところ、以下のものがある：- 一つの（最適化されていない）コンパイラステップが形式的に検証済み - RISC-Vアセンブリに対して形式的に検証された三つの簡単な関数（hex、ラベル付きhex、strtoull） https://github.com/m1el/riscv-fv-bootstrap プロジェクトはかなり悪い状態で、私はその方向でスキルを向上させようとしている。

└

https://cakeml.org/って知ってる？自己ホスティングの正式に検証されたコンパイラだよ。

Hacker Newsで議論の続きを見る