Timezone: »

 
Spotlight Poster
Grounding Neural Inference with Satisfiability Modulo Theories
Zifan Wang · Saranya Vijayakumar · Kaiji Lu · Vijay Ganesh · Somesh Jha · Matt Fredrikson

Thu Dec 14 08:45 AM -- 10:45 AM (PST) @ Great Hall & Hall B1+B2 #505
in Poster Session 5 »

Recent techniques that integrate solver layers into Deep Neural Networks (DNNs) have shown promise in bridging a long-standing gap between inductive learning and symbolic reasoning techniques. In this paper we present a set of techniques for integrating Satisfiability Modulo Theories (SMT) solvers into the forward and backward passes of a deep network layer, called SMTLayer.Using this approach, one can encode rich domain knowledge into the network in the form of mathematical formulas.In the forward pass, the solver uses symbols produced by prior layers, along with these formulas, to construct inferences; in the backward pass, the solver informs updates to the network, driving it towards representations that are compatible with the solver's theory.Notably, the solver need not be differentiable. We implement SMTLayer as a Pytorch module, and our empirical results show that it leads to models that 1) require fewer training samples than conventional models, 2) that are robust to certain types of covariate shift, and 3) that ultimately learn representations that are consistent with symbolic knowledge, and thus naturally interpretable.

Author Information

Zifan Wang (Carnegie Mellon University)
Saranya Vijayakumar (Carnegie Mellon University)
Kaiji Lu (Carnegie Mellon University)
Vijay Ganesh (University of Waterloo)
Vijay Ganesh

Dr. Vijay Ganesh is an associate professor at the University of Waterloo and the Co-Director of the Waterloo Artificial Intelligence Institute. Prior to joining Waterloo in 2012, he was a research scientist at MIT (2007-2012) and completed his PhD in computer science from Stanford in 2007. Vijay's primary area of research is the theory and practice of SAT/SMT solvers aimed at AI, software engineering, security, mathematics, and physics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, Z3 string, MapleSAT, and MathCheck. He has also proved several decidability and complexity results in the context of first-order theories. He has won over 25 awards, honors, and medals to-date for his research, including an ACM Impact Paper Award at ISSTA 2019, ACM Test of Time Award at CCS 2016, and a Ten-Year Most Influential Paper citation at DATE 2008. He is the Editor-in-Chief of the Springer book series "Progress in Computer Science and Applied Logic" (PCSAL) and has co-chaired many conferences, workshops, and seminars including a Simons Institute semester @ Berkeley on Boolean Satisfiability in 2021.

Somesh Jha (University of Wisconsin, Madison)
Matt Fredrikson (CMU)

More from the Same Authors