Author name cluster

Jan Jakubuv

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

2 author rows

IJCAI Conference 2025 Conference Paper

Automated Strategy Invention for Confluence of Term Rewrite Systems

Liao Zhang
Fabian Mitterwallner
Jan Jakubuv
Cezary Kaliszyk

Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system properties, automatic term rewriting tools work in an extensive parameter space. This complexity exceeds human capacity for parameter selection, motivating an investigation into automated strategy invention. In this paper, we focus on confluence of term rewrite systems, and apply AI techniques to invent strategies for automatic confluence proving. Moreover, we randomly generate a large dataset to analyze confluence for term rewrite systems. We improve the state-of-the-art automatic confluence prover CSI: When equipped with our invented strategies, it surpasses its human-designed strategies both on the augmented dataset and on the original human-created benchmark dataset ARI-COPS, proving/disproving the confluence of several term rewrite systems for which no automated proofs were known before.

PDF Details DOI

LPAR Conference 2024 Conference Paper

First Experiments with Neural cvc5

Jelle Piepenbrock
Mikolás Janota
Josef Urban
Jan Jakubuv

The 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 instan- tiation with a neural network that guides the choice of the quantified formulas and their instances. For that we develop a relatively fast graph neural network that repeatedly scores all available instantiation options with respect to the available formulas. The network runs directly on a CPU without the need for any special hardware. We train the neural guidance on a large set of proofs generated by the e-matching instantiation strategy and evaluate its performance on a set of previously unseen problems.

Details

ECAI Conference 2024 Conference Paper

Machine Learning for Quantifier Selection in cvc5

Jan Jakubuv
Mikolás Janota
Jelle Piepenbrock
Josef Urban

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 represent a significant challenge for SMT and are technically a source of undecidability. In our approach, we train an efficient machine learning model that informs the solver which quantifiers should be instantiated and which not. Each quantifier may be instantiated multiple times and the set of the active quantifiers changes as the solving progresses. Therefore, we invoke the ML predictor many times, during the whole run of the solver. To make this efficient, we use fast ML models based on gradient boosted decision trees. We integrate our approach into the state-of-the-art cvc5 SMT solver and show a considerable increase of the system’s holdout-set performance after training it on a large set of first-order problems collected from the Mizar Mathematical Library.

Details

LPAR Conference 2024 Conference Paper

Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery

Kristina Aleksandrova
Jan Jakubuv
Cezary Kaliszyk

While many of the state-of-art Automated Theorem Provers (ATP) like E and Vampire, were subject to extensive tuning of strategy schedules in the last decade, the classical ATP prover Prover9 has never been optimized in this direction. Both E and Vampire provide the user with an automatic mode to select good proof search strategies based on the properties of the input problem, while Prover9 provides by default only a relatively weak auto mode. Interestingly, Prover9 provides more varied means for proof control than its competitors. These means, however, must be manually investigated and that is possible only by experienced Prover9 users with a good understanding of how Prover9 works. In this paper, we investigate the possibilities of automatic configuration of Prover9 for user-specified benchmark problems. We employ the automated strategy invention system Grackle to generate Prover9 strategies with both basic and advanced proof search options which require sophisticated strategy space features for Grackle. We test the strategy invention on AIM train/test problem collection and we show that Prover9 can outperform both E and Vampire on these problems. To test the generality of our approach we train and evaluate strategies also on TPTP problems, showing that Prover9 can achieve reasonable complementarity with other ATPs.

Details

ICAPS Conference 2016 Conference Paper

Recursive Polynomial Reductions for Classical Planning

Jan Tozicka
Jan Jakubuv
Martin Svatos
Antonín Komenda

Reducing accidental complexity in planning problems is a well-established method for increasing efficiency of classical planning. Removal of superfluous facts and actions, and problem transformation by recursive macro actions are representatives of such methods working directly on input planning problems. Despite of its general applicability and thorough theoretical analysis, there is only a sparse amount of experimental results. In this paper, we adopt selected reduction methods from literature and amend them with a generalization-based reduction scheme and auxiliary reductions. We show that all presented reductions are polynomial in time to the size of an input problem. All reductions applied in a recursive manner produce only safe (solution preserving) abstractions of the problem, and they can implicitly represent exponentially long plans in a compact form. Experimentally, we validate efficiency of the presented reductions on the IPC benchmark set and show average 24% reduction over all problems. Additionally, we experimentally analyze the trade-off between increase of coverage and decrease of the plan quality.

Details

EUMAS Conference 2015 Conference Paper

From Public Plans to Global Solutions in Multiagent Planning

Jan Tozicka
Jan Jakubuv
Antonín Komenda

Abstract Multiagent planning addresses the problem of coordinated sequential decision making of a team of cooperative agents. One possible approach to multiagent planning, which proved to be very efficient in practice, is to find an acceptable public plan. The approach works in two stages. At first, a public plan acceptable to all the involved agents is computed. Then, in the second stage, the public solution is extended to a global solution by filling in internal information by every agent. In the recently proposed distributed multiagent planner, the winner of the Competition of Distributed Multiagent Planners (CoDMAP 2015), this principle was utilized, however with unnecessary use of combination of both public and internal information for extension of the public solution. In this work, we improve the planning algorithm by enhancements of the global solution reconstruction phase. We propose a new method of global solution reconstruction which increases efficiency by restriction to internal information. Additionally, we employ reduction techniques downsizing the input planning problem. Finally, we experimentally evaluate the resulting planner and prove its superiority when compared to the previous approach.

Details DOI

ECAI Conference 2014 Conference Paper

Generating Multi-Agent Plans by Distributed Intersection of Finite State Machines

Jan Tozicka
Jan Jakubuv
Antonín Komenda

Deterministic multi-agent planning described by MA-STRIPS formalism requires mixture of coordination and synthesis of local agents' plans. All agents' plans, as sequences of actions, can be implicitly described by an appropriate generative structure. Having all local plans of all participating agents described by such a structure and having a merged process of such structures, we can induce a global multi-agent plan by successive elimination of unfeasible combinations of local agents' plans.

Details