あなたは、ミステリーを解決しようとしている探偵だと想像してください。ただし、暗い路地裏で手がかりを探すのではなく、コンピュータプログラムの中で手がかりを探しています。具体的には、どちらの道に進むかを決めるためにコイン投げをするような、ランダムな選択を行うプログラムを探しています。コンピュータサイエンスの世界では、これは「確率的プログラム（probabilistic program）」と呼ばれます。これらのプログラムは、まるで魔法のサイコロ使いのようです。単に一つのことを行うのではなく、起こる確率に応じて多くのことを行います。ランダムであるため、「それはうまくいったか？」と聞くことはできません。「平均してどれくらいうまくいったか？」そして「試行錯誤している間に、どれだけのエネルギーや時間を無駄にしたか？」と聞かなければならないのです。

長い間、これらのランダムなプログラムを検証することは、素手で滑りやすい魚を捕まえようとするようなものでした。魚（コード）は見えますし、数学（確率論）も分かっています。しかし、そのコスト（時間やバッテリーなど）が正確にどれくらいになるかを証明するのは、非常に困難です。通常、あなたは二つの別々の物語を書かなければなりません。一つはプログラムが何をするかについての物語、そしてもう一つは、いかにコストがかかるかについての長く退屈なマニュアルです。そして、それらが一致するように、一行ずつ手作業で二つの物語を縫い合わせなければなりません。これは非常に退屈で、ヒューマンエラーが起きやすく、人々が彼らのランダムなアルゴリズムが実際に安全で効率的であることを検証するのを妨げてきました。

ここで、オーストリアとドイツの研究チームが新しいツールを携えて登場します。彼らは、Liquid Haskellというプログラミング言語のための、特別な「コストを意識した確率モナド（cost-aware probability monad）」を構築しました。モナドを、プログラムが持ち運ぶ「魔法のバックパック」だと考えてください。通常、このバックパックはランダムな選択の結果だけを保持します。しかし、研究者たちが作ったこの新しいバックパックは特別です。そこには、組み込みの計算機とGPSが付いています。プログラムがステップを踏むたびに、バックパックは自動的にステップの総コストと、そのステップが発生する確率を更新します。それは単にデータを保持するだけでなく、数学を知っているのです。このスマートなバックパックを使用することで、研究者たちは、コンピュータがランダムなプログラムのコストを自動的にチェックできることを示し、困難な手作業のパズルを、ほぼ自動的なプロセスへと変えました。彼らはこれを、リストのソートやデータの管理といった古典的な問題でテストし、彼らの新しい手法が正確であるだけでなく、従来の方法よりもはるかに高速で使いやすいことを証明しました。

ランダムなプログラムのための魔法のバックパック

ビデオゲームで、キャラクターが障害物を飛び越えなければならない場面を想像してください。コンピュータが仮想のダイスを振る方法によって、ゲームが簡単なこともあれば、難しいこともあります。コンピュータサイエンスでは、これらを「確率的アルゴリズム（probabilistic algorithms）」と呼びます。これらは、厳格でステップ・バイ・ステップの指示よりも速く、よりスマートになれるため、非常に有用です。しかし、落とし穴があります。ランダム性に依存しているため、どれくらいの「燃料」（時間、お金、または計算資源）を消費するかを正確に予測するのが難しいのです。

長年、コンピュータサイエンティストたちはある問題に直面してきました。ランダムなプログラムが効率的であることを証明するには、二つのことを別々に行う必要がありました。まず、プログラムが正しく動作することを証明し、次に、平均コストを計算するための全く新しい証明を書き上げる必要があったのです。それは、ケーキを焼いた後に、レシピに書いてあるからといって、砂糖を正しい量使ったことを証明するために別途エッセイを書かなければならないようなものでした。このプロセスは遅く、間違いが起きやすいものでした。

この論文の著者であるMatthias Hetzenberger、Georg Moser、およびFlorian Zulegerは、プログラムのための新しい種類の「バックパック」を作ることで、これを解決することに決めました。プログラミングの世界では、「モナド」とは計算を扱いやすくするためにラップする方法のことです。チームは、「コストを意識した確率モナド」を作成しました。これは、ランダムなコイン投げの結果を運ぶだけでなく、コストと確率の経過累計も一緒に運ぶ、魔法のバックパックのようなものです。

仕組みは以下の通り、簡単に説明します：

1. バックパックは数学を知っている： プログラムがコインを投げる（ランダムな選択をする）とき、バックパックは自動的にその投げの平均コストを計算します。人間が数学を書き留める必要はありません。バックパックがあなたに代わってやってくれます。
2. すべてを追跡する： プログラムが実行されるにつれ、バックパックはスコアを記録していきます。もしプログラムが1ユニットの時間かかるステップを踏めば、バックパックは合計に1を加算します。もしプログラムが二つの経路に分岐した場合、バックパックは両方の経路を合わせた平均コストを算出します。
3. コンピュータと対話する： 研究者たちは、コードのミスをチェックする非常にスマートなロボットのようなツールである「Liquid Haskell」を使用しました。彼らの「コストを意識したバックパック」をLiquid Haskellに組み込むことで、ロボットが数学を自動的にチェックできるようにしました。ロボットはコードを見て、「はい、このランダムなソートアルゴリズムはおよそ 2(n+1) 倍の調和数から 4n を引いたステップを取ります」と、人間が証明を書き出すことなく答えることができるのです。

バックパックのテスト：ヒープから採用問題まで

彼らの新しいバックパックが本当に機能するかどうかを確認するために、チームはいくつかの有名なコンピュータサイエンスの問題に挑戦しました。彼らは、ロボットが数学のパズルを自動的に解けるのか、それとも依然として助けが必要なのかを確認したかったのです。

1. メルダブル・ヒープ（簡単な勝利）
まず、彼らは「メルダブル・ヒープ（meldable heap）」と呼ばれるデータ構造を見ました。想像してみてください、二つのカードの山があり、それらを一つの大きな山にまとめたいとします。プログラムは、どちらのカードをどこに配置するかを決めるために、コインを投げてこれを行います。研究者たちは、彼らのバックパックがこれをほぼ完全に自動化したことを見出しました。ロボットはコードをチェックし、コストが対数的（つまり、山が巨大になっても非常にゆっくりとしか増えないこと）であることを即座に確認しました。人間が与えた唯一の助けは、対数に関する小さなヒントだけでした。これは、一部の問題において、彼らの手法がほぼ完璧であり、手作業がほとんど必要ないことを示しています。

2. ランダム化クイックソート（より難しいパズル）
次に、彼らは有名な「ランダム化クイックソート（Randomised Quicksort）」に取り組みました。これは、数字のリストをソートする有名な方法です。これは少しトリッキーです。プログラムはリストを分割するためにランダムな数を選び、その後、小さな部分と大きな部分をそれぞれソートします。ここでの数学はより複雑で、和やパターンを含み、推測するのがより難しいものです。
ロボットは基本的な部分は処理できましたが、最終的な答え（調和数を含む特定の公式）を得るためには、人間が介入して、より難しい数学のステップへとロボットを導く必要がありました。それは、ロボットはレースを走れるものの、最後のラップの戦略を教えるためのコーチを必要としているような状態でした。それでも、この追加の助けがあっても、チームは彼らの手法が、同じことを証明する他の方法よりもはるかに短く、かつ簡潔であることを発見しました。

3. スプレイ木と採用問題（中間領域）
彼らはまた、「ランダム化スプレイ木（Randomised Splay Trees）」（頻繁に使用されるアイテムをトップに移動させるデータ整理法）と、「採用問題（Hiring Problem）」（候補者を面接し、これまでの最高の人材を雇っていくシナリオ）についてもテストしました。

• スプレイ木については、バックパックが「ポテンシャル」（残された作業量を示す専門用語）と回転のコストを追跡するのを助けました。対数に関する人間のヒントを必要としましたが、ロボットが重労働を引き受けました。
• 採用問題については、候補者をランダムな順序で面接する場合、誰を雇う回数の平均が特定のパターンに従うことを証明するために、バックパックを使用しました。ロボットは問題を小さな和へと分解することで、この問題を正常に証明し、この手法が異なるタイプのランダムアルゴリズムに対してうまく機能することを示しました。

これが将来にもたらす意味

この論文の大きな教訓は、私たちはもはや「自動的であること」と「正確であること」のどちらか一方を選ぶ必要はないということです。以前は、コンピュータにランダムなプログラムのコストをチェックさせたい場合、多くの場合、多大な手作業が必要でした。もし完全に自動化したいのであれば、答えが役に立たないほど問題を大幅に簡略化しなければなりませんでした。

著者たちは、プログラムの構造（バックパック）の中に直接コスト追跡を組み込むことで、両方の良い面を得られることを示しました。コンピュータはほとんどの作業を自動的に行うことができますが、数学が本当に難しくなったとき、人間は証明全体を最初から書き直すことなく、ロボットを導くために介入することができます。

彼らはまた、彼らの手法が「健全（sound）」であることも証明しました。これは、彼らの方法が数学的に正しいことを意味する専門的な言葉です。彼らは単に推測したのではなく、もしロボットがコストはXであると言えば、コストは本当にXであることを示しました。

しかし、限界もあります。論文では、彼らのバックパックは現在、有限の時間と有限の結果で終了するプログラムにのみ機能すると述べています。まだ、永遠に走り続けたり、無限の可能性を持ったりするプログラムを扱うことはできません。しかし、今日私たちが使用している大多数の有用なランダムアルゴリズムにとって、この新しいツールはゲームチェンジャーです。それは、退屈で間違いの多い作業を、合理化された、ほぼ自動的なプロセスへと変え、より速く、より安く、より信頼性の高いソフトウェアを構築することを容易にします。

要約すると、研究者たちは私たちのデジタルな探索者たちのために、よりスマートなバックパックを作りました。今や、私たちのプログラムがランダムな冒険に出かけるとき、それらは自分自身の地図と計算機を持ち歩き、お宝に到達するのにどれくらいのコストがかかるかを正確に把握できるようになりました。