(57)【要約】  短時間に仮説を算出することができる仮説推論装置（１）等を提供する。仮説推論装置（１）は、前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する仮説生成部（２）と、所定の処理に従い、作成した仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出する変換部（３）と、算出された制約条件と、算出された重みとに基づき、所定の条件を満たしている場合における仮説を算出するソルバ部（４）と、を備える。
2020003585.tif 000002
【特許請求の範囲】
【請求項１】
前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する仮説生成手段と、
所定の処理に従い、作成した前記仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出するSAT変換手段と、
算出された前記制約条件と、算出された前記重みとに基づき、所定の条件を満たしている場合における仮説を算出するソルバ手段と、を備える仮説推論装置。
【請求項２】
前記SAT変換手段は、前記所定の処理に従い、前記仮説候補集合における論理式に基づき、必ず満たさなければいけない制約条件と、必ずしも満たす必要がない制約条件とを作成し、
前記ソルバ手段は、作成した前記制約条件に基づき、前記所定の条件を満たしている場合における仮説を算出する
請求項１に記載の仮説推論装置。
【請求項３】
前記SAT変換手段は、
仮説候補を整数線形計画問題に変換する、ILP問題変換手段と、
ILP問題変換手段で変換された整数線形計画問題を、ハードな制約として扱う論理式とソフトな制約として扱う論理式に変換する、ILP-SAT変換手段と、をさらに備える請求項１に記載の仮説推論装置。
【請求項４】
前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する第１ステップと、
所定の処理に従い、作成した前記仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出する第２ステップと、
算出された前記制約条件と、算出された前記重みとに基づき、所定の条件を満たしている場合における仮説を算出する第３ステップと、を備える仮説推論方法。
【請求項５】
前記第２ステップは、前記所定の処理に従い、前記仮説候補集合における論理式に基づき、必ず満たさなければいけない制約条件と、必ずしも満たす必要がない制約条件とを作成し、
前記第３ステップは、作成した前記制約条件に基づき、前記所定の条件を満たしている場合における仮説を算出する
請求項４に記載の仮説推論方法。
【請求項６】
前記第２ステップは、
仮説候補を整数線形計画問題に変換する第４ステップと、
変換された整数線形計画問題を、ハードな制約として扱う論理式とソフトな制約として扱う論理式に変換する第５ステップと、をさらに備える請求項４に記載の仮説推論方法。
【請求項７】
前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する第１ステップと、
所定の処理に従い、作成した前記仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出する第２ステップと、
算出された前記制約条件と、算出された前記重みとに基づき、所定の条件を満たしている場合における仮説を算出する第３ステップと、をコンピュータに実行させるプログラムが格納された非一時的なコンピュータ可読媒体。
【請求項８】
前記第２ステップは、前記所定の処理に従い、前記仮説候補集合における論理式に基づき、必ず満たさなければいけない制約条件と、必ずしも満たす必要がない制約条件とを作成し、
前記第３ステップは、作成した前記制約条件に基づき、前記所定の条件を満たしている場合における仮説を算出する
請求項７に記載のプログラムが格納された非一時的なコンピュータ可読媒体。
【請求項９】
前記第２ステップは、
仮説候補を整数線形計画問題に変換する第４ステップと、
変換された整数線形計画問題を、ハードな制約として扱う論理式とソフトな制約として扱う論理式に変換する第５ステップと、をさらに備える請求項７に記載のプログラムが格納された非一時的なコンピュータ可読媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、仮説を作成する仮説推論装置、仮説推論方法及びコンピュータ可読媒体に関する。
【背景技術】
【０００２】
仮説推論処理方式の一例が、非特許文献１に記載されている。仮説推論処理方式は、図１０に示すように、仮説候補の集合（Candidate hypotheses）を生成する手段と、個々の仮説候補の蓋然性を評価することで、観測論理式を最も過不足なく説明できるような仮説候補を、仮説候補の集合から選び出す手段から構成されている。当該仮説推論処理方式は、観測論理式（Observation）と知識ベース（Background knowledge）を入力として受け取り、観測論理式に対する説明として最良仮説を出力する。当該仮説推論処理方式においては、観測論理式には「どの観測情報を重視するか」を表すパラメータ（コスト）が与えられ、知識ベースに含まれる個々の推論知識（Axiom）には「後件が成り立つ時に前件が成り立つ信頼度」を表すパラメータ（重み、Weights）が与えられており、仮説候補を評価する手続きにおいてはそれらのパラメータを考慮して評価値（Evaluation）が計算される。このような方式によれば、観測論理式をより良く、より簡潔に説明できるような説明を生成することが可能である。【０００３】
例えば、観測論理式として「犯罪者Ａと警察Ｂが居て、２人とも同じパトカーに乗っている」という情報を表した論理式が与えられ、知識ベースとして「ｘがｙを逮捕するなら、ｘは警察でありｙは犯罪者である」「逮捕された人物はパトカーに乗る」「警察はパトカーに乗る」のような知識を表した推論知識が与えられたとき、図１０に示すような手続きによって、仮説推論方式は、観測論理式に対して、各推論知識を観測論理式に対して後ろ向きに適用することによって、最終的に、図１１に示すような仮説候補を解仮説として出力することが期待される。即ち、「ＢがＡを逮捕した」という言説だけ仮説すれば、全ての観測情報は、その仮説から背景知識を用いて演繹的に導出できることを示している。即ち、「ＢがＡを逮捕した」という仮説によって、観測論理式は過不足なく説明される。
【先行技術文献】
【非特許文献】
【０００４】
【非特許文献１】Naoya Inoue and Kentaro Inui. ILP-based Reasoning for Weighted Abduction. In Proceedings of AAAI Workshop on Plan, Activity and Intent Recognition, pp. 25-32, August 2011.
【非特許文献２】Vasco Manquinho, Joao Marques-Silva, Jordi Planes. Algorithms for Weighted Boolean Optimization, International Conference on Theory and Applications of Satisfiability Testing, pp. 495-508,2009.
【非特許文献３】Naoya Inoue and Kentaro Inui. Large-scale Cost-based Abduction in Full-fledged First-order Predicate Logic with Cutting Plane Inference. In Proceedings of the 13th European Conference on Logics in Artificial Intelligence (JELIA), pp.281-293, September 2012
【非特許文献４】Dowling, William F and Gallier, Jean H, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, The Journal of Logic Programming, pp. 267-284, 1984.
【非特許文献５】Williams, Ryan and Gomes, Carla P and Selman, Bart, Backdoors to typical case complexity, IJCAI, pp.1173-1178, 2003.
【非特許文献６】「Open-WBO製品情報」、インターネット〈http://sat.inesc-id.pt/open-wbo/〉
【非特許文献７】株式会社  オクトーバー・スカイ、「Gurobi Optimizer製品情報」、インターネット〈https://www.octobersky.jp/products/gurobi.html〉
【非特許文献８】「SCIP製品情報」、インターネット〈http://scip.zib.de/〉
【発明の概要】
【発明が解決しようとする課題】
【０００５】
非特許文献１に開示されている仮説推論処理方式の問題として、ビックデータ利用や、推論を複数回繰り返すシステムにおいては、仮説を得るまでに長い処理時間がかかるという問題があった。本発明は、以上の背景に鑑みなされたものであり、短時間に仮説を算出することができる仮説推論装置等を提供することを主たる目的とする。
【課題を解決するための手段】
【０００６】
本発明は、仮説推論装置であって、前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する仮説生成部と、所定の処理に従い、作成した前記仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出するSAT変換部と、算出された前記制約条件と、算出された前記重みとに基づき、所定の条件を満たしている場合における仮説を算出するソルバ部と、を備えるものである。【０００７】
また、本発明は、仮説推論方法であって、前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する第１ステップと、所定の処理に従い、作成した前記仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出する第２ステップと、算出された前記制約条件と、算出された前記重みとに基づき、所定の条件を満たしている場合における仮説を算出する第３ステップと、を備えるものである。【０００８】
さらに、本発明は、プログラムであって、前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する第１ステップと、所定の処理に従い、作成した前記仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出する第２ステップと、算出された前記制約条件と、算出された前記重みとに基づき、所定の条件を満たしている場合における仮説を算出する第３ステップと、をコンピュータに実行させるものである。
【発明の効果】
【０００９】
本発明によれば、短時間に仮説を算出することができる。
【図面の簡単な説明】
【００１０】
【図１】本発明の概要について説明する図である。
【図２】仮説推論方法について説明する図である。
【図３】実施の形態１にかかる仮説推論装置の動作を示すフローチャートである。
【図４】本実施形態にかかる仮説推論装置に関する実験結果である。比較手法は、非特許文献１に記載されているアルゴリズムである。
【図５】仮説候補集合を示す模式図である。
【図６】仮説と各変数の真偽値割り当てについて説明する模式図である。
【図７】各ブール変数に対する真理値を示す表である。
【図８】実施の形態２にかかる仮説推論装置の構成を示す模式図である。
【図９】本発明を実施するための実施の形態２における仮説推論装置の動作を示すフローチャートである。
【図１０】関連する仮説推論処理方式について説明する模式図である。
【図１１】関連する仮説推論処理方式について説明する模式図である。
【発明を実施するための形態】
【００１１】
以下に、図面を参照して、本発明の実施の形態について例示的に詳しく説明する。ただし、以下の実施の形態に記載されている構成要素は単なる例示であり、本発明の技術範囲をそれらのみに限定する趣旨のものではない。
【００１２】
［本発明の特徴］
本発明の実施の形態の説明に先立って、本発明の特徴についてその概要をまず説明する。図１は、本発明の概要について説明する図である。図１に示すように、本発明にかかる仮説推論装置１は、仮説生成部２と、変換部３と、ソルバ部４と、を備える。
【００１３】
仮説生成部２は、前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する。変換部３は、所定の処理に従い、作成した仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出する。ソルバ部４は、算出された制約条件と、算出された重みとに基づき、所定の条件を満たしている場合における仮説を算出する。このようにすることで短時間に仮説を算出することができる。
【００１４】
［実施の形態１］
以下、図面を参照して本発明の実施の形態１について説明する。
【００１５】
［構成の説明］
実施の形態１にかかる仮説推論装置における仮説推論方法について、図２を用いて説明する。図２は、実施の形態１にかかる仮説推論装置の構成について示す模式図である。この仮説推論装置における仮説推論方法では、仮説推論における処理にて生み出される仮説候補の集合から、例えば、最良仮説を導く際の問題を、Weighted Partial MaxSAT問題に変換し、SATソルバを利用することによって仮説が作成される。Weighted Partial MaxSAT問題は、例えば、非特許文献２に開示されているため、本実施形態においては、概略を説明することとし、詳細な説明については省略する。
【００１６】
ここで、MaxSAT（最大充足割当問題、Maximum satisfiability problem）とは、CNF(連言標準形、Conjunctive normal form)で書かれた論理式内の変数に対して、満たす節(clause)の数が最も多くなるような真理値の割り当てを求める問題である。ここで、真理値は、例えば、1（真値、真）,0（偽値、偽）という数値にて表現される。CNFとは、リテラル xi,jに対し、∧∨xi,j の形式をした論理式のことである。「∧」は論理積演算を表す。「∨」は論理和演算を表す。例えば、(A ∨ B) ∧ (¬B ∨ C ∨ ¬D) ∧ (D ∨ ¬E) のような論理式は、CNFに従い記述された論理式である。
【００１７】
次に、Weighted(重み付き) MaxSATとは、CNFで書かれた論理式内の節に重みが与えられている場合に、論理式内の変数に対して、満たす節の重みの和が最も大きくなるような真理値の割り当てを求める問題である。
【００１８】
また、本実施形態において、Weighted Partial MaxSATとは、前述のWeighted MaxSATに対し、必ず満たさなければいけない節(hard clause)と、必ずしも満たされるとは限らない節(soft clause)を含む最適化問題である。当該最適化問題は、例えば、以下のように定義される。
【００１９】
Weighted Partial(重み付き部分) MaxSAT とは、CNFの論理式φ={(C1, w1), …, (Cm, wm), (Cm+1, ∞), …, (Cm+m’, ∞)}が与えられたときに、偽となる節の重みの和が最小となるような真理値の割り当てIを求める問題である。ただし、φの各要素は、節と、節に対する重みとが関連付けされた情報を表し、m個の節(例えば、C1〜Cm)は、ソフト（soft）であり、m’個の節(例えば、Cm+1〜Cm+m’)は、ハード（hard）である。また、「∞」は、重みがw1〜wmと比べて十分に大きな値であることを概念的に表す。
【００２０】
SATソルバ１０５は、上述したような問題を表す入力に対して、例えば、当該問題の解（この場合、仮説）を出力する装置である。当該処理は、例えば、非特許文献４、及び、非特許文献５に開示されている方法を用いて実現することができる。このため、本実施形態においては、当該処理に関する詳細な説明を省略する。
【００２１】
図２に示すように、仮説推論装置１０７は、仮説候補生成部１０３と、SAT変換部１０４と、SATソルバ１０５と、仮説出力部１０６と、を含む。仮説推論装置１０７は、知識データベース１０２に通信可能に接続されている。知識データベース１０２には、仮説を作成する基となる所与のルール（知識）を表す情報が格納されている。
【００２２】
仮説候補生成部１０３は、観測論理式１０１と、知識データベース１０２に格納されている情報とを入力として、仮説候補集合を出力する。観測論理式１０１は、観測された情報が論理式を用いて表されている情報である。ここで、仮説候補集合は、与えられた観測論理式に対し、知識データベース内のルール（すなわち、前件が成り立てば後件が成り立つという、所与のルール）を後ろ向きに適用していくことにより生成される仮説を、少なくとも１つ以上含む集合を表す。すなわち、該ルールは、前件から後件を導出する論理式である。さらに、知識データベースに格納されている情報は、前件から後件を導出する論理式が表された知識情報であると表すことができる。例えば、任意の時点での仮説候補集合をH’としたときに、ある仮説候補q(A)⊆H’に対して、推論知識p(x)⇒q(x)を後ろ向きに適用することによって、p(A)が新たに仮説候補集合に追加される。この結果、仮説候補集合Hは、「H’ ∧ p(A)」に更新される。この場合に、「p(x)」は、前件を表す。「q(x)」は、後件を表す。「推論知識p(x)⇒q(x)」は、１つのルールを表す。「x」は、当該ルールにおける変数を表す。
【００２３】
SAT変換部１０４は、仮説候補生成部１０３で導出された仮説候補集合を入力として、Weighted Partial MaxSAT問題への変換を行い、SATソルバ１０５に入力する。
【００２４】
仮説出力部１０６は、SATソルバ１０５で得られた結果から最良仮説を出力する。
【００２５】
尚、説明の便宜上、各実施形態においては、最良という言葉を用いて説明するが、必ずしも、最良でなくともよい。仮説が成り立っている可能性が高いほど、当該仮説は、良い仮説である。逆に、仮説が成り立っている可能性が低いほど、当該仮説は、悪い仮説である。
【００２６】
［動作の説明］
図３は、実施の形態１にかかる仮説推論装置の動作を示すフローチャートである。
【００２７】
図３に示すように、まず、仮説候補生成部１０３は、入力として観測論理式を受け付ける。(ステップS1)。次に、仮説候補生成部１０３は、仮説候補集合に観測論理式を追加する（ステップS2）。仮説候補集合は、例えば、記憶部（不図示）に格納されていてもよい。また、仮説候補集合は、あらかじめ、空集合にて初期化されているとする。
【００２８】
続いて、仮説候補生成部１０３は、仮説候補集合内の要素に対して、ルールを後ろ向きに適用することによって、仮説候補を生成する（ステップS3）。なお、仮説候補生成部１０３は、作成した仮説候補集合を表す情報を記憶部（不図示）に格納してもよい。続いて、仮説候補生成部１０３は、生成した仮説候補を仮説候補集合に追加する（ステップS4）。仮説候補生成部１０３は、作成した仮説候補集合を、SAT変換部１０４に入力する。すなわち、仮説候補生成部１０３は、前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する。
【００２９】
続いて、仮説候補生成部１０３は、仮説候補集合内の要素に対して、知識データベース内のルール（すなわち、知識）を後ろ向きに適用できるものが無くなったか（または、設定した終了条件になったか）、否か、を判定する（ステップS5）。知識データベース内のルールを後ろ向きに適用できるものが無くなった場合（YESの場合）、続くステップS6に処理を進め、知識データベース内のルールを後ろ向きに適用できるものが無くなっていない場合（NOの場合）、ステップS3に処理を戻す。
【００３０】
続いて、SAT変換部１０４は、得られた仮説候補集合をWeighted Partial MaxSAT問題に変換する（ステップS6）。SAT変換部１０４は、変換後の情報をSATソルバ１０５に入力する。すなわち、SAT変換部１０４は、実施例１等にて例示される所定の処理に従い、作成した仮説候補集合に関する制約条件（実施例１にて詳述する。「¬(hq(y)∧¬rq(y))」等）と、当該制約条件に対する重み（実施例１にて詳述する。「cost(q(y)」、「∞」等）を算出する。SATソルバ１０５は、変換された問題にSATソルバを適用する。当該処理の結果として、SATソルバ１０５は、例えば、最良仮説を作成する。すなわち、SATソルバ１０５は、算出された制約条件と、算出された重みとに基づき、所定の条件を満たしている場合における仮説を算出する。所定の条件は、例えば、仮説に関するコストを最小、または、略最小にするという条件である。所定の条件は、仮説に関するコストが、ある閾値よりも低いという条件であってもよい。所定の条件は、上述した例に限定されない。すなわち、SATソルバ１０５が、所定の条件を満足している場合における仮説を算出することによって、成り立っている可能性が高い仮説を算出することができる。
【００３１】
続いて、仮説出力部１０６は、SATソルバ１０５が作成した最良仮説を、例えば、外部に出力する（ステップS7）。
【００３２】
[効果の説明]
次に本実施の形態の効果について説明する。非特許文献３には、一階述語論理上での仮説候補集合に対して、logical termの数をnとしたときO(n3)個という膨大な推移律に関する制約式が生成されることが開示されている。
【００３３】
一方、特許文献４、及び、非特許文献５には、論理式を構成している節のうち、ホーン節で構成されている割合が高いCNFを入力とするSAT問題は、高速に解くことができることが知られている。ホーン節では仮説推論の仮説候補集合に対して生成する制約式の推移律に対応する。
【００３４】
本発明者は、仮説を作成する場合に、作成した当該仮説においてはホーン節の割合が高いという規則を見出した。そして、本発明者は、仮説を作成する場合には、上述したようなSAT問題に従い仮説を作成した方が、処理時間が短いという規則を見出した。したがって、本発明者は、見出した当該規則に従い高速な処理が行えるよう、仮説推論装置１０７における各構成要素を構成した。この結果、本実施形態にかかる仮説推論装置１０７は、短時間に仮説を生成することができる。
【００３５】
図４は、本実施形態にかかる仮説推論装置１０７に関する実験結果である。比較手法は、非特許文献１に記載されているアルゴリズムである。非特許文献１に記載されているアルゴリズムは、仮説候補集合をILP（Integer linear programming）問題に変換し、ILPソルバが最適解を見つけるアルゴリズムである。その際にILPソルバとしてはGurobi（非特許文献７参照）、SCIP（非特許文献８参照）を用いている。
【００３６】
一方、本実施の形態を実施するために用いたSATソルバはopenWBO（非特許文献６参照）である。
【００３７】
ILP問題、SAT問題ともNP困難であることが知られているが、仮説推論に適用した場合、SATソルバは、実験結果より、本実施形態は大きい知識データベースに対し、比較手法のGurobiの約１０倍、SCIPの約１００倍の高速化されたことがわかる。一方小さい知識データベースに関して、比較手法で高速に動作していたものに対して、本実施形態も同様の速度で高速に動作することがわかる。
【００３８】
[実施例１]
仮説推論の代表的な一つである、Weighted Abductionを例に説明する。
知識データベースBと観測論理式Oは以下のような例を考える
【００３９】
B(Rule)
r(x)→s(x),
s(x)∧t(y)→q(x)
【００４０】
O(query)
∃x, y q(y)∧r(A)∧s(x)
【００４１】
すなわち、知識データベース１０２には、知識データベースBにて示されたルールが格納されているとする。また、観測論理式１０１は、観測論理式Oにて示された論理式であるとする。仮説推論装置１０７は、当該ルールと、当該論理式とを入力として受け取る。
【００４２】
この入力に対し、仮説候補生成部１０３は、以下のように仮説候補集合を生成する。まず、仮説候補生成部１０３は、仮説論理式のq(y)に対し、知識データベース中のs(x)∧t(y)→q(x)を後ろ向きに適用することで、s(y)∧t(u)が仮説候補に追加する。仮説候補生成部１０３は、変数yに関係ない変数としてuを導入する。仮説候補生成部１０３は、同様に、後ろ向き適用を繰り返すことで、最終的に図５に示す仮説候補集合を作成する。
【００４３】
仮説候補集合内に含まれる各要素に対して、以下の論理変数を導入する。以降ではp, qを仮説候補集合内の任意のリテラルとする。
【００４４】
hp: リテラルpを仮説に含む場合は、True。
rp: リテラルpがコストを払わない場合は、True。
up,q: リテラルpがリテラルqと単一化される場合は、True。
【００４５】
例えば、図６に示すように知識データベースB(Rule)と、観測論理式O(query)が与えられたときに、仮説候補生成部１０３は、生成された仮説候補集合に対して上述した変数（例えば、ある変数によって指し示される記憶領域）を導入し、各変数に対して、(hp:T  rp:T), (hs:T  rs:F), (hr:T  rr:F), (ht1:F  rt1:F), (ht2:T  rt2:F), (hq:T  rq:F), (ut1,t2 : F)のように値を格納する。これは、仮説H={s, r, q}を表す。仮説と各変数の真偽値割り当ての詳細に関しては、例えば、非特許文献１に開示されている。
【００４６】
しかし、各変数に対する真偽値割り当てを正しく行わないと、解として満たさないものが生成される。例として、H’={s, p}は解としては不良であり、「s ∧ r -> p」のルールを後ろ向きに適用することによりsが生成される。それと同時に、rも生成される。例で用いられているH’={s, p}は本来生成されるrに別のルールを適用されてほかのリテラルが生成されているわけでもなく、rがH’の要素としているわけでもない。よってH’は観測論理式に対し、知識データベース内のルールを後ろ向きに適用して生み出す仮説としては生成されないものとなる。
【００４７】
次に、SAT変換部１０４における処理について説明する。
そこで、仮説としての解の性質を満たすために以下のように制約を考える必要がある。Partial Weighted MAX SATの制約として以下の制約１及び制約３ように記述することができる。まずは、命題論理の範囲にて当該制約を説明する。
【００４８】
制約１：「観測に含まれるリテラルは常に含まれるか、仮説候補に説明されている。」
【００４９】
各p∈観測Oに対し  制約論理式：hp
【００５０】
制約２：「仮説に含まれるリテラルがコストを払わないときは、そのリテラルがほかのリテラルに説明されているときか、単一化するときである。」
「説明する可能性があるリテラルがandでつながっている場合は全て仮説候補に含むか全て含まないかである。」
【００５１】
各p∈仮説Pに対し、制約論理式は、以下のようになる。
【００５２】
【数１】
2020003585.tif 000003
【００５３】
ここで、Bは知識データベースに含まれるルール集合である。
expl(p)={e | e∈P, {e}∨B |= p}
sml(p)= {q | q∈P, c(q)<c(p)}
ただし、c(p)はリテラルpに割り振られるコストを表す。
and(p)は、pを説明しうるリテラルで、andでつながっているリテラルa∈Pを表す。
【００５４】
制約３：「単一化されるときは、単一化されるリテラルはすべて仮説されている」
【００５５】
各p,q∈仮説Pに対し、制約論理式：
(¬up,q ∨ hp) ∧ (¬up,q ∨ hq)
【００５６】
次に、一階述語論理の範囲にて当該制約を説明する。
リテラルの引数の変数x∈Vと、定数または変数y∈(V ∨ C)について
sx,y =  True(xにyが代入されるとき)
False(それ以外)
を与える。
【００５７】
制約４：「単一化されるリテラルの引数は全て等しい」
リテラルpとqを単一化する際に必要な変数代入の組集合up, qに対して、制約論理式は以下のようになる。
【００５８】
【数２】
2020003585.tif 000004
【００５９】
制約５：「一つの変数に複数の定数が同時に割り当てられることはない」
【００６０】
【数３】
2020003585.tif 000005
【００６１】
制約６：「３変数間の推移律」
制約論理式：
¬sx,y ∨ ¬sy,z ∨ sx,z
¬sx,z ∨ ¬sx,y ∨ sy,z
¬sy,z ∨ ¬sx,z ∨ sx,y
【００６２】
上記に基づき実際に作成されるSAT制約式は以下である。
制約1: hq(y)
制約2:¬rs(x)∨hr(x), ¬rq(y)∨hs(y)∨ht(u) ; hs(y)∨ht(u)
制約3:(¬ur(x),r(A)∨hr(x))∧(¬ur(x),r(A)∨hr(A)), (¬us(y),s(x)∨hs(y))∧(¬us(y),s(x)∨hs(x))
制約4:ur(x),r(A)→sx,A
制約5:(sx,A∧¬sx,B)∨(¬sx,A∧sx,B)
制約6:¬sy,A ∨¬sx,A ∨sx,y
¬sx,A ∨¬sx,y ∨sy,A
¬sx,A ∨¬sx,y ∨sy,A
【００６３】
これらに対し、各ブール変数に対する真理値表は図７に示すようになる。したがって、SAT変換部１０４は、仮説候補生成部が１０３が作成した仮説から、上述したような処理に従い制約条件を表す情報を作成し、作成した制約を表す情報を用いて
【００６４】
論理式φ
={ (¬(hq(y)∧¬rq(y)), cost(q(y))), (¬(hr(A)∧¬rr(A)), cost(r(A))), …,
(hq(y), ∞), (¬rs(x)∨hr(x), ∞), …,(¬sx,A ∨¬sx,y ∨sy,A, ∞)}
を作成する。
【００６５】
これは、Weighted Partial MaxSAT問題にて用いられる形式にて表された情報である。すなわち、SAT変換部１０４は、仮説候補生成部１０３が作成した仮説を、Weighted Partial MaxSAT問題に変換する。したがって、SAT変換部１０４は、上述した制約１〜制約６を満たしている制約を、それぞれ、特定し、特定した各制約に応じた重みを割り当てる。上述した例において、SAT変換部１０４は、制約１、制約２、及び、制約６に対しては、十分な大きさの重み（すなわち、模式的に表した「∞」、必ず満たさなければいけないハード節に対する重み）を割り当てる。すなわち、これらの制約は、ハード（hard）な制約として扱う論理式であるということもできる。
【００６６】
また、SAT変換部１０４は、制約３、制約４、及び、制約５に対して、各制約を導出する場合におけるコストを重み(すなわち、必ずしも満たすとは限らないソフト節に対する重み)として割り当てる。すなわち、これらの制約は、ソフトな制約として扱う論理式であるということもできる。
【００６７】
したがって、SAT変換部１０４は、仮説候補集合に基づき、ハードな制約として扱う論理式と、ソフトな制約として扱う論理式とを作成し、作成した当該論理式を制約条件として含む最適化問題（すなわち、Weighted Partial MaxSAT問題）に変換する。
【００６８】
SAT変換部１０４は、作成した情報をSATソルバ１０５に入力する。
この中からSATソルバ１０５が最良仮説の「q(y)∧r(A)∧s(x)∧r(x)∧x=A」を算出する。すなわち、SATソルバ１０５は、仮説候補生成部１０３が作成した仮説を用いて、尤もらしい仮説を作成する。SATソルバ１０５が出力する最適解が、例えば、最良仮説である。したがって、SATソルバ１０５は、当該最適化問題に対して、所定の条件を満たしている場合における仮説を算出する。
【００６９】
実施の形態２
以下、図面を参照して本発明の実施の形態２について説明する。
【００７０】
［構成の説明］
図８は、実施の形態２にかかる仮説推論装置２０１の構成を示す模式図である。図８に示すように、仮説推論装置２０１は、仮説候補生成部１０３と、ILP問題変換部２０４と、ILP-SAT変換部２０５とSATソルバ１０５と、出力部２０７と、を含む。仮説推論装置２０１は、観測論理式１０１を入力として受け取る。仮説推論装置２０１は、知識データベース１０２に通信可能に接続されている。
ILP問題変換部２０４は、仮説候補生成部１０３で導出された仮説候補集合を入力として、ILP問題への変換を行う。ILP問題への変換方法は、例えば、非特許文献１に記述されている方法である。ILP問題への変換方法は、上記に限定されない。ILP-SAT変換部２０５は、ILP問題を、上述したようなWeighted Partial MaxSAT問題に変換を行う。変換方法は例えば、非特許文献２に記述されている。変換方法は、上述した例に限定されない。
SATソルバ１０５は、ILP-SAT変換部で得られたSAT問題を解き、最良仮説出力部では得られた最適解から最良仮説を出力する。
【００７１】
［動作の説明］
図９は、本発明を実施するための実施の形態２における仮説推論装置の動作を示すフローチャートである。
【００７２】
図９に示すように、仮説候補生成部１０３は、入力として観測論理式を受け取る(ステップS101)。次に、仮説候補生成部１０３は、仮説候補集合に観測論理式を追加する（ステップS102）。仮説候補集合は、例えば、記憶部（不図示）に格納されていてもよい。また、仮説候補集合は、あらかじめ、空集合にて初期化されているとする。
【００７３】
続いて、仮説候補生成部１０３は、仮説候補集合内の要素に対して、ルールを後ろ向きに適用する（ステップS103）。記憶部(不図示)には、初期化された仮説候補集合を表す情報が予め格納されている。仮説候補生成部１０３は、当該観測論理式が追加された仮説候補集合を表す情報を記憶部(不図示)に格納してもよい。なお、仮説候補生成部１０３は、作成した仮説候補集合を表す情報を記憶部（不図示）に格納してもよい。
【００７４】
続いて、仮説候補生成部１０３は、生成された仮説候補を仮説候補集合に追加する（ステップS104）。仮説候補生成部１０３は、作成した仮説候補集合を、ILP問題変換部２０４に入力する。
【００７５】
続いて、仮説候補生成部１０３は、仮説候補集合内の要素に対して、知識データベース１０２内のルールを後ろ向きに適用できるものが無くなったか否かを判定する（ステップS105）。知識データベース内のルールを後ろ向きに適用できるものが無くなった場合（YESの場合）、続くステップS106に処理を進め、知識データベース内のルールを後ろ向きに適用できるものが無くなっていない場合（NOの場合）、ステップS103に処理を戻す。
【００７６】
ILP問題変換部２０４は、得られた仮説候補集合をILP問題に変換し（ステップS106）、変換したILP問題をILP-SAT変換部２０５に入力する。
【００７７】
ILP-SAT変換部２０５は、ILP問題をWeighted Partial MaxSAT問題に変換し（ステップS107）、変換した当該問題をSATソルバ１０５に入力する。
【００７８】
SATソルバ１０５は、当該問題に対して、図３を参照しながら上述したような処理をおこなうことによって最良仮説を出力する（ステップS108）。
【００７９】
［実施例２］
実施例１と変更のある、ILP問題変換部２０４、ILP-SAT変換部２０５のみの説明を行う。
【００８０】
与えられる知識データベースBと観測論理式Oは実施例１と同じとする。まずILP問題変換部２０４は、仮説候補生成部１０３で作成された仮説候補に対して、非特許文献１に従いILP制約を以下のように作成する。
【００８１】
制約1: hq(y) = 1
制約2: rs(x) ≦ hr(x); hs(y)=ht(u), ２rq(y) ≦ hs(y)＋ht(u)
制約3: 2ur(x), r(A) ≦ hr(x) + hr(A), 2us(y), s(x) ≦ hs(y) + hs(x)
制約4: ur(x), r(A) ≦ sx,A
制約5: sx,A + sx,B ≦ 1
制約6: sy,A - sx,A - sx,y ≧ -1
【００８２】
ILP-SAT変換部２０５は、これらのILP制約式を非特許文献２に基づき、実施例１のSAT制約に変換する。これによりSATソルバ１０５への入力が可能になる。
【００８３】
なお、本発明は上記実施の形態に限られたものではなく、趣旨を逸脱しない範囲で適宜変更することが可能である。
【００８４】
以上のように、本発明によれば、仮説推論を高速に行うことができるため、大規模な知識データベースを利用することができ、観測の規模が大きいものにも対応することができる。
【００８５】
例えば、コンピュータセキュリティーの分野においては、作成した仮説を用いてマルウェアを検出するルール、または、マルウェアを検出する処理を決定することができる。この場合に、知識データベース１０２には、例えば、「あるプログラムがアカウントを管理するファイルを開けば、当該あるプログラムは通信ネットワークに接続する」等の所与の知識を表す情報が格納されている。仮説推論装置１０７は、観測論理式（例えば、「あるプログラムがマルウェアである」という論理式）を導出する仮説を作成する。仮説推論装置１０７は、作成した当該仮説を構成している各論理式が成り立つか否かを判定してもよい。仮説推論装置１０７は、当該仮説に含まれている論理式が成り立っている場合には、仮説推論装置１０７は、当該あるプログラムがマルウェアであると判定する。この場合に、仮説推論装置１０７は、当該あるプログラムに関するコンピュータセキュリティーをチェックすることができる。
【００８６】
例えば、複数の構成要素によって構成されている装置が故障した場合に、当該故障に関連している構成要素を特定する場合にも、仮説推論装置１０７が作成した仮説を用いることができる。この場合に、知識データベース１０２には、例えば、「ある装置に障害が起きたら、当該ある装置によって生産される生産量が減少する」等の所与の知識を表す情報が格納されている。この場合に、観測論理式は、例えば、「当該装置が故障した」ことを表す論理式である。仮説推論装置１０７は、作成した当該仮説を構成している各論理式が成り立つか否かを判定してもよい。仮説推論装置１０７は、当該仮説に含まれている論理式が成り立っている場合には、仮説推論装置１０７は、当該装置が故障したと判定する。この場合に、仮説推論装置１０７は、当該装置において故障が生じた構成要素を特定することができる。
【００８７】
仮説推論により作成された仮説を用いることができる分野は、コンピュータセキュリティーや、故障診断装置等に限定されない。
【００８８】
上述の実施の形態では、本発明をハードウェアの構成として説明したが、本発明は、これに限定されるものではない。本発明は、各処理を、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）に制御プログラムを実行させることにより実現することも可能である。
【００８９】
上述の仮説推論方法を実現するための制御プログラムは、様々なタイプの非一時的なコンピュータ可読媒体（ｎｏｎ−ｔｒａｎｓｉｔｏｒｙ  ｃｏｍｐｕｔｅｒ  ｒｅａｄａｂｌｅ  ｍｅｄｉｕｍ）を用いて格納され、コンピュータに供給することができる。非一時的なコンピュータ可読媒体は、様々なタイプの実体のある記録媒体（ｔａｎｇｉｂｌｅ  ｓｔｏｒａｇｅ  ｍｅｄｉｕｍ）を含む。非一時的なコンピュータ可読媒体の例は、磁気記録媒体（例えばフレキシブルディスク、磁気テープ、ハードディスクドライブ）、光磁気記録媒体（例えば光磁気ディスク）、ＣＤ−ＲＯＭ（Ｒｅａｄ  Ｏｎｌｙ  Ｍｅｍｏｒy）、ＣＤ−Ｒ、ＣＤ−Ｒ／Ｗ、半導体メモリ（例えば、マスクＲＯＭ、ＰＲＯＭ（Ｐｒｏｇｒａｍｍａｂｌｅ  ＲＯＭ）、ＥＰＲＯＭ（Ｅｒａｓａｂｌｅ  ＰＲＯＭ）、フラッシュＲＯＭ、ＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）を含む。また、プログラムは、様々なタイプの一時的なコンピュータ可読媒体（ｔｒａｎｓｉｔｏｒｙ  ｃｏｍｐｕｔｅｒ  ｒｅａｄａｂｌｅ  ｍｅｄｉｕｍ）によってコンピュータに供給されてもよい。一時的なコンピュータ可読媒体の例は、電気信号、光信号、及び電磁波を含む。一時的なコンピュータ可読媒体は、電線及び光ファイバ等の有線通信路、又は無線通信路を介して、プログラムをコンピュータに供給できる。
【００９０】
以上、実施の形態を参照して本願発明を説明したが、本願発明は上記によって限定されるものではない。本願発明の構成や詳細には、発明のスコープ内で当業者が理解し得る様々な変更をすることができる。
【００９１】
この出願は、２０１８年６月２５日に出願された日本出願特願２０１８−１１９７７１を基礎とする優先権を主張し、その開示の全てをここに取り込む。
【符号の説明】
【００９２】
１  仮説推論装置
２  仮説生成部
３  変換部
４  ソルバ部
１０１  観測論理式
１０２  知識データベース
１０３  仮説候補生成部
１０４  変換部
１０５  ソルバ
１０６  仮説出力部
１０７  仮説推論装置
２０１  仮説推論装置
２０４  問題変換部
２０５  ILP-SAT変換部
２０７  出力部
【図１】
2020003585.tif 000006
【図２】
2020003585.tif 000007
【図３】
2020003585.tif 000008
【図４】
2020003585.tif 000009
【図５】
2020003585.tif 000010
【図６】
2020003585.tif 000011
【図７】
2020003585.tif 000012
【図８】
2020003585.tif 000013
【図９】
2020003585.tif 000014
【図１０】
2020003585.tif 000015
【図１１】
2020003585.tif 000016
【手続補正書】
【提出日】令和2年12月15日(2020.12.15)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する仮説生成手段と、
所定の処理に従い、作成した前記仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出するSAT変換手段と、
算出された前記制約条件と、算出された前記重みとに基づき、所定の条件を満たしている場合における仮説を算出するソルバ手段と、を備える仮説推論装置。
【請求項２】
前記SAT変換手段は、前記所定の処理に従い、前記仮説候補集合における論理式に基づき、必ず満たさなければいけない制約条件と、必ずしも満たす必要がない制約条件とを作成し、
前記ソルバ手段は、作成した前記制約条件に基づき、前記所定の条件を満たしている場合における仮説を算出する
請求項１に記載の仮説推論装置。
【請求項３】
前記SAT変換手段は、
仮説候補を整数線形計画問題に変換する、ILP問題変換手段と、
ILP問題変換手段で変換された整数線形計画問題を、ハードな制約として扱う論理式とソフトな制約として扱う論理式に変換する、ILP-SAT変換手段と、をさらに備える請求項１に記載の仮説推論装置。
【請求項４】
コンピュータが、
前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成し、
所定の処理に従い、作成した前記仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出し、
算出された前記制約条件と、算出された前記重みとに基づき、所定の条件を満たしている場合における仮説を算出する、仮説推論方法。
【請求項５】
前記制約条件及び当該制約条件に対する重みの算出では、前記所定の処理に従い、前記仮説候補集合における論理式に基づき、必ず満たさなければいけない制約条件と、必ずしも満たす必要がない制約条件とを作成し、
前記仮説の算出では、作成した前記制約条件に基づき、前記所定の条件を満たしている場合における仮説を算出する
請求項４に記載の仮説推論方法。
【請求項６】
前記制約条件及び当該制約条件に対する重みの算出では、
仮説候補を整数線形計画問題に変換し、
変換された整数線形計画問題を、ハードな制約として扱う論理式とソフトな制約として扱う論理式に変換する、請求項４に記載の仮説推論方法。
【請求項７】
前件から後件を導出する論理式が表された知識情報を含む知識データベースに基づき、観測された情報が、論理式が導出される仮説を含む仮説候補集合を作成する第１ステップと、
所定の処理に従い、作成した前記仮説候補集合に関する制約条件と、当該制約条件に対する重みを算出する第２ステップと、
算出された前記制約条件と、算出された前記重みとに基づき、所定の条件を満たしている場合における仮説を算出する第３ステップと、をコンピュータに実行させる制御プログラム。
【請求項８】
前記第２ステップは、前記所定の処理に従い、前記仮説候補集合における論理式に基づき、必ず満たさなければいけない制約条件と、必ずしも満たす必要がない制約条件とを作成し、
前記第３ステップは、作成した前記制約条件に基づき、前記所定の条件を満たしている場合における仮説を算出する
請求項７に記載の制御プログラム。
【請求項９】
前記第２ステップは、
仮説候補を整数線形計画問題に変換する第４ステップと、
変換された整数線形計画問題を、ハードな制約として扱う論理式とソフトな制約として扱う論理式に変換する第５ステップと、をさらに備える請求項７に記載の制御プログラム。
【手続補正３】
【補正対象書類名】明細書
【補正対象項目名】００３３
【補正方法】変更
【補正の内容】
【００３３】
一方、非特許文献４、及び、非特許文献５には、論理式を構成している節のうち、ホーン節で構成されている割合が高いCNFを入力とするSAT問題は、高速に解くことができることが知られている。ホーン節では仮説推論の仮説候補集合に対して生成する制約式の推移律に対応する。
【国際調査報告】
2020003585.tif 000017
2020003585.tif 000018
2020003585.tif 000019
2020003585.tif 000020