Kshitij Bansal

Email: mail@kshitij.io

I am currently working at Google on theorem proving and machine learning.

I did my PhD from New York University in Computer Science and was advised by Clark Barrett and Thomas Wies.

publications

Language Modeling for Formal Mathematics
Markus N. Rabe, Dennis Lee, Kshitij Bansal, Christian Szegedy
Preprint
Learning to Reason in Large Theories without Imitation
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy
Preprint
Mathematical Reasoning in Latent Space
Dennis Lee, Christian Szegedy, Markus Rabe, Sarah Loos, Kshitij Bansal
International Conference on Learning Representations (ICLR), 2020
Graph Representations for Higher-Order Logic and Theorem Proving
Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy
AAAI Conference on Artificial Intelligence, 2020
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox
International Conference on Machine Learning (ICML), 2019
[Website].
Reasoning with Finite Sets and Cardinality Constraints in SMT
Kshitij Bansal, Clark Barrett, Andrew Reynolds, Cesare Tinelli
Logical Methods in Computer Science, 2018
Automatic Generation of Precise and Useful Commutativity Conditions
Kshitij Bansal, Eric Koskinen, Omer Tripp
In Proceedings of TACAS, 2018.
[Tool], Evaluation [data].
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli
In Proceedings of IJCAR, 2016.
Deciding Local Theory Extensions via E-matching
Kshitij Bansal, Andrew Reynolds, Tim King,
Clark Barrett, and Thomas Wies
In Proceedings of CAV, 2015.
[Examples], Evaluation [data], [slides].
Eager and Lazy Approaches to Bit-vectors
Liana Hadarean, Kshitij Bansal, Dejan Jovanovic,
Clark Barrett, and Cesare Tinelli
In Proceedings of CAV, 2014.
Model Checking Bounded Multi-Pushdown Systems
Kshitij Bansal, Stephane Demri
In Proceedings of CSR, 2013.
Techincal report available at [arXiv]. [slides].
Structural Counter Abstraction
Kshitij Bansal, Eric Koskinen, Damien Zufferey, Thomas Wies
In Proceedings of TACAS, 2013.
Evaluation [data]. [slides].
Beyond Shapes: Lists with Ordered Data
Kshitij Bansal, Remi Brochenin, Etienne Lozes
In Proceedings of FoSSaCS, 2009.

projects

DeepHOL
An automated tactic-based neural theorem prover.
CVC4
A Satisfiability Modulo Theory (SMT) solver.
Servois
Automatically generating commutativity conditions from data-structure specifications.

articles

A branching heuristic
An article describing a branching heuristic implemented in CVC4.