23 citations · 117 across the 10 of their papers we have counts for
11 papers
CodeGemma: Open Code Models Based on Gemma
CodeGemma Team, Heri Zhao, Jeffrey Hui +24
This paper introduces CodeGemma, a collection of specialized open code models built on top of Gemma, capable of a variety of code and natural language generation tasks. We release…
Mathematical Reasoning via Self-supervised Skip-tree Training
Markus N. Rabe, Dennis Lee, Kshitij Bansal +1
We examine whether self-supervised language modeling applied to mathematical formulas enables logical reasoning. We suggest several logical reasoning tasks that can be used to eval…
Reducing Commutativity Verification to Reachability with Differencing Abstractions
Eric Koskinen, Kshitij Bansal
Commutativity of data structure methods is of ongoing interest, with roots in the database community. In recent years commutativity has been shown to be a key ingredient to enablin…
Mathematical Reasoning in Latent Space
Dennis Lee, Christian Szegedy, Markus N. Rabe +2
We design and conduct a simple experiment to study whether neural networks can perform several steps of approximate reasoning in a fixed dimensional latent space. The set of rewrit…
Learning to Reason in Large Theories without Imitation
Kshitij Bansal, Christian Szegedy, Markus N. Rabe +2
In this paper, we demonstrate how to do automated theorem proving in the presence of a large knowledge base of potential premises without learning from human proofs. We suggest an…
Graph Representations for Higher-Order Logic and Theorem Proving
Aditya Paliwal, Sarah Loos, Markus Rabe +2
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.…
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe +2
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…
Automatic Generation of Precise and Useful Commutativity Conditions (Extended Version)
Kshitij Bansal, Eric Koskinen, Omer Tripp
Reasoning about commutativity between data-structure operations is an important problem with applications including parallelizing compilers, optimistic parallelization and, more re…
Reasoning with Finite Sets and Cardinality Constraints in SMT
Kshitij Bansal, Clark Barrett, Andrew Reynolds +1
We consider the problem of deciding the satisfiability of quantifier-free formulas in the theory of finite sets with cardinality constraints. Sets are a common high-level data stru…
On Deciding Local Theory Extensions via E-matching
Kshitij Bansal, Andrew Reynolds, Tim King +2
Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories of data types that commonly occur in software. This makes them important tools for automat…
A Note on the Complexity of Model-Checking Bounded Multi-Pushdown Systems
Kshitij Bansal, Stéphane Demri
In this note, we provide complexity characterizations of model checking multi-pushdown systems. Multi-pushdown systems model recursive concurrent programs in which any sequential p…