SMTソルバーで任意長のリストを扱うDueList
DueList: A Theory of Lists with Combinators for SMT Solvers
この論文をやさしく読む
ひとことで言うと
プログラム検証で、長さが決まっていないリストの操作をSMTソルバーに判断させる手法です。
何に役立つ？
リストと高階の操作を使うプログラムの自動検証に役立つと考えられます。要旨では752件の問題で充足可能性の判定範囲と性能を比較しています。
この研究の面白いところ
既存のSMTソルバーの上に抽象化・精緻化の層を置き、従来判定しにくかったリストの問題を扱います。比較対象はZ3とCVC5などです。
どこまで分かった？
対象のリストは指定された抽象的な結合演算子を通じて操作するものです。任意のリスト操作すべてに同じ結果が出るとは、要旨からは言えません。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
形式検証ツールは、線形整数演算、配列、文字列などの論理理論を使い、プログラムの構成要素や検証条件を符号化して、SMTソルバーによる自動推論に頼ることが多い。近年の進歩にもかかわらず、現代の関数型言語で広く使われるリストのような再帰的データ構造の推論は、依然として難しい。さらに、リストは、すべての要素に関数を一般的に適用するような高階の結合演算子と併用されることが多い。 本研究では、SMTソルバーにリスト推論を第一級の機能として提供する。対象は任意長のリストで、map-reduceの考え方に従い、一組の抽象的な結合演算子だけを通じて操作する。このために、リスト推論向けの抽象化・精緻化手法DueListを提案し、既製のSMTソルバーの上に実装した。効率を評価するため、先行研究と実際のプログラムから集めた多様な752件のベンチマークを用意し、Z3やCVC5などの最先端のソルバーと比較した。実験では、DueListは既存ソルバーの推論能力を拡張し、より広範な問題について充足可能か不可能かを判定できた。また、従来も扱えた事例の大多数で、既存ソルバーより高い性能を示した。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-24（UTC）
- 最新改訂
- 2026-09-24 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-24 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Formal verification tools commonly rely on SMT solvers to automatically reason about programs, leveraging a range of logical theories, e.g., linear integer arithmetic, arrays, or strings, to encode program constructs and verification conditions. Despite recent advances, such solvers still struggle when reasoning about recursive data structures such as lists, which are pervasive in modern functional languages. Additionally, lists are commonly used in conjunction with higher-order combinators to, e.g., generically apply a function to all elements of the list. In this work, we provide first-class support for reasoning about lists within SMT solvers. We focus on lists of arbitrary size that, following the map-reduce paradigm, can be manipulated exclusively through a set of abstract combinators. To this end, we introduce DueList, an abstraction-refinement approach geared towards list reasoning, which we implement on top of off-the-shelf SMT solvers. To evaluate the efficiency of our approach, we assemble a diverse set of 752 benchmarks curated from previous works and real-world programs, and compare DueList against state-of-the-art solvers such as Z3 and CVC5. Our experimental evaluation shows that DueList extends reasoning facilities of existing solvers, allowing to conclude about the (un)satisfiability of a larger range of problems, while outperforming existing solvers in the vast majority of previously supported cases.
著者のコメント
Revised from Q1 2026 submission
arXiv ID: 2609.29962 ／ 要約の誤りについて