Learning Reliable Logical Rules with SATNet

Summary

The authors propose a new framework to generate interpretable and verifiable logical rules through differentiable learning. The framework is built upon SATNet, but the paper proposes a new interpretation method called maximum equality to decode the weights of SATNet into logical rules. The paper also proposes several verification methods to validate the decoded rules against ground truth rules. Experiments show that the decoded rules are highly reliable and functionally equivalent to the ground truth rules.

Strengths

- The impressive contribution of this paper is to distill the black box weights of a differentiable logic program like SATNet into human interpretable rules (boolean expressions) that can be verified. - Moreover, while the initial SATNet itself fails to achieve 100% test accuracy, the decoded interpretable rules manage to achieve perfect 100% test accuracy. This is remarkable because in the realm of logical reasoning, true generalization is a binary outcome: either the logical rules have truly been learned or they have not. In this paper, they show that they indeed have been learned, and verifiably so.

Weaknesses

- A major caveat to this work is that the 100% test accuracy was achieved by adding symbolic constraints that represent domain knowledge (e.g. rules of Sudoku). However, this is not necessarily a weakness, because incorporating domain knowledge is a useful thing to do in general, and it's great that the authors propose a recipe for doing so. - It would be nice to see the authors apply their technique to visual Sudoku. That was one of the hallmark contributions of the original SATNet paper that learned to play Sudoku by looking at images of digits.

Questions

- The paper mentions that the thresholding function was set to be approximately one-fifth of the average absolute value of non-zero elements in C. How was this decided, and how sensitive is the performance relative to the chosen threshold? It would be nice to see a graph of this.

Rating

7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.

Confidence

3: You are fairly confident in your assessment. It is possible that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.

Soundness

3 good

Presentation

3 good

Contribution

3 good

Limitations

The limitations section was well-written. If possible, I'd like to see an extended discussion of future work (perhaps in the Appendix), so the authors can provide useful directions for future research.

Summary

This paper builds on the SATNet framework on MaxSAT problems, adds an interpretation method that allows the conversion between its weight and propositional logical rules. Effective verification methods are proposed to see if the decoded rules from SATNet are functionally equivalent to the ground truth. Experiments on stream transformation and Sudoku problems show that the decoded "hard" logical rules achieve better performance than SATNet itself. The logical rules are verified to be equivalent to the ground truth.

Strengths

- The proposed interpretation method is well motivated and grounded theoretically. - The proposed interpretation method allows for the integration of symbolic knowledge as additive weights, which is flexible for the injection of human domain knowledge. - The verification methods are sound and have been practised on the experimental tasks of stream transformations and Sudoku. - The paper is well-written. - The decoded logical rules outperform SATNet on the experimental tasks, showing its practical effectiveness. Overall, it's a solid contribution to the interpretability of deep learning and neuro-symbolic computation communities.

Weaknesses

For the machine learning readers, perhaps the authors can give a bit more elaboration when propositions are stated. A couple of worked examples can also help the reader understand a lot better.

Questions

What challenges do you foresee when extending this work to more expressive logics like FOL and HOL, apart from the scaling issues mentioned in the discussions section? Are there fundamental bottlenecks to this? I would like to see more discussions on this, as propositional logic seems slightly limiting.

Rating

8: Strong Accept: Technically strong paper, with novel ideas, excellent impact on at least one area, or high-to-excellent impact on multiple areas, with excellent evaluation, resources, and reproducibility, and no unaddressed ethical considerations.

Confidence

3: You are fairly confident in your assessment. It is possible that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.

Soundness

4 excellent

Presentation

4 excellent

Contribution

4 excellent

Limitations

The authors addressed the limitations and scoped the work well.

Summary

The authors show that interpreting the SATNet model is not reliable. They reformulate the SATNet objective to a 'maximum equality specification' on matrix $C$. Assuming $C$ is ternary instead of continuous, the objective can be interpreted as a MaxSat problem. This problem can then be verified. Furthermore, the new objective is amenable to injecting symbolic background knowledge. Post rebuttal: I appreciate in-depth responses of the authors. I will keep my score.

Strengths

The paper is well-written and easy to follow. The structure is excellent, interleaving some experiments to motivate some choices. The problem of interpretability of learned rules is important and often overlooked in these logic-inspired architectures. I do not believe SATNet has been studied in this context before. The paper presents interesting failure cases of SATNet. The symbolic background knowledge injection through compiling inside matrix $C$ is a very useful result, increasing the model's applicability.

Weaknesses

I have some questions about the theoretical ideas presented in the paper, particularly on the limitations of SATNet. The experiments are somewhat simple and could be presented more clearly or on more tasks (for instance, on ILP benchmarks like in $\partial$ILP [1]). - The experiments could be a lot clearer with a table for the different tasks and the different evaluations. Ie, Compare SATNet and SATNet* as a continuous model and in the MaxSAT version. - The benefits of the maximum equality specification for interpretability are not entirely apparent to me (see questions). [1] Evans, R., & Grefenstette, E. (2018). Learning explanatory rules from noisy data. Journal of Artificial Intelligence Research, 61, 1-64.

Questions

- Limitations of $S$ (p4, 145-155): The matrix given does not represent parity / XOR. I think coordinate (3, 4) should be a -1 (ie the last row is -1 -1 -1). Otherwise the (correct) input $110$ is rejected. On this corrected matrix $S$, I computed $S^T S$ and did not get a zero matrix as claimed but a diagonal matrix ($4 I$ in particular). This is not due to the correction, as $S_\top^T S_\top = 4$, so coordinate (1, 1) is necessarily 4. - Same part: The claim is that since $S^T S$ collapses, SATNet cannot theoretically represent a range of logical rules. I think this claim should be made a bit stronger: What (I think) you want to show is that two non-semantically equivalent CNF formulas map to the same $S^T S$. For instance, is there another problem than parity for which $S^T S$ equals $4 I$? - Have you tried interpreting the matrix $S$ instead when using the sparsification procedure? Instead of the MaxSAT procedure? Would that be worse than the MaxSAT interpretation? - Experiments: What exactly makes SATNet* different from SATNet? The sparsification? - 348: Why is SATNet* not evaluated on 9x9 sudokus?

Rating

6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

2 fair

Presentation

4 excellent

Contribution

3 good

Limitations

While the authors developed a sparsification method, the MaxSAT problem will likely be huge and hard to interpret or verify. The verification part of this limitation is mentioned, not the interpretability. The verification method amounts to enumerating IO Pairs. I would have hoped the interpretable rules would allow symbolic reasoning to prove equivalence. The authors argue this is impossible because it would require a transformation of SAT into MaxSAT (or vice-versa).

Summary

This paper builds on SATNet, a differentiable MaxSMT solver that was proposed in the past to learn logical rules from input-output examples. SANet is based on a "low rank semidefinite programming approach" and uses a learnable matrix S to capture the logical rules. SATNet was shown to learn to solve e.g. Sudoku puzzles with near perfect accuracy. The problem addressed in this paper is that the S matrix and the learned weights in SATNet lack a clear, logical meaning. The authors first describe a set of (failed) experiments that aim to extract the meaning from S. Then they describe a new formulation called maximum equality which enables them to formulate MaxSMT formulas that can be solved with off-the-shelf solvers. The authors demonstrate both theoretically and empirically that this new formulation indeed captures the underlying logical rules; it also opens up the possibility of new applications, such as adding domain specific constraints to a problem

Strengths

* The paper is very well written. It provides a gentle introduction to teh problem and a clear running example to illustrate the technique. * The paper makes a clear contribution over the previous SATNet approach.The proposed approach is very interesting and has many practical applications. * The novelty is not only in the "decoding" but also in teh functional comparison between the decoded rules and teh ground truth.

Weaknesses

none

Questions

none

Rating

7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.

Confidence

2: You are willing to defend your assessment, but it is quite likely that you did not understand the central parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.

Soundness

3 good

Presentation

3 good

Contribution

3 good

Limitations

The paper describes carefully the limitations of the proposed approach.

Summary

The work investigates the problem of generating interpretable and verifiable logical rules through differential learning. Specifically, a deep network layer for satisfiability solving (SATNet) in a differentiable maximum satisfiability (MAXSAT) solver that learns logical rules from input-output examples was used. Through experiments, the authors claim that the learned weights in SATNet lack explainability. To address this issue, a method called maximum equality is proposed to interpretate the weights of SATNet into a set of propositional logical rules. Stream transformations and Sudoku problems were taken as the tasks to evaluate the method. Post rebuttal: I have read the authors' rebuttal and I appreciate the authors' effort in addressing my concerns. I agree with the authors' point on interpretable logical rules in the rebuttal. My concerns on the application of the proposed methods to models beyond SATNet and other more complex tasks still hold.

Strengths

+The work proposes a method called maximum equality to interpretate the weights of SATNet into a set of propositional logical rules to improve the explainability of SATNet. +The method was evaluated on the Stream transformations and Sudoku tasks and the results show that decoded rules from the maximum equality method are better than the ones out of the original SATNet. +To a certain extent, it improves the explainability of learned logical rules from input-output examples.

Weaknesses

-The work builds upon a specific satisfiability solving method (SATNet), which limits the impact of the work. -It is claimed that the lack of interpretation of SATNet was due to that the clause matrixS is not enforced as ternary and a method of rounding S to a ternary matrix didn't yield correct logical rules. However, it would be interesting to investigate how to interpretate S through a learnable network or another approach. -The matrix C = S^T S is decomposed, and the objective of maximum equality is to minimize the similarity between each pair of variable vectors of S. A weight c_{ij} is associated with the similarity between each pair of variable vectors. It is not clear how c_{ij} will affect the generated logical rules. -The work relies on the prior work SATNet and a few terms are not explained, which hinders understanding the work. For example, SATNet - satisfiability solving network; MaxSAT - maximum satisfiability (MAXSAT) solver. -In Eq. 2 and Eq. 3, mimimize -> minimize

Questions

-Would it be feasible to use a deep neural network to interpret S of SATNet? -Is c_{ij} predefined or learnable? -How is an appropriate value set for n_a? -The visual Sudoku problem was used in the SATNet work, have you tested your maximum equality method on this task as well?

Rating

4: Borderline reject: Technically solid paper where reasons to reject, e.g., limited evaluation, outweigh reasons to accept, e.g., good evaluation. Please use sparingly.

Confidence

3: You are fairly confident in your assessment. It is possible that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.

Soundness

3 good

Presentation

2 fair

Contribution

2 fair

Limitations

The authors have mentioned the limitation of this work in only learning propositional logical rules and not being able to handle rules in first-order or higher-order logic.

Rebuttal acknowledged

I thank the authors for their replies.