Kshitij Bansal

Email: mail@kshitij.io

My research interests are in automated reasoning, machine learning, and formal methods.

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

projects

CodeGemma, Gemini, etc.
Large language models (for code)
DeepHOL
An automated tactic-based neural theorem prover.
CVC4
A Satisfiability Modulo Theory (SMT) solver.
Servois
Automatically generating commutativity conditions from data-structure specifications.

publications

Decomposing Data Structure Commutativity Proofs with mn-Differencing
Eric Koskinen, Kshitij Bansal
VMCAI (Verification, Model Checking, and Abstract Interpretation), 2021
Mathematical Reasoning via Self-supervised Skip-tree Training
Markus N. Rabe, Dennis Lee, Kshitij Bansal, Christian Szegedy
ICLR, 2021
Synthesizing Precise and Useful Commutativity Conditions
Kshitij Bansal, Eric Koskinen, Omer Tripp
Journal of Automated Reasoning (JAR), 2020
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.

articles

CodeGemma: Open Code Models Based on Gemma
with 25 others
Learning to Reason in Large Theories without Imitation
Kshitij Bansal, Christian Szegedy, Sarah M. Loos, Markus N. Rabe, and Viktor Toman
A branching heuristic
An article describing a branching heuristic implemented in CVC4.