DeepMath - Deep Sequence Models for Premise Selection

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F16%3A00311253" target="_blank" >RIV/68407700:21730/16:00311253 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

DeepMath - Deep Sequence Models for Premise Selection

Original language description

We study the effectiveness of neural sequence models for premise selection in automated theorem proving, a key bottleneck for progress in formalized 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 theorem proving on a large scale.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

R - Projekt Ramcoveho programu EK

Publication year

2016

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Advances in Neural Information Processing Systems 2016

ISBN

—

ISSN

1049-5258

e-ISSN

—

Number of pages

9

Pages from-to

2243-2251

Publisher name

Neural Information Processing Systems Foundation, Inc.

Place of publication

—

Event location

Barcelona

Event date

Dec 5, 2016

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—