arXiv subjects

Michal Šustr

Publications and source records attributed to Michal Šustr.

6 recordsLinked to original sources

arXiv2025

LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4

Automated theorem proving (ATP) has been a classical problem in artificial intelligence since its inception, yet it remains challenging due to its vast state and action space. Large language models (LLMs) have recently emerged as a promising heuristic for ATP, but they lack correctness guarantees and thus require interaction with a proof verifier. Such interactions typically follow one of two approaches: black-box interaction, which does not utilize intermediate proof states, or white-box approaches, which allow for incremental proof construction and examination of intermediate states. While black-box approaches have directly benefited from recent LLM advances, white-box methods have comparatively lagged behind. In this paper, we address this gap by introducing LeanTree, which consists of (i) a tool built in the Lean 4 language that factorizes complex proof states into simpler, independent branches, and (ii) a dataset of these factorized intermediate states. Our white-box tooling offers several advantages over black-box approaches: it simplifies evaluation, reduces necessary context, generates richer training data, enables parallel search across multiple states, supports efficient reuse of states, and provides feedback in case of errors. Our preliminary results hint that white-box approaches outperform black-box alternatives in some settings.

cs.LG↗

arXiv2025

Meta-Learning in Self-Play Regret Minimization

Regret minimization is a general approach to online optimization which plays a crucial role in many algorithms for approximating Nash equilibria in two-player zero-sum games. The literature mainly focuses on solving individual games in isolation. However, in practice, players often encounter a distribution of similar but distinct games. For example, when trading correlated assets on the stock market, or when refining the strategy in subgames of a much larger game. Recently, offline meta-learning was used to accelerate one-sided equilibrium finding on such distributions. We build upon this, extending the framework to the more challenging self-play setting, which is the basis for most state-of-the-art equilibrium approximation algorithms for domains at scale. When selecting the strategy, our method uniquely integrates information across all decision states, promoting global communication as opposed to the traditional local regret decomposition. Empirical evaluation on normal-form games and river poker subgames shows our meta-learned algorithms considerably outperform other state-of-the-art regret minimization algorithms.

cs.GT↗

arXiv2024

Learning not to Regret

The literature on game-theoretic equilibrium finding predominantly focuses on single games or their repeated play. Nevertheless, numerous real-world scenarios feature playing a game sampled from a distribution of similar, but not identical games, such as playing poker with different public cards or trading correlated assets on the stock market. As these similar games feature similar equilibra, we investigate a way to accelerate equilibrium finding on such a distribution. We present a novel "learning not to regret" framework, enabling us to meta-learn a regret minimizer tailored to a specific distribution. Our key contribution, Neural Predictive Regret Matching, is uniquely meta-learned to converge rapidly for the chosen distribution of games, while having regret minimization guarantees on any game. We validated our algorithms' faster convergence on a distribution of river poker games. Our experiments show that the meta-learned algorithms outpace their non-meta-learned counterparts, achieving more than tenfold improvements.

cs.GT↗

arXiv2023

Revisiting Game Representations: The Hidden Costs of Efficiency in Sequential Decision-making Algorithms

Recent advancements in algorithms for sequential decision-making under imperfect information have shown remarkable success in large games such as limit- and no-limit poker. These algorithms traditionally formalize the games using the extensive-form game formalism, which, as we show, while theoretically sound, is memory-inefficient and computationally intensive in practice. To mitigate these challenges, a popular workaround involves using a specialized representation based on player specific information-state trees. However, as we show, this alternative significantly narrows the set of games that can be represented efficiently. In this study, we identify the set of large games on which modern algorithms have been benchmarked as being naturally represented by Sequential Bayesian Games. We elucidate the critical differences between extensive-form game and sequential Bayesian game representations, both theoretically and empirically. We further argue that the impressive experimental results often cited in the literature may be skewed, as they frequently stem from testing these algorithms only on this restricted class of games. By understanding these nuances, we aim to guide future research in developing more universally applicable and efficient algorithms for sequential decision-making under imperfect information.

cs.GT↗

arXiv2021

Sound Algorithms in Imperfect Information Games

Search has played a fundamental role in computer game research since the very beginning. And while online search has been commonly used in perfect information games such as Chess and Go, online search methods for imperfect information games have only been introduced relatively recently. This paper addresses the question of what is a sound online algorithm in an imperfect information setting of two-player zero-sum games. We argue that the~fixed-strategy~definitions of exploitability and $ε$-Nash equilibria are ill-suited to measure an online algorithm's worst-case performance. We thus formalize $ε$-soundness, a concept that connects the worst-case performance of an online algorithm to the performance of an $ε$-Nash equilibrium. As $ε$-soundness can be difficult to compute in general, we introduce a consistency framework -- a hierarchy that connects an online algorithm's behavior to a Nash equilibrium. These multiple levels of consistency describe in what sense an online algorithm plays "just like a fixed Nash equilibrium". These notions further illustrate the difference between perfect and imperfect information settings, as the same consistency guarantees have different worst-case online performance in perfect and imperfect information games. The definitions of soundness and the consistency hierarchy finally provide appropriate tools to analyze online algorithms in repeated imperfect information games. We thus inspect some of the previous online algorithms in a new light, bringing new insights into their worst-case performance guarantees.

cs.GT↗

arXiv2018

Multi-platform Version of StarCraft: Brood War in a Docker Container: Technical Report

We present a dockerized version of a real-time strategy game StarCraft: Brood War, commonly used as a domain for AI research, with a pre-installed collection of AI developement tools supporting all the major types of StarCraft bots. This provides a convenient way to deploy StarCraft AIs on numerous hosts at once and across multiple platforms despite limited OS support of StarCraft. In this technical report, we describe the design of our Docker images and present a few use cases.

cs.AI↗