Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations
本論文は、信頼できないLLMがプログラミング言語間の自己証明的かつ忠実度段階的な翻訳を生成することを可能にする、Lean 4で機械化された計算体系と二重平面システム（「ハーディ・ガーディ」）を提示し、それによって、継続的に進化する人間検証済みの信頼グラフが、増大し続ける確証を伴いながら決定可能なプログラムの問いへと収束することを保証する。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
探偵のジレンマ：メッセンジャーを信頼できないとき
あなたは、自動車のエンジンやビデオゲームのキャラクターの挙動のような、複雑な機械に関する謎を解こうとしていると想像してください。あなたには次のような問いがあります。「時速50マイルでアクセルを踏んだら、この車は衝突するか？」これに答えるためには、単に車を見るだけでは不十分です。車の乱雑で現実世界的なメカニズムを、超高性能なコンピュータ・ソルバー（計算機）が理解できる言語、例えば数学の方程式へと翻訳しなければなりません。しかし、ここに落とし穴があります。その翻訳者がミスをするかもしれないのです。あるギアを忘れたり、ブレーキの仕組みを誤解したりするかもしれません。もし翻訳者が間違っていれば、数学的ソルバーは「間違った問い」に対して完璧な答えを出してしまいます。
コンピュータサイエンスの世界において、これは「翻訳」の問題と呼ばれます。プログラムの安全性を確認するために、プログラムをある言語（CやPythonなど）から別の言語（ソルバーのための論理パズルなど）へ移動させることがよくあります。伝統的に、科学者たちは、橋が誰かが通行する前に安全であることを証明するように、翻訳者が完全に正しいことを一度限りで証明しようとしてきました。しかし、翻訳者が複雑であったり、あるいは人工知能によって書かれていたりする場合、それは非常に困難なことです。この論文は異なる問いを投げかけます。「翻訳者が完璧であることを証明しようとするのをやめて、代わりに、動作している最中に翻訳者のミスを捕まえるシステムを構築したらどうだろうか？」これは、たった一人のガイドに森への案内を任せるのではなく、複数のガイドのチームを作り、お互いの地図をチェックさせ、「もし意見が食い違ったら、立ち止まって誰が間違っているのかを突き止める」というルールを設けることの違いなのです。
「ハーディ・ガーディ」マシン：信頼できる回答を生み出す工場
この論文は、hurdy-gurdy（音楽を奏でるためにハンドルを回す楽器にちなんで名付けられましたが、ここでは答えを繰り出すという意味です）と呼ばれるシステムを紹介しています。Christoph Kirsch氏率いる著者らは、コンピュータプログラムを扱う新しい方法を提案しています。それは、すべてのステップがチェックされ、すべての回答に「レシート（受領書）」が付いてくる「伝言ゲーム」のようにプログラムを扱うというものです。
核心となるアイデアはシンプルですが強力です。「翻訳者を信じるのではなく、プロセスを信じろ」。
あるC言語で書かれたプログラムについて質問があるとします。システムは単に一つの翻訳者に送るのではなく、プログラムを二つの異なる経路に送ります。
- 翻訳： プログラムは、より単純な論理言語へと翻訳されます（小説を数学の方程式に変換するようなものです）。
- ダブルチェック： システムは、元のプログラムと翻訳されたバージョンを並行して実行します。そして、それらが同じように振る舞うかどうかをチェックします。もし同じであれば、成功です。もし異なれば、システムは、まるで審判が選手がファウルした瞬間に笛を吹くように、どのステップで両者が乖離したのかを正確に指し示します。
- 「ウィットネス（証人）」のトリック： もしソルバーが「はい、クラッシュの可能性があります」と言ったとしても、システムはソルバーの言葉をそのまま鵜呑みにしません。システムはその「証明」（クラッシュを引き起こす具体的な条件）を取り、それを翻訳を通じて「逆方向に」走らせます。その条件を元のプログラムに投入するのです。もし元のプログラムが実際にクラッシュすれば、その答えは100%本物です。システムは「犯罪現場を再現」したことになります。
二つの平面：構築と使用
このシステムには、工場の作業場とショールームのような、二つの明確なモードがあります。
- 使用平面（ショールーム）： ここでは回答が行われます。ここでは、AI（または人間）が質問を投げかけます。システムは推測するのではなく、ルートを選択し、翻訳をチェックし、もし答えが「はい、可能です」であれば、再現を実行して証明します。もし答えが「いいえ、不可能です」であれば、システムは、複数の翻訳者、複数のソルバー、さらには数学的に検証された証明書といった、一連のチェックの積み重ねに依拠して確信を得ます。
- 進化平面（工場）： ここではシステムが成長します。もしシステムが質問に答えられない場合、単に諦めるのではなく、「なぜ失敗したのか」（例：「この特定の種類のループに対する翻訳者が存在しない」など）を書き留めます。そして、その空白を埋めるための新しい翻訳者を構築するためにAIを使用します。構築された後、新しい翻訳者は古いものと比較テストされます。合格すれば、レジストリに追加されます。失敗すれば、修正されます。このループは無期限に回り続け、システムをより賢く、より信頼できるものにしていきますが、決定的なのは、この成長プロセス自体は質問に答えることはないという点です。それはツールを構築することだけを行います。
「信頼できない著者」という展開
この論文で最も驚くべき部分は、翻訳者自体が信頼できないAIエージェントによって構築されたという点です。著者らは翻訳者を手作業でコーディングしたのではなく、AIモデルに対し、一枚の解説文に基づいて作成するよう依頼しました。通常、これは悲劇を招きます。しかし、システムがすべてのステップをチェックするため、AIのミスは即座に発見されました。
例えば、あるテストにおいて、AI翻訳者が特定の命令を見落としたため、元のプログラムとは異なる挙動を示しました。システムの「スクエア・チェック（並行比較）」は、このエラーを即座に特定し、正確な行と変数を突き止めました。その後、システムは翻訳者を修正しました。この論文は、たとえ間違える可能性のあるAIが著者であっても、システムのアーキテクチャが最終的な回答の信頼性を保証することを証明しています。
システムが見つけたもの（および見つけられなかったもの）
著者らは、2026年7月時点の彼らの成果を用いてこのシステムを実行しました。測定結果は以下の通りです。
- カバレッジ（網羅率）： 彼らは、13種類の異なる言語（C、Python、さらには化学反応ネットワークを含む）のプログラムを論理ソルバーへと翻訳することに成功しました。RISC-Vプロセッサ言語については、96個の96個の特定の命令タイプをカバーしており、これはシステムが、情報を失うことなくそのセット内のすべての命令を扱えることを意味します。
- 一致度： 同じ質問を二つの異なる翻訳経路（一つはマニュアルに基づくもの、もう一つは形式モデルに基づくもの）に送ったところ、テストケースにおいて回答は**100%**一致しました。
- 検出された欠陥： システムは、自身の翻訳者やツールの中に24個の特定の欠陥を発見しました。単純なタイポもあれば、AIがコンピュータの命令の仕組みを誤解した論理エラーもありました。決定的なのは、人間がコードを確認することなく、システムがこれらのエラーを発見したことです。
- 「死角」： システムは限界も見出しました。もし二つの異なる翻訳者が、全く同じミス（同じルールを誤解したために）をした場合、システムはそれを検知できません。これは「コモンモード故障」と呼ばれます。論文はこのリスクを認めていますが、翻訳のソースを多様化することで、システムはこのリスクを最小限に抑えるよう設計されています。
- LLMプレイヤー： AIがシステムを使用して回答できるかをテストしました。ある実験では、ツールを持たないAIは8問中7問に正解しましたが、難しい問題では推測しました。システムを用いたAIは、8問中8問すべてに正解し、すべての回答にマシンチェックされた証明が付随していました。
結論
この論文は、すべてのコンピュータの安全性の問題を解決したと主張しているわけではありません。AI翻訳者が完璧になったと言っているわけでもありません。そうではなく、信頼できないパーツから、信頼できるシステムを構築できることを証明しています。
すべての翻訳を潜在的なミスとして扱い、改善を定着させるための「ラチェット（逆転防止装置）」を構築することで、システムは信頼の梯子を作り上げます。もし質問が「これは起こり得るか？」であれば、システムはイベントを再現して証明できます。もし答えが「いいえ、これは起こり得ない」であれば、システムは独立したチェックと数学的に検証された証明書の連鎖を用いて確信を得ます。
著者らは、グラフによるルートの利用、全ステップのチェック、そして証拠の再現というアプローチが、現代のソフトウェアの複雑さを扱うための、実行可能な方法であることを結論付けています。たとえ、ツールを構築する人々（あるいはAI）が過ちを犯す可能性があるとしても、これは「著者を信頼する」ことから「アーキテクチャを信頼する」ことへの転換なのです。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。