Deep Network Guided Proof Search

DOI10.29007/8mwczbMath1403.68197arXiv1701.06972OpenAlexW2963376030WikidataQ108482125 ScholiaQ108482125MaRDI QIDQ4645728

Sarah M. Loos, Cezary Kaliszyk, Christian Szegedy, Geoffrey Irving

Publication date: 10 January 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1701.06972

zbMATH Keywords

theorem provingfirst-order logicdeep learning

Mathematics Subject Classification ID

Related Items (14)

Improving stateful premise selection with transformers ⋮ Fast and slow enigmas and parental guidance ⋮ Vampire with a brain is a good ITP hammer ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Prolog Technology Reinforcement Learning Prover ⋮ Towards finding longer proofs ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ The role of entropy in guiding a connection prover ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper). ⋮ Machine learning guidance for connection tableaux ⋮ Towards the automatic mathematician ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)

Uses Software

• MPTP 0.2
• TPTP
• Mizar
• Satallax
• TensorFlow
• seL4
• FEMaLeCoP
• Adam
• Holophrasm

Cites Work

• Mizar

This page was built for publication: Deep Network Guided Proof Search