@inproceedings{19665, abstract = {As AI-based decision-makers increasingly influence human lives, it is a growing concern that their decisions may be unfair or biased with respect to people's protected attributes, such as gender and race. Most existing bias prevention measures provide probabilistic fairness guarantees in the long run, and it is possible that the decisions are biased on any decision sequence of fixed length. We introduce *fairness shielding*, where a symbolic decision-maker---the fairness shield---continuously monitors the sequence of decisions of another deployed black-box decision-maker, and makes interventions so that a given fairness criterion is met while the total intervention costs are minimized. We present four different algorithms for computing fairness shields, among which one guarantees fairness over fixed horizons, and three guarantee fairness periodically after fixed intervals. Given a distribution over future decisions and their intervention costs, our algorithms solve different instances of bounded-horizon optimal control problems with different levels of computational costs and optimality guarantees. Our empirical evaluation demonstrates the effectiveness of these shields in ensuring fairness while maintaining cost efficiency across various scenarios.}, author = {Cano Cordoba, Filip and Henzinger, Thomas A and Könighofer, Bettina and Kueffner, Konstantin and Mallik, Kaushik}, booktitle = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Philadelphia, PA, United States}, number = {15}, pages = {15659--15668}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Fairness shields: Safeguarding against biased decision makers}}, doi = {10.1609/aaai.v39i15.33719}, volume = {39}, year = {2025}, } @inproceedings{19666, abstract = {Markov decision processes (MDP) are a well-established model for sequential decision-making in the presence of probabilities. In *robust* MDP (RMDP), every action is associated with an *uncertainty set* of probability distributions, modelling that transition probabilities are not known precisely. Based on the known theoretical connection to stochastic games, we provide a framework for solving RMDPs that is generic, reliable, and efficient. It is *generic* both with respect to the model, allowing for a wide range of uncertainty sets, including but not limited to intervals, L1- or L2-balls, and polytopes; and with respect to the objective, including long-run average reward, undiscounted total reward, and stochastic shortest path. It is *reliable*, as our approach not only converges in the limit, but provides precision guarantees at any time during the computation. It is *efficient* because -- in contrast to state-of-the-art approaches -- it avoids explicitly constructing the underlying stochastic game. Consequently, our prototype implementation outperforms existing tools by several orders of magnitude and can solve RMDPs with a million states in under a minute.}, author = {Meggendorfer, Tobias and Weininger, Maximilian and Wienhöft, Patrick}, booktitle = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Philadelphia, PA, United States}, number = {25}, pages = {26631--26641}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Solving robust Markov decision processes: Generic, reliable, efficient}}, doi = {10.1609/aaai.v39i25.34865}, volume = {39}, year = {2025}, } @inproceedings{19667, abstract = {The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial intelligence, program analysis, etc. While there has been much work on checking satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck in the existing methods is a computationally expensive quantifier elimination step. In this work, we propose a novel method for efficient quantifier elimination in quantified LRA and NRA formulas. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. The key technical ingredient in our approach are Positivstellensätze theorems from algebraic geometry, which allow for an efficient manipulation of polynomial inequalities. Our method offers a range of appealing theoretical properties combined with a strong practical performance. On the theory side, our method is sound, semi-complete, and runs in subexponential time and polynomial space, as opposed to existing sound and complete quantifier elimination methods that run in doubly-exponential time and at least exponential space. On the practical side, our experiments show superior performance compared to state of the art SMT solvers in terms of the number of solved instances and runtime, both on LRA and on NRA benchmarks.}, author = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Karrabi, Mehrdad and Motwani, Harshit J. and Seeliger, Maximilian and Zikelic, Dorde}, booktitle = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Philadelphia, PA, United States}, number = {11}, pages = {11158--11166}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Quantified linear and polynomial arithmetic satisfiability via template-based skolemization}}, doi = {10.1609/aaai.v39i11.33213}, volume = {39}, year = {2025}, } @inproceedings{19668, abstract = {Learning-based methods provide a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. To ensure the satisfaction of a safety property, learning-based methods jointly learn a control policy together with a certificate function for the property. Popular examples include barrier functions for safety and Lyapunov functions for asymptotic stability. While there has been significant progress on learning-based control with certificate functions in the white-box setting, where the correctness of the certificate function can be formally verified, there has been little work on ensuring their reliability in the black-box setting where the system dynamics are unknown. In this work, we consider the problems of certifying and repairing neural network control policies and certificate functions in the black-box setting. We propose a novel framework that utilizes runtime monitoring to detect system behaviors that violate the property of interest under some initially trained neural network policy and certificate. These violating behaviors are used to extract new training data, that is used to re-train the neural network policy and the certificate function and to ultimately repair them. We demonstrate the effectiveness of our approach empirically by using it to repair and to boost the safety rate of neural network policies learned by a state-of-the-art method for learning-based control on two autonomous system control tasks.}, author = {Yu, Zhengqi and Zikelic, Dorde and Henzinger, Thomas A}, booktitle = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Philadelphia, PA, United States}, number = {25}, pages = {26409--26417}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Neural control and certificate repair via runtime monitoring}}, doi = {10.1609/aaai.v39i25.34840}, volume = {39}, year = {2025}, } @inproceedings{19669, abstract = {We consider a class of optimization problems defined by a system of linear equations with min and max operators. This class of optimization problems has been studied under restrictive conditions, such as, (C1) the halting or stability condition; (C2) the non-negative coefficients condition; (C3) the sum upto 1 condition; and (C4) the only min or only max operator condition. Several seminal results in the literature focus on special cases. For example, turn-based stochastic games correspond to conditions C2 and C3; and Markov decision process to conditions C2, C3, and C4. However, the systematic computational complexity study of all the cases has not been explored, which we address in this work. Some highlights of our results are: with conditions C2 and C4, and with conditions C3 and C4, the problem is NP-complete, whereas with condition C1 only, the problem is in UP intersects coUP. Finally, we establish the computational complexity of the decision problem of checking the respective conditions.}, author = {Chatterjee, Krishnendu and Luo, Ruichen and Saona Urmeneta, Raimundo J and Svoboda, Jakub}, booktitle = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, location = {Philadelphia, PA, United States}, number = {11}, pages = {11150--11157}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Linear equations with min and max operators: Computational complexity}}, doi = {10.1609/aaai.v39i11.33212}, volume = {39}, year = {2025}, } @article{19713, abstract = {Distributed optimization is the standard way of speeding up machine learning training, and most of the research in the area focuses on distributed first-order, gradient-based methods. Yet, there are settings where some computationally-bounded nodes may not be able to implement first-order, gradient-based optimization, while they could still contribute to joint optimization tasks. In this paper, we initiate the study of hybrid decentralized optimization, studying settings where nodes with zeroth-order and first-order optimization capabilities co-exist in a distributed system, and attempt to jointly solve an optimization task over some data distribution. We essentially show that, under reasonable parameter settings, such a system can not only withstand noisier zeroth-order agents but can even benefit from integrating such agents into the optimization process, rather than ignoring their information. At the core of our approach is a new analysis of distributed optimization with noisy and possibly-biased gradient estimators, which may be of independent interest. Our results hold for both convex and non-convex objectives. Experimental results on standard optimization tasks confirm our analysis, showing that hybrid first-zeroth order optimization can be practical, even when training deep neural networks.}, author = {Talaei, Shayan and Ansaripour, Matin and Nadiradze, Giorgi and Alistarh, Dan-Adrian}, issn = {2374-3468}, journal = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, number = {19}, pages = {20778--20786}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Hybrid decentralized optimization: Leveraging both first- and zeroth-order optimizers for faster convergence}}, doi = {10.1609/aaai.v39i19.34290}, volume = {39}, year = {2025}, } @inproceedings{15321, abstract = {Boolean Networks (BNs) are widely used as a modeling formalism in several domains, notably systems biology and computer science. A fundamental problem in BN analysis is the enumeration of trap spaces, which are hypercubes in the state space that cannot be escaped once entered. Several methods have been proposed for enumerating trap spaces, however they often suffer from scalability and efficiency issues, particularly for large and complex models. To our knowledge, the most efficient and recent methods for the trap space enumeration all rely on Answer Set Programming (ASP), which has been widely applied to the analysis of BNs. Motivated by these considerations, our work proposes a new method for enumerating trap spaces in BNs using ASP. We evaluate the method on a mix of 250+ real-world and 400+ randomly generated BNs, showing that it enables analysis of models beyond the capabilities of existing tools (namely pyboolnet, mpbn, trappist, and trapmvn).}, author = {Trinh, Giang and Benhamou, Belaid and Pastva, Samuel and Soliman, Sylvain}, booktitle = {Proceedings of the 38th AAAI Conference on Artificial Intelligence}, isbn = {1577358872}, issn = {2374-3468}, number = {9}, pages = {10714--10722}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Scalable enumeration of trap spaces in boolean networks via answer set programming}}, doi = {10.1609/aaai.v38i9.28943}, volume = {38}, year = {2024}, } @inproceedings{14830, abstract = {We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks.}, author = {Zikelic, Dorde and Lechner, Mathias and Henzinger, Thomas A and Chatterjee, Krishnendu}, booktitle = {Proceedings of the 37th AAAI Conference on Artificial Intelligence}, issn = {2374-3468}, keywords = {General Medicine}, location = {Washington, DC, United States}, number = {10}, pages = {11926--11935}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Learning control policies for stochastic systems with reach-avoid guarantees}}, doi = {10.1609/aaai.v37i10.26407}, volume = {37}, year = {2023}, } @article{12510, abstract = {We introduce a new statistical verification algorithm that formally quantifies the behavioral robustness of any time-continuous process formulated as a continuous-depth model. Our algorithm solves a set of global optimization (Go) problems over a given time horizon to construct a tight enclosure (Tube) of the set of all process executions starting from a ball of initial states. We call our algorithm GoTube. Through its construction, GoTube ensures that the bounding tube is conservative up to a desired probability and up to a desired tightness. GoTube is implemented in JAX and optimized to scale to complex continuous-depth neural network models. Compared to advanced reachability analysis tools for time-continuous neural networks, GoTube does not accumulate overapproximation errors between time steps and avoids the infamous wrapping effect inherent in symbolic techniques. We show that GoTube substantially outperforms state-of-the-art verification tools in terms of the size of the initial ball, speed, time-horizon, task completion, and scalability on a large set of experiments. GoTube is stable and sets the state-of-the-art in terms of its ability to scale to time horizons well beyond what has been previously possible.}, author = {Gruenbacher, Sophie A. and Lechner, Mathias and Hasani, Ramin and Rus, Daniela and Henzinger, Thomas A and Smolka, Scott A. and Grosu, Radu}, isbn = {978577358350}, issn = {2374-3468}, journal = {Proceedings of the AAAI Conference on Artificial Intelligence}, keywords = {General Medicine}, number = {6}, pages = {6755--6764}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{GoTube: Scalable statistical verification of continuous-depth models}}, doi = {10.1609/aaai.v36i6.20631}, volume = {36}, year = {2022}, } @inproceedings{12568, abstract = {We treat the problem of risk-aware control for stochastic shortest path (SSP) on Markov decision processes (MDP). Typically, expectation is considered for SSP, which however is oblivious to the incurred risk. We present an alternative view, instead optimizing conditional value-at-risk (CVaR), an established risk measure. We treat both Markov chains as well as MDP and introduce, through novel insights, two algorithms, based on linear programming and value iteration, respectively. Both algorithms offer precise and provably correct solutions. Evaluation of our prototype implementation shows that risk-aware control is feasible on several moderately sized models.}, author = {Meggendorfer, Tobias}, booktitle = {Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022}, isbn = {1577358767}, issn = {2374-3468}, location = {Virtual}, number = {9}, pages = {9858--9867}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Risk-aware stochastic shortest path}}, doi = {10.1609/aaai.v36i9.21222}, volume = {36}, year = {2022}, } @article{12511, abstract = {We consider the problem of formally verifying almost-sure (a.s.) asymptotic stability in discrete-time nonlinear stochastic control systems. While verifying stability in deterministic control systems is extensively studied in the literature, verifying stability in stochastic control systems is an open problem. The few existing works on this topic either consider only specialized forms of stochasticity or make restrictive assumptions on the system, rendering them inapplicable to learning algorithms with neural network policies. In this work, we present an approach for general nonlinear stochastic control problems with two novel aspects: (a) instead of classical stochastic extensions of Lyapunov functions, we use ranking supermartingales (RSMs) to certify a.s. asymptotic stability, and (b) we present a method for learning neural network RSMs. We prove that our approach guarantees a.s. asymptotic stability of the system and provides the first method to obtain bounds on the stabilization time, which stochastic Lyapunov functions do not. Finally, we validate our approach experimentally on a set of nonlinear stochastic reinforcement learning environments with neural network policies.}, author = {Lechner, Mathias and Zikelic, Dorde and Chatterjee, Krishnendu and Henzinger, Thomas A}, isbn = {9781577358350}, issn = {2374-3468}, journal = {Proceedings of the AAAI Conference on Artificial Intelligence}, keywords = {General Medicine}, number = {7}, pages = {7326--7336}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Stability verification in stochastic control systems via neural network supermartingales}}, doi = {10.1609/aaai.v36i7.20695}, volume = {36}, year = {2022}, } @inproceedings{10669, abstract = {We show that Neural ODEs, an emerging class of timecontinuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Stochastic Lagrangian Reachability (SLR), an abstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states over a given time-horizon), and provide stochastic guarantees in the form of confidence intervals for the Reachtube bounds. SLR inherently avoids the infamous wrapping effect (accumulation of over-approximation errors) by performing local optimization steps to expand safe regions instead of repeatedly forward-propagating them as is done by deterministic reachability methods. To enable fast local optimizations, we introduce a novel forward-mode adjoint sensitivity method to compute gradients without the need for backpropagation. Finally, we establish asymptotic and non-asymptotic convergence rates for SLR.}, author = {Grunbacher, Sophie and Hasani, Ramin and Lechner, Mathias and Cyranka, Jacek and Smolka, Scott A and Grosu, Radu}, booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence}, isbn = {978-1-57735-866-4}, issn = {2374-3468}, location = {Virtual}, number = {13}, pages = {11525--11535}, publisher = {AAAI Press}, title = {{On the verification of neural ODEs with stochastic guarantees}}, volume = {35}, year = {2021}, } @inproceedings{10671, abstract = {We introduce a new class of time-continuous recurrent neural network models. Instead of declaring a learning system’s dynamics by implicit nonlinearities, we construct networks of linear first-order dynamical systems modulated via nonlinear interlinked gates. The resulting models represent dynamical systems with varying (i.e., liquid) time-constants coupled to their hidden state, with outputs being computed by numerical differential equation solvers. These neural networks exhibit stable and bounded behavior, yield superior expressivity within the family of neural ordinary differential equations, and give rise to improved performance on time-series prediction tasks. To demonstrate these properties, we first take a theoretical approach to find bounds over their dynamics, and compute their expressive power by the trajectory length measure in a latent trajectory space. We then conduct a series of time-series prediction experiments to manifest the approximation capability of Liquid Time-Constant Networks (LTCs) compared to classical and modern RNNs.}, author = {Hasani, Ramin and Lechner, Mathias and Amini, Alexander and Rus, Daniela and Grosu, Radu}, booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence}, isbn = {978-1-57735-866-4}, issn = {2374-3468}, location = {Virtual}, number = {9}, pages = {7657--7666}, publisher = {AAAI Press}, title = {{Liquid time-constant networks}}, volume = {35}, year = {2021}, } @inproceedings{11436, abstract = {Asynchronous distributed algorithms are a popular way to reduce synchronization costs in large-scale optimization, and in particular for neural network training. However, for nonsmooth and nonconvex objectives, few convergence guarantees exist beyond cases where closed-form proximal operator solutions are available. As training most popular deep neural networks corresponds to optimizing nonsmooth and nonconvex objectives, there is a pressing need for such convergence guarantees. In this paper, we analyze for the first time the convergence of stochastic asynchronous optimization for this general class of objectives. In particular, we focus on stochastic subgradient methods allowing for block variable partitioning, where the shared model is asynchronously updated by concurrent processes. To this end, we use a probabilistic model which captures key features of real asynchronous scheduling between concurrent processes. Under this model, we establish convergence with probability one to an invariant set for stochastic subgradient methods with momentum. From a practical perspective, one issue with the family of algorithms that we consider is that they are not efficiently supported by machine learning frameworks, which mostly focus on distributed data-parallel strategies. To address this, we propose a new implementation strategy for shared-memory based training of deep neural networks for a partitioned but shared model in single- and multi-GPU settings. Based on this implementation, we achieve on average1.2x speed-up in comparison to state-of-the-art training methods for popular image classification tasks, without compromising accuracy.}, author = {Kungurtsev, Vyacheslav and Egan, Malcolm and Chatterjee, Bapi and Alistarh, Dan-Adrian}, booktitle = {35th AAAI Conference on Artificial Intelligence, AAAI 2021}, isbn = {9781713835974}, issn = {2374-3468}, location = {Virtual, Online}, number = {9B}, pages = {8209--8216}, publisher = {AAAI Press}, title = {{Asynchronous optimization methods for efficient training of deep neural networks with guarantees}}, volume = {35}, year = {2021}, } @inproceedings{10665, abstract = {Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for verification of an idealized model of the actual network which works over real arithmetic and ignores rounding imprecisions. This idealization is in stark contrast to network quantization, which is a technique that trades numerical precision for computational efficiency and is, therefore, often applied in practice. Neglecting rounding errors of such low-bit quantized neural networks has been shown to lead to wrong conclusions about the network’s correctness. Thus, the desired approach for verifying quantized neural networks would be one that takes these rounding errors into account. In this paper, we show that verifying the bitexact implementation of quantized neural networks with bitvector specifications is PSPACE-hard, even though verifying idealized real-valued networks and satisfiability of bit-vector specifications alone are each in NP. Furthermore, we explore several practical heuristics toward closing the complexity gap between idealized and bit-exact verification. In particular, we propose three techniques for making SMT-based verification of quantized neural networks more scalable. Our experiments demonstrate that our proposed methods allow a speedup of up to three orders of magnitude over existing approaches.}, author = {Henzinger, Thomas A and Lechner, Mathias and Zikelic, Dorde}, booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence}, isbn = {978-1-57735-866-4}, issn = {2374-3468}, location = {Virtual}, number = {5A}, pages = {3787--3795}, publisher = {AAAI Press}, title = {{Scalable verification of quantized neural networks}}, volume = {35}, year = {2021}, } @inproceedings{14186, abstract = {The goal of the unsupervised learning of disentangled representations is to separate the independent explanatory factors of variation in the data without access to supervision. In this paper, we summarize the results of Locatello et al., 2019, and focus on their implications for practitioners. We discuss the theoretical result showing that the unsupervised learning of disentangled representations is fundamentally impossible without inductive biases and the practical challenges it entails. Finally, we comment on our experimental findings, highlighting the limitations of state-of-the-art approaches and directions for future research.}, author = {Locatello, Francesco and Bauer, Stefan and Lucic, Mario and Rätsch, Gunnar and Gelly, Sylvain and Schölkopf, Bernhard and Bachem, Olivier}, booktitle = {The 34th AAAI Conference on Artificial Intelligence}, isbn = {9781577358350}, issn = {2374-3468}, location = {New York, NY, United States}, number = {9}, pages = {13681--13684}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{A commentary on the unsupervised learning of disentangled representations}}, doi = {10.1609/aaai.v34i09.7120}, volume = {34}, year = {2020}, } @article{9197, abstract = {In this paper we introduce and study all-pay bidding games, a class of two player, zero-sum games on graphs. The game proceeds as follows. We place a token on some vertex in the graph and assign budgets to the two players. Each turn, each player submits a sealed legal bid (non-negative and below their remaining budget), which is deducted from their budget and the highest bidder moves the token onto an adjacent vertex. The game ends once a sink is reached, and Player 1 pays Player 2 the outcome that is associated with the sink. The players attempt to maximize their expected outcome. Our games model settings where effort (of no inherent value) needs to be invested in an ongoing and stateful manner. On the negative side, we show that even in simple games on DAGs, optimal strategies may require a distribution over bids with infinite support. A central quantity in bidding games is the ratio of the players budgets. On the positive side, we show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation for the optimal strategy for that ratio. We also implement it, show that it performs well, and suggests interesting properties of these games. Then, given an outcome c, we show an algorithm for finding the necessary and sufficient initial ratio for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally, while the general case has not previously been studied, solving the specific game in which Player 1 wins iff he wins the first two auctions, has been long stated as an open question, which we solve.}, author = {Avni, Guy and Ibsen-Jensen, Rasmus and Tkadlec, Josef}, isbn = {9781577358350}, issn = {2374-3468}, journal = {Proceedings of the AAAI Conference on Artificial Intelligence}, location = {New York, NY, United States}, number = {02}, pages = {1798--1805}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{All-pay bidding games on graphs}}, doi = {10.1609/aaai.v34i02.5546}, volume = {34}, year = {2020}, }