充足可能性モジュロ理論

提供: testwiki
ナビゲーションに移動 検索に移動

計算機科学および数理論理学における充足可能性モジュロ理論（じゅうそくかのうせいモジュロりろん、テンプレート:Lang-en-short、SMT）とは、ある数学的な論理式が充足可能であるかどうかを判定する問題である。SMTは充足可能性問題（SAT）を、実数・整数やリスト・配列・テンプレート:仮リンク・テンプレート:仮リンクといった各種のデータ構造を扱うより複雑な論理式へと一般化したものである。この名称は、これらの式が等号付き一階述語論理における特定の形式的理論の内部で（すなわち「モジュロ」その理論のもとで）解釈されることに由来する（多くの場合、量化子は許容されない）。SMTソルバは、実用的な入力の部分集合について SMT 問題を解くことを目的としたツールである。テンプレート:仮リンク や テンプレート:仮リンク などの SMT ソルバは、自動定理証明、テンプレート:仮リンク、プログラム検証、ソフトウェアテストなど、計算機科学の広範な応用の構成要素として用いられてきた。

ブール充足可能性がすでにNP完全であるため、SMT 問題は一般にNP困難であり、多くの理論ではテンプレート:仮リンクである。研究者たちは、どの理論あるいは理論の部分集合が決定可能な SMT 問題を導くのか、および決定可能な場合の計算複雑性について研究している。得られた決定手続きはしばしば SMT ソルバに直接実装される（例としてプレスバーガー算術の決定可能性を参照）。SMT は制約充足問題と見なすこともでき、したがって制約プログラミングへの一定の形式化されたアプローチとも言える。

用語と例

形式的に述べれば、SMT インスタンスとは、いくつかの関数記号や述語記号に追加の解釈が与えられた一階述語論理の論理式であり、SMT はそのような論理式が充足可能であるかを判定する問題である。言い換えると、充足可能性問題（SAT）のインスタンスにおいて、テンプレート:仮リンクの一部が、二値でない変数の適当な集合上のテンプレート:仮リンクで置き換えられたものを想像すればよい。述語とは、二値でない変数を引数とする二値関数のことである。述語の例としては、線形不等式（例: 3x+2y−z≥4）や、テンプレート:仮リンクおよび関数記号を含む等式（例: f(f(u,v),v)=f(u,v)。ここで f は2引数の未指定の関数）などがある。これらの述語は、それぞれ割り当てられた理論に従って分類される。たとえば、実数変数上の線形不等式は線形実算術の理論の規則を用いて評価され、非解釈項および関数記号を含む述語は等号付きテンプレート:仮リンクの理論（テンプレート:仮リンクと呼ばれることもある）の規則を用いて評価される。その他の理論には、（コンピュータプログラムのモデル化・検証に有用な）配列およびリスト構造の理論や、（テンプレート:仮リンクのモデル化・検証に有用な）テンプレート:仮リンクの理論などがある。部分理論も可能である。たとえばテンプレート:仮リンクは線形算術の部分理論であり、各不等式は変数 x, y と定数 c による x−y>c という形に制限される。

上の例は線形整数算術による不等式の使用を示している。他の例を挙げる。

  • 充足可能性: x∨(y∧¬z) が充足可能かどうかを判定する。
  • 配列アクセス: 配列 A に対して A[0] = 5 となる値を見つける。
  • ビットベクトル算術: x と y が異なる 3 ビット数であるかを判定する。
  • 非解釈関数: f(x)=2 かつ g(x)=3 となる x, y の値を見つける。

ほとんどの SMT ソルバは論理式の量化子を含まない断片のみをサポートするテンプレート:要出典。

自動定理証明との関係

SMT 解法と自動定理証明（ATP）には実質的な重なりがある。一般に、自動定理証明系は量化子を含む完全な一階述語論理の支援に注力するのに対し、SMT ソルバはより多様な理論（解釈付き述語記号）の支援に注力する。ATP は量化子が多く含まれる問題に強く、SMT ソルバは量化子を含まない大規模な問題を得意とする[1]。両者の境界はあいまいであり、ATP の一部は SMT-COMP に参加し、SMT ソルバの一部は テンプレート:仮リンク に参加している[2]。

表現力

SMT インスタンスは、変数の各集合が多様な基礎理論に由来するテンプレート:仮リンクで置き換えられたブール SAT インスタンスの一般化である。SMT 論理式は、ブール SAT 論理式で可能なものよりもはるかに豊かなモデリング言語を提供する。たとえば、SMT 論理式では、マイクロプロセッサのテンプレート:仮リンク演算をビット単位ではなくワード単位でモデル化できる。

比較として、解集合プログラミングもまた述語に基づく（より正確には、原子論理式から作られる原子文に基づく）。SMT とは異なり、解集合プログラムには量化子がなく、線形算術やテンプレート:仮リンクのような制約を容易に表現できない。解集合プログラミングは、非解釈関数のテンプレート:仮リンクに還元できるブール問題に最も適している。解集合プログラミングにおいて 32 ビット整数をビットベクトルとして実装することは、初期の SMT ソルバが直面したのと同じ問題の多くを抱える。すなわち、x + y = y + x のような「自明な」恒等式を導出することが困難である。

制約論理プログラミングは線形算術制約のサポートを提供しているが、完全に異なる理論的枠組みの中でであるテンプレート:要出典。SMT ソルバは高階論理の論理式を解くようにも拡張されてきた[3]。

ソルバのアプローチ

SMT インスタンスを解く初期の試みでは、それらをブール SAT インスタンスに変換していた（たとえば、32 ビット整数変数を適切な重み付きの 32 個の 1 ビット変数として符号化し、「加算」のようなワードレベルの演算をビット上のより低レベルの論理演算に置き換えるといった具合である）。そしてこの論理式をブール SAT ソルバに渡していた。このアプローチは、イーガーアプローチ（ビットブラスティング）と呼ばれ、以下の利点を持つ。すなわち、SMT 論理式を等価なブール SAT 論理式に前処理することで、既存のブール SAT ソルバを「そのまま」利用でき、時間とともに得られる性能・容量の改善を活用できる。他方で、基礎理論の高レベル意味論が失われることは、（整数加算の x+y=y+x のような）「自明な」事実を発見するためにブール SAT ソルバが必要以上に多く働かねばならないことを意味する。この観察を受けて、DPLL 方式の探索によるブール推論と、与えられた理論の述語の論理積（AND）を扱う理論固有ソルバ（T ソルバ）とを密結合する多くの SMT ソルバが開発された。このアプローチはレイジーアプローチと呼ばれる[4]。

テンプレート:仮リンク[5]と呼ばれるこのアーキテクチャは、ブール推論の責任を DPLL に基づく SAT ソルバに委ね、SAT ソルバは適切に定義されたインタフェースを通じて理論 T のソルバと対話する。理論ソルバは、SAT ソルバが論理式のブール探索空間を探索する際に SAT ソルバから渡される理論述語の論理積の充足可能性を確認することだけを心配すればよい。ただし、この統合がうまく機能するためには、理論ソルバが伝搬と衝突解析に参加できる必要がある。すなわち、既に確立された事実から新しい事実を導出でき、また理論衝突が生じた際には非充足性の簡潔な説明を提供できなければならない。言い換えれば、理論ソルバはインクリメンタルであり、かつバックトラック可能でなければならない。

決定可能な理論

研究者たちは、どの理論あるいは理論の部分集合が決定可能な SMT 問題を導くのか、また決定可能な場合の計算複雑性について研究している。完全な一階述語論理はテンプレート:仮リンクでしかないため、研究の一つの方向はテンプレート:仮リンクのような一階述語論理の断片に対する効率的な決定手続きを見出すことを試みる[6]。

もう一つの研究方向は、有理数および整数上の線形算術、固定幅ビットベクトル[7]、浮動小数点算術（多くの場合、SMT ソルバでは bit-blasting、すなわちビットベクトルへの還元によって実装される）[8][9]、テンプレート:仮リンク[10]、(余)データ型[11]、（動的配列のモデル化に用いられる）列[12]、有限集合および関係[13][14]、テンプレート:仮リンク[15]、有限体[16]、その他多くを含む、専門化されたテンプレート:仮リンクの開発を含む。

ブール単調理論は、効率的な理論伝搬と衝突解析を支援する理論のクラスであり、DPLL(T) ソルバ内で実用的に使用できる[17]。単調理論はブール変数のみをサポートし（ブールが唯一のソートである）、そのすべての関数と述語 テンプレート:Mvar は次の公理に従う。

p(…,bi−1,0,bi+1,…)⟹p(…,bi−1,1,bi+1,…)

単調理論の例には、テンプレート:仮リンク、凸包の衝突判定、最小カット、計算木論理などがある[18]。すべての テンプレート:仮リンク プログラムは単調理論として解釈できる[19]。

決定不能な理論に対する SMT

一般的な SMT アプローチのほとんどはテンプレート:仮リンクをサポートする。しかし、航空機とその挙動のような現実世界の多くのシステムは、超越関数を含む実数上の非線形算術によってのみモデル化できる。この事実が、SMT 問題を非線形理論へ拡張する動機となる。たとえば以下の等式が充足可能かどうかを判定するといった問題である。

(sin⁡(x)3=cos⁡(log⁡(y)⋅x)∨b∨−x2≥2.3y)∧(¬b∨y<−34.4∨exp⁡(x)>yx)

ここで

b∈𝔹,x,y∈ℝ.

このような問題は、一般にはテンプレート:仮リンクである。（他方で、実閉体の理論、したがって実数の完全な一階の理論は、テンプレート:仮リンクによって決定可能である。これはアルフレト・タルスキによる。）自然数における加算（だが乗算は含まない）の一階の理論、プレスバーガー算術と呼ばれるものもまた決定可能である。定数による乗算はネストした加算として実装できるため、多くのコンピュータプログラムにおける算術はプレスバーガー算術で表現でき、その結果決定可能な論理式が得られる。

決定不能な実数の算術理論に由来する理論原子のブール結合を扱う SMT ソルバの例としては、古典的な DPLL(T) アーキテクチャと（必然的に不完全な）従属理論ソルバとしての非線形最適化パケットを採用する テンプレート:仮リンク、iSAT アルゴリズムと呼ばれる DPLL SAT 解法と区間制約伝搬の統合の上に構築される iSAT[20]、そして テンプレート:仮リンク が挙げられる[21]。

テンプレート:Vanc

以下の表は、多くの利用可能な SMT ソルバの機能の一部をまとめたものである。「SMT-LIB」列は SMT-LIB 言語との互換性を示す。「yes」と示されている多くのシステムは、SMT-LIB の古いバージョンのみをサポートしているか、言語の部分的なサポートしか提供していない場合がある。「CVC」列は テンプレート:Abbr 言語のサポートを示す。「DIMACS」列は テンプレート:仮リンク フォーマットのサポートを示す。

プロジェクトは、機能や性能だけでなく、周辺コミュニティの実現可能性、プロジェクトへの継続的な関心、ドキュメント・修正・テスト・拡張への貢献能力においても異なる。

プラットフォーム 機能 備考
名称 OS ライセンス SMT-LIB CVC DIMACS 組み込み理論 API SMT-COMP
ABsolver Linux CPL テンプレート:Yes テンプレート:No テンプレート:Yes 線形算術、非線形算術 C++ no DPLL ベース
テンプレート:仮リンク Linux、Mac OS、Windows CeCILL-C（おおよそ LGPL と同等） テンプレート:Yes テンプレート:No テンプレート:No 空理論、線形整数・有理算術、非線形算術、多相配列、列挙型データ型、AC 記号、ビットベクトル、レコード型、量化子 OCaml 2008 ML 風の多相一階入力言語。SAT ソルバベース。理論モジュロ推論のために Shostak 風と Nelson–Oppen 風のアプローチを組み合わせる
Barcelogic Linux プロプライエタリ テンプレート:Yes 空理論、差分論理 C++ 2009 DPLL ベース、テンプレート:仮リンク
Beaver Linux、Windows BSD テンプレート:Yes テンプレート:No テンプレート:No ビットベクトル OCaml 2009 SAT ソルバベース
Boolector Linux MIT テンプレート:Yes テンプレート:No テンプレート:No ビットベクトル、配列 C 2009 SAT ソルバベース
CVC3 Linux BSD テンプレート:Yes テンプレート:Yes 空理論、線形算術、配列、タプル、型、レコード、ビットベクトル、量化子 C/C++ 2010 HOL への証明出力
CVC4 Linux、Mac OS、Windows、FreeBSD BSD テンプレート:Yes テンプレート:Yes 有理・整数線形算術、配列、タプル、レコード、帰納的データ型、ビットベクトル、文字列、非解釈関数記号上の等号 C++ 2021 バージョン 1.8 が 2021 年 5 月にリリース
テンプレート:仮リンク Linux、Mac OS、Windows BSD テンプレート:Yes テンプレート:Yes 有理・整数線形算術、配列、タプル、レコード、帰納的データ型、ビットベクトル、有限体、文字列、列、バッグ、および非解釈関数記号上の等号 C++、Python、Java 2021 バージョン 1.0 が 2022 年 4 月にリリース
Decision Procedure Toolkit (DPT) Linux Apache テンプレート:No OCaml no DPLL ベース
iSAT Linux プロプライエタリ テンプレート:No 非線形算術 no DPLL ベース
MathSAT Linux、Mac OS、Windows プロプライエタリ テンプレート:Yes テンプレート:Yes 空理論、線形算術、非線形算術、ビットベクトル、配列 C/C++、Python、Java 2010 DPLL ベース
MiniSmt Linux LGPL テンプレート:Yes 非線形算術 OCaml 2010 SAT ソルバベース、Yices ベース
Norn 文字列制約用の SMT ソルバ
テンプレート:仮リンク Linux AGPL テンプレート:No テンプレート:No テンプレート:No 確率論理、算術、関係モデル C++、Scheme、Python no 部分グラフ同型
OpenSMT Linux、Mac OS、Windows GPLv3 テンプレート:Yes テンプレート:Yes 空理論、差分、線形算術、ビットベクトル C++ 2011 遅延評価 SMT ソルバ
raSAT Linux GPLv3 テンプレート:Yes 実数および整数の非線形算術 2014, 2015 テスト付き区間制約伝搬と中間値定理の拡張
SatEEn ? プロプライエタリ テンプレート:Yes 線形算術、差分論理 なし 2009
SMTInterpol Linux、Mac OS、Windows テンプレート:仮リンク テンプレート:Yes 非解釈関数、線形実算術、線形整数算術 Java 2012 高品質でコンパクトな補間を生成することに注力
SMCHR Linux、Mac OS、Windows GPLv3 テンプレート:No テンプレート:No テンプレート:No 線形算術、非線形算術、ヒープ C no テンプレート:仮リンクを用いて新しい理論を実装できる
SMT-RAT Linux、Mac OS MIT テンプレート:Yes テンプレート:No テンプレート:No 線形算術、非線形算術 C++ 2015 SMT 対応実装のコレクションからなる、戦略的・並列 SMT 解法のためのツールボックス
SONOLAR Linux、Windows プロプライエタリ テンプレート:Yes ビットベクトル C 2010 SAT ソルバベース
Spear Linux、Mac OS、Windows プロプライエタリ テンプレート:Yes ビットベクトル 2008
STP Linux、OpenBSD、Windows、Mac OS MIT テンプレート:Yes テンプレート:Yes テンプレート:No ビットベクトル、配列 C、C++、Python、OCaml、Java 2011 SAT ソルバベース
SWORD Linux プロプライエタリ テンプレート:Yes ビットベクトル 2009
UCLID Linux BSD テンプレート:No テンプレート:No テンプレート:No 空理論、線形算術、ビットベクトル、および制約ラムダ（配列、メモリ、キャッシュなど） no SAT ソルバベース、テンプレート:仮リンク で書かれている。入力言語は SMV モデル検査器。よく文書化されている。
veriT Linux、OS X BSD テンプレート:Yes 空理論、有理・整数線形算術、量化子、非解釈関数記号上の等号 C/C++ 2010 SAT ソルバベース、証明を生成可能
テンプレート:Visible anchor Linux、Mac OS、Windows、FreeBSD GPLv3 テンプレート:Yes テンプレート:No テンプレート:Yes 有理・整数線形算術、ビットベクトル、配列、非解釈関数記号上の等号 C 2014 ソースコードはオンラインで入手可能
テンプレート:仮リンク Linux、Mac OS、Windows、FreeBSD MIT テンプレート:Yes テンプレート:Yes 空理論、線形算術、非線形算術、ビットベクトル、配列、データ型、量化子、文字列 C/C++、.NET、OCaml、Python、Java、Haskell 2011 ソースコードはオンラインで入手可能

標準化と SMT-COMP ソルバ競技会

SMT ソルバ（および自動定理証明系。この用語はしばしば同義的に用いられる）への標準化されたインタフェースを記述する複数の試みがある。最も顕著なのは SMT-LIB 標準[22]であり、これは S式に基づく言語を提供する。他に一般的に支援されている標準化された形式には、多くのブール SAT ソルバによって支援される DIMACS 形式や、CVC 自動定理証明系が用いる CVC 形式がある。

SMT-LIB 形式にはいくつかの標準化されたベンチマークも付属しており、SMT-COMP と呼ばれる SMT ソルバ間の年次競技会を可能にしている。当初、この競技会は テンプレート:仮リンク 会議（CAV）の間に開催されていた[23][24]。しかし 2020 年からは、テンプレート:仮リンク（IJCAR）と提携する SMT ワークショップの一部として競技会が開催されている[25]。

応用

SMT ソルバは、プログラムのテンプレート:仮リンクの証明、テンプレート:仮リンクに基づくソフトウェアテストといった検証、およびプログラム合成（可能なプログラムの空間を探索してプログラム断片を生成する）の両方に有用である。ソフトウェア検証の外でも、SMT ソルバは型推論[26][27]や、核軍備管理における当事者の信念のモデル化を含む理論的シナリオのモデル化にも用いられている[28]。

検証

コンピュータプログラムのコンピュータ支援検証では、しばしば SMT ソルバが用いられる。一般的な技法は、事前条件、事後条件、ループ条件、およびアサーションを SMT 論理式に変換し、すべての性質が成立するかを判定するものである。

テンプレート:仮リンクの上に構築された検証器は数多い。Boogie は Z3 を用いて単純な命令型プログラムを自動的に検査する中間検証言語である。並行 C のための VCC 検証器は Boogie を用いており、命令型オブジェクトベースプログラム向けの Dafny、並行プログラム向けの Chalice、C# 向けの Spec# も同様である。F* は Z3 を用いて証明を見つける依存型付き言語であり、コンパイラはこれらの証明を証明担持バイトコードの生成にまで持ち込む。Viper 検証インフラストラクチャは検証条件を Z3 に符号化する。sbv ライブラリは Haskell プログラムの SMT ベース検証を提供し、ユーザは Z3、ABC、Boolector、cvc5、MathSAT、Yices など多数のソルバから選択できる。

テンプレート:仮リンク SMT ソルバの上に構築された検証器も数多い。以下は成熟した応用の一覧である。

  • Why3、演繹的プログラム検証のためのプラットフォーム。主要な証明系として Alt-Ergo を用いる。
  • CAVEAT、CEA によって開発され Airbus によって使用される C 検証器。Alt-Ergo は最近の航空機の一つの DO-178C 認証に含まれた。
  • テンプレート:仮リンク、C コード解析のためのフレームワーク。（「演繹的プログラム検証」専用の）Jessie および WP プラグインで Alt-Ergo を用いる。
  • テンプレート:仮リンク は SPARK 2014 における一部のアサーションの検証を自動化するために（GNATprove の背後で）CVC4 と Alt-Ergo を用いる。
  • テンプレート:仮リンク は主要な証明系の代わりに Alt-Ergo を用いることができる（ANR Bware プロジェクトのベンチマークで成功率が 84% から 98% に増加した[29]）。
  • テンプレート:仮リンク、Systerel によって開発された B メソッドフレームワークで、Alt-Ergo をバックエンドとして用いることができる。
  • Cubicle、配列ベース遷移システムの安全性を検証するオープンソースのモデル検査器。
  • EasyCrypt、敵対的コードを含む確率的計算の関係的性質について推論するためのツール集。

多くの SMT ソルバは、SMTLIB2 と呼ばれる共通のインタフェース形式を実装している（そのようなファイルは通常「.smt2」拡張子を持つ）。LiquidHaskell ツールは、cvc5、MathSat、Z3 など任意の SMTLIB2 準拠ソルバを使用できる、Haskell 向けの精密化型に基づく検証器を実装している。

シンボリック実行に基づく解析とテスト

SMT ソルバの重要な応用は、プログラムの解析とテストのためのテンプレート:仮リンクである（テンプレート:仮リンクなど）。特にセキュリティ脆弱性の発見を目的としているテンプレート:要出典。このカテゴリのツール例には、Microsoft Research の SAGE、KLEE、S2E、Triton などがある。シンボリック実行の応用に用いられてきた SMT ソルバには、Z3、STP、Z3str 系ソルバ、Boolector などがあるテンプレート:要出典。

対話的定理証明

SMT ソルバは、テンプレート:仮リンク[30]や テンプレート:仮リンク[31]など、証明支援系と統合されてきた。

合成

SMT ソルバは、仕様からプログラムを自動生成するプログラム合成の中核的構成要素である。代表的なアプローチはテンプレート:仮リンク（CEGIS）であり、そこでは合成系が候補プログラムを提案し、SMT ソルバがそれを検証する。失敗した検査からの反例が、正しい解が見つかるまで合成系を誘導する[32]。

関連する応用として、テンプレート:仮リンクがある。バグのあるプログラムとテストスイートが与えられると、その解がパッチを生じさせる SMT 論理式が構築される。たとえば Nopol は、修復された条件式を見つける問題を SMT インスタンスとして符号化し、解を Java プログラムのソースコードパッチへと変換し戻す[33]。

脚注

  1. ↑ テンプレート:Cite journal
  2. ↑ テンプレート:Cite journal
  3. ↑ テンプレート:Cite book
  4. ↑ テンプレート:Cite book
  5. ↑ テンプレート:Citation
  6. ↑ テンプレート:Cite conference
  7. ↑ テンプレート:Cite book
  8. ↑ テンプレート:Cite conference
  9. ↑ テンプレート:Cite conference
  10. ↑ テンプレート:Cite book
  11. ↑ テンプレート:Cite book
  12. ↑ テンプレート:Cite journal
  13. ↑ テンプレート:Cite book
  14. ↑ テンプレート:Cite book
  15. ↑ テンプレート:Cite book
  16. ↑ テンプレート:Cite book
  17. ↑ テンプレート:Cite journal
  18. ↑ テンプレート:Cite book
  19. ↑ テンプレート:Cite journal
  20. ↑ テンプレート:Citation
  21. ↑ テンプレート:Cite book
  22. ↑ テンプレート:Cite web
  23. ↑ テンプレート:Cite book
  24. ↑ テンプレート:Cite book
  25. ↑ テンプレート:Cite web
  26. ↑ テンプレート:Cite book
  27. ↑ Loncaric, Calvin, et al. "A practical framework for type inference error explanation." ACM SIGPLAN Notices 51.10 (2016): 781-799.
  28. ↑ テンプレート:Cite book
  29. ↑ テンプレート:Cite web
  30. ↑ テンプレート:Cite book
  31. ↑ テンプレート:Cite journal
  32. ↑ テンプレート:Cite book
  33. ↑ テンプレート:Cite journal

参考文献

テンプレート:Refbegin

テンプレート:Refend

関連項目

「https://ja.wiki.beta.math.wmflabs.org/w/index.php?title=充足可能性モジュロ理論&oldid=14376」から取得