💻 computer science

Towards Bottom-Up Enumeration in miniKanren via Pruning and Memoization

本論文は、深いターゲットに対する関係的プログラム合成の性能を大幅に向上させるために、観測的重複排除とメモ化を用いたボトムアップの列挙を可能にする2つのminiKanriライブラリコンビネータ、`prute`および`defrel/bank`を導入するとともに、標準的な深さ優先順序がコンパクトな代表元を見つけられないケースに対処するための重み付きバリアントを提案するものである。

原著者： Nikolai Kudasov

公開日 2026-07-29

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Nikolai Kudasov

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

あなたは、ミステリーを解決しようとしている探偵だと想像してください。ただし、手がかりを探す代わりに、特定の仕事ができる機械を作ることを目指しています。例えば、2を4に、3を9に、4を16に変えるような機械です。あなたは、その機械がどのような数式を使っているのか正確には知りません。分かっているのは、結果だけです。これは「例示によるプログラミング（Programming by Example）」と呼ばれます。答えを見つけるために、あなたは、最も単純な歯車やレバーから始めて、一つずつあらゆる可能な機械を作り上げ、それが機能するかどうかをテストするという方法を取るかもしれません。これは、シェフが、小麦粉、砂糖、卵のあらゆる組み合わせを試して、納得のいく味になるまで何度も焼き続けて、秘伝のレシピを見つけ出そうとする作業に似ています。

コンピュータサイエンスの世界には、「関係プログラミング（relational programming）」と呼ばれる特別な考え方があります。コンピュータに手順を一つずつ指示するのではなく、答えが「どのような姿をしているか」を記述し、経路の特定はコンピュータに任せるという方法です。これは、ロボットに対して「左に曲がって、3歩歩いて、それから右に曲がって」と指示するのではなく、「迷路の中の道を見つけて」と伝えることに似ています。コンピュータは多くの経路を一度に探索することに長けていますが、厄介な癖があります。それは、同じ行き止まりを何度も探索したり、すぐ隣にある短くて賢い近道を見逃して、長く曲がりくねったトンネルの中で立ち往生したりしてしまうことです。この論文は、コンピュータがいかにして、より賢く、より整理された探索者になれるかを教えることで、この問題に取り組んでいます。

問題点：迷路で迷子になること

あなたが、何百万もの鍵で溢れかえった、巨大で散らかった屋根裏部屋で、特定の鍵を探していると想像してください。ほとんどの鍵は見た目が異なりますが、すべて同じドアを開けることができます。もしあなたが不器用な探索者なら、一つの鍵を手に取り、それを試して、それが機能することを確認した後、他の鍵も試すのに何時間も費やしてしまうかもしれません。見た目は違っても、実は同じ仕事をする鍵を、念のために確認しようとするからです。これは時間の無駄です。

コンピュータプログラムの世界では、このようなことが頻繁に起こります。コンピュータが、入力を出力へと変換するプログラムを作ろうとする際、何千もの異なる見た目のコードの断片（スニペット）を生成します。これらの断片の多くは、正体を隠した「双子」です。つまり、内部的な見た目は違っても、実際には全く同じことを行っているのです。標準的なコンピュータ探索メソッドは、深いダイブを行う探索者のように、一つの双子をチェックし、次の双子をチェックし、また次の双子をチェックするという動きをします。そのため、屋根裏部屋が大きくなるにつれて、どんどん動作が遅くなっていきます。それは、まるで、何百万もの針が入った干し草の山の中から針を探しているようなものです。しかも、その干し草の山は、見た目が少しずつ異なる何百万もの針でできているのです。

解決策：「プルーン（間引き）」と「バンク（銀行）」

この論文の著者であるニコライ・クダソフ（Nikolai Kudasov）は、この混乱を解決するために2つの巧妙なツールを考案しました。これらは、魔法のフィルターとスマートな図書室のようなものです。

1. 「プルーン」ツール（フィルター）
機械からコンベアベルトに乗って鍵が流れてくる様子を想像してください。「プルーン」ツールは、ベルトの横に立っているガードマンです。各鍵が到着するたびに、ガードマンはその鍵がどのドアを開けるかを確認します。もしガードマンが、すでに同じドアを開ける鍵を見たことがあれば、新しい鍵をテストすることなく、そのままゴミ箱に投げ捨てます。彼らは、特定のドアを開ける「最初の鍵」だけを保持します。これにより、コンベアベルトにはユニークで有用な鍵だけが運ばれます。コンピュータは重複したものに時間を浪費することを止められます。

2. 「バンク」ツール（スマートな図書室）
次に、鍵が必要になるたびにゼロから鍵を作るのではなく、魔法の図書室を持っていると想像してください。あなたが図書室に鍵を求めると、図書室は単に一つを渡すのではなく、下から積み上げるようにして、ユニークな鍵の棚全体を一度に作り上げ、それを保存します。もし後でまた鍵が必要になったら、図書室はすでに構築済みのものを手渡すだけです。

論文の言葉では、これは defrel/bank と呼ばれます。これは、コンピュータが候補となるプログラムを、特定の組織化された方法（最も単純なものから始める方法）で構築することを強制し、その結果を保存します。もしコンピュータが後でプログラムの一部を使用する必要が生じた場合、それを再構築するのではなく、そのパーツを「バンク」から取り出すだけです。これは、コンピュータが同じ作業を二度と繰り返さなくて済むため、膨大な時間の節約になります。

逆転現象：時には「速い」ことが「最善」ではない

著者たちは、単に整理整頓されているだけでは不十分なこともあると気づきました。時には、「バンク」が作る棚の順番が、コンピュータにとっては速いものの、人間にとっては遅いことがあります。例えば、バンクがすべての「掛け算」の機械を先に作り、ずっと後になってから「足し算」の機械を作るかもしれません。もし探している答えが「足し算」の機械だった場合、コンピュータは、目的の機械を見つける前に何千もの掛け算の機械をチェックしなければならない可能性があります。

これを解決するために、彼らは defrel/bank-w（「重み付き」バンク）という第3のツールを作成しました。このツールは、どの種類の鍵が答えである可能性が高いかを知っている司書のようなものです。彼は、どの鍵を最初に見せるかを決定するために、特別な「スコア」を使用します。たとえ図書室の奥深くに埋もれていたとしても、最もシンプルでコンパクトな鍵を最初に提示しようとします。これは、最も優雅な解を求めている場合には素晴らしいですが、答えが非常に複雑で深い機械である場合には、動作が遅くなる可能性があります。

彼らが発見したこと：スピード vs 戦略

著者たちは、一連の数学および文字列パズル（例：「Hello」を「Hello, World!」に変えるなど）を用いて、これらのツールをテストしました。以下に、彼らの発見をまとめます。

「バンク」はスピードの怪物である： 8つの難しい数学問題のうち6つにおいて、defrel/bank ツールは、従来の標準的な探索方法よりも 9倍から99倍高速 でした。それは非常に高速で、従来のメソッドでは完了までに数分かかっていた問題を、わずか数分の一の秒数で解決しました。
しかし、盲点がある： バンクは非常に組織化されているため、答えが図書室の訪れるのが遅い場所に隠れている場合、その答えを見逃してしまうことがあります。例えば、答えが特定の形式の足し算（例： $(1+x)^5$ ）を含む場合、バンクは数千の掛け算の例をチェックすることに時間を取られてしまうかもしれません。このようなケースでは、異なる順序でチェックを行う従来の、より遅いメソッドの方が勝利します。
「重み付き」バンクはトレードオフである： defrel/bank-w ツールは、最もコンパクトで優雅な答えを見つけるのに優れています。それは、トリッキーな文字列パズルに対して、標準的なメソッドの 31.5ミリ秒 を beating（打ち負かし）、10.4ミリ秒 で正解を見つけました。しかし、非常に深い数学の問題に対しては、あまりに多くの可能性をチェックしようとしてタイムアウトしてしまうこともありました。

結論

この論文は、コンピュータサイエンスのあらゆる問題を解決したと主張しているわけではありません。その代わりに、「プルーン（間引き）」と「バンキング（保存）」を少し加えるだけで、コンピュータが他のプログラムを構築する速度を劇的に向上させられることを示しています。

著者たちは、パズルを解くシステムを構築する場合、通常は最も高速である バンク ツールをデフォルトとして使用することを推奨しています。しかし、非常に特定のコンパクトな解を探している場合や、問題が浅く単純な場合は、重み付きバンク や、あるいは従来の方法を使用するのがよいでしょう。それは、一つのツールが完璧であるということではなく、解こうとしているパズルの形状に合わせて、適切なツールを選ぶことが重要であるということです。論文は、これらのツールがリストや型付きデータを理解するプログラムの構築といった、より複雑なパズルにおいても、このスピードアップが現実世界で通用するかどうかを検証するために、今後の研究を行うことを示唆して締めくくられています。

技術要約：pruning（枝刈り）とmemoization（メモ化）によるminiKanrenにおけるボトムアップ列挙に向けて

問題定義

現代のプログラム例によるプログラミング（PBE）シンセサイザは、通常、観測的な重複排除を伴うボトムアップ列挙に依存しています。この手法は、候補となる式のワークリストを保持し、それらを例入力に対する振る舞いに基づいて重複排除し、レベルごとに展開しながら一致するものを見つけ出します。これは命令型や関数型の設定では非常に効果的ですが、関係プログラミング（具体的にはminiKanren）においては、自然な探索規律が候補の公平なストリームに対するトップダウン解決であるため、その戦略は不自然な形で浮いてしまいます。

関係的インタプリタを記述してそれを「逆方向に」実行したり、深さ制限を用いた「列挙とテスト」のアプローチをとったりする既存のminiKanrenレシピは、現実的な探索深度において著しい非効率性に直面します。主な問題は、探索木の中に振る舞いが等価な式が多数存在することです。素朴な深さ制限付き列挙器は、各再帰レベルで新しい重複排除テーブルを作成するため、前のレベルで行われた作業を再利用することができません。これにより、振る舞いが同一の候補が繰り返し再評価されるという指数関数的な爆発が生じます。

手法

著者らは、未変更の $\mu$ Kanrenコアの上に構築された2つの小さなライブラリコンビネータを提案し、ボトムアップのPBEと関係プログラミングの間の溝を埋めます。これらのコンビネータは、ホストの探索規律を変更することなく、ボトムアップ列挙と観測的な重複排除を導入します。

1. `prune` コンビネータ

最初のコンビネータである prune は、ユーザー指定のキー関数に基づいて回答ストリームをフィルタリングします。

メカニズム: これはゴールをラップし、キー関数の異なる値（例：候補式の入力/出力の振る舞い）につき、高々1つの状態を放出します。
論理変数の扱い: キーが未束縛の論理変数に依存する場合を扱うため、prune は番兵値（skip-prune）を使用します。項が未だground（接地）していないためにキーが計算できない場合、その状態は記録されずに放出されます。この状態は、変数が束縛され項がgroundになった時点で初めて重複排除の対象となります。
スコープ: 重複排除は呼び出しごとに厳密に適用されます。各 prune の呼び出しに対して新しいハッシュテーブルが作成されます。これは、「外側の変数として既知であること」と「内側の変数として既已知であること」を混同することを避けるためであり、混同すると再帰的な定義において完全性が損なわれるためです。

2. `defrel/bank` コンビネータ

2番目のコンビネータである defrel/bank は、prune を拡張して、関係のすべてのコールサイト間で共有される重複排除を伴う真のボトムアップ列挙を実現します。

標準的な変数（Canonical Variables）: これは、最も一般的な関係の呼び出しを表す、空の状態の最初の $N$ 個のフレッシュ変数に対して関係をメモ化します。
「バンク（Bank）」: 関係の本体は、これらの標準的な変数に対して一度だけ実行され、標準的なストリーム（「バンク」）を生成します。このストリームはボトムアップで構築され、決定された同値類（#:prune キーによって決定）につき、正確に1つの代表者を含みます。
再生（Replay）: その後の関係の呼び出しは、本体を再実行しません。代わりに、呼び出し側の特定の引数に対して標準的なストリームを再生します。これには、標準的な代入を歩き、内部変数を呼び出し側の名前空間にリネームし、結果を呼び出し側の引数と単一化するプロセスが含まれます。
効率性: このアプローチにより、(run ...) クエリがどのように多く回されたとしても、重複排除の作業が一度だけ行われることが保証されます。

3. `defrel/bank-w` バリアント（ベストファースト）

標準の defrel/bank は深さ優先探索を用い、列挙順序に偏り（例：加算よりも乗算の右スパイン鎖を優先する）を生じさせます。ターゲットの解が標準的な順序の深い位置にあるケースに対処するため、著者らは defrel/bank-w を導入しています。

重み付きストリーム: このバリアントは、未成熟なストリームセルに許容可能な上限（重み）を付与します。
深さ減衰: 再帰的なコールサイトにおいて減衰係数が適用されます。これにより、浅い代表者がより低い重みを持ち、ソートされたマージロジック（mplus-w）によって最初に放出されるようになります。
遅延ヒューリスティクス: システムは「レイジー・シーリング（lazy-ceiling）」規律を使用し、重みをアンダーラインのスランク（thunk）を強制することなく覗き見ます。これにより、重みの天井が許容可能なヒューリスティックとして機能するA*探索のような探索を実現します。

主な貢献

prune: ユーザー指定の関数によってキー付けされる、汎用的な回答ストリーム重複排除コンビネータ。項レベルの関数をpruneキーへと持ち上げるためのヘルパー（ground-key, when-ground）をサポートしています。
defrel/memo と defrel/bank: 標準的なフレッシュ変数に対して関係をメモ化するためのコンビネータ。defrel/bank は特に、共有された重複排除を伴うボトムアップ列挙を提供し、標準的なPBEの「ワークリスト」パターンを関係的設定へと効果的に移植します。
defrel/bank-w: 重み付きの未成熟ストリームを用いてベストファースト列挙を回復させる、深さ減衰型のコンビネータ。これにより、自然な深さ優先順序が目標を見逃す場合でも、コンパクトな代表者を見つけることが可能になります。
実装の工夫: ペアリングヒープを用いたソート済みマージや「スランク崩壊（thunk-collapse）」技術などのエンジニアリング上の最適化を詳述し、メモ化されたアプローチが深さ制限付きのベースラインと同等の性能を発揮するようにしています。

結果

著者らは、算術および文字列のPBEベンチマーク（深さ0–6）を用いた予備的な経験的評価を提示しています。

性能向上: 8つの深い算術ターゲットのうち6つにおいて、defrel/bank は深さ制限付きのベースライン（bounded）よりも 9〜99倍高速 です。これは、bank が再帰レベルごとにサブ式を再的にプルーニングすることを避けているためです。
列挙順序のバイアス: defrel/bank の性能は列挙順序に強く依存します。ターゲットの解が標準的な深さ優先順序の初期段階にある場合（例： $x^k$ や $x^k + c$ ）には優れていますが、 $(1+x)^k$ のような、標準的なストリームの非常に遅い位置（例：深さ4で243,158番目）に現れるターゲットに対しては苦戦するか、タイムアウトします。
ベストファーストのトレードオフ: defrel/bank-w は、 $(1+x)^k$ のようなターゲットに対してコンパクトな代表者を早期に見つけることに成功しています。しかし、「幅優先のコスト」が発生します。深さ $K$ のセルを放出するには、深さ $<K$ のすべてのセルを放出する必要があります。振る舞いの空間が広い場合（深さ3で数千の異なる振る舞いがある場合）、defrel/bank が成功する深い算術ターゲットにおいてタイムアウトにつながります。
ホスト・ベースラインとの比較: 非関係的なホスト言語のベースライン（host-bank）は、浅いターゲットや $(1+x)^k$ ファミリーには良好に動作しますが、関係エンジン外で網羅的なバンクを構築するコストのため、深い右スパインのターゲットに対しては壊滅的に失敗します。defrel/bank は関係的インターフェースを維持しつつ、列挙のバイアスが有利な場合には host-bank のスピードアップの大部分を回収しています。

意義と主張

本論文は、これらのコンビネータが、関係的パラダイムを離れず、かつホストの探索規律を変更することなく、標準的なボトムアップ列挙と観測的重複排除を関係的設定に持ち込むことに成功したと主張しています。

オプトイン・セマンティクス: このアプローチは厳密にオプトインです。重複排除は、prune でラップされているか defrel/bank を通じて定義された関係にのみ適用され、標準的なminiKanrenの関係のセマンティクスを変更することはありません。
完全性: 著者らは、プルーニングがユーザー指定の同値性に関して完全性を保持すると主張しています。各振る舞いに対して、少なくとも1つの代表者が発見されます。
限界: 著者らは、評価が予備的であり、2つのドメイン（算術および文字列）に限定されており、特定の文法に依存していることを認め、その範囲について謙虚な姿勢を示しています。また、defrel/bank は普遍的な解決策ではないことも明言しています。その成功は、ターゲットの形状と列挙順序の相互作用に依存します。彼らは、公平な結合（fair conjunction）は defrel/bank の列挙バイアスを解決できないと明言しています。なぜなら、バイアスはバンク内にどのセルが存在するかという点にあり、それらがどのようにインターリーブされるかという点にはないからです。
今後の展望: 論文では、 $(1+x)^k$ のバイアスを幅優先のコストなしに修正するための、標準的な本体に対する反復深化、飽和検出、およびより豊かな制約ストアや他のPBEドメイン（ビットベクトル、リストなど）への拡張を含む、今後の研究方向を特定しています。

要約すると、本論文は、標準的な変数に対して関係をメモ化し、観測的な同値性によってプルーニングを行うことで、列挙順序がターゲットの構造と一致している限り、関係的PBE合成において大幅な性能向上を達成できることを示しています。