Hammering Mizar by Learning Clause Guidance

2 April 2019

Papers citing "Hammering Mizar by Learning Clause Guidance"

27 / 27 papers shown

Title
Efficient Neural Clause-Selection Reinforcement Martin Suda 97 0 0 10 Mar 2025
Learning Conjecturing from Scratch Thibault Gauthier J. Urban LRM 80 1 0 03 Mar 2025
Machine Learning for Quantifier Selection in cvc5 Jan Jakubův Mikoláš Janota Jelle Piepenbrock Josef Urban 61 0 0 26 Aug 2024
Solving Hard Mizar Problems with Instantiation and Strategy Invention Jan Jakubuv Mikoláš Janota Josef Urban 66 0 0 25 Jun 2024
A Survey on Deep Learning for Theorem Proving Zhaoyu Li Jialiang Sun Logan Murphy Qidong Su Zenan Li Xian Zhang Kaiyu Yang Xujie Si LRM 123 32 0 15 Apr 2024
Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek David M. Cerna Thibault Gauthier Jan Jakubruv C. Kaliszyk Martin Suda Josef Urban LRM 93 5 0 06 Mar 2024
Translating SUMO-K to Higher-Order Set Theory C. Brown A. Pease Josef Urban LRM 50 2 0 13 May 2023
MizAR 60 for Mizar 50 Jan Jakubruv Karel Chvalovský Z. Goertzel C. Kaliszyk Mirek Olvsák Bartosz Piotrowski S. Schulz Martin Suda Josef Urban 82 13 0 12 Mar 2023
Alien Coding Thibault Gauthier Miroslav Olsák J. Urban 72 8 0 27 Jan 2023
The Isabelle ENIGMA Z. Goertzel Jan Jakubruv C. Kaliszyk Miroslav Olvsák Jelle Piepenbrock Josef Urban AIMat 44 13 0 04 May 2022
Proving Theorems using Incremental Learning and Hindsight Experience Replay Eser Aygun Laurent Orseau Ankit Anand Xavier Glorot Vlad Firoiu Lei M. Zhang Doina Precup Shibl Mourad CLL LRM 104 18 0 20 Dec 2021
Learning Theorem Proving Components Karel Chvalovský Jan Jakubuv Miroslav Olsák Josef Urban LRM 51 8 0 21 Jul 2021
Fast and Slow Enigmas and Parental Guidance Z. Goertzel Karel Chvalovský Jan Jakubuv Miroslav Olsák Josef Urban 78 11 0 14 Jul 2021
Learning to Guide a Saturation-Based Theorem Prover Ibrahim Abdelaziz Mayank Agarwal B. Makni Vernon Austil Cristina Cornelio ... Pavan Kapanipathi Ndivhuwo Makondo Kavitha Srinivas Michael Witbrock Achille Fokoue 54 17 0 07 Jun 2021
The Role of Entropy in Guiding a Connection Prover Zsolt Zombori Josef Urban Miroslav Olsák 64 11 0 31 May 2021
Improving ENIGMA-Style Clause Selection While Learning From History Martin Suda 45 1 0 26 Feb 2021
Proof Artifact Co-training for Theorem Proving with Language Models Jesse Michael Han Jason M. Rute Yuhuai Wu Edward W. Ayers Stanislas Polu AIMat 117 127 0 11 Feb 2021
Vampire With a Brain Is a Good ITP Hammer Martin Suda 71 12 0 06 Feb 2021
Make E Smart Again Z. Goertzel 44 6 0 19 Apr 2020
Prolog Technology Reinforcement Learning Prover Zsolt Zombori Josef Urban C. Brown OffRL 58 14 0 15 Apr 2020
Learning to Prove Theorems by Learning to Generate Theorems Mingzhe Wang Jia Deng NAI 132 50 0 17 Feb 2020
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) Jan Jakubuv Karel Chvalovský Miroslav Olsák Bartosz Piotrowski Martin Suda Josef Urban 65 44 0 13 Feb 2020
Property Invariant Embedding for Automated Reasoning Miroslav Olsák C. Kaliszyk Josef Urban NAI 66 41 0 27 Nov 2019
A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving Mayank Agarwal Ibrahim Abdelaziz B. Makni Spencer Whitehead Cristina Cornelio Pavan Kapanipathi Kavitha Srinivas Veronika Thost Michael Witbrock Achille Fokoue LRM 83 10 0 05 Nov 2019
Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic Thibault Gauthier 51 13 0 25 Oct 2019
Towards Finding Longer Proofs Zsolt Zombori Adrián Csiszárik Henryk Michalewski C. Kaliszyk Josef Urban OffRL LRM 83 16 0 30 May 2019
ENIGMAWatch: ProofWatch Meets ENIGMA Z. Goertzel Jan Jakubuv Josef Urban 59 16 0 23 May 2019