Learning Reliable Logical Rules with SATNet

TL;DR

This paper introduces a novel method to extract human-readable, verifiable logical rules from differentiable SATNet models, significantly improving interpretability and reliability in logical reasoning tasks.

Contribution

It proposes a new specification technique called 'maximum equality' to decode SATNet's learned weights into interpretable logical rules and verifies their correctness.

Findings

Decoded rules achieve 100% accuracy with exact solvers.

The method ensures logical rules are functionally equivalent to ground truth.

Improves interpretability and verification of learned logical rules.

Abstract

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.