Author name cluster

Markus N. Rabe

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

13 papers

2 author rows

ICLR Conference 2022 Conference Paper

Memorizing Transformers

Yuhuai Wu
Markus N. Rabe
DeLesley Hutchins
Christian Szegedy

Language models typically need to be trained or finetuned in order to acquire new knowledge, which involves updating their weights. We instead envision language models that can simply read and memorize new data at inference time, thus acquiring new knowledge immediately. In this work, we extend language models with the ability to memorize the internal representations of past inputs. We demonstrate that an approximate $k$NN lookup into a non-differentiable memory of recent (key, value) pairs improves language modeling across various benchmarks and tasks, including generic webtext (C4), math papers (arXiv), books (PG-19), code (Github), as well as formal theorems (Isabelle). We show that the performance steadily improves when we increase the size of memory up to 262K tokens. On benchmarks including code and mathematics, we find that the model is capable of making use of newly defined functions and theorems during test time.

Details

ICML Conference 2021 Conference Paper

LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning

Yuhuai Wu
Markus N. Rabe
Wenda Li
Jimmy Ba
Roger B. Grosse
Christian Szegedy

While designing inductive bias in neural architectures has been widely studied, we hypothesize that transformer networks are flexible enough to learn inductive bias from suitable generic tasks. Here, we replace architecture engineering by encoding inductive bias in the form of datasets. Inspired by Peirce’s view that deduction, induction, and abduction are the primitives of reasoning, we design three synthetic tasks that are intended to require the model to have these three abilities. We specifically design these tasks to be synthetic and devoid of mathematical knowledge to ensure that only the fundamental reasoning biases can be learned from these tasks. This defines a new pre-training methodology called "LIME" (Learning Inductive bias for Mathematical rEasoning). Models trained with LIME significantly outperform vanilla transformers on four very different large mathematical reasoning benchmarks. Unlike dominating the computation cost as traditional pre-training approaches, LIME requires only a small fraction of the computation cost of the typical downstream task. The code for generating LIME tasks is available at https: //github. com/tonywu95/LIME.

Details

ICLR Conference 2021 Conference Paper

Mathematical Reasoning via Self-supervised Skip-tree Training

Markus N. Rabe
Dennis Lee 0003
Kshitij Bansal
Christian Szegedy

We demonstrate that self-supervised language modeling applied to mathematical formulas enables logical reasoning. To measure the logical reasoning abilities of language models, we formulate several evaluation (downstream) tasks, such as inferring types, suggesting missing assumptions and completing equalities. For training language models for formal mathematics, we propose a novel skip-tree task. We find that models trained on the skip-tree task show surprisingly strong mathematical reasoning abilities, and outperform models trained on standard skip-sequence tasks. We also analyze the models' ability to formulate new conjectures by measuring how often the predictions are provable and useful in other proofs.

Details

ICLR Conference 2021 Conference Paper

Teaching Temporal Logics to Neural Networks

Christopher Hahn
Frederik Schmitt
Jens U. Kreber
Markus N. Rabe
Bernd Finkbeiner

We study two fundamental questions in neuro-symbolic computing: can deep learning tackle challenging problems in logics end-to-end, and can neural networks learn the semantics of logics. In this work we focus on linear-time temporal logic (LTL), as it is widely used in verification. We train a Transformer on the problem to directly predict a solution, i.e. a trace, to a given LTL formula. The training data is generated with classical solvers, which, however, only provide one of many possible solutions to each formula. We demonstrate that it is sufficient to train on those particular solutions to formulas, and that Transformers can predict solutions even to formulas from benchmarks from the literature on which the classical solver timed out. Transformers also generalize to the semantics of the logics: while they often deviate from the solutions found by the classical solvers, they still predict correct solutions to most formulas.

Details

ICLR Conference 2020 Conference Paper

Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning

Gil Lederman
Markus N. Rabe
Sanjit A. Seshia
Edward A. Lee

We demonstrate how to learn efficient heuristics for automated reasoning algorithms for quantified Boolean formulas through deep reinforcement learning. We focus on a backtracking search algorithm, which can already solve formulas of impressive size - up to hundreds of thousands of variables. The main challenge is to find a representation of these formulas that lends itself to making predictions in a scalable way. For a family of challenging problems, we learned a heuristic that solves significantly more formulas compared to the existing handwritten heuristics.

Details

ICLR Conference 2020 Conference Paper

Mathematical Reasoning in Latent Space

Dennis Lee 0003
Christian Szegedy
Markus N. Rabe
Sarah M. Loos
Kshitij Bansal

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 rewrites (i.e. transformations) that can be successfully performed on a statement represents essential semantic features of the statement. We can compress this information by embedding the formula in a vector space, such that the vector associated with a statement can be used to predict whether a statement can be rewritten by other theorems. Predicting the embedding of a formula generated by some rewrite rule is naturally viewed as approximate reasoning in the latent space. In order to measure the effectiveness of this reasoning, we perform approximate deduction sequences in the latent space and use the resulting embedding to inform the semantic features of the corresponding formal statement (which is obtained by performing the corresponding rewrite sequence using real formulas). Our experiments show that graph neural networks can make non-trivial predictions about the rewrite-success of statements, even when they propagate predicted latent representations for several steps. Since our corpus of mathematical formulas includes a wide variety of mathematical disciplines, this experiment is a strong indicator for the feasibility of deduction in latent space in general.

Details

SAT Conference 2019 Conference Paper

Clausal Abstraction for DQBF

Leander Tentrup
Markus N. Rabe

Abstract Dependency quantified Boolean formulas (DQBF) is a logic admitting existential quantification over Boolean functions, which allows us to elegantly state synthesis problems in verification such as the search for invariants, programs, or winning regions of games. In this paper, we lift the clausal abstraction algorithm for quantified Boolean formulas (QBF) to DQBF. Clausal abstraction for QBF is an abstraction refinement algorithm that operates on a sequence of abstractions that represent the different quantifier levels. For DQBF we need to generalize this principle to partial orders of abstractions. The two challenges to overcome are: (1) Clauses may contain literals with incomparable dependencies, which we address by the recently proposed proof rule called Fork Extension, and (2) existential variables may have spurious dependencies, which we prevent by tracking consistency requirements during the execution. Our implementation $\textsc {dCAQE}$ solves significantly more formulas than the existing DQBF algorithms.

Details

ICML Conference 2019 Conference Paper

HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving

Kshitij Bansal
Sarah M. Loos
Markus N. Rabe
Christian Szegedy
Stewart Wilcox

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 arbitrary mathematical theories and thereby present an interesting challenge for deep learning. We provide an open-source framework based on the HOL Light theorem prover that can be used as a reinforcement learning environment. HOL Light comes with a broad coverage of basic mathematical theorems on calculus and the formal proof of the Kepler conjecture, from which we derive a challenging benchmark for automated reasoning approaches. We also present a deep reinforcement learning driven automated theorem prover, DeepHOL, that gives strong initial results on this benchmark.

Details

SAT Conference 2017 Conference Paper

A Resolution-Style Proof System for DQBF

Markus N. Rabe

Abstract This paper presents a sound and complete proof system for Dependency Quantified Boolean Formulas (DQBF) using resolution, universal reduction, and a new proof rule that we call fork extension. This opens new avenues for the development of efficient algorithms for DQBF.

Details

I&C Journal 2016 Journal Article

Efficient approximation of optimal control for continuous-time Markov games

John Fearnley
Markus N. Rabe
Sven Schewe
Lijun Zhang

We study the time-bounded reachability problem for continuous-time Markov decision processes (CTMDPs) and games (CTMGs). Existing techniques for this problem use discretisation techniques to partition time into discrete intervals of size ε, and optimal control is approximated for each interval separately. Current techniques provide an accuracy of O ( ε 2 ) on each interval, which leads to an infeasibly large number of intervals. We propose a sequence of approximations that achieve accuracies of O ( ε 3 ), O ( ε 4 ), and O ( ε 5 ), that allow us to drastically reduce the number of intervals that are considered. For CTMDPs, the performance of the resulting algorithms is comparable to the heuristic approach given by Buchholz and Schulz, while also being theoretically justified. All of our results generalise to CTMGs, where our results yield the first practically implementable algorithms for this problem. We also provide memoryless strategies for both players that achieve similar error bounds.

Details DOI

SAT Conference 2016 Conference Paper

Incremental Determinization

Markus N. Rabe
Sanjit A. Seshia

Abstract We present a novel approach to solve quantified boolean formulas with one quantifier alternation (2QBF). The algorithm incrementally adds new constraints to the formula until the constraints describe a unique Skolem function - or until the absence of a Skolem function is detected. Backtracking is required if the absence of Skolem functions depends on the newly introduced constraints. We present the algorithm in analogy to search algorithms for SAT and explain how propagation, decisions, and conflicts are lifted from values to Skolem functions. The algorithm improves over the state of the art in terms of the number of solved instances, solving time, and the size of the certificates.

Details

Highlights Conference 2014 Conference Abstract

The Linear-Hyper-Branching Spectrum of Temporal Logics

Markus N. Rabe

The family of temporal logics has recently been extended with logics for the specification of hyperproperties, such as noninterference or observational determinism. Hyperproperties relate multiple execution traces of a system by requiring that they satisfy a certain relationship, such as an identical valuation of the low-security outputs. Unlike classic temporal logics like LTL or CTL*, which refer to one execution trace at a time, temporal logics for hyperproperties like HyperLTL and HyperCTL* can express such relationships by explicitly quantifying over multiple execution traces simultaneously. In this talk, we study the extended spectrum of temporal logics by relating the new logics to the linear-branching spectrum of process equivalences.

PDF Details

TCS Journal 2013 Journal Article

Optimal time-abstract schedulers for CTMDPs and continuous-time Markov games

Markus N. Rabe
Sven Schewe

We study time-bounded reachability in continuous-time Markov decision processes (CTMDPs) and games (CTGs) for time-abstract scheduler classes. Reachability problems play a paramount rôle in probabilistic model checking. Consequently, their analysis has been studied intensively, and approximation techniques are well understood. From a mathematical point of view, however, the question of approximation is secondary compared to the fundamental question whether or not optimal control exists. In this article, we demonstrate the existence of optimal schedulers for the time-abstract scheduler classes for CTMDPs. For CTGs, we distinguish two cases: the simple case where both players face the same restriction to use time-abstract strategies (symmetric CTGs) and the case where one player is a completely informed adversary (asymmetric CTGs). While for the former case optimal strategies exist, we prove that for asymmetric CTGs there is not necessarily a scheduler that attains the optimum. It turns out that for CTMDPs and symmetric CTGs optimal time-abstract schedulers have an amazingly simple structure: they converge to a memoryless scheduling policy after a finite number of steps. This allows us to compute time-abstract strategies with finite memory.

Details DOI