Learning Reliable Logical Rules with SATNet

要約

論理的推論と深層学習の橋渡しは、高度なAIシステムにとって極めて重要である。本研究では、事前に指定された論理構造に依存することなく、微分可能な学習によって解釈可能で検証可能な論理ルールを生成することで、この目標に取り組む新しいフレームワークを提示する。我々のアプローチは、入出力例から基礎となるルールを学習する微分可能なMaxSATソルバーであるSATNetを基盤としている。その有効性にもかかわらず、SATNetの学習された重みは素直に解釈できるものではなく、人間が読めるルールを生成できない。この問題に対処するため、我々は「最大等式」と呼ばれる新しい指定法を提案する。この指定法は、SATNetの学習された重みと、重み付きMaxSAT形式の命題論理ルールセットとの間の交換を可能にする。デコードされた重み付きMaxSAT式を用いて、それを基底真理則に対して検証するために、さらにいくつかの効果的な検証手法を導入する。ストリーム変換と数独問題に対する実験から、我々のデコードされたルールは高い信頼性を持つことが示された。さらに、我々のデコードした論理ルールが基底真理ルールと機能的に等価であることを正式に検証する。

要約(オリジナル)

Bridging logical reasoning and deep learning is crucial for advanced AI systems. In this work, we present a new framework that addresses this goal by generating interpretable and verifiable logical rules through differentiable learning, without relying on pre-specified logical structures. Our approach builds upon SATNet, a differentiable MaxSAT solver that learns the underlying rules from input-output examples. Despite its efficacy, the learned weights in SATNet are not straightforwardly interpretable, failing to produce human-readable rules. To address this, we propose a novel specification method called ‘maximum equality’, which enables the interchangeability between the learned weights of SATNet and a set of propositional logical rules in weighted MaxSAT form. With the decoded weighted MaxSAT formula, we further introduce several effective verification techniques to validate it against the ground truth rules. Experiments on stream transformations and Sudoku problems show that our decoded rules are highly reliable: using exact solvers on them could achieve 100% accuracy, whereas the original SATNet fails to give correct solutions in many cases. Furthermore, we formally verify that our decoded logical rules are functionally equivalent to the ground truth ones.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL