形式手法言語Alloyを使ってSAT問題を解く

ナレッジグラフ推論チャレンジで、形式手法言語であるAlloyが評価されたので簡単に紹介をしたいと思う。
http://alloytools.org/

　ナレッジグラフ推論チャレンジとは、解釈可能AIの基礎技術を探索する目的で2018年に開催されたコンテストだ。ちなみに、第2回が今度開かれる。シャーロックホームズの「まだらの紐」という短編小説を題材にして、ホームズが推理する場面までのデータを利用し、「犯人をあてること」と「犯人である根拠を示すこと」を数理技術で行うことが求められる。
http://challenge.knowledge-graph.jp/

　話がずれてしまうが、解釈可能性AIとか説明的AIとかは、昨今ニュースでちょこちょこ現れてきている言葉である。聞いたことがある人も多いと思う。人工知能の判断や結果の根拠をうまく提示できずブラックボックスになりがちなため、重要な判断での利用が躊躇されてしまうことが大きな業界の課題となってしまっている。そこを解決することが求められているのである、特に、今回のAIブームの継続には、この解釈可能性という課題がひとつのハードルになっていて、ここが解決しなければ飽和も近いのではないかとさえ言われている。

　さて、話を元に戻して、コンテストでのAIの推理技術のなかで、SAT問題とAlloyという2つの面白いおもちゃ（?）が評価されたので、ぜひ紹介したい。

　Alloyというは、形式手法言語のAlloyAnalyzerのことだ。まず最初に簡単に説明すると、ある設計したシステムに不具合がないことを調べるためであったり、不具合があればどのようなバグがあるかを見つける、モデル検査という領域で主に使われている。*1与えたルールと状態に関する事実を使って、ルールの間に矛盾があるかどうかや、あるアクションがルールに整合しているかをチェックしくれるソフトウェアである。

　たとえば、何かプログラムを書いたら、いろいろなケースを想定して、バグがないかテストをすることは、誰でも行うとは思う。プログラムだけでなく、何かの業務ルールであったり、セキュリティ上のルールでもよい。何かたくさんのルールを策定した時には、そのルール同士、矛盾がないかとか穴がないかを調べることは当たり前に行うことである。通常は、いくつかの数値やデータを想定して代入し、問題がないことをチェックするが、形式手法やモデル検査ではそのルール自体を論理学の言葉で書き表して、チェックしようという考え方をする。現在では、ルールに支配される対象として、プログラム以外にも検査対象となる事例があり、社内業務や道路交通でさえも対象となる。数理論理の形でルールを書くことで、明確で厳密な設計を目指すために利用されているのである。

　具体的に、論理をチェックするとはどういうことかを、コンテストの資料の例で見てみる。たとえば、表のように2人の人物がいて、人は誰かを殺すことができ、いま片方のみ死んでいる状況としよう。ここでは、存在する対象、支配する論理、観測された事実の3要素に分けて、チェックしたいことを書き、この状況下での整合可能な状況を探索させる。

構成	具体	Alloy形式
対象	ある人物A、Bがいる	abstract sig Person { kill : this -> Person} one sig A,B extends Person {}
論理	人は殺されると死ぬ	pred dead[q:Person] { some Person.kill.q}
事実	Aは生きている Bは死んでいる	fact{ dead[B] not dead[A] }

以上の構成を、Alloyのスクリプトに起こすと次のようになる。上に書いたことを、そのまま書くだけで、動く。
github.com

abstract sig Person { 
	kill : this -> Person}
one sig A,B extends Person {}

pred dead[q:Person] { some Person.kill.q}

fact{
dead[B]
not dead[A]
}

pred show {}
run show

最後の2行は、表示用のおまじない。

実行することで、このルールと観測事実から可能な状態がすべて出力される。

例を聞いただけだと、AがBを殺したという一番左のケースしかないように思うが、dead[q:Person]の定義を見る限り、自分自身を殺す状況が排除されていない。つまり、（無理やり解釈すると）「Bの自殺にAが協力した」、「Bが自殺した」の2つの解まで論理上は可能な解として提示される。少しわざとらしい例かもしれないが、このように検証したいルールと事実を記述して、考えていることの漏れがないかを網羅的に調べ上げることで、ルールの矛盾や漏れをチェックするのである。ちなみに、コンテストでは、登場人物の所在や移動の情報（アリバイ）と殺害方法を、ルールとして記述し、Alloyが可能な犯行状況を探し出すことで、犯人を特定している。

もうすこし、実際の業務っぽい話だと、レンタルシステムなどが良く例に挙がる。たとえば、次のようなレンタルシステムを考えたとしよう。

レンタルシステムの条件
・入会は成人ができる。
・入会すると会員になる。
・会員になると、図書が借りられる。
・会員は希望すれば退会できる。

普通に業務として回りそうだが、このシステムでは、会員は図書を借りたまま退会できてしまうので、 モデル （業務） の不備だ。ほかにも、実際に使われている例は少ないが調べてみると、鉄道システムでの利用*2があった。ダイアグラム（時刻表）と侵入ホームを設計するのは一苦労だろうし、人身事故が発生してしまえば、ダイアを緊急で書き直して、チェックしなければいけないので、機械的に行うことのニーズがあるのだろう。

このように、形式手法やモデル検査の知識と、Alloyなどのような言語を使うことで、ITシステムや業務システムを抽象化して、厳密に検証することができる。昨今では、コンプライアンス周りの監査ルールや法文など判断間違いでの事故を起こせないケースで、確率ベースの深層学習からルールベースの方法が取り入れられようともされ、期待が高い。
　今回紹介したAlloy自体は、特定の層の人たちにはよく知られているものだと思うので、ここではAlloyや形式手法を使わない人に何ができるのかということだけ伝えることに専念したため、結構荒かったかもしれない。類似の言語がいくつかあるので、興味があったら調べてみてほしい。

*1:システムの仕様を擬似コードに書き表すことで、Alloyがそのシステムが論理的に正しいかを検証したり、システムが可能な状態を（小スコープ仮説※のもとで）網羅的に調べ上げてくれる。モデル検査技術のひとつである。

*2:衝突回避のための条件（論理式） ①任意の相異なる２つの列車は同時刻に同線路区間にいないダイア設計になっていることの検査。 https://www.ipa.go.jp/files/000005272.pdf ②切符を持たない客が、駅構内の改札内エリアに入れない構造になっているかの検査。