tozima's blog

主に自分のための、論文の読書記録

Induction duality: primal-dual search for invariants

by Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken

与えられた状態遷移系から、状態上の述語を頂点に持つ遷移系を構成する手法の提案。ならびに、状態上の遷移系の分析と述語上の遷移系の分析を、情報を交換しながら並行して行う手法の提案。

概要

整数変数を持つプログラムのような無限状態遷移系の安全性の自動検証において、パフォーマンスの鍵となるのが適切な述語を見つける問題である。本論文は、双対的な視点からこの問題にアプローチするものである。

ということで、視点を変えて、重要そうな述語の代わりに重要そうな状態を見つける問題を考えてみよう。なにがしかの述語  P が与えられている状況を仮定すると、注目すべき状態とは「 P が安全性の証拠になっていない」ことを表す状態、例えば  s \to s' であって  P(s) \wedge \neg P(s') を満たす状態  s,s' などが考えられるだろう。状態と述語の役割を逆にすると、この論文が提案する述語発見方法(DualHoudini)になる。この述語発見手法(=DualHoudini)と、述語候補の集合を入力に取る通常の安全性判定手法(=PrimalHoudini、つまり普通の Houdini)を交互に実行するのが、本論文による Primal-Dual 版の Houdini である。

状態と述語の役割を逆にするということは、述語を頂点にもつ遷移系を考える必要がある。本論文のポイントは、その定義にある。状態遷移系  (S, s_0, \to) と述語遷移系  (Preds, \top, \rightsquigarrow) が与えられたとする*1。ここで  Preds S 上の述語の集合の適当な部分集合である。ただし各  P \in Preds s_0 上で真であることを仮定する。これらが双対であるとは、

 (s \to s') \wedge (P \rightsquigarrow P') \wedge P(s) \wedge P(s') \wedge P'(s) \Longrightarrow P'(s')

が成り立つことと定義される*2。面白いのは次の性質である:

  •  s_0 \to^* s' かつ  \top \rightsquigarrow^* P ならば  P(s')。つまり、述語の方の遷移系で到達可能な述語たちは、すべての到達可能集合を含んでいる*3

こうして状態と述語が対称な概念となったので、「安全性に違反する状態に至る状態遷移列を探す技術」を「安全性を証明する述語に至る述語遷移列を探す技術」だとみなすことができるようになるわけである。この基盤技術として Houdini アルゴリズムを使ったのが本論文である。

ひとつ注意しておくこととしては、述語上の遷移関係  \rightsquigarrow *4 は計算が容易ではことが挙げられる。論文ではページを割いて、この遷移系の取り扱いを議論している。

感想

述語の上の遷移系の定義は新しいし面白い。特に「状態遷移系の安全性証明」が「述語遷移系の到達可能性」に帰着することで、「安全性証明に便利な命題探し」を「述語遷移系における初期状態からのパス探し」だとみなす視点の切り替えはすばらしい。

ただ、読み終わってから振り返るに、論文の議論の中には本質からズレたものも多かったのではないだろうかという気がする。例えば論文では、状態遷移系を種として3つの遷移系(述語上の遷移系2つと、状態上の遷移系1つ)を定義して、元の状態遷移系と合わせた4つ組を主に取り扱っているが、私としては導入された3つのうち1つ以外は不要だったように思う。こうした理論展開になっている理由は、たぶん、論文中で「k-indutively provable」と呼ばれている概念に基づく述語遷移系が、状態遷移系の双対として(唯一? カノニカルな?)述語上の遷移系であるといった主張を展開するためだと思われる。私はこれは違うのではないかと思う。述語遷移系の選択は(双対である限りにおいて)理論的にはなんでも良いとした方がクリアだっただろう(ただし、述語遷移系の選択は計算効率と証明能力に影響するから慎重に行う必要はある)。ということなので、述語遷移系の遷移が何を意味するかとかの議論は軽く流しつつ読むのがオススメである。

*1:記号は論文のものとは異なる

*2:これを双対と呼ぶのは良くないと思う。双対なシステムはひとつではなく、遷移を減らす操作で閉じている。特に、どのような遷移系も遷移が一切ない遷移系と双対である。個人的には、論文の意味で「双対」な中でも最も遷移が多いシステムだけが双対の名にふさわしいと思う。なお、双対の意味を「双対」な中で最も遷移が多いものとしたとしても、双対の双対は元の遷移系とは限らず、一般には元よりも多くの遷移を含む。

*3:実はより強く、到達可能集合を含み、状態遷移で閉じた述語であることまで言える

*4:論文が採用しているもの、あるいは、その他の使えそうなもの。もちろん述語上の遷移関係が空集合でも双対性は満足し、この遷移関係の計算は自明に行えるが、それが誘導する自動検証器の証明能力は0である。

Beautiful Interpolants

by Aws Albarghouthi and Kenneth L. McMillan

良い interpolant を計算するための手法の提案。

概要

Interpolant は SMT ソルバの証明から抽出することができるが、従来の DILL(T) を基盤とする SMT ソルバの返す証明(およびそこから抽出される interpolant)は複雑になりがちという問題があった。この論文では、簡単な論理式による interpolant を与える手法を提案している。

基本となるのは  A \Rightarrow I かつ  I \Rightarrow \neg B を満足する「簡単な」述語  I が存在するかどうかというクエリであり、これを繰り返すことで interpolant を見つける。簡単な述語の例としては、half-space  a_1 x_1 + a_2 x_2 + \dots + a_n x_n \le b という形の論理式が挙げられている。ここで  x_1, \dots, x_n は変数で、 a_1, \dots, a_n, b は述語を特徴づけるパラメータ(=述語にとっては定数)である。「この形の論理式で interpolant が存在するか」という問題は Farkas の補題というものを用いることで普通の線形計画問題(の解の存在判定)に帰着することができ、効率的に計算することができる。

 A, B がもう少し複雑な形の場合、例えば  A = \bigvee_{i \in I} A_i かつ  B = \bigvee_{j \in J} B_j のような形の場合についても議論されている。原理的には各  (i,j) \in I \times J について上記手順で half-space による interpolant  a_1^{i,j} x_1 + \dots + a_n^{i,j} x_n \le b^{i,j} を求めればその Boolean combination が interpolant になるが、それでは interpolant が複雑過ぎるので、できるだけ多くの  (i,j) の組で一つの half-space を共通して使うように計算する手法が提案されている。

感想

名前だけは知っていたが、読んだことはなかった論文。読んだ感想としては、あまりの驚きの無さにショックであった。歴史的な背景はきちんと追えていないのだが、もしかしたらこの論文が template-based で Farkas's Lemma を使う推論手法そのものの初出なのかもしれない。そうだとすれば、この論文に驚きがないのは手法が既に業界に広く知られているからであって、驚きがないことが偉大な論文ということになるだろう。

Complexity and Information in Invariant Inference

by Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv and Sharon Shoham

Propositional classical logic で記述された LTS の invariant 発見問題についての計算量や情報理論による解析。遷移関係  \delta については black-box として扱い、Hoare triple  \{ A \} \delta \{B\} が成立するかどうか(成立しない場合は反例も返す)を使って invariant を探すという設定。

概要

上記の設定において「多項式長の invariant を探す問題」について考察している。主結果は次の通り。

  • こうした推論問題においては invariant 候補をいかに上手く一般化するかが(実用上の)鍵になるが、上記の設定において性能の改善できるような一般化方法はない。問題を解くには指数回の Hoare クエリを必要とする。
  • PDR と ICE の推論方法を比較すると、PDR の方が指数的に優れている例が存在する。

後者において PDR と ICE の違いをどこに求めるかが一つの焦点であるが、本論文では Hoare クエリの種類の違いが本質的であるという観察をしている。つまり、PDR では  \{A\}\delta\{B\} A \neq B の場合も用いるが、ICE では  \{A\}\delta\{A\} (つまり  A が invariant であるか)しか用いない。この差が本質的な違いとなって、先述の指数的な差を生む。

(設定さえ上手くできれば)前者についてはそんなものだろうという気がする*1ので、後者について解説する。

差がつく例として利用されるのは、本論文で maximal systems for monotone invariant と呼ばれる種類の遷移系である。monotone invariant というのは、二値ブール代数  \mathbb{B} = \{ 0, 1 \} 0 < 1 という順序集合として理解したときに、invariant が  \mathbb{B}^n \to \mathbb{B} という関数として anti-monotone であることを指す。遷移系が invariant  I に対して maximal であるとは、 T = (I \times I) \cup (I^c \times I^c) であること、つまり任意の  I を満足する2状態は直接遷移可能で、さらに任意の  I を満足しない2状態も直接遷移可能である場合である。こうしたシステムの invariant 発見は非常に簡単で、初期状態の1ステップ forward image を計算すれば、それが invariant である。

forward image の計算は Hoare クエリそのものではないが、実は上手く Hoare クエリを繰り返すことで forward image が計算できる。PDR のように事前条件と事後条件に別のものを指定するクエリを利用すれば、(事前条件は初期状態に固定して) \{\mathrm{init}\} \delta \{B\} というクエリによって  B が invariant の過大近似であるかどうかを判定することができる。実際に invariant に入っている点  \vec{v} \in I (だけからなる singleton を表す性質)から初めて、変数の個数回ほど上記クエリを発行して2分探索を行うことにより、 I を conjunctive normal form で書いたときの節を1つ見つけることができる*2。これを  I の節の個数回だけ繰り返せば  I が得られる。

一方で ICE 型のクエリではこのようにして forward image を計算することはできず、一般の場合と同様の理由で指数回のクエリが必要となってしまう。

なお論文では Hoare クエリよりも少し強力な interpolation クエリについても議論されており、こちらでもやはり指数回のクエリ呼び出しを必要とするケースがあることが示されている。

感想

文句ない POPL paper だなあという内容であった。分析手法は新しく面白いし、概要は Sections 1, 2 を読めば概ね分かるので、興味のある人は読むのを勧める。PDR と ICE の効率の差を理論的に示せると考えたことはなかったので、結果は非常に印象的であった。一方で、証明手法を読んでいると、妥当そうな仮定を積み重ねて現実から離れたところに行ってしまったという印象を受けた。仮定のうち現実にそぐわないものとしては、例えば遷移関係  \delta が見えないという仮定*3やその複雑さが無制限であるという仮定*4が挙げられるだろう。また本論文の解析手法を整数等の無限データがある場合にどのように拡張することができるかも、興味深い非自明な問であろう。

余談だが、てっきり distinguished paper かと思っていたら、そうではなかったらしい。個人的には distinguished paper の水準にあると思う。

*1:証明が自明と言っているわけではないです。

*2: I が monotone であるという仮定は、上記の2分探索で構成される節の候補が本当に  I の節であるということの証明に用いる。Cf. Theorem 7.7

*3:実際には ICE 流の学習でも、反例集めなどの際に  \delta の中身を見ながら上手く集めるというようなことはされるはず。

*4:実際には1ステップ遷移関係はプログラムの1命令の実行に概ね対応しており、そのため遷移関係の複雑さは命令の複雑さ程度で押さえられるとしても良さそう。

An Automaton Learning Approach to Solving Safety Games over Infinite Graphs

by Daniel Neider and Ufuk Topcu

有限状態オートマトンで表現された (safety) 無限ゲームをオートマトン学習で解くというもの。Winning set を記述するオートマトンを反例駆動で探す。なお本論文で扱っているゲームは通常の意味での games over pushdown graph よりも難しいことに注意。

概要

有限アルファベット  \Sigma を固定して、ノード集合が  \Sigma^* であるような safety game を考える。Safety game  G = (V_0, V_1, E, I, F) はプレイヤー 0 と 1 の頂点  V_0, V_1 (ただし  V_0 \cap V_1 = \emptyset)と辺  E \subseteq (V_0 \cup V_1) \times (V_0 \cup V_1) と初期頂点集合  I \subseteq (V_0 \cup V_1) と到達してはいけない頂点集合  F \subseteq (V_0 \cup V_1) で定まる。ゲームが regular であるということを、この論文では、 (V_0 \cup V_1) \subseteq \Sigma^* であって、部分集合  V_0, V_1, I, F がすべて正規言語であって、 E が(有限状態非決定性トランスデューサで表現できるという意味で)正規関係であることをいう。それぞれのオートマトン表現を入力とし、ゲームにプレイヤー 0 が勝てるか否か(そして勝てる場合には winning set)を出力する問題を考える。

本論文の手法は regular な winning set をオートマトン学習で予想するというものである。正規言語  W \subseteq (V_0 \cup V_1) が与えられたときに、それが winning set であるかどうかの判定は容易にできる。Winning set でない場合には、次の4種類の反例のうちいずれかを構成することができる。

  1.  I \not\subseteq W であることの証拠となる  v \in I \setminus W (positive counterexample)
  2.  F \cap W \neq \emptyset であることの証拠となる  v \in F \cap W (negative counterexample)
  3. (プレイヤー 0 の次の手の非存在) v \in W \cap V_0 から  W 内への辺がないことの証拠である、組  (v, \{ u \mid (v, u) \in E \}) であって  v \in V_0 \cap W かつ  \{ u \mid (v, u) \in E \} \cap W = \emptyset であるもの (existential implicational counterexample)
  4. (プレイヤー 1 の合法手の考慮不足) W v \in W \cap V_1 から到達可能な頂点で閉じていないことの証拠である、組  (v, \{ w \mid (v, w) \in E \}) であって  v \in V_1 \cap W かつ  \{ u \mid (u, w) \in E \} \setminus W \neq \emptyset であるもの (universal implicational counterexample)

winning set の学習は、上記反例を蓄積しつつ、これまでに与えられた反例たちと consistent なオートマトンのうち最小サイズのものを作ることで行われる。最小サイズのオートマトンの構成は propositional SAT への帰着する。具体的には「状態数 N のオートマトンで、これまでに与えられた反例たちと consistent なオートマトンが存在する」ことを表す命題論理式を作り、UNSAT だった場合には N をインクリメントすることを繰り返す。命題論理式は、素朴に「各状態が受理状態か」を表す命題変数 N 個と、「状態 i で記号 a を読んだ時に状態 j に遷移するか」を表す命題変数  N \times |\Sigma| \times N 個を使って自然に表現したものを使う。

私見

まずはゲームの表現力について。まずは下限から。論文では pushdown game などと比べられているが、本論文の "regular game" は通常の意味の "pushdown game" (= pushdown automaton の configuration graph 上のゲーム)よりも強いことに注意*1。実際、pushdown automaton の configuration 上の遷移関係  (\gamma, q) \stackrel{a}{\to} (\gamma', q') は regular relation であるので、pushdown automaton の configuration graph は本論文の意味で regular である。あとは一工夫して、スタック  \gamma と状態  q と読むべき語  w の3つ組を頂点としたゲームグラフを考えて、初期ノード集合を (初期スタック、初期状態、任意の語) という形の組み合わせすべてとすると、pushdown automaton の受理言語が全体集合  \Sigma^* かという問題を、本論文のゲームに帰着できる。よって特に本論文のゲームは決定不能である*2

つぎに上限だが、body に ∀ を許した CHC よりは弱いことが容易に分かる。したがって、 \mu-calculus + 文字列データの  \mu\nu-fragment に帰着可能でもある。その意味で Beyene et al. POPL14 の game solving で扱っている問題(=CHC + ∃-head + well-foundedness predicate)よりは、理論的には大幅に簡単である。

設定さえ正しく理解できれば、手法自体は素朴という印象であった。

*1:この点から、先行研究が使っている呼称 reachability games on automatic graphs の方が適切であろう。

*2:決定不能性は論文中でも触れられている。

Cyclic Program Synthesis

by Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe and Ilya Sergey

帰納法を用いた証明において帰納法の仮定を適切に強める(=補題発見)ことが本質的な課題であることは広く知られているが、同様にプログラムの自動合成では適切な補助関数の生成が本質的な課題である。「プログラムと証明は同じものである」というアイデアを使って、本論文では循環証明 (cyclic proof) の証明探索を通してヒープを扱うプログラムを自動合成する方法が提案されている。

概要

一言で言えば、本論文の手法は Synthetic Separation Logic (SSL) という先行研究の cyclic な拡張である。これだけだとあんまりなので、以下ではもう少し詳しく説明する。

難しい例として論文で挙げられているのが2分木をリストに変換するプログラム flatten の自動合成である。ノードが葉である場合は良いとして、問題はノードが葉でない場合である。それぞれの子供を引数に再帰的に flatten を呼ぶまではよいのだが、その結果として2つのリストが手に入ってしまう。最終的な出力は1つのリストなので、2つのリストを1つにまとめることが必要なのだが、既存研究ではこの手続きを自動で合成することができなかった*1。これは「2つのリストを1つのリストにする手続きが必要」ということを発見するのが難しいためで、このことをヒントとして与えれば(例えば append 関数を利用可能な関数一覧に加えておくとか、append 関数の仕様をヒントとして入力するとか)既存手法でも解くことができる。

本論文のアプローチは cyclic proof なので、再帰的なデータ構造を見つけたら取り敢えずパターンマッチをしてみて、「生成対象の仕様が(偶然)これまでに見たものと一致したら、1回目の部分にジャンプする」*2ようなプログラムを合成することになる。リストの例では

2つのリスト xs, ys から、1つのリスト zs を作る (*)

ということが仕様を満足するプログラムを探索するのに、xs にパターンマッチをして、xs が空のケースとそうでないケースの両方でプログラムを合成することを目指す。空のケースはいいとして、空でないケースを考えると、xs = (a :: xs') という形だと分かるので、

1つの要素 a と2つのリスト xs', ys から、1つのリスト zs を作る

というのが新たな仕様となる。(zs = (a :: zs')) とすることで、

2つのリスト xs' と ys から、1つのリスト zs' を作る

という仕様を満足するプログラムを見つければよい。しかしこれは、(*)の変数名を変えたものに過ぎないので、そこへのジャンプ(または関数呼び出し)に代えられる。こうして、提案手法は flatten の合成に成功することになる。

私見

本手法はそれなりに強力なようだが、一見して気になる制限として、補題発見を能動的に行わない点を挙げる。cyclic proof の文脈でいうなら、cut を行わずに証明探索を行っている。したがって、自然に推論していって上の例のように "たまたま" cycle が構成できる場合はいいが、一般にはそういうことは期待できないはずで、そうした場合には本手法でも上手く合成はできないだろう。どれくらい多くの仕様(に対する推論)が自然に cycle を生成するのか、というのは重要な問題である。ライブラリ関数などは、その普遍性・一般性ゆえに、こういう制約下でも合成しやすそうである。

一般の cyclic proof 探索に応用できるような新しいアイデアがあるわけではなく、cyclic proof の推論としてはむしろ非常に素朴(かつ限界が明らかなもの)である。「一定程度ちゃんと動く実装」のための様々な工夫が大変そうであった。

*1:Eguchi et al. APLAS 2018 でも本当にできないのだろうか? できそうな気もするのだが。

*2:正確には、2度出現した仕様を発見したら、1度目の出現をその入出力関係を満足するような(再帰)関数の定義の始まりだと理解し、2度目の出現は再帰呼出とするプログラムを合成する。

Testing Machine Learning Code using Polyhedral Region

by Md Sohel Ahmed, Fuyuki Ishikawa and Mahito Sugiyama

機械学習の学習を行うコードのバグを発見するためのテスト手法。

こういったコードの検証が重要であることは論を待たないが、挙動が入力に強く依存しているためテストが難しい。正しさの保証された「参照実装」があればそれとの比較に持ち込めるが、そもそも「正しい出力」を定義することができるのかというレベルから問題がある。

既存研究でのアプローチは、主に2つあったらしい。1つは複数の実装を用意して多数決で決めるというもの。もう1つは metamorphic testing という手法で「入力に〇〇という変換をすると出力が□□のように変化するはず」という学習手法に関する知識を利用するものである。入力の変換の例としては画像の RGB を入れ替えるというものが挙げられている。

本論文では Polyhedral Lemma という補題を使ってテストする手法が提案されている。Polyhedral Lemma とは、入力データから計算されるある polyhedron 上では学習結果のモデルの出力が変化しないという性質で、比較的最近 (2016) に示されたものらしい。本論文の提案は、Polyhedral Lemma が成り立つ学習アルゴリズムを対象として、実際にその polyhedron 上で値が変化しないことをテストするというものである。

アルゴリズムの細部をテストするのではなくて、アルゴリズムが満足するはずの性質をテストしていこう、というアイデアは面白いと思った。(その発見自体を本論文の貢献としてよいのかは、私には判断が付きませんが。)

Machine Learning in Compiler Optimization

by Zhenng Wang and Michael O'Boyle

コンパイラにおける最適化への機械学習の応用に関するサーベイ。はじめての accessible introduction を謳っていて、中身も良くまとまっている良いサーベイ

概要

「新しい高度なプログラム変換」を機械学習で発見する話かと思って期待していたが、そうではなくて、本論文の主題は「最適なコンパイルオプションを探す」というものだった。考えてみればそれはそうで、明らかに後者の方が有望だろうし、むしろ何で前者のようなものを期待したのだろうか*1。「最適なコンパイラオプションを探す」という課題にしても(もちろん)簡単なものではなくて、何を学習させるかや、プログラムをどのように機械学習コンポーネントへの入力にするのかといった点の選択を適切に行う必要がある。その重要性も明らかで、ターゲットのOSやプロセッサごとに最適なオプションを探すことが如何に大変であるかが量的な情報と共に議論されている*2

何を学習させるかについては、コスト関数を学習させるものと、最適なオプションを学習させるものとに分けられて解説されている。議論の分量から量るに、主要なポイントではないように思われる。

特徴量の取り扱いは詳しく議論されており、重要度の高さが伺える。静的な量(例:命令の種類や数)の他に、構文木や制御フローグラフのような構造(に工夫をしたもの)や、動的に得られる情報(例:ループ回数、ホットコード、CPU負荷、動的命令数、L1キャッスミス数など。左から右に高レベルから低レベルとなっている)を使うこともできる。特に印象的だったのは動的特徴量の重要性に関する議論で、ほとんど実行されない部分についての情報が機械学習コンポーネントを混乱させることがあるという指摘である。また reaction-based な手法というものもあって、これは予め注意深く定められた複数のコンパイルオプションでの実行結果から特徴量を抽出するというものである。特徴量抽出を Deep Learning を用いて自動で行う方法も議論されているが、これは静的な情報しか扱えず、動的な情報から特徴量を抽出するにはまだ人手が必要らしい。

私見

新しいプログラム変換の自動発見のような期待したものは future work のようで残念だったが、特徴量エンジニアリングの節と参考文献は検証屋にも興味深い内容ではないだろうか。あと、上では述べていないが、(たぶん第一著者の趣味もあって)並列プログラムの最適化についての内容が厚く、そこも面白いかもしれない。

*1:もちろん理由は明らかで、個人的な興味が複雑なプログラムの性質の推論にあるからです。

*2:例えば、手で良いコスト関数を作るには、アーキテクチャごとに数ヶ月から年単位の開発が必要だそう。