HackerPapers

arXiv:1608.02644cs.AI

Holophrasm: a neural Automated Theorem Prover for higher-order logic

Daniel Whalen

Abstract

I propose a system for Automated Theorem Proving in higher order logic using deep learning and eschewing hand-constructed features. Holophrasm exploits the formalism of the Metamath language and explores partial proof trees using a neural-network-augmented bandit algorithm and a sequence-to-sequence model for action enumeration. The system proves 14% of its test theorems from Metamath's set.mm module.

arXiv comments
9 pages, 1 figure
Journal reference
DOI
Subjects
cs.AIArtificial Intelligence cs.LOLogic in Computer Science

On Hacker News

Linked by 2 identifiable commenters in 3 comments across 3 threads, from Aug 2019 to Dec 2022.

Comments linking this paper, per year.

Discussed in comments3 threads

  1. Introduction to Homotopy Type Theory 1 comment

    • Do not nerd snipe me! There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's able to check the entire Metamath proof database in a few hundred milliseconds. This is orders of magnitude faster than…

      raphlinusView on HNParent context

  2. Number theorist fears many proofs widely considered to be true are wrong 1 comment

    • It's not really like that. NN's are only used when searching for new proofs or steps which can be used to fill in details, the verification of a finished proof is done by a classical program by a series of substitutions which are very straightforward and spelled out in detail.…

      drchewbaccaView on HNParent context

  3. Learning to prove theorems via interacting with proof assistants 1 comment

    • And another https://arxiv.org/pdf/1608.02644.pdf I'd really love to see someone like Deepmind get a hold of this. They are perfectly placed to apply a lot of resources to it and it's right in their wheelhouse. Don't know how to contact them about it though.

      drchewbaccaView on HNParent context

Submitted to Hacker News

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