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

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

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

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

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

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

Claude Code/Codexを使ったことがあるけど、すごく良いよね。でも、ちょっと質問があるんだ。Leanみたいなツールは使ったことがないんだけど、もしLLMがLeanで証明を書くとしたら、そのコード自体（証明の中で）が正しいかどうかどうやって確認するの？それとも、Leanってそんなに厳密だから、そういうことは起こりにくいのかな？

記事の約2/3のところに埋もれてるけど、「私は正式化計画の50%のところにいます…」って。これを見た瞬間、私は懐疑的になった。AIツールを使ったことがある人なら、プロジェクトの最初の80%は稲妻のように進むけど、最後の20%はAIにとってほとんど不可能だってことを見たことがあるはず。たとえそれが他のコードよりも複雑に見えなくてもね。AIはコードが大きくなるにつれて、要求が具体的になると苦労するんだ。とにかく、プログラマーに「50%」のマークを正確に判断させるのは絶対に信じない方がいいよ。90%に達したら、ゴールに到達するためにさらに90%必要になるから。

これが私のClaude Codeの経験をうまくまとめてる。素晴らしいツールだけど、しっかり管理しないといけない。課題は、特定のユースケースに対してどこでどんな問題が起きるかを、広範に使ってみるまでわからないことだね。著者の場合、あまり自信を持てない形式的な証明を作るのは逆効果に感じる。ここで重要な部分を見落としている可能性が高い。もしかしたら、大規模言語モデルをタスクに集中させ、その出力を検証し、私たちの代わりに挑戦するために特別に訓練されたモデルが必要なのかも。とはいえ、深い専門知識は依然として不可欠だよ。それがないと、物事が奇妙な方法や意図しない方法で構築されることがある。実用的な回避策（典型的なアプリ開発や形式的な検証ではなく）は、システムをブラックボックスとして扱い、慎重に書かれた仕様やテストケースに頼ることかもしれない。多くの状況で、そのアプローチが不確実なプロセスから確実性を引き出そうとするよりも効果的かもしれない。

これには非常に驚いているし、君もそう思うべきだと思う。なぜか？私の最初の仮定は、Claude CodeがLean証明を書くのが非常に得意だということだ。記事に書かれている理由の多くからそう思う。証明を書くために自分のコーディングワークフローを試すのはずっとやりたかったことなんだ。OPがやってくれて嬉しい。でも、彼がなぜこれに驚いているのかは書かれていなかった。 編集: 明確にするために言うと、私はこの部分について話している: > Claude Codeが定理証明に驚くほど良い理由の一部だと思う。Leanは受け入れるプログラムに非常に厳格だから。これが人間にとってLeanを書くのを苦痛にするけど、AIエージェントには詳細なフィードバックを与えることになる。私は最初にRustプログラムを書くときにこれに出会った。最初はCursor（人間的モデルを使用）で、今はClaude Codeで。状況は改善されたけど、最初はRustがトレーニングセットにあまりよく表現されていなくて、エージェントはひどい初心者のミスを犯していた。Rust風の構文でJavascriptのようなコードを書いて、それが動くと思っていた。でもrustcコンパイラは非常に良いエラーを出してくれて、文脈や修正の提案もしてくれる。2、3回の反復で、私が関与することなくすべてのミスを修正してくれた。そして、Rustの型システムと安全性の保証が非常に厳格だから、コンパイルできる段階に達すると、たぶんうまくいく。あの経験以来（コーディングエージェントを使った最初の経験）、機械チェックされた証明を書くのが非常に得意だろうと仮定している。