HackerPapers

arXiv:1606.04442cs.AI

DeepMath - Deep Sequence Models for Premise Selection

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 the first time deep learning has been applied to theorem proving on a large scale.

arXiv comments
Journal reference
DOI
Subjects
cs.AIArtificial Intelligence cs.LGMachine Learning cs.LOLogic in Computer Science

On Hacker News

Linked by 4 identifiable commenters in 4 comments across 4 threads, from Jul 2016 to Oct 2020. Found in 1 HN submission from Jul 2016 to Jul 2016. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments4 threads

  1. Neurosymbolic AI – Combining neural nets and symbolic AI 1 comment

    • IIRC these nets don't actually build a knowledge base (though I may be wrong, it's been a while). They're still functioning in lossy continuous space. This is probably fine with a low number of symbols and relations, but once you get to the level of a neural theorem prover you…

      popinman322View on HNParent context

  2. Summary of 'Programs with Common Sense' (1959) by John McCarthy 1 comment

    • This seems to be relevant for premise selection https://arxiv.org/pdf/1606.04442.pdf but not found anything yet on premise collection

      jackhoyView on HNParent context

  3. Tensorflow Deepmath: Experiments towards neural network theorem proving 1 comment

    • Check out the "Deepmath" paper linked above. (The paper is from a few months ago, the source code is new IIUC.) https://arxiv.org/abs/1606.04442

      danblickView on HNParent context

  4. Behind Wolfram Alpha’s Mathematical Induction-Based Proof Generator 1 comment

    • It seems kind of strange that he never thought of using computer proof systems for checking whether his proofs were right in class, and that he took a pattern-matching approach rather than using any of the existing AI proof-deriving systems like https://arxiv.org/abs/1606.04442…

      aab0View on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.