2 citations · 4 across the 6 of their papers we have counts for
8 papers
OrLog: Resolving Complex Queries with LLMs and Probabilistic Reasoning
Mohanna Hoveyda, Jelle Piepenbrock, Arjen P de Vries +2
Resolving complex information needs that come with multiple constraints should consider enforcing the logical operators encoded in the query (i.e., conjunction, disjunction, negati…
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 for Quantifier Selection in cvc5
Jan Jakubův, Mikoláš Janota, Jelle Piepenbrock +1
In this work we considerably improve the state-of-the-art SMT solving on first-order quantified problems by efficient machine learning guidance of quantifier selection. Quantifiers…
Graph2Tac: Online Representation Learning of Formal Math Concepts
Lasse Blaauwbroek, Miroslav Olšák, Jason Rute +3
In proof assistants, the physical proximity between two formal mathematical concepts is a strong predictor of their mutual relevance. Furthermore, lemmas with close proximity regul…
Graph Neural Networks For Mapping Variables Between Programs -- Extended Version
Pedro Orvalho, Jelle Piepenbrock, Mikoláš Janota +1
Automated program analysis is a pivotal research domain in many areas of Computer Science -- Formal Methods and Artificial Intelligence, in particular. Due to the undecidability of…
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…