21 citations · 29 across the 9 of their papers we have counts for
17 papers
Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA
Mikoláš Janota, Jan Jakubův
This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance…
Quantifier Instantiations: To Mimic or To Revolt?
Jan Jakubův, Mikoláš Janota
Quantified formulas pose a significant challenge for Satisfiability Modulo Theories (SMT) solvers due to their inherent undecidability. Existing instantiation techniques, such as e…
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…
Automated Strategy Invention for Confluence of Term Rewrite Systems
Liao Zhang, Fabian Mitterwallner, Jan Jakubuv +1
Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system propertie…
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…
Solving Hard Mizar Problems with Instantiation and Strategy Invention
Jan Jakubův, Mikoláš Janota, Josef Urban
In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75\% to above…
Learning Theorem Proving Components
Karel Chvalovský, Jan Jakubův, Miroslav Olšák +1
Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selectio…
Fast and Slow Enigmas and Parental Guidance
Zarathustra Goertzel, Karel Chvalovský, Jan Jakubův +2
We describe several additions to the ENIGMA system that guides clause selection in the E automated theorem prover. First, we significantly speed up its neural guidance by adding se…
First Neural Conjecturing Datasets and Experiments
Josef Urban, Jan Jakubův
We describe several datasets and first experiments with creating conjectures by neural methods. The datasets are based on the Mizar Mathematical Library processed in several forms…
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
Jan Jakubův, Karel Chvalovský, Miroslav Olšák +3
We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems…
ENIGMAWatch: ProofWatch Meets ENIGMA
Zarathustra Goertzel, Jan Jakubův, Josef Urban
In this work we describe a new learning-based proof guidance -- ENIGMAWatch -- for saturation-style first-order theorem provers. ENIGMAWatch combines two guiding approaches for the…
Hammering Mizar by Learning Clause Guidance
Jan Jakubův, Josef Urban
We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated…
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
Karel Chvalovský, Jan Jakubův, Martin Suda +1
We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. Unlike in the first ENIGMA implementation wh…
ProofWatch: Watchlist Guidance for Large Theories in E
Zarathustra Goertzel, Jan Jakubův, Stephan Schulz +1
Watchlist (also hint list) is a mechanism that allows related proofs to guide a proof search for a new conjecture. This mechanism has been used with the Otter and Prover9 theorem p…
ENIGMA: Efficient Learning-based Inference Guiding Machine
Jan Jakubův, Josef Urban
ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many proof searches are classified as positive and negative b…
BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Jan Jakubuv, Josef Urban
Inventing targeted proof search strategies for specific problem sets is a difficult task. State-of-the-art automated theorem provers (ATPs) such as E allow a large number of user-s…
Extending E Prover with Similarity Based Clause Selection Strategies
Jan Jakubův, Josef Urban
E prover is a state-of-the-art theorem prover for first-order logic with equality. E prover is built around a saturation loop, where new clauses are derived by inference rules from…