HackerPapers

arXiv:1611.05990cs.LO

Monte Carlo Tableau Proof Search

Michael Färber, Cezary Kaliszyk, Josef Urban

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

We study Monte Carlo Tree Search to guide proof search in tableau calculi. This includes proposing a number of proof-state evaluation heuristics, some of which are learnt from previous proofs. We present an implementation based on the leanCoP prover. The system is trained and evaluated on a large suite of related problems coming from the Mizar proof assistant, showing that it is capable to find new and different proofs.

arXiv comments
Journal reference
Proceedings of the 26th International Conference on Automated Deduction, CADE 2017
DOI
doi:10.1007/978-3-319-63046-5_34
Subjects
cs.LOLogic in Computer Science cs.AIArtificial Intelligence cs.LGMachine Learning

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Dec 2017 to Dec 2017.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Google's AlphaZero Beats Stockfish In 100-Game Match 1 comment

    • Quick, someone apply AlphaZero algorithm to this MCTS prover for math: https://arxiv.org/abs/1611.05990 I actually prefer "expert iteration" and "tree-policy target" term instead of "AlphaZero algorithm", because they emphasize what is novel about it among the entire system.…

      sanxiynView on HNParent context

Submitted to Hacker News

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