Showing 1–2 of 2 results for author: Een, N
-
DeepMath - Deep Sequence Models for Premise Selection
Authors:
Alex A. Alemi,
Francois Chollet,
Niklas Een,
Geoffrey Irving,
Christian Szegedy,
Josef Urban
Abstract:
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is t…
▽ More
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.
△ Less
Submitted 26 January, 2017; v1 submitted 14 June, 2016;
originally announced June 2016.
-
A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction
Authors:
Niklas Een,
Alan Mishchenko,
Nina Amla
Abstract:
This paper presents an efficient, combined formulation of two widely used abstraction methods for bit-level verification: counterexample-based abstraction (CBA) and proof-based abstraction (PBA). Unlike previous work, this new method is formulated as a single, incremental SAT-problem, interleaving CBA and PBA to develop the abstraction in a bottom-up fashion. It is argued that the new method is si…
▽ More
This paper presents an efficient, combined formulation of two widely used abstraction methods for bit-level verification: counterexample-based abstraction (CBA) and proof-based abstraction (PBA). Unlike previous work, this new method is formulated as a single, incremental SAT-problem, interleaving CBA and PBA to develop the abstraction in a bottom-up fashion. It is argued that the new method is simpler conceptually and implementation-wise than previous approaches. As an added bonus, proof-logging is not required for the PBA part, which allows for a wider set of SAT-solvers to be used.
△ Less
Submitted 11 August, 2010;
originally announced August 2010.
