💻 computer science

Automated Reasoning with Nested Datatypes

本論文は、非標準モデルを防止するためにデータ型と配列の組み合わせを制限する入れ子状データ型の理論を導入し、その正当性が証明された決定手続きを提供し、実世界のベンチマークおよび作成されたベンチマークにおけるこの手続きの実装を評価するものである。

原著者： Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett, Cesare Tinelli

公開日 2026-07-01

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

CC BY 4.0

原著者： Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett, Cesare Tinelli

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

あなたは、2種類の異なるレゴブロック、すなわち**データ型（Datatypes）と配列（Arrays）**を使って、複雑なデジタル都市を建設していると想像してください。

データ型は、家系図や組織図のようなものです。これらは階層構造を持っています。「人」は「子供」を持つことができ、その「子供」はさらに自分の「子供」を持つことができます。ここでのルールは単純です。**「誰も自分自身の先祖になってはならない」**ということです。人が自分の祖父になるような家系図を作ることはできません。それは論理的なループ（サイクル）を生み出し、構造を破壊してしまうからです。
配列は、郵便受けやロッカーのようなものです。これらは平面的であり、番号（インデックス）によって任意のアイテムを即座に掴み取ることができます。この中には、家系図のようなものさえも入れることができます。

問題点：「無限ループ」の罠

この論文は、これら2つのシステムを不用意に組み合わせたときに発生する、危険なグリッチ（不具合）について指摘することから始まります。

あなたが、ある**「人」（データ型）を持っており、その人に「家族」というフィールドがあると考えてみましょう。通常の環境であれば、「家族」は「人々」のリストです。しかし、このグリッチが発生している世界では、「家族」は「配列」**（ロッカー）になっています。

特定の**「人」（仮にボブとしましょう）を、「ロッカー#5」**に入れます。
そして、ボブの「家族」フィールドを**「ロッカー#5」**として定義します。

さて、何が起こるか見てみましょう。

ボブの家族を見つけるために、**「ロッカー#5」**を開けます。
**「ロッカー#5」**の中に、ボブがいます。
すると、ボブの家族を見つけるために、再び**「ロッカー#5」**を開けます。
そこに、再びボブがいるのです。

あなたは無限ループに陥りました。コンピュータサイエンスにおいて、これは**「非標準モデル（non-standard model）」**と呼ばれます。まるで蛇が自分の尻尾を飲み込んでいるような状態です。コンピュータ技術的にはこれを許容する場合もありますが、データ構造が本来あるべき直感的なルールを壊してしまいます。これは、存在してはならない「サイクル」を作り出しているのです。

解決策：「入れ子になったデータ型（Nested Datatype）」理論

著者であるトム・ハカック（Tomer Hakak）とそのチームは、「このような『蛇が自分の尻尾を食べる』シナリオを防ぐためのルールブックが必要です」と述べています。

彼らは、**「入れ子のデータ型（Nested Datatypes）」**という新しい理論を導入しました。これは、あなたのデジタル都市における厳格な建築基準法のようなものです。

ルール： ロッカーの中に家系図を入れることも、家系図の中にロッカーを入れることもできます。しかし、元の場所に戻ってしまうような経路を作成することはできません。
目標： ある人から出発し、その人の家族の配列を通って別の人に辿り着き、再びその家族の配列を通って元の人物に戻るという経路を辿ったとしても、決して元の人物に戻ってきてはなりません。

彼らが解決した方法：「翻訳機」マシン

難しいのは、コンピュータは「家系図」が正しいかどうかをチェックするのは得意ですが、「ロッカー」が正しいかどうかをチェックするのも得意ですが、それらを「組み合わせたとき」にループが発生するかどうかをチェックするのは苦手だという点です。

著者たちは、「翻訳機（Translator）」（決定手続き）を構築しました。その仕組みを比喩を使って説明します。

あなたは、2種類の異なるピースを持つパズルを持っていると想像してください。それは**「ツリーのピース」と「ボックスのピース」**です。コンピュータは、これらが混ざり合った状態でのループのチェック方法を知りません。

翻訳： 著者たちのアルゴくリズムは、この混ざり合ったパズルを取り込み、コンピュータが理解できる言語へと翻訳します。それは「ボックスのピース」を、見た目はボックスだが振る舞いはツリーである、特別な「ツリーのピース」へと変換します。
セーフティネット： 彼らは、この翻訳に「ガードレール（補題/lemmas）」を追加しました。これらのガードレールは、もし元の混ざり合ったパズルの中にループが存在するはずであった場合、翻訳されたツリー版において即座に矛盾（例えば、重力に逆らって塔を建てようとするような事態）が生じることを保証します。
チェック： コンピュータは翻訳されたパズルをチェックします。
- もし翻訳されたパズルが「不可能（unsatisfiable）」であれば、元の混ざり合ったパズルには禁止されたループが存在していたことを意味します。
- もし翻訳されたパズルが機能するならば、元のパズルは安全です。

なぜこれが重要なのか（論文による記述）

著者たちは単に理論を書いたのではありません。彼らは、cvc5（ソフトウェアの検証に使用されるツール）という実世界のコンピュータプログラムの中にプロトタイプを構築しました。

実世界テスト： 彼らは、スマートコントラクト（デジタル通貨の契約）の検証に使用されるツールであるMove Proverのベンチマークを用いて、これをテストしました。これらのコントラクトは、しばしば複雑に入れ子になったデータを使用します。
合成テスト： 彼らは、他のソルバーを無限ループに陥らせるために特別に設計された、偽のパズルを作成しました。
結果： 彼らの新しい手法は、他の手法が見逃したループを正常に検知することに成功しました。多くの場合、同様のタスクに使用される既存のツールであるZ3よりも、高速かつ正確でした。

まとめ

要約すると、この論文は、コンピュータが複雑なデータを理解する方法におけるバグを修正することについて述べています。

バグ： 「家系図」と「郵便受け」を混ぜると、人が自分自身の先祖になるという、意図しない無限ループが誤って作成される可能性があります。
修正： これらのループを厳格に禁止する新しいルール（入れ子のデータ型の理論）です。
ツール： これらの複雑に混ざり合ったルールを、コンピュータが安全性を容易にチェックできる形式へと変換する翻訳機であり、これにより、あなたのデジタルデータ構造が論理的で、ループのない状態であることを保証します。

技術要約：入れ子状のデータ型を用いた自動推論

1. 問題提起

SMT-LIBのデータ型理論は、リストや木構造のようなデータ構造の便利なエンコーディングを提供しており、ソフトウェア検証において不可欠である。しかし、その表現力は更新操作やランダムアクセス機能の欠如によって制限されている。これに対処するため、データ型と配列の理論を素朴に組み合わせる試みがしばしば行われる。

本研究で特定された核心的な問題は、そのような素朴な組み合わせが非標準的なモデルを導入してしまうことである。具体的には、データ値はそれ自身を含むことはできないという「非循環性（acyclicity）」の原則が、配列が関与することで回避されてしまう。すなわち、あるデータ型の値が、配列の要素として現れ、さらにその配列が同じデータ型の値のフィールドとなっている場合、サイクルが発生する。このサイクルは、データ型成分と配列成分の間で「分割」されているため、標準的な理論の組み合わせ（Nelson-Oppen経由）では検出できない。これらの非標準的なモデルは、検証を意図した入れ子状のデータ構造の直感的な意味論と一致しないため、望ましくないものである。

2. 手法

著者らは、これらの非標準的なモデルを明示的に排除する**入れ子状のデータ型（nested datatypes）**の理論を提案している。この手法は、理論の形式的な定義と、還元に基づく決定手続きの2つの主要なコンポーネントで構成される。

2.1. 形式的定義

本理論は、データ型と配列の標準的な組み合わせを制限することによって定義される。

良基性（Well-foundedness）: 著者らは、配列のソート（sort）の存在を考慮した、新しい良基的なソートの定義（定義10）を導入している。これにより、配列の要素が関与する場合でも、データ型の再帰的構造が良基的であることが保証される。
NDT関係: 非標準的なモデルを排除するために、著者らは構造上の関係 $\mathcal{R}_{\mathcal{A}}$ を定義している（定義16）。この関係は、項とその部分項、および配列とその要素を結びつける。構造が有効なNDT構造と見なされるのは、この関係が良基的である場合に限られる。これにより、データ型の値が配列を介して間接的に自身を参照するようなサイクルが効果的に排除される。

2.2. 決定手続き

本論文では、入れ子状のデータ型の充足可能性問題を、データ型、配列、および未解釈関数（EUF）の（素朴な）組み合わせへと還元する決定手続きを提示している。手続きは以下の通りである。

シグネチャの翻訳: 新しいシグネチャ $\Sigma_{\varphi}$ を構築する。
- 配列のソートは、サイクルチェック用のデータ型ソート（ $\sigma^*$ ）と、標準的な配列推論用の配列ソート（ $\sigma'$ ）の2つのコンポーネントに分割される。
- データ型のコンストラクタは、新しいソート上で動作するようにコピーされる。
- 特殊なコンストラクタが導入され、配列を有限のタプルとして表現し、入力式に存在するインデックスによってアクセスされる要素を捕捉する。
- 配列ソートの表現（ $\sigma'$ ）とデータ型ソートの表現（ $\sigma^*$ ）をリンクするために、未解釈関数（ $f_A, g_A$ ）が追加される。
式の翻訳: 入力式 $\varphi$ は $\text{trFormula}(\varphi)$ へと翻訳される。
- 標準的なリテラル（例： $x = \text{select}(a, i)$ ）は、新しいシグネチャにおける対応するものへとマッピングされる。
- 補題（Lemmas）: 決定的なのは、翻訳に一連の補題（ $L(\varphi)$ ）が付加される点である。これらは、元の式における配列操作と、新しいシグネチャにおけるタプルベースの表現との間の対応関係を強制する。これらの補題により、「隠れたサイクル」が翻訳された式の中で露出される。
解決（Solving）: 得られた式 $\text{trFormula}(\varphi)$ は、既存のデータ型、配列、およびEUFの組み合わせを扱える能力を持つSMTソルバ（例：Nelson-Oppen法を用いるもの）を用いて、充足可能性がチェックされる。

2.3. 正当性と決定可能性

本論文は、データ型理論が共有されるソートに対して安定して無限（stably infinite）であるという仮定の下で、翻訳が充足可能性を保存することを証明している（定理31）。その結果、入れ子状のデータ型の理論は決定可能である（定理32）。

3. 主な貢献

本論文の主な貢献は以下の3点である：

理論の定義: データ型と配列の相互作用から生じる非標準的な循環モデルを防止する、精密な入れ子状のデータ型理論の導入。
決定手続き: 入れ子状のデータ型の問題を、未解釈関数で拡張された標準的な理論の組み合わせへと変換する、還元ベースの決定手続き。
実装と評価: cvc5 SMTソルバ内でのプロトタイプ実装、およびそのアプローチの有効性を示す経験的評価。

4. 実験結果

著者らは、以下の2つのベンチマークスイートを用いて実装の評価を行った。

合成ベンチマーク: データ型と配列の間で様々なサイズのサイクルを生成するように系統的に設計された式。
- 不充足なインスタンス（サイクルが存在する場合）において、cvc5 は500個のベンチマークすべてを解決し、Z3（平均299.8個を解決、ただし表によればZ3はより少ない総インスタンスしか解決していない）を上回った。
- 充足可能なインスタンス（サイクルが断たれている場合）において、cvc5 は50個中25個を解決したが、Z3 はわずか1個しか解決できなかった。
実世界のベンチマーク: スマートコントラクトの永続的データ構造をモデル化するために、Move Prover 検証ツールから派生した式。
- 両方のソルバがすべてのMove Proverベンチマークを迅速に解決した。
- 充足可能なインスタンスにおいて、cvc5 はZ3と同等、あるいはわずかに高速であった。

5. 意義と主張

本論文は、提案された理論と決定手続きが、データ型と配列の組み合わせにおける非標準的なモデルの問題を解決できることを主張している。これは、既存のソルバ（Z3など）が暗黙的に処理している可能性はあるものの、厳密な理論的定義や、非循環性に関する保証を持たない問題である。

著者らは、自身のアプローチが「有望である」と述べており、実世界のベンチマークにおいては既存のソリューションと同等の競争力を持ち、サイクル検出をテストするために設計された合成ベンチマークにおいては優れていることを示している。彼らは、この研究が、そのような入れ子状の構造が頻繁に登場するMove Proverのニーズによって動機付けられたことを強調している。

論文の結論は控えめであり、現在の研究は配列の特定のケースを解決しているものの、検出されないサイクルの広範な問題は他のデータ構造（シーケンス、集合など）にも存在すると述べている。著者らは、配列に対する彼らの解決策が、素朴な理論結合の問題に対するより一般的な解決策の基礎となり得ることを示唆している。今後の課題として、増分的な解決（incremental solving）および量化子（quantifiers）へのサポート拡大を挙げている。