research
∙
03/08/2023
Baldur: Whole-Proof Generation and Repair with Large Language Models
Formally verifying software properties is a highly desirable but labor-i...
share
research
∙
05/25/2022
Autoformalization with Large Language Models
Autoformalization is the process of automatically translating from natur...
research
∙
03/16/2022
Memorizing Transformers
Language models typically need to be trained or finetuned in order to ac...
research
∙
12/10/2021
Self-attention Does Not Need O(n^2) Memory
We present a very simple algorithm for attention that requires O(1) memo...
research
∙
07/25/2021
Neural Circuit Synthesis from Specification Patterns
We train hierarchical Transformers on the task of synthesizing hardware ...
research
∙
06/08/2020
Mathematical Reasoning via Self-supervised Skip-tree Training
We examine whether self-supervised language modeling applied to mathemat...
research
∙
03/06/2020
Teaching Temporal Logics to Neural Networks
We show that a deep neural network can learn the semantics of linear-tim...
research
∙
09/26/2019
Mathematical Reasoning in Latent Space
We design and conduct a simple experiment to study whether neural networ...
research
∙
05/31/2019
Understanding and Extending Incremental Determinization for 2QBF
Incremental determinization is a recently proposed algorithm for solving...
research
∙
05/25/2019
Learning to Reason in Large Theories without Imitation
Automated theorem proving in large theories can be learned via reinforce...
research
∙
04/05/2019
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version)
We present an environment, benchmark, and deep learning driven automated...
research
∙
04/05/2019
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
We present an environment, benchmark, and deep learning driven automated...
research
∙
03/22/2019
A Model Counter's Guide to Probabilistic Systems
In this paper, we systematize the modeling of probabilistic systems for ...
research
∙
08/27/2018
Synthesis of Boolean Functions with Clausal Abstraction
Dependency quantified Boolean formulas (DQBF) is a logic admitting exist...
research
∙
07/20/2018
Learning Heuristics for Automated Reasoning through Deep Reinforcement Learning
We demonstrate how to learn efficient heuristics for automated reasoning...
research
∙
03/26/2018