2 citations · 2 across the 2 of their papers we have counts for
4 papers
First Experiments with Neural cvc5
Jelle Piepenbrock, Mikoláš Janota, Jan Jakubův
he cvc5 solver is today one of the strongest systems for solving first order problems with theories but also without them. In this work we equip its enumeration-based instantiation…
Machine Learning Meets The Herbrand Universe
Jelle Piepenbrock, Josef Urban, Konstantin Korovin +3
The appearance of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is thus to apply SAT sol…
The Isabelle ENIGMA
Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk +3
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In parti…
Learning Equational Theorem Proving
Jelle Piepenbrock, Tom Heskes, Mikoláš Janota +1
We develop Stratified Shortest Solution Imitation Learning (3SIL) to learn equational theorem proving in a deep reinforcement learning (RL) setting. The self-trained models achieve…