Assessing SATNet's Ability to Solve the Symbol Grounding Problem

• URL: http://arxiv.org/abs/2312.11522v1
• Date: Wed, 13 Dec 2023 04:29:32 GMT
• Title: Assessing SATNet's Ability to Solve the Symbol Grounding Problem
• Authors: Oscar Chang, Lampros Flokas, Hod Lipson, Michael Spranger
• Abstract summary: SATNet is an award-winning MAXSAT solver that can be used to infer logical rules and integrated as a differentiable layer in a deep neural network. We show that in the absence of intermediate labels that identify individual Sudoku digit images with their logical representations, SATNet completely fails at visual Sudoku. We propose an MNIST based test as an easy instance of the symbol grounding problem that can serve as a sanity check for differentiable symbolic solvers in general.
• Score: 19.52506478494672
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: SATNet is an award-winning MAXSAT solver that can be used to infer logical rules and integrated as a differentiable layer in a deep neural network. It had been shown to solve Sudoku puzzles visually from examples of puzzle digit images, and was heralded as an impressive achievement towards the longstanding AI goal of combining pattern recognition with logical reasoning. In this paper, we clarify SATNet's capabilities by showing that in the absence of intermediate labels that identify individual Sudoku digit images with their logical representations, SATNet completely fails at visual Sudoku (0% test accuracy). More generally, the failure can be pinpointed to its inability to learn to assign symbols to perceptual phenomena, also known as the symbol grounding problem, which has long been thought to be a prerequisite for intelligent agents to perform real-world logical reasoning. We propose an MNIST based test as an easy instance of the symbol grounding problem that can serve as a sanity check for differentiable symbolic solvers in general. Naive applications of SATNet on this test lead to performance worse than that of models without logical reasoning capabilities. We report on the causes of SATNet's failure and how to prevent them.

Related papers

• LinSATNet: The Positive Linear Satisfiability Neural Networks [116.65291739666303]
  This paper studies how to introduce the popular positive linear satisfiability to neural networks. We propose the first differentiable satisfiability layer based on an extension of the classic Sinkhorn algorithm for jointly encoding multiple sets of marginal distributions.
  arXiv  Detail & Related papers  (2024-07-18T22:05:21Z)
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  We present GraSS, a novel approach for automatic SAT solver selection based on tripartite graph representations of instances. We enrich the graph representation with domain-specific decisions, such as novel node feature design. We demonstrate that this combination of raw representations and domain-specific choices leads to improvements in runtime.
  arXiv  Detail & Related papers  (2024-05-17T18:00:50Z)
• Learning Reliable Logical Rules with SATNet [7.951021955925275]
  We build on SATNet, a differentiable MaxSAT solver that learns the underlying rules from input-output examples. We 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.
  arXiv  Detail & Related papers  (2023-10-03T15:14:28Z)
• Efficient Symbolic Reasoning for Neural-Network Verification [48.384446430284676]
  We present a novel program reasoning framework for neural-network verification. The key components of our framework are the use of the symbolic domain and the quadratic relation. We believe that our framework can bring new theoretical insights and practical tools to verification problems for neural networks.
  arXiv  Detail & Related papers  (2023-03-23T18:08:11Z)
• Are Deep Neural Networks SMARTer than Second Graders? [85.60342335636341]
  We evaluate the abstraction, deduction, and generalization abilities of neural networks in solving visuo-linguistic puzzles designed for children in the 6--8 age group. Our dataset consists of 101 unique puzzles; each puzzle comprises a picture question, and their solution needs a mix of several elementary skills, including arithmetic, algebra, and spatial reasoning. Experiments reveal that while powerful deep models offer reasonable performances on puzzles in a supervised setting, they are not better than random accuracy when analyzed for generalization.
  arXiv  Detail & Related papers  (2022-12-20T04:33:32Z)
• Learning Symmetric Rules with SATNet [9.238700679836855]
  We present SymSATNet, a variant of SATNet that translates the given symmetries of the target rules to a condition on the parameters of SATNet. We also describe a technique for automatically discovering symmetries of the target rules from examples. Our experiments with Sudoku and Rubik's cube show the substantial improvement of SymSATNet over the baseline SATNet.
  arXiv  Detail & Related papers  (2022-06-28T13:36:34Z)
• Neural-Symbolic Solver for Math Word Problems with Auxiliary Tasks [130.70449023574537]
  Our NS-r consists of a problem reader to encode problems, a programmer to generate symbolic equations, and a symbolic executor to obtain answers. Along with target expression supervision, our solver is also optimized via 4 new auxiliary objectives to enforce different symbolic reasoning.
  arXiv  Detail & Related papers  (2021-07-03T13:14:58Z)
• Techniques for Symbol Grounding with SATNet [19.70820500506061]
  We present a self-supervised pre-training pipeline that enables SATNet to overcome the Symbol Grounding Problem. We demonstrate that our method allows SATNet to attain full accuracy even with a harder problem setup. We additionally introduce a proofreading method that further improves the performance of SATNet architectures.
  arXiv  Detail & Related papers  (2021-06-16T18:42:12Z)
• Goal-Aware Neural SAT Solver [2.609784101826762]
  Modern neural networks obtain information about the problem and calculate the output solely from the input values. We argue that it is not always optimal, and the network's performance can be significantly improved by augmenting it with a query mechanism. We propose a neural SAT solver with a query mechanism called QuerySAT and show that it outperforms the neural baseline on a wide range of SAT tasks.
  arXiv  Detail & Related papers  (2021-06-14T04:51:24Z)
• Machine Number Sense: A Dataset of Visual Arithmetic Problems for Abstract and Relational Reasoning [95.18337034090648]
  We propose a dataset, Machine Number Sense (MNS), consisting of visual arithmetic problems automatically generated using a grammar model--And-Or Graph (AOG) These visual arithmetic problems are in the form of geometric figures. We benchmark the MNS dataset using four predominant neural network models as baselines in this visual reasoning task.
  arXiv  Detail & Related papers  (2020-04-25T17:14:58Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.