118 citations · 344 across the 22 of their papers we have counts for
9 papers · 1 filter
Teaching Temporal Logics to Neural Networks
Christopher Hahn, Frederik Schmitt, Jens U. Kreber +2
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 l…
Understanding and Extending Incremental Determinization for 2QBF
Markus N. Rabe, Leander Tentrup, Cameron Rasmussen +1
Incremental determinization is a recently proposed algorithm for solving quantified Boolean formulas with one quantifier alternation. In this paper, we formalize incremental determ…
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…
A Model Counter's Guide to Probabilistic Systems
Marcell Vazquez-Chanlatte, Markus N. Rabe, Sanjit A. Seshia
In this paper, we systematize the modeling of probabilistic systems for the purpose of analyzing them with model counting techniques. Starting from unbiased coin flips, we show how…
Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning
Gil Lederman, Markus N. Rabe, Edward A. Lee +1
We demonstrate how to learn efficient heuristics for automated reasoning algorithms for quantified Boolean formulas through deep reinforcement learning. We focus on a backtracking…
Encodings of Bounded Synthesis
Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe +1
The reactive synthesis problem is to compute a system satisfying a given specification in temporal logic. Bounded synthesis is the approach to bound the maximum size of the system…
What's Decidable about Syntax-Guided Synthesis?
Benjamin Caulfield, Markus N. Rabe, Sanjit A. Seshia +1
Syntax-guided synthesis (SyGuS) is a recently proposed framework for program synthesis problems. The SyGuS problem is to find an expression or program generated by a given grammar…
Temporal Logics for Hyperproperties
Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini +3
Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths…
A Temporal Logic for Hyperproperties
Bernd Finkbeiner, Markus N. Rabe, César Sánchez
Hyperproperties, as introduced by Clarkson and Schneider, characterize the correctness of a computer program as a condition on its set of computation paths. Standard temporal logic…