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 MathematicsMarkus N. Rabe, Dennis Lee, Kshitij Bansal, Christian Szegedy

Preprint

Learning to Reason in Large Theories without ImitationKshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy

Preprint

Mathematical Reasoning in Latent SpaceDennis Lee, Christian Szegedy, Markus Rabe, Sarah Loos, Kshitij Bansal

International Conference on Learning Representations (ICLR), 2020

Graph Representations for Higher-Order Logic and Theorem ProvingAditya 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 ProvingKshitij 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 SMTKshitij Bansal, Clark Barrett, Andrew Reynolds, Cesare Tinelli

Logical Methods in Computer Science, 2018

Automatic Generation of Precise and Useful Commutativity ConditionsA New Decision Procedure for Finite Sets and Cardinality Constraints in SMTKshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli

In Proceedings of IJCAR, 2016.

Deciding Local Theory Extensions via E-matchingEager and Lazy Approaches to Bit-vectorsLiana Hadarean, Kshitij Bansal, Dejan Jovanovic,

Clark Barrett, and Cesare Tinelli

In Proceedings of CAV, 2014.

Model Checking Bounded Multi-Pushdown SystemsStructural Counter AbstractionBeyond Shapes: Lists with Ordered DataKshitij Bansal, Remi Brochenin, Etienne Lozes

In Proceedings of FoSSaCS, 2009.

projects

DeepHOLAn automated tactic-based neural theorem prover.CVC4A Satisfiability Modulo Theory (SMT) solver.ServoisAutomatically generating commutativity conditions from data-structure specifications.

articles

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