日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

関数型プログラムの不変条件の ICE 流学習手法
千葉 知也

佐藤 亮介

松田 一孝

小林 直樹

プログラムの不変条件の発見はプログラム検証での鍵となるステップである．Garg らは機械学習によって不変条件を発見する，ICE と呼ばれる手法を提案した．ICE は，学習用データとして，通常の正例，負例に加え含意制約というものを含めることにより，帰納的な不変条件を効果的に発見できる．本研究では，ICE を一階の関数型プログ
ラムの不変条件を発見出来るように拡張する．そのため，含意制約や負例を，複数回関数呼び出しする相互再帰関数の不変条件を発見するのに適する形に拡張し，それに応じて不変条件の学習法も拡張する．さらに，教師が学習者の推測を検証し，間違っているならば新たな学習用のデータを発見するアルゴリズムを与える．この手法を実装し，実験により有効性を確認した．

let rec mc91 x =1 はじめに

if x > 100 then不変条件とは，プログラムの実行中に常に満たされる条件であり，その発見はプログラム検証においx - 10elseて鍵となるステップである．実際，高階モデル検査に基づいた関数型プログラム用自動検証器である

MoCHi [5,6,9] のボトルネックとなっているのは，プ

mc91 (mc91 (x+11))in
if n < 102 then assert (mc91 n = 91)

ログラムの抽象解釈やプログラムを述語抽象するのに適切な述語を発見することである．

図1

関数型プログラムの例

本研究の目的は関数型プログラムの不変条件の発見である．ここでの関数型プログラムにおいての不変条

ので事後条件は x ≤ 101 ⇒ r = 91 である．このよう件とは，各関数の事前条件と事後条件，すなわちプロ

な不変条件を発見するのが本研究の目的である．

グラムの実行中の各関数呼び出しの引数と返り値の間

本 研 究 で は ，Garg ら に よ る 不 変 条 件 発 見 手 法に常に満たされる条件を指すものとする．例えば，図ICE [4] を関数型プログラム用に拡張する．ICE は機1 に示すマッカーシーの９１関数を計算するプログラ

械学習手法の一種であり，不変条件を推測する学習者

ムの場合，引数 x の値は 111 以下なので事前条件はと，その不変条件の妥当性を検証する教師の 2 種類

x ≤ 111，x の値が 101 以下ならば返り値 r は 91 なのモジュールから構成される．学習者はプログラムのICE-based Learning of Invariants for Functional
Programs
Tomoya Chiba, Ryosuke Sato, Naoki Kobayashi, 東京
大学情報理工学系研究科, Graduate School of Information Science and Technology, The University ofTokyo.
Kazutaka Matsuda, 東北大学大学院情報科学研究科,
Graduate School of Information Science, TOHOKU
University.

内容を知らず，教師から与えられる学習データのみから不変条件の候補を見つけ，教師は，プログラムと照らしあわせてその候補が妥当であるか否かを判定し，妥当でなければその候補に矛盾する学習データを学習者に伝える，というやりとりを繰り返す．
通常の教師つき機械学習と比較して ICE の特徴的な点は学習データにある．ICE の学習データは，不変条件 I(x) を満たすべき正例 x の (部分) 集合，不本論文の構成は以下の通りである．2 節では対象言変条件を満たすべきではない負例 y の集合に加えて，語を定義する．3 節では我々の不変条件発見手法の定「I(x) が成り立つならば I(y) も成り立つ」ことを表式化を行う．4 節では実装と実験結果について述べる．

す含意制約 (x, y) の集合からなる．含意制約が必要で5 節では関連研究について議論し，6 節で結論と今後あるのは，教師による不変条件の妥当性判定のための課題を述べる．

に，プログラムから生成される検証条件が用いられるからである．手続き型言語におけるループ不変条

2 対象言語件に関する検証条件式は I(x) ∧ Q(x, y) ⇒ I(y) の形

本節では，関数型プログラムの不変条件の発見の対をしているため，学習が成功するためには，不変条件の中でも，特にそのような条件式を満たす不変条件 I（このような不変条件は一般に帰納的不変条件と呼ば象となる言語を導入する．
対象言語は，以下の構文で定義される一階の関数型言語である．

れる）が見つかる必要がある．したがって，学習者にP ::= let rec D in t

も I(x) ∧ Q(x, y) ⇒ I(y) を満たす x, y の組を含意制

D ::= {f1 (ze1 ) = t1 , . . . , fn (fzn ) = tn }約として与えなければ効果的に不変条件の発見を行

t ::= x | let x = e in t | if v then t1 else t2 | failうことはできない．

e ::= v | op(v1 , v2 ) | f (ev)

本 論 文 で は ，上 記 の ICE の 含 意 制 約 を ，v ::= n | x「I(x1 ), . . . , I(xn ) が成り立つならば I(y) も成り立

メタ変数 P ，D ，t，e，v ，n，x，op はそれぞれプロつ」ことを表す ({x1 , . . . , xn }, y) の形に拡張する．こグラム，関数定義の集合，項，単純式，値，整数，変れは，多重再帰を含む関数型プログラムの場合，検証数，整数上のプリミティブ演算を表す．ze および v
eは条件式が I(x1 ) ∧ · · · ∧ I(xn ) ∧ P (x1 , . . . , xn ) ⇒ I(y)それぞれ変数および値の列を表す．関数 fk の定義がの形になるからである．例えば，図 1 のプログラム

fk (ez ) = t のとき，ze の長さを fk のアリティと呼び，の場合，mc91 の事後条件を I(x, r)，事前条件を簡単

arity(fk ) と書く．算術式の定義で，f (ev ) 中の ve の長さのために true（恒真）とすると，else 部に関する検は f のアリティと一致していなければならない．また，

証条件式は

束縛変数名は互いに異なるものとする．ブール値は整′′I(x + 11, r ) ∧ I(r , r) ∧ ¬(x > 100) ⇒ I(x, r)である．したがって，この場合には({(x1 , r1 ), (x2 , r2 )}, (x, r))の形の含意制約が必要である．

数を使って表し，0 を false とみなす．fail はプログラ
ムの異常終了を表す特別な項である．これを用いることで，表明 assert(e) (e が true に評価されるべきであるという表明) は let x = e in if x then true else fail

本論文では，相互再帰や多重再帰を許す一階の関数と書くことができる．簡単のため，この言語では A型言語を対象とし，上記のような含意制約の拡張を施

正規化されたプログラムしか許していないが，一般した上で，学習者および教師の手続きを定式化する．

のプログラムを A 正規化することができる [3] ため，

また，実装・実験によりその有効性を確認する．本研

これは本質的な制限ではない．

究の貢献は以下の通りである．

関数定義 D における簡約関係 −→D は図 2 によっ• 多重再帰や相互再帰を許す一階の関数型プログて定義される．[[op]] は op によって示される演算であラムの不変条件を発見できるように，ICE の学

り，例えば，[[+]](1, 2) = 3 となる．関数定義 D が文習データを拡張した．

脈から明らかなときは，−→D を −→ と書く．

• 学習データの拡張に合わせ，教師と学習者のア
ルゴリズムを拡張した．

• 実装および実験により，提案手法の有効性を確認した．

本研究の目的は，プログラムの実行が途中で停止しない (fail に到達しない) ことを証明するのに充分強い不変条件，すなわち，各関数毎の事前条件，事後条件を発見することである．ここで，P = let rec D in t かつ

VC (A, v, B) = A ⇒ [v/r]B
VC (A, fail , B) = ¬A
VC (A, if v then t1 else t2 , B) = VC (A ∧ v ̸= 0, t1 , B) ∧ VC (A ∧ v = 0, t2 , B)
VC (A, let x = v in t, B) = VC (A ∧ x = v, t, B)
VC (A, let x = op(v1 , v2 ) in t, B) = VC (A ∧ x = op(v1 , v2 ), t, B)
v /zek , x/rk ]Hkpost , t, B))
VC (A, let x = fk (ev ) in t, B) = A ⇒ ([ev /zek ]Hkpre ∧ VC ([eVC p (let rec {f1 (ze1 ) = t1 , . . . , fn (fzn ) = tk } in t) = ∧VC (Hkpre , tk , Hkpost ) ∧ VC (true, t, true)k∈{1,...,n}

図3

検証条件 VC p の生成規則の評価結果 r が B を満たすための十分条件を表す．

E[let x = v in t] −→D E[[v/x]t]

VC p (let rec D in t) が恒真のとき，t −↛ ∗D E[fail ]が成り立つ．

E[op(v1 , v2 )] −→D E[[[op]](v1 , v2 )]v ̸= 0E[if v then t1 else t2 ] −→D E[t1 ]3 発見手法
本節では，本研究の提案である，関数型言語のプ
ログラムの不変条件手法について述べる．まず，学習v=0
E[if v then t1 else t2 ] −→D E[t2 ]データの拡張について述べ，その後，教師と学習者の具体的なアルゴリズムについて述べる．

f (ez) = t ∈ D
E[f (ev )] −→D E[[e
z /e
v ]t]

3. 1 拡張された学習データ
学習データは {ξ1 , . . . , ξn } という形の負例制約のE ::= [ ] | let x = E in t
図2

集合 C と，({ξ1 , . . . , ξn }, ξ ′ ) という形の含意制約の集合 I から構成される．1 節にて，含意制約を拡張す

意味論る必要があることは既に述べた．負例制約を拡張す′

f (ez ) = t ∈ D のとき，P において H

preが f の事前

るのも，同様に多重再帰を扱うためである．ここで，条件であるとは，任意の v
e について，t −→∗D E[f (ev )]各 ξ1 , . . . , ξn および ξ は，データポイントであり，3が成り立つことを言う．また，P

つ組 (pre, k, ve) もしくは 4 つ組 (post, k, ve, a) のいず

が f の事後条件であるとは，任意のれかの形をしている．データポイント ξ が例である

ve，v について，t −→∗D E[f (ev )] かつ f (ev ) −→∗D v のとは，もし ξ = (pre, k, ve) という形ならば，求める関のとき，[ev /ez ]Hにおいて H

postpreが成り立つことを言う．以下，

数 fk の事前条件が引数 v
e に対し成り立つこと，もし関数 fk の事前条件，事後条件をそれぞれ Hkpre ，Hkpostξ = (post, k, ve, a) という形ならば，求める関数 fk のと書く．

事後条件が引数 ve とそのときの返り値 a に対し成り

とき，[e
v /e
z , v/r]H

post

事前条件と事後条件の候補が与えられたとき，そ立つことと定義する．

れらが実際に事前条件，事後条件になっているこ

直感的には，負例制約 {ξ1 , . . . , ξn } は，少なくともと，プログラム P の実行が途中で異常終了しない

一つの ξi が例ではない（すなわち，負例である）とことの検証条件 VC p (P ) は，図 3 のように定義できいう制約を表し，含意制約 ({ξ1 , . . . , ξn }, ξ ′ ) は，もる．ここで，VC (A, t, B) は，A が成り立つときに t

し {ξ1 , . . . , ξn } が全て例であれば ξ ′ もまた例でなけ約 ({η(P1 ), . . . , η(Pn )}, η(P ′ )) を生成する．ただし，ればならないという制約を表す．
元の ICE とは異なり，我々の拡張において，正例（制約）は，含意制約の (∅, ξ) という形の特殊な場合

η(P ) は以下で定義される関数である．

3. 2 教師アルゴリズム

η(P )(pre, k, θ(ex))
if P = [fxk /zek ]Hkpre=
(post, k, θ(ex), θ(y)) if P = [fxk /zek , y/rk ]Hkpost
一方，θ の下で (H2) の形のホーン節が偽であった

次に教師アルゴリズムについて述べる．教師は，学とする．この式を真にするためには，P1 , . . . , Pn のい習から事前・事後条件の候補を受けとり，その候補のずれかが偽であることが必要である．このとき，それ妥当性をプログラムと照らしあわせて検査し，もし妥に対応して，教師は負例制約 {η(P1 ), . . . , η(P2 )} を当でなければ新たな学習データを生成し学習者に渡

生成する．

となる．

す．教師アルゴリズムは以下の 3 ステップからなる．

教師は，こうして生成された含意制約と負例制約を

1. 対象プログラムと，学習者より受けとった各関集めて，以前の教師フェイズまでで得られた含意制約

数毎の事前条件の候補 Hkpre と事後条件の候補と負例制約に追加し，学習者に渡す．

Hkpost から図 3 に従い検証条件 VC p を生成する．
2. SMT ソルバを用いて，検証条件が恒真かどう

3. 3 学習者アルゴリズム
最後に，学習者アルゴリズムについて説明する．学か検査する．

3. もし恒真であれば，その検証条件を出力し，拡習者は，教師から学習データ I, C を受けとり，それのみから各関数の事前・事後条件の候補を発見し，そ張 ICE を終了する．

3’ もし恒真でなければ，SMT ソルバから得られれらを教師へと渡す．

た反例から新たな学習データを作成し，学習者に学習者のアルゴリズムは以下の 4 ステップからなる．

渡す．

1. 各関数について，事前・事後条件のテンプレー
トを準備する．

2. テンプレートのパラメータに関する制約を，教3. 2. 1 学習データの生成ステップ 3’ における学習データの生成について詳しく述べる．VC p が恒真でないため，VC p θ が偽となるような代入 θ が存在することなる．一方で，VC pは以下のいずれかの形をしたホーン節の連言で表現

師から受けとった学習データより求める．

3. 制約を SMT ソルバ等を利用して解消し，具体的な事前・事後条件の候補を求める．

4. 得られた各関数毎の事前・事後条件の候補を教
師に渡す．

できる．

(P1 ∧ · · · ∧ Pn ∧ C) ⇒ P′(P1 ∧ · · · ∧ Pn ∧ C) ⇒ C′

ここで，P1 , . . . , Pn および P

′

(H1)
(H2)

は [f
xk /zek ]Hkpre もしく

以下，ステップ 1 で準備するテンプレートと，ス
テップ 2 で生成する制約について詳しく述べる．

3. 3. 1 事前・事後条件のテンプレートは [fxk /zek , y/rk ]Hkpost のいずれかの形の論理式であ

事前・事後条件のテンプレートには，ICE [4] と同り，C はそれ以外の形の論理式である．今，θ の下で様に，以下の形に表される，線形不等式の Lj 個の論

VC p が偽であるので，こうした形のホーン節の中に理積の Li 個の論理和を用いる．

θ の下で偽になるものが少なくとも一つ存在することになる．

Ĥkt (xk1 , ..., xkm )
∨
∧
=

k
ij
k
ij
(sij
kt1 xv ij +skt2 xv ij ≤ ckt )i∈{1,...,Li } j∈{1,...,Lj }

kt1

kt2

もし，θ の下で (H1) の形のホーン節が偽であった

ここで，t はシンボル pre もしくは post であり，k はとする．この式を真にするためには，P1 , . . . , Pn の関数 fk に対するテンプレートであることを表す．ま

いずれかが偽であるか，P ′ が真であることが必要である．このとき，それに対応して，教師は含意制

た，xk1 , ..., xkm は fk の引数と返り値を表す変数である．つまり，t = pre のときは (xk1 , ..., xkm ) = (zek ) でテンプレートのパラメータに関する制約 ψ が得らあり，t = post のときは (xk1 , ..., xkm ) = (zek , rk ) でれた後，学習者は SMT ソルバ等を利用することで制ある．

約 ψ を解消する．もし制約解消が成功し，ψθ が真と

上記テンプレートにおいて Li と Lj は，初めは小さな値（例えば 1 や 2）にしておき，解が見つからな

なるような代入 θ を得られれば，事前・事後条件の候
補 Hkt を Ĥkt θ により得て，これを教師に渡す．

かったときに徐々に大きくすればよい．
（ただし，4 節

もし，そのような代入が得らない場合は，現在のテで述べる実装では，簡単のため，プログラムごとに固ンプレートでは事前・事後条件が表現できないことを定している．
）一般に Li や Lj が大きくなると制約解意味する．その場合は定数 Li ，Lj ，M を増加して再消の時間が大きく増加する．一方，Li や Lj が小さび拡張 ICE を実行する．

すぎると適切な事前・事後条件の候補がテンプレート

4 実装と実験で表現できない場合がある．

3. 3. 2 テンプレートのパラメータに関する制約の提案手法に基づき，不変条件発見器のプロトタイプ
を OCaml で実装し，実験による評価を行った．

生成と解消
学習は，教師から受けとった学習データ C ，I かijij
ら，テンプレートのパラメータ sij
ktl ，vktl ，ckt に関

4. 1 実装

する制約 ψ を図 4 に従い生成する．この制約 ψ の構

不変条件発見は 3 節で述べた手法を用い，そのう成は，元の ICE の構成法の単純な拡張になっている．

ち，学習者の不変条件候補の制約式と，教師の不変条

ここで，i，j ，k ，t，l および x の動く範囲は，i が件が検証条件を満たすかを表す式を解くための SMT{1, . . . , Li }，j が {1, . . . , Lj }，k は対象プログラムのソルバとして Z3 [2] を用いた．不変条件候補の制約関数の集合を {f1 , . . . , fn } とすると {1, . . . , n}，t は

式は，制約がインクリメンタルに増えていくため，Z3{pre, post}，l は {1, 2}，そして x は学習データ I とのインクリメンタルに制約を解く機能を用いた．

C 中のデータポイント全体である．制約 ψ は，sij
ktl ，
ij
ij
ij
ij
ij
vktl ，ckt 以外に，変数 bx ，bx ，dxl および rxl を含に固定し，事後条件の論理和と論理積の数および各テんでいる．これらの変数の直感的意味は以下の通りでンプレートの定数項の範囲は対象プログラムごとにある．

ユーザが指定するようにした．

事前条件のテンプレートを論理和と論理積の数は 1• bξ は，ξ が例であるかどうかを表す真偽値．
• bij
ξ は，ξ に対する (i, j) 番目の線形不等式の真偽値．すなわち，sij
kt1 xv ij

ktl1

k = K(ξ), t = T (ξ)，xvij

≤ cij
kt の，
kt1
ij
= nth(ξ, vkt2 ) とし+ sij
kt2 xv ij

kt2

たときの真偽値．

•
•

ij
dij
ξl は，ξ に対する skt2 xv ij の値．
ktl
ij
rξl
は，ξ に対する xvij の値．
ktl

4. 2 実験
複数の簡単なプログラムについて，実験を行った結果を図 5 に示す．
図 5 中の Li は，3. 3. 1 節の事後条件のテンプレー
ト中の節の論理和の個数であり，Lj は各節中の論理積の個数である．M は，テンプレート中の線形不等

また，M は定数であり，Li や Lj と同様に，小さなij
式の上限の範囲であり，各 cij
kt は，−M ≤ ckt ≤ M

値からはじめて解が見つからない場合に徐々に大きくを満たす．また，図 5 中の「学習データの個数」は，していく．

不変条件が見つかった時点での学習データの個数で

ij
ij
一見，変数 bξ ，bij
ξ ，dξl および rξl は不要に見えるある．

かもしれない．しかし，これらの変数を利用するこ実験に用いたプログラムは以下のとおり．

とにより，ψ は量化子のない一階の整数線形算術の• ack，sum，mc91 は，MoCHi [5] のベンチマー

論理式として表現でき [4]，その充足可能性の判定を，ク集に含まれるものである．mc91 はマッカーZ3 [2] などの SMT ソルバを用いて行うことができる．

シーの９１関数を評価して，引数が 101 以下な

(
)
ij
ij
ψ (sijktl )i,j,k,t,l , (vktl )i,j,k,t,l , (ckt )i,j,k,t :=

 
 

∧
∧ ∨
∧
∧
∨ ∧ ij(¬bξ ) ∧ (bξ ) ⇒ bξ′  ∧  (bξ ⇔bξ )
(Ξ,ξ′ )∈I ξ∈ΞΞ∈C ξ∈Ξ

∧


∧

∑

(bij
ξ ⇔ (

ξ,i,j







i

ξ

∧

ij
∧
rξl
≤ cij
K(ξ)T (ξ) ))j(−M ≤ cijkt ≤ M )i,j,k,tl∈{1,2}ij
sij
K(ξ)T (ξ)l = 0 ⇒ rξl = 0 ∧  ij
ij
ij
 s

∧
 K(ξ)T (ξ)l = 1 ⇒ rξl = dξl


ξ,i,j
ij
ij
ij
sK(ξ)T (ξ)l = −1 ⇒ rξl = −dξll∈{1,2}
 ∧
∧


ξ,i,j

l∈{1,2}

∧




ij
ij

(vK(ξ)T(ξ)l = h ⇒ dξl = nth(ξ, h))h∈{1,...,arity(K(ξ))+1}




 ∧

(−1 ≤ sij∧ktl ≤ 1)
i,j,k,tl∈{1,2}
 ∧(1 ≤ vkijpre l ≤ arity(fk )) ∧
∧

i,j,k
l∈{1,2}K((pre, k, ve)):=k

K((post, k, ve, a)):=k

T ((pre, k, ve))

:=

pre

T ((post, k, ve, a))

:=

post
図4

Program

∧





∧



ij
ij 

(1 ≤ vkijpost l ≤ arity(fk ) + 1)
(vkt1
̸= vkt2)
∧i,j,k,ti,j,kl∈{1,2}nth((pre, k, ve), h):=nth((post, k, ve, a), h)

:=

vh

v

h

if 1 ≤ h ≤ arity(fk )aif h = arity(fk ) + 1

テンプレートのパラメータに関する制約式

学習データの

時間

Li

Lj

M

ack

1

1

10

21

0.59

sum

2

2

30

4

0.12

mc91

2

2

110

135

975.49

mc11

2

2

30

135

26.55

mc11-multi

2

2

30

373

697.72

fib

2

2

10

30

3.68

mutual1

2

2

10

101

25.53

mutual2

2

2

30

108

29.95

個数

図5

実験結果

ら返り値が 91 であることをチェックし，成り立

ラムである．mc11-multi は mc11 を相互再帰をたなければ fail するプログラムである．

用いるように変形したものである．

• mc11 は mc91 の変種であり，引数が 21 以下な• fib は，n 番目のフィボナッチ数列を再帰を用い

ら返り値が 11 になることをチェックするプログて計算し，結果が n − 1 以上であることをチェックするプログラムである．

見手法との実験的比較などが挙げられる．

• mutual1, mutual2 は相互再帰を用いたプログラ
ムである．
いずれのプログラムについても，プログラムが failで異常終了しないことを検証するのに充分強い不変

謝辞
本研究は JSPS 研究費 15H05706，23220001 の助成を受けたものです．

条件が求まった．プログラム mc91 に時間がかかっているのは，不変条件中に必要な定数が大きいためで

参 考 文 献あり，そのような不変条件をより高速に求める方法を[ 1 ] Cousot, P. and Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis
of Programs by Construction or Approximation of
Fixpoints, Proceedings of the 4th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages, POPL ’77, New York, NY, USA,ACM, 1977, pp. 238–252.
[ 2 ] de Moura, L. M. and Bjørner, N.: Z3: An Efficient SMT Solver, Tools and Algorithms for theConstruction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Partof the Joint European Conferences on Theory andPractice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Ramakrishnan, C. R. and Rehof, J.(eds.), Lecture
Notes in Computer Science, Vol. 4963, Springer,
2008, pp. 337–340.
[ 3 ] Flanagan, C., Sabry, A., Duba, B. F., andFelleisen, M.: The Essence of Compiling with Continuations, Proceedings of the ACM SIGPLAN’93
Conference on Programming Language Design and
Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993, Cartwright, R.(ed.),ACM, 1993, pp. 237–247.
[ 4 ] Garg, P., Löding, C., Madhusudan, P., and Neider, D.: ICE: A Robust Framework for Learning
Invariants, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of
the Vienna Summer of Logic, VSL 2014, Vienna,
Austria, July 18-22, 2014. Proceedings, Biere, A.
and Bloem, R.(eds.), Lecture Notes in Computer
Science, Vol. 8559, Springer, 2014, pp. 69–87.
[ 5 ] Kobayashi, N., Sato, R., and Unno, H.: Predicate abstraction and CEGAR for higher-ordermodel checking, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose,
CA, USA, June 4-8, 2011, Hall, M. W. and Padua,
D. A.(eds.), ACM, 2011, pp. 222–233.
[ 6 ] Sato, R., Unno, H., and Kobayashi, N.: Towards
a scalable software model checker for higher-orderprograms, Proceedings of the ACM SIGPLAN 2013
Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, Rome, Italy, January 2122, 2013, Albert, E. and Mu, S.(eds.), ACM, 2013,
pp. 53–62.
[ 7 ] Terauchi, T.: Dependent types from counterexamples, Proceedings of the 37th ACM SIGPLAN-

考えることは今後の課題である．また，mc11 に比べて mc11-multi の検証に時間がかかっているのは相互再帰のために求める不変条件の個数が倍になったためであると考えられる．また，実験全体を通して，学習データとして引数と返り値が 1 しか違わないなど，非常に似ているものが多く発見されており，より効果的な学習データの選別も今後の課題である．

5 関連研究1 節で述べたとおり，本論文の手法は，Garg らによる不変条件発見手法 ICE [4] を関数型プログラム用に拡張したものである．ICE の含意制約は多重再帰を持つ関数の不変条件の発見には適していないため，含意制約を拡張した．
不変条件の発見手法の研究にはさまざまなものがあり，関数型プログラム用の不変条件発見手法にかぎっても，抽象解釈 [1] に基づく手法，interpolant に基づく手法 [7, 8]，テスト実行に基づく手法 [10] など様々なものが提案されている．それらの中でも本論文の手法に関連が深いのは，関数型プログラム用の不変条件発見問題をホーン節集合に対する求解問題に帰着して解く手法 [8] である．ホーン節集合が本論文で用いた検証条件に対応しており，本論文の手法では学習者に
はホーン節は示さずに例のみを与えているのに対し，
上記手法 [8] ではホーン節集合の解を直接求めようとしている点に違いがある．

6 まとめと今後の課題
本論文では，不変条件学習手法 ICE の枠組みを拡張し，関数型プログラムの不変条件の発見手法を提案した．今後の課題としては，実装の改良，高階関数を扱うための拡張，他の関数型プログラムの不変条件発

SIGACT Symposium on Principles of Programming
Languages, POPL 2010, Madrid, Spain, January
17-23, 2010, Hermenegildo, M. V. and Palsberg,J.(eds.), ACM, 2010, pp. 119–130.
[ 8 ] Unno, H. and Kobayashi, N.: Dependent type
inference with interpolants, Proceedings of the 11th
International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming,
September 7-9, 2009, Coimbra, Portugal, Porto,
A. and López-Fraguas, F. J.(eds.), ACM, 2009,
pp. 277–288.
[ 9 ] Unno, H., Terauchi, T., and Kobayashi, N.: Automating relatively complete verification of higher-

order functional programs, The 40th Annual ACM
SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, POPL ’13, Rome, Italy January 23 - 25, 2013, Giacobazzi, R. and Cousot,
R.(eds.), ACM, 2013, pp. 75–86.
[10] Zhu, H., Nori, A. V., and Jagannathan, S.: Dependent Array Type Inference from Tests, Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015,
Mumbai, India, January 12-14, 2015. Proceedings,
D’Souza, D., Lal, A., and Larsen, K. G.(eds.),
Lecture Notes in Computer Science, Vol. 8931,
Springer, 2015, pp. 412–430.