Stateful Premise Selection by Recurrent Neural Networks
In this work, we develop a new learning-based method for selecting facts (premises) when proving new goals over large formal libraries. Unlike previous methods that choose sets of facts independently of each other by their rank, the new method uses the notion of \emph{state} that is updated each time a choice of a fact is made. Our stateful architecture is based on recurrent neural networks which have been recently very successful in stateful tasks such as language translation. The new method is combined with data augmentation techniques, evaluated in several ways on a standard large-theory benchmark, and compared to state-of-the-art premise approach based on gradient boosted trees. It is shown to perform significantly better and to solve many new problems.
Code (0)
등록된 구현이 없습니다.
Tasks
Data AugmentationTranslationSimilar Papers 제목 키워드 기반
Exploiting the ConvLSTM: Human Action Recognition using Raw Depth Video-Based Recurrent Neural Networks
As in many other different fields, deep learning has become the main approach in most computer vision applications, such as scene understanding, object recognition, computer-human interaction or human action recognition …
Action RecognitionObject RecognitionScene UnderstandingTemporal Action LocalizationComprehensive forecasting based analysis using stacked stateless and stateful Gated Recurrent Unit models
Photovoltaic power is a renewable source of energy which is highly used in industries. In economically struggling countries it can be a potential source of electric energy as other non-renewable resources are already exh…
Combining Textual and Structural Information for Premise Selection in Lean
Premise selection is a key bottleneck for scaling theorem proving in large formal libraries. Yet existing language-based methods often treat premises in isolation, ignoring the web of dependencies that connects them. We …
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. A good method for premise selection in complex mathematical libraries is the application of machine…
Mathematical ProofsDeepCruiser: Automated Guided Testing for Stateful Deep Learning Systems
Deep learning (DL) defines a data-driven programming paradigm that automatically composes the system decision logic from the training data. In company with the data explosion and hardware acceleration during the past dec…
Deep LearningSpeech-to-Text