Name
Abstract | ||
|---|---|---|
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. |
Year | Venue | DocType |
|---|---|---|
2016 | NIPS | Conference |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Geoffrey Irving | 1 | 2101 | 78.49 |
| Christian Szegedy | 2 | 7278 | 292.63 |
| Alexander A. Alemi | 3 | 70 | 9.92 |
| Niklas Eén | 4 | 0 | 0.34 |
| François Chollet | 5 | 51 | 3.85 |
| Josef Urban | 6 | 635 | 46.75 |