Kshitij Bansal
Kshitij works in the areas of machine learning, automated reasoning, and formal methods.
Research Areas
Authored Publications
Sort By
Preview abstract
This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem provers allow for the formalization of most mathematical theories and have been shown to pose a significant challenge for deep learning. Higher-order logic is highly expressive and, even though it is well-structured with a clearly defined grammar and semantics, there still remains no well-established method to convert formulas into graph-based representations. In this paper, we consider several graphical representations of higher-order logic and evaluate them against the HOList benchmark for higher-order theorem proving.
View details
Preview abstract
We study the feasibility of performing reasoning steps in higher order logic purely in latent space of fixed dimension.
We fix a class of rewrite rules in higher-order logic that can succeed or fail, and if they succeed, they produce a new mathematical expression.
We train graph neural networks to predict the success of rewrite rules and the latent representation of the resulting mathematical formula in case the rewrite is successful.
To study multi-step reasoning in latent space we then feed the predicted latent representations back into the neural network and study how well it predicts the success of rewrite rules without seeing the actual mathematical formula that resulted from the rewrite.
Our experimental findings are that neural networks can make non-trivial predictions about the rewrite-success, even when they only see the predicted latent representations for several steps.
Since our corpus of mathematical formulas includes a wide variety of mathematical disciplines, this experiment is a strong indicator for the feasibility of deduction in latent space.
View details
HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving
Sarah Loos
Markus Rabe
Christian Szegedy
Stewart James Wilcox
Thirty-sixth International Conference on Machine Learning (ICML) (2019) (to appear)
Preview abstract
We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and thereby present an interesting, open-ended challenge for deep learning. We provide an open-source framework based on the HOL Light theorem prover that can be used as a reinforcement learning environment. HOL Light comes with a broad coverage of basic mathematical theorems on calculus and the formal proof of the Kepler conjecture, from which we derive a challenging benchmark for automated reasoning. We also present a deep reinforcement learning driven automated theorem prover, DeepHOL, with strong initial results on this benchmark.
View details
A new decision procedure for finite sets and cardinality constraints in SMT
Andrew Reynolds
Cesare Tinelli
Clark Barrett
Logical Methods in Computer Science, Volume 14, Issue 4 (2018)
Preview abstract
We consider the problem of deciding the satisfiability of quantifier-free for- mulas in theory of finite sets with cardinality constraints. Sets are a common high-level data structure used in programming; thus, such a theory is useful for modeling program constructs directly. More importantly, sets are a basic construct of mathematics and thus natural to use when formalizing the properties of computational systems. We develop a calculus describing a modular combination of a procedure for reasoning about member- ship constraints with a procedure for reasoning about cardinality constraints. Cardinality reasoning involves tracking how different sets overlap. For efficiency, we avoid considering Venn regions directly, as done in previous work. Instead, we develop a novel technique wherein potentially overlapping regions are considered incrementally as needed. We use a graph to track the interaction among the different regions. The calculus has been designed to facilitate its implementation within SMT solvers based on the DPLL(T) architecture. Initial experimental results demonstrate that the new techniques are competitive with previous techniques and scale much better on certain classes of problems.
View details
