4 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…
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…
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…
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…