ハクソク

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

クロードは時々それを証明できる

2025年9月17日原文(galois.com)

概要

  • AnthropicのClaude Code は、 対話型定理証明（ITP） で高い性能を発揮
  • Lean などのITPツールは強力だが、従来は 専門家でも扱いが難しい
  • Claude Codeは 証明作業を自律的に進める が、全体管理には人間が必要
  • AIエージェント として、従来のAIチャットボットよりも多様な作業に対応
  • AI活用による定理証明の民主化 と効率化への期待

Claude Codeによる対話型定理証明の革新

  • AnthropicのClaude Code は、AIによる ソフトウェアエンジニアリング支援エージェント
  • Lean などの対話型定理証明（ITP）ツールで、 複雑な証明ステップの自動化 を実現
  • ITPツール は暗号ライブラリやOSなどの 重要なシステムの形式的検証 に利用
  • 従来、 ITPは専門家でも時間と労力がかかる分野
  • Claude Codeは 証明作業を自律的に実行 し、ユーザーは プロジェクトマネージャー的役割 に集中可能
  • AI活用により、ITPの敷居が下がり、より多くの人が利用可能 になる可能性

対話型定理証明（ITP）の難しさ

  • ITP は、 自動化しやすい数学の制限 と 一般性・強力さ のトレードオフが存在
  • SMTソルバー は単純な論理式の証明自動化に強いが、数学的な一般性は低い
  • LeanやCoq などのITPツールは、 ほぼあらゆる数学的対象 を扱えるが 操作が難解
  • インターフェースの複雑さ、ライブラリの不足、エラーメッセージの難解さ などが障壁
  • 抽象的思考力 や 細かい形式的記述への忍耐力 が要求されるため、 専門家でも挫折しやすい

定理証明は「証明」だけではない

  • ITPツールの利用は 単一の定理証明だけではなく、証明工学的作業全体 が重要
    • 概念の定式化、 Leanへのマッピング、 定理の分解、 証明の実装、 エラー解析 など多岐
  • AIモデル は個別定理の証明には使えるが、 全体的な証明プロジェクト管理 には不十分
  • 現実的なITP作業は ソフトウェアエンジニアリングに近い「証明工学」
  • 抽象選択、リファクタリング、要件分析、失敗修正 なども重要な作業

Claude Codeとは何か

  • Claude Code は、 コマンドラインで動作するAIコーディングエージェント
  • ChatGPTのような単発Q&A型ではなく、複雑なタスクを自動で分解・実行
  • 例：
    • 未コミット変更のレビューとコミット作成
    • スレッドプールの表現選定と定義
    • 証明不可能な定理の原因調査と修正提案
  • 各サブタスクを自動でTODO化し、ファイル探索・ビルド・エラー解析・修正案作成 などを実行
  • コマンド実行にはユーザー承認が必要 で、安全性には注意が必要

Claude CodeによるLean証明の実際

  • Lean形式化プロジェクト （Deny-Guarantee Reasoning論文）でClaude Codeを活用
  • 研究論文をテキスト化し、形式化計画を策定
  • プロジェクトマネージャーとしてAIに指示し、段階的に定理定義・証明を進行
  • 定理定義と証明を分離し、まずダミー証明（sorry）で構造構築
  • AIは エラー検出→修正→再ビルド のサイクルで正しい証明を自動生成
  • Leanの厳格なエラー出力 がAIの自己修正能力を高める要因

AIエージェントの今後と定理証明の未来

  • AIエージェントの進化 によって、 専門家不要な定理証明 の時代が到来する可能性
  • 証明工学の民主化 により、形式的手法の普及・効率化が期待
  • AIに最適化したツール設計 （失敗情報の詳細出力など）が今後の課題
  • 安全性・セキュリティ問題 への配慮も重要な研究テーマ

Hackerたちの意見

私が見つけたのは、間違いを検出できるツールがあれば、エージェントはそれを修正できることが多いということです。この記事全体で最も重要な一文です。AIソフトウェア開発のマニフェストを2年間にわたって繰り返し考えてきた中で、私が見つけた最も重要な属性は、経験的検証でした。AI（と人間）は自分の仕事を正確に判断できないけれど、AI（と人間）に経験的検証の能力を与えると、その成功率は急上昇します。これは直感的かもしれませんが、AIにもこれが当てはまることをテストしている論文がまだあります。AIにユニットテストを書かせようとする中で、私はファジングを取り入れています。そうすれば、AIはボーナステストでズルをできなくなるからです。学校に戻ってインタラクティブ定理証明を使うというアイデアは全く思いつかなかったのですが、今それが提案されて、AIの使い方を進めるための全く新しいパラダイムシフトになりました。AIは人間にはできない速度で反復できます。基本的な経験的検証（コードを構築し、テストを実行する）さえあれば、人間をループから外せます。それをファジング（例えばGolangを使って）に移行すれば、人間が介入する前に、はるかに良いカバレッジと進捗が得られます。だから、インタラクティブ定理証明がAIにぴったり合うのは驚くことではありません。この同じ教訓が他のところでもどう展開されるかが面白いです。記事の前半で > 「なぜITPはそんなに難しいのか？」いくつかの理由はかなり明白です：インターフェースが混乱している、ライブラリが乏しい、ドキュメントが不十分、エラーメッセージが謎めいている。でも、これらは面白い問題ではありません。llvmが素晴らしいC++エラーメッセージを提供したときのことを覚えていますか？それは人生を変えるものでした。高品質なエラーメッセージは、エラーを迅速に見つけて修正し、素早く反復できることを意味します。これらは実際に最も面白い問題で、ユーザーがより早く学ぶことを可能にします。ユーザーが高い成功を収めると、その製品を何度も使うようになります。すべてのツールで高品質なエラーメッセージがあれば、Claudeのコードは人間の介入なしに問題に長く取り組むことができ、ミスも少なく、全体的に速く作業できるようになります。エラーメッセージは常に良いものであるべきですが、新たな問いがこのことを強調します。「AIがこのエラーメッセージに遭遇したとき、それを修正できるのか？」

└

これです。今、さまざまなリンターや静的チェックにもっと時間を投資するのは、実際に非常にコストパフォーマンスが良いです。AIはリンターを書くのに10%の時間で助けてくれるだけでなく、リンターは通常、実際にテストしやすい短いスクリプトなので、AIにとっては楽な道です。でも、例えば大規模なリファクタリングをした後に「このリンターを通すようにして」とAIに頼むのは、非常に効果的で時間を節約できます。

生成的ML（および他のヒューリスティック手法）と形式的手法を組み合わせるのが、システム設計において最も有望な進展方法です。形式的手法（およびシステムの複雑さを制限するような他の制約）がなければ、私たちは混沌とした状態に向かってコードを書いてしまうでしょう。

└

我々は混沌に向かってバイブコードしていくことになる。公平を期すために言うと、過去50年間、AIがなくてもそうしてきたけどね。

インタラクティブ定理証明器を聞いたことがある人は、これは天国のマッチになるだろうと思ったでしょう。LLMは実装の手間を減らしますが、レビューの手間は膨大になります。インタラクティブ定理証明器はレビューの手間を減らしますが、実装にはもっと多くの作業が必要です。両者を組み合わせることで、機械の思考のスピードで両方の良いところを得ることができます。

（おおよそ）サイモン・ペイトン・ジョーンズの言葉を引用します。「プログラムを書くのは難しくない。プログラムが何をすべきかを指定するのが難しい。」何を証明するの？著者は、エイリアンが「gccの正しさを要求する」問題についてよく知っています。また、「誰も正しさを気にしない」とか「人々は遵守を気にする」と言っている他の投稿も楽しみました。ほとんどの人は専門家ではなく、専門家になることもないと言っても安全です。実装が仕様を満たしていることを確認するために、適切な仕様を考え出すスキルを身につけることは、AIのハイプ業界がもはや必要ないと保証するような、すべての形式的なトレーニングを必要とするでしょう。だから、専門家が使うときにLLMがトークンを操作するのが得意でも、大きな意味ではあまり役に立ちません。彼らが良い方向でコスト・ベネフィットのバランスを変えることが期待されますが、業界の大きな問題はそのまま残るでしょう。より根本的な変化が必要なのは、もっと多くの人が仕様の価値を理解することです。これは教育の問題で、逆説的にAIが多くの助けになる可能性があると思います…もし人間が専門家になるためにAIを使うことに十分な興味があれば。

└

この変化は今まさに起きています。私の作業リポジトリは、主にエージェント向けに意図されたマークダウンが増えてきていますが、それは私がソフトウェアエンジニアとして役立つように、要求や重要な設計決定を伝える密な専門用語です。低レベルのコードからこれらの仕様を書く手間は、今日ではかなり少なくなっています。なぜなら、LLMもそれを大いに助けてくれるからです。

└

プログラムを書くのは難しくない。プログラムが何をするべきかを指定するのが難しい。でも、この二つはちょっと同じことなんだ。プログラムを書くっていうのは、何をするべきかを非常に具体的であいまいさのない方法で指定することがほとんどだから。だから、プログラミング言語があって、英語は使わないんだ。PRD、設計書、そしてコード自体は、指定のレベルが上がるにつれて、みんな同じようなものなんだ。もし正式な仕様に触れたことがあるなら、「あれ、結局プログラムの別の実装を書いてるだけじゃん！」って気づいたことがあるかもしれないけど、実際そうなんだよね。

└

あなたは、ソフトウェアの正しさや形式的手法のサークル内でのもっと内部的な議論を見逃してると思うよ。「良い/正しいソフトウェアを書く」っていう一般的な議論よりもね。演繹的定理証明は1970年代にすごく流行って、トニー・ホーアやダイクストラのような著名な人たちが、正しいソフトウェアを書く唯一の方法だと信じていたほどなんだ。年月が経つにつれて、モデルチェックから不健全な手法（コンコリックテストやプロパティベーステスト、コードレビューなど）に焦点が移って、演繹的証明の支持者たちが考えていたよりも効果的だと証明されてきたんだ（トニー・ホーアは90年代に自分の間違いを認めた）。演繹的証明の問題は、全か無かってことなんだ。つまり、定理を証明するかしないかのどちらかで、他の方法よりもコストと信頼性のトレードオフを調整するのがずっと難しいんだ。その結果、定理証明は他の代替手法ほど自動化の恩恵を受けていなくて、今ではコストに対してリターンが低すぎると見なされている。でも、もしLLMが演繹的定理証明の自動化を助けられるなら、形式的手法のサークル内で徐々に人気が薄れてきたこのアプローチが復活するかもしれない。もちろん、仕様はすべての方法で同じくらい重要だけど、定理証明の特定の方法は他の形式的および半形式的手法と比べて不利な立場にあったと思うし、著者もそれが変わることを望んでいるんじゃないかな。

└

あなたの読み方はアラン・ケイのQuoraみたいで、敬意を表します、同志。

一般的なアドバイスの中で、私のCLAUDE.mdは、Claudeに各変更単位が期待通りに機能することを証明するように求めています。私は通常、テストを書いて、それが実際に実行されて合格していることを納得させてくれることを期待しています。ここで証明支援ツールは過剰な気がしますが、Claudeはしばしばこれらの非公式な証明を組み立てるのに苦労しています。オープンエンドの言葉による証明と比べて、より形式的な証明言語の利点が見えると思います。「過剰」という言葉はもちろん編集的な言葉で、https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...について知っているなら、多くの静的型付けプログラミング言語が本質的に証明支援ツールであり、証明の目標は適切に型付けされたプログラムを生成することだとわかるでしょう。LLMは、例えばRustの借用チェッカーとやり取りする際に、すでにかなり得意です。

最近gpt-5-highを使っていて、遅いけど、解決できる問題の種類にはかなり感心しています。Claudeがつまずいたコーディングタスクを与えたら、同じツールセットでうまく対処してくれました。本当に印象的でした。信頼性が高くなることで新しい能力を解放しそうな感じがします。著者がClaudeのコードに感心していたなら、gpt-5に驚かされてもおかしくないですね。

Hacker Newsで議論の続きを見る