海外の反応
2026年11月10日
【海外の反応】DeepMindがSignalの暗号を形式的に証明、海外エンジニアらが議論
DeepMindが発表した「AlphaProof Code」は、複数のAIエージェントが研究チームのように作業を分担し、コードが仕様どおりに動くことをLeanという形式手法で数学的に証明する仕組みだ。今回はメッセージアプリ「Signal」の暗号プロトコルの検証に使われ、海外の技術者向け掲示板Hacker Newsで話題になった。コメント欄では「いずれ未検証のソフトウェアを動かすこと自体が、平文HTTPを使うのと同じくらい異常に見える時代が来る」という楽観論と、「検証されたのは暗号プロトコルだけでSignalアプリ全体ではない」「Leanの仕様が実際のRustコードの動きと本当に一致しているかは別問題」という慎重論が入り混じった。
AlphaProofコード — DeepMindによる、コードを自動で形式的に検証する新技術の発表
出典: deepmind.google / 元記事はこちら
3
海外の名無しさん
2026-11-10 13:06
近いうち、2〜3年のうちに、未検証のソフトウェアを動かしていたこと自体が、今からするとTelnetや暗号化なしのHTTPを使っていたのと同じくらい『正気とは思えない』行為に見えるようになると思う。
4
海外の名無しさん
2026-11-10 13:07
「AlphaProof Codeは、研究チームのように形式検証の作業を分担するマルチLLMエージェントフレームワーク」とあるけど、この表現は正確なのか怪しい。少なくとも言い回しがちょっと変だ。本当に言いたいのは『マルチエージェントシステム』(複数のLLMを使うことを含む場合が多いが、必須ではない)なんじゃないかと思う。
5
海外の名無しさん
2026-11-10 12:34
すごいな。去年は『AIにコードを書かせる機会が増えて、これからソフトウェアはもっとバグが増えるだろう』と思っていたけど、こういうツールが出てくると、むしろソフトウェアの未来はもっと安全になるんじゃないかと希望が持てる。
18
海外の名無しさん
2026-11-10 12:42
AIが巨大な証明を壊していないか確認するのに、CIを1回実行するたびに1万ドルかかるようになれば、さらに『安心』だね。
6
海外の名無しさん
2026-11-10 12:44
論文はこちら: https://google-deepmind.github.io/code-verification/
7
海外の名無しさん
2026-11-10 12:50
そのうちCPUの検証もできるようになってほしい。もちろんそれはずっと難しい。CPUはオープンソースではなく物理的なものだから、完全に検証するには物理現象までシミュレートする必要がある。
19
海外の名無しさん
2026-11-10 12:56
一部はある。https://www.crowdsupply.com/sutajio-kosagi/precursor …ゴホン、CPUっぽいもの。
8
海外の名無しさん
2026-11-10 12:56
Leanのコードが、証明対象のコードの内容を正しく表していることをどうやって証明するの?
9
海外の名無しさん
2026-11-10 12:28
これにいくらかかったんだろう
20
海外の名無しさん
2026-11-10 12:39
新しいFableが出た日の夜に一発で作られたらしいよ
35
海外の名無しさん
2026-11-10 12:48
記事によると4週間かかったらしい。
36
海外の名無しさん
2026-11-10 12:40
で、結局何百万ドル?何十億ドル?
10
海外の名無しさん
2026-11-10 12:27
謝辞にサンダー・ピチャイの名前が入ってる。まあ分かるんだけど、それにしても…
21
海外の名無しさん
2026-11-10 12:35
これは絶対、内輪のジョークだろ
11
海外の名無しさん
2026-11-10 12:31
次はTelegramでもやって、『Telegramは独自の暗号方式を作るべきじゃなかった』論争に決着をつけてほしい
12
海外の名無しさん
2026-11-10 12:58
『何を証明すべきかは人間の専門家がAIと一緒に決める』とあるけど、なぜそこもAIにやらせられないんだろう?これがAIの本質的な限界なのか?
22
海外の名無しさん
2026-11-10 13:11
『何を証明すべきか』は本質的に価値判断の問題で、単なる機械的な推論の適用ではないからだと思う。
23
海外の名無しさん
2026-11-10 13:06
まだ人間をループに入れているのは、その方が人間が納得しやすいからだよ
13
海外の名無しさん
2026-11-10 12:28
『形式証明』については全然詳しくないんだけど、深く調べなくても気になる点がある。これはハルティング問題(停止性問題)、あるいは結局そこに行き着く関連問題をどう扱っているんだろう?
24
海外の名無しさん
2026-11-10 12:38
ハルティング問題が妨げるのは、証明器が『すべての』プログラムに対応できることだけだよ。『stop』や『while(true)』みたいなプログラムなら証明は簡単。もっと洗練された解析器を使えば、対応できるプログラムの範囲はどんどん広がる。
27
海外の名無しさん
2026-11-10 12:41
ゲーデルの不完全性定理が数学の証明を不可能にしているわけではないのと同じ理屈だよ(これ、皮肉で言ってるわけじゃないからね)。
29
海外の名無しさん
2026-11-10 12:31
Leanはハルティング問題とは関係ない。証明をコードとして書けるようにした言語で、そのコードを処理するコンパイラが数学的な制約を適切に強制する仕組み、と考えればいい。
14
海外の名無しさん
2026-11-10 12:21
我々の『ロボット支配者』からもSignalが好評らしくて安心した。
15
海外の名無しさん
2026-11-10 12:26
Signalほどの巨大なコードベースが、実用上の意味だけでなく、厳密な形式的な意味でも安全だというのは本当に驚きだ。Signalのコードを書いた人たちは、最高クラスの技術者に違いない。
30
海外の名無しさん
2026-11-10 12:53
これが検証したのはSignalアプリそのものじゃなくて、Signalの暗号プロトコルだけだよ
31
海外の名無しさん
2026-11-10 12:31
うん、それでもかなりすごいけど。
32
海外の名無しさん
2026-11-10 12:36
暗号部分は安全かもしれないけど、残りのコードについてはそこまで自信を持てないな。
16
海外の名無しさん
2026-11-10 13:07
Leanで作ったプロセッサのモデル上で動くコンパイル済みのRustコードの挙動が、実際のプロセッサの挙動と一致していることは、どうやって保証されるんだろう?そもそも、仕様書をもとに書かれたLeanの仕様が、Signalを実装しているRustコードの実際の動きと一致していることは、どうやって分かるの?
28
海外の名無しさん
2026-11-10 12:32
『ハルティング問題が障害にならない理由』を聞いてるのか、『ハルティング問題自体の証明方法』を聞いてるのか、どっち?前者への答えはいつも同じで、『すべてが証明可能だと保証しない、特に有限時間内での証明可能性は保証しない』というだけの話。
34
海外の名無しさん
2026-11-10 12:52
Signalプロトコルの暗号化を行う実際のライブラリを変更する機会って、そんなに多い?アプリに機能を追加するのに暗号化部分を変える必要はないはずだけど。
38
海外の名無しさん
2026-11-10 12:38
いや、確かに関係はあるよ。ハルティング問題のせいで、気にしているすべての性質を証明できるわけではないかもしれない。でもそれはどちらかというと理論上の問題で、実用上の問題ではない。
40
海外の名無しさん
2026-11-10 12:44
連絡先をホワイトリスト化していれば、記者が軍事作戦の計画グループに誤って追加されるという失態は防げたはずだ
42
海外の名無しさん
2026-11-10 12:56
本当にそうかな?記憶している限り、その記者の番号はiOSの何らかの『親切機能』によって既存の連絡先に追加されてしまったはずで、ホワイトリストがどう役立つのかは分からない。
この話題の背景と論点
形式検証(フォーマルベリフィケーション)は、プログラムの振る舞いを数学的に証明する手法で、航空機や暗号など高信頼性が求められる分野で使われてきたが、証明を書く手間の大きさが普及の壁だった。AlphaProof Codeは、この証明作業を複数のAIエージェントに分担させて効率化を試みたもので、対象になったのはSignalの「暗号プロトコル」部分であり、アプリ全体の安全性が保証されたわけではない点は誤解しやすい(レス30・32が指摘)。スレではハルティング問題(停止性問題)を持ち出す声もあったが、形式検証はすべてのプログラムの停止性を証明する必要はなく、対象を絞れば現実的に機能する。レス40が触れた「記者が機密チャットに誤って追加された」事件は、2025年に米政権内で実際に起きたSignalの運用上のトラブルで、暗号方式自体の脆弱性ではなく連絡先管理の設定ミスだった点も押さえておきたい。
※本記事は海外掲示板 Hacker News のスレッド「AlphaProof Code」から抜粋し、編集部で日本語に意訳したものです。訳文の責任は当サイトにあります。
この記事のリアクション
まだコメントはありません。