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)DeepHOLAn automated tactic-based neural theorem prover.CVC4A Satisfiability Modulo Theory (SMT) solver.ServoisAutomatically generating commutativity conditions from data-structure specifications.
publications
Decomposing Data Structure Commutativity Proofs with mn-DifferencingEric Koskinen, Kshitij Bansal
VMCAI (Verification, Model Checking, and Abstract Interpretation), 2021
Mathematical Reasoning via Self-supervised Skip-tree TrainingMarkus N. Rabe, Dennis Lee, Kshitij Bansal, Christian Szegedy
ICLR, 2021
Synthesizing Precise and Useful Commutativity ConditionsKshitij Bansal, Eric Koskinen, Omer Tripp
Journal of Automated Reasoning (JAR), 2020
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.
articles
CodeGemma: Open Code Models Based on Gemmawith 25 others
Learning to Reason in Large Theories without ImitationKshitij Bansal, Christian Szegedy, Sarah M. Loos, Markus N. Rabe, and Viktor Toman
A branching heuristicAn article describing a branching heuristic implemented in CVC4.