@inproceedings{18071,
  abstract     = {Recent advancements on DAG-based consensus protocols allow for blockchains with improved metrics and properties, such as throughput and censorship-resistance. Variants of the Bullshark [18] consensus protocol are adopted for practical use by the Sui blockchain, for improved latency. However, the protocol is leader-based, and is strongly affected by crashed leaders that can lead to various performance issues, for example, decreased transaction throughput. In this paper, we propose HammerHead, a DAG-based consensus protocol, that is inspired by Carousel [8] and provides Leader-Utilization. Our proposal differs from Carousel, which is built for a chained consensus protocol; in HammerHead chain quality is inherited by the DAG. HammerHead needs to preserve safety and liveness, despite validators committing leader vertices asynchronously. The key idea is to update leader schedules dynamically, based on the validators' scores during the previous schedule. We implement HammerHead and show a minor improvement in performance for cases without faults. The major improvements in comparison to Bullshark appear in faulty settings. Specifically, we show a drastic, 2x-latency improvement and up to 40% increased throughput when crash faults occur (100 validators, 33 faults).},
  author       = {Tsimos, Giorgos and Kichidis, Anastasios and Sonnino, Alberto and Kokoris Kogias, Eleftherios},
  booktitle    = {Proceedings - International Conference on Distributed Computing Systems},
  isbn         = {9798350386059},
  issn         = {2575-8411},
  location     = {Jersey City, NJ, United States},
  pages        = {1377--1387},
  publisher    = {IEEE},
  title        = {{HammerHead: Leader reputation for dynamic scheduling}},
  doi          = {10.1109/ICDCS60910.2024.00129},
  year         = {2024},
}

@article{18073,
  abstract     = {Conserved signaling cascades monitor protein-folding homeostasis to ensure proper cellular function. One of the evolutionary conserved key players is IRE1, which maintains endoplasmic reticulum (ER) homeostasis through the unfolded protein response (UPR). Upon accumulation of misfolded proteins in the ER, IRE1 forms clusters on the ER membrane to initiate UPR signaling. What regulates IRE1 cluster formation is not fully understood. Here, we show that the ER lumenal domain (LD) of human IRE1α forms biomolecular condensates in vitro. IRE1α LD condensates were stabilized both by binding to unfolded polypeptides as well as by tethering to model membranes, suggesting their role in assembling IRE1α into signaling-competent stable clusters. Molecular dynamics simulations indicated that weak multivalent interactions drive IRE1α LD clustering. Mutagenesis experiments identified disordered regions in IRE1α LD to control its clustering in vitro and in cells. Importantly, dysregulated clustering of IRE1α mutants led to defects in IRE1α signaling. Our results revealed that disordered regions in IRE1α LD control its clustering and suggest their role as a common strategy in regulating protein assembly on membranes.},
  author       = {Kettel, Paulina and Marosits, Laura and Spinetti, Elena and Rechberger, Michael and Giannini, Caterina and Radler, Philipp and Niedermoser, Isabell and Fischer, Irmgard and Versteeg, Gijs A. and Loose, Martin and Covino, Roberto and Karagöz, G. Elif},
  issn         = {1460-2075},
  journal      = {EMBO Journal},
  number       = {20},
  pages        = {4668--4698},
  publisher    = {Embo Press},
  title        = {{Disordered regions in the IRE1α ER lumenal domain mediate its stress-induced clustering}},
  doi          = {10.1038/s44318-024-00207-0},
  volume       = {43},
  year         = {2024},
}

@phdthesis{18076,
  abstract     = {The new era of Ge has opened up new possibilities in quantum computing. The maturity of Ge
spin qubits is unquestioned, while hybrid semiconductor-superconductor Ge circuits are on track
to enter the game. Gate-tunable transmons (gatemons) employing semiconductor Josephson
junctions have recently emerged as building blocks for such hybrid quantum circuits. In this
thesis, we present a gatemon fabricated in planar Germanium. We induce superconductivity
in a two-dimensional hole gas by evaporating aluminum atop a thin spacer, which separates
the superconductor from the Ge quantum well. The Josephson junction is then integrated
into an Xmon circuit and capacitively coupled to a transmission line resonator. We showcase
the qubit tunability in a broad frequency range with resonator and two-tone spectroscopy.
Time-domain characterizations reveal energy relaxation and coherence times up to 75 ns. Our
results, combined with the recent advances in the spin qubit field, pave the way towards novel
hybrid and protected qubits in a group IV, CMOS-compatible material.},
  author       = {Sagi, Oliver},
  issn         = {2663-337X},
  pages        = {111},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Hybrid circuits on planar Germanium}},
  doi          = {10.15479/at:ista:18076},
  year         = {2024},
}

@article{18087,
  abstract     = {We present a theory describing the interaction of structured light, such as light carrying orbital angular momentum, with molecules. The light-matter interaction Hamiltonian we derive is expressed through couplings between spherical gradients of the electric field and the (transition) electric multipole moments of a particle of any nontrivial rotation point group. Our model can therefore accommodate an arbitrary complexity of the molecular and electric field structure, and it can be straightforwardly extended to atoms or nanostructures. Applying this framework to rovibrational spectroscopy of molecules, we uncover the general mechanism of angular momentum exchange between the spin and orbital angular momenta of light, molecular rotation, and its center-of-mass motion. We show that the nonzero vorticity of Laguerre-Gaussian beams can strongly enhance certain rovibrational transitions that are considered forbidden in the case of nonhelical light. We discuss the experimental requirements for the observation of these forbidden transitions in state-of-the-art spatially resolved spectroscopy measurements.},
  author       = {Maslov, Mikhail and Koutentakis, Georgios and Hrast, Mateja and Heckl, Oliver H. and Lemeshko, Mikhail},
  issn         = {2643-1564},
  journal      = {Physical Review Research},
  number       = {3},
  publisher    = {American Physical Society},
  title        = {{Theory of angular momentum transfer from light to molecules}},
  doi          = {10.1103/physrevresearch.6.033277},
  volume       = {6},
  year         = {2024},
}

@inproceedings{18097,
  abstract     = {In our companion paper "Tight bounds for the learning of homotopy à la Niyogi, Smale, and Weinberger for subsets of Euclidean spaces and of Riemannian manifolds" we gave optimal bounds (in terms of the two one-sided Hausdorff distances) on a sample P of an input shape 𝒮 (either manifold or general set with positive reach) such that one can infer the homotopy of 𝒮 from the union of balls with some radius centred at P, both in Euclidean space and in a Riemannian manifold of bounded curvature. The construction showing the optimality of the bounds is not straightforward. The purpose of this video is to visualize and thus elucidate said construction in the Euclidean setting.},
  author       = {Attali, Dominique and Kourimska, Hana and Fillmore, Christopher D and Ghosh, Ishika and Lieutier, Andre and Stephenson, Elizabeth R and Wintraecken, Mathijs},
  booktitle    = {40th International Symposium on Computational Geometry},
  isbn         = {9783959773164},
  location     = {Athens, Greece},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{The ultimate frontier: An optimality construction for homotopy inference (media exposition)}},
  doi          = {10.4230/LIPIcs.SoCG.2024.87},
  volume       = {293},
  year         = {2024},
}

@article{18107,
  abstract     = {We consider a dilute fully spin-polarized Fermi gas at positive temperature in dimensions  d∈{1,2,3} . We show that the pressure of the interacting gas is bounded from below by that of the free gas plus, to leading order, an explicit term of order  adρ2+2/d, where a is the p-wave scattering length of the repulsive interaction and  ρ  is the particle density. The results are valid for a wide range of repulsive interactions, including that of a hard core, and uniform in temperatures at most of the order of the Fermi temperature. A central ingredient in the proof is a rigorous implementation of the fermionic cluster expansion of Gaudin, Gillespie and Ripka (Nucl. Phys. A, 176.2 (1971), pp. 237–260).},
  author       = {Lauritsen, Asbjørn Bækgaard and Seiringer, Robert},
  issn         = {2050-5094},
  journal      = {Forum of Mathematics, Sigma},
  publisher    = {Cambridge University Press},
  title        = {{Pressure of a dilute spin-polarized Fermi gas: Lower bound}},
  doi          = {10.1017/fms.2024.56},
  volume       = {12},
  year         = {2024},
}

@article{18108,
  abstract     = {Here we announce the construction and properties of a big commutative subalgebra of the Kirillov algebra attached to a finite dimensional irreducible representation of a complex semisimple Lie group. They are commutative finite flat algebras over the cohomology of the classifying space of the group. They are isomorphic with the equivariant intersection cohomology of affine Schubert varieties, endowing the latter with a new ring structure. Study of the finer aspects of the structure of the big algebras will also furnish the stalks of the intersection cohomology with ring structure, thus ringifying Lusztig’s q-weight multiplicity polynomials i.e., certain affine Kazhdan–Lusztig polynomials.},
  author       = {Hausel, Tamás},
  issn         = {1091-6490},
  journal      = {Proceedings of the National Academy of Sciences of the United States of America},
  number       = {38},
  publisher    = {National Academy of Sciences},
  title        = {{Commutative avatars of representations of semisimple Lie groups}},
  doi          = {10.1073/pnas.2319341121},
  volume       = {121},
  year         = {2024},
}

@article{18109,
  abstract     = {Venous thromboembolism (VTE) is a common, deadly disease with an increasing incidence despite preventive efforts. Clinical observations have associated elevated antibody concentrations or antibody-based therapies with thrombotic events. However, how antibodies contribute to thrombosis is unknown. Here, we show that reduced blood flow enabled immunoglobulin M (IgM) to bind to FcμR and the polymeric immunoglobulin receptor (pIgR), initiating endothelial activation and platelet recruitment. Subsequently, the procoagulant surface of activated platelets accommodated antigen- and FcγR-independent IgG deposition. This leads to classical complement activation, setting in motion a prothrombotic vicious circle. Key elements of this mechanism were present in humans in the setting of venous stasis as well as in the dysregulated immunothrombosis of COVID-19. This antibody-driven thrombosis can be prevented by pharmacologically targeting complement. Hence, our results uncover antibodies as previously unrecognized central regulators of thrombosis. These findings carry relevance for therapeutic application of antibodies and open innovative avenues to target thrombosis without compromising hemostasis.},
  author       = {Stark, Konstantin and Kilani, Badr and Stockhausen, Sven and Busse, Johanna and Schubert, Irene and Tran, Thuy Duong and Gärtner, Florian R and Leunig, Alexander and Pekayvaz, Kami and Nicolai, Leo and Fumagalli, Valeria and Stermann, Julia and Stephan, Felix and David, Christian and Müller, Martin B. and Heyman, Birgitta and Lux, Anja and Da Palma Guerreiro, Alexandra and Frenzel, Lukas P. and Schmidt, Christoph Q. and Dopler, Arthur and Moser, Markus and Chandraratne, Sue and Von Brühl, Marie Luise and Lorenz, Michael and Korff, Thomas and Rudelius, Martina and Popp, Oliver and Kirchner, Marieluise and Mertins, Philipp and Nimmerjahn, Falk and Iannacone, Matteo and Sperandio, Markus and Engelmann, Bernd and Verschoor, Admar and Massberg, Steffen},
  issn         = {1097-4180},
  journal      = {Immunity},
  number       = {9},
  pages        = {2140--2156},
  publisher    = {Elsevier},
  title        = {{Antibodies and complement are key drivers of thrombosis}},
  doi          = {10.1016/j.immuni.2024.08.007},
  volume       = {57},
  year         = {2024},
}

@article{18110,
  abstract     = {We study a chaotic particle-conserving kinetically constrained model, with a single parameter which allows us to break reflection symmetry. Through extensive numerical simulations we find that the domain wall state shows a variety of dynamical behaviors from localization all the way to ballistic transport, depending on the value of the reflection breaking parameter. Surprisingly, such anomalous behavior is not mirrored in infinite-temperature dynamics, which appear to scale diffusively, in line with expectations for generic interacting models. However, studying the particle density gradient, we show that the lack of reflection symmetry affects infinite-temperature dynamics, resulting in an asymmetric dynamical structure factor. This is in disagreement with normal diffusion and suggests that the model may also exhibit anomalous dynamics at infinite temperature in the thermodynamic limit. Finally, we observe low-entangled eigenstates in the spectrum of the model, a telltale sign of quantum many-body scars.},
  author       = {Brighi, Pietro and Ljubotina, Marko},
  issn         = {2469-9969},
  journal      = {Physical Review B},
  number       = {10},
  publisher    = {American Physical Society},
  title        = {{Anomalous transport in the kinetically constrained quantum East-West model}},
  doi          = {10.1103/PhysRevB.110.L100304},
  volume       = {110},
  year         = {2024},
}

@inproceedings{18113,
  abstract     = {The emergence of accurate open large language models (LLMs) has led to a race towards performant quantization techniques which can enable their execution on end-user devices. In this paper, we revisit the problem of “extreme” LLM compression—defined as targeting extremely low bit counts, such as 2 to 3 bits per parameter—from the point of view of classic methods in Multi-Codebook Quantization (MCQ). Our algorithm, called AQLM, generalizes the classic Additive Quantization (AQ) approach for information retrieval to advance the state-of-the-art in LLM compression, via two innovations: 1) learned additive quantization of weight matrices in input-adaptive fashion, and 2) joint optimization of codebook parameters across each transformer blocks. Broadly, AQLM is the first scheme that is Pareto optimal in terms of accuracy-vs-model-size when compressing to less than 3 bits per parameter, and significantly improves upon all known schemes in the extreme compression (2bit) regime. In addition, AQLM is practical: we provide fast GPU and CPU implementations of AQLM for token generation, which enable us to match or outperform optimized FP16 implementations for speed, while executing in a much smaller memory footprint.},
  author       = {Egiazarian, Vage and Panferov, Andrei and Kuznedelev, Denis and Frantar, Elias and Babenko, Artem and Alistarh, Dan-Adrian},
  booktitle    = {Proceedings of the 41st International Conference on Machine Learning},
  issn         = {2640-3498},
  location     = {Vienna, Austria},
  pages        = {12284--12303},
  publisher    = {ML Research Press},
  title        = {{Extreme compression of large language models via additive quantization}},
  volume       = {235},
  year         = {2024},
}

@inproceedings{18114,
  abstract     = {This paper presents Mechanistic Neural Networks, a neural network design for machine learning applications in the sciences. It incorporates a new Mechanistic Block in standard architectures to explicitly learn governing differential equations as representations, revealing the underlying dynamics of data and enhancing interpretability and efficiency in data modeling. Central to our approach is a novel Relaxed Linear Programming Solver (NeuRLP) inspired by a technique that reduces solving linear ODEs to solving linear programs. This integrates well with neural networks and surpasses the limitations of traditional ODE solvers enabling scalable GPU parallel processing. Overall, Mechanistic Neural Networks demonstrate their versatility for scientific machine learning applications, adeptly managing tasks from equation discovery to dynamic systems modeling. We prove their comprehensive capabilities in analyzing and interpreting complex scientific data across various applications, showing significant performance against specialized state-of-the-art methods. Source code is available at https://github.com/alpz/mech-nn.},
  author       = {Pervez, Adeel A and Locatello, Francesco and Gavves, Efstratios},
  booktitle    = {Proceedings of the 41st International Conference on Machine Learning},
  issn         = {2640-3498},
  location     = {Vienna, Austria},
  pages        = {40484--40501},
  publisher    = {ML Research Press},
  title        = {{Mechanistic neural networks for scientific machine learning}},
  volume       = {235},
  year         = {2024},
}

@inproceedings{18115,
  abstract     = {We study the data selection problem, whose aim is to select a small representative subset of data that can be used to efficiently train a machine learning model. We present a new data selection approach based on k-means clustering and sensitivity sampling. Assuming access to an embedding representation of the data with respect to which the model loss is Holder continuous, our approach provably allows selecting a set of “typical” k+1/ε2 elements whose average loss corresponds to the average loss of the whole dataset, up to a multiplicative (1±ε)
 factor and an additive ελΦk, where Φk represents the k-means cost for the input embeddings and λ is the Holder constant. We furthermore demonstrate the performance and scalability of our approach on fine-tuning foundation models and show that it outperforms state-of-the-art methods. We also show how it can be applied on linear regression, leading to a new sampling strategy that surprisingly matches the performance of leverage score sampling, while being conceptually simpler and more scalable.},
  author       = {Axiotis, Kyriakos and Cohen-Addad, Vincent and Henzinger, Monika H and Jerome, Sammy and Mirrokni, Vahab and Saulpic, David and Woodruff, David P. and Wunder, Michael},
  booktitle    = {Proceedings of the 41st International Conference on Machine Learning},
  issn         = {2640-3498},
  location     = {Vienna, Austria},
  pages        = {2086--2107},
  publisher    = {ML Research Press},
  title        = {{Data-efficient learning via clustering-based sensitivity sampling: Foundation models and beyond}},
  volume       = {235},
  year         = {2024},
}

@inproceedings{18116,
  abstract     = {As a staple of data analysis and unsupervised learning, the problem of private clustering has been widely studied, under various privacy models. Centralized differential privacy is the first of them, and the problem has also been studied for the local and the shuffle variation. In each case, the goal is to design an algorithm that computes privately a clustering, with the smallest possible error. The study of each variation gave rise to new algorithm: the landscape of private clustering algorithm is therefore quite intricate. In this paper, we show that a 20 year-old algorithm can be slightly modified to work for any of those models. This provides a unified picture: while matching almost all previously known results, it allows us to improve some of them, and extend to a new privacy model, the continual observation setting, where the input is changing over time and the algorithm must output a new solution at each time step.},
  author       = {La Tour, Max Dupré and Henzinger, Monika H and Saulpic, David},
  booktitle    = {Proceedings of the 41st International Conference on Machine Learning},
  issn         = {2640-3498},
  location     = {Vienna, Austria},
  pages        = {12046--12086},
  publisher    = {ML Research Press},
  title        = {{Making old things new: A unified algorithm for differentially private clustering}},
  volume       = {235},
  year         = {2024},
}

@inproceedings{18117,
  abstract     = {We investigate parameter-efficient fine-tuning (PEFT) methods that can provide good accuracy under limited computational and memory budgets in the context of large language models (LLMs). We present a new PEFT method called Robust Adaptation (RoSA) inspired by robust principal component analysis that jointly trains low-rank
 and highly-sparse components on top of a set of fixed pretrained weights to efficiently approximate the performance of a full-fine-tuning (FFT) solution. Across a series of challenging generative tasks such as grade-school math and SQL query generation, which require fine-tuning for good performance, we show that RoSA outperforms LoRA, pure sparse fine-tuning, and alternative hybrid methods at the same parameter budget, and can even recover the performance of FFT on some tasks. We provide system support for RoSA to complement the training algorithm, specifically in the form of sparse GPU kernels which enable memory- and computationally-efficient training, and show that it is also compatible with low-precision base weights, resulting in the first joint representation combining quantization, low-rank and sparse approximations. Our code is available at https://github.com/IST-DASLab/RoSA.},
  author       = {Nikdan, Mahdi and Tabesh, Soroush and Crncevic, Elvir and Alistarh, Dan-Adrian},
  booktitle    = {Proceedings of the 41st International Conference on Machine Learning},
  issn         = {2640-3498},
  location     = {Vienna, Austria},
  pages        = {38187--38206},
  publisher    = {ML Research Press},
  title        = {{RoSA: Accurate parameter-efficient fine-tuning via robust adaptation}},
  volume       = {235},
  year         = {2024},
}

@inproceedings{18118,
  abstract     = {We introduce a new framework for studying meta-learning methods using PAC-Bayesian theory. Its main advantage over previous work is that it allows for more flexibility in how the transfer of knowledge between tasks is realized. For previous approaches, this could only happen indirectly, by means of learning prior distributions over models. In contrast, the new generalization bounds that we prove express the process of meta-learning much more directly as learning the learning algorithm that should be used for future tasks. The flexibility of our framework makes it suitable to analyze a wide range of meta-learning mechanisms and even design new mechanisms. Other than our theoretical contributions we also show empirically that our framework improves the prediction quality in practical meta-learning mechanisms.},
  author       = {Zakerinia, Hossein and Behjati, Amin and Lampert, Christoph},
  booktitle    = {Proceedings of the 41st International Conference on Machine Learning},
  issn         = {2640-3498},
  location     = {Vienna, Austria},
  pages        = {58122--58139},
  publisher    = {ML Research Press},
  title        = {{More flexible PAC-Bayesian meta-learning by learning learning algorithms}},
  volume       = {235},
  year         = {2024},
}

@article{18153,
  abstract     = {Attention supports decision making by selecting the features that are relevant for decisions. Selective enhancement of the relevant features and inhibition of distractors has been proposed as potential neural mechanisms driving this selection process. Yet, how attention operates when relevance cannot be directly determined, and the attention signal needs to be internally constructed is less understood. Here we recorded from populations of neurons in the anterior cingulate cortex (ACC) of mice in an attention-shifting task where relevance of stimulus modalities changed across blocks of trials. In contrast with V1 recordings, decoding of the irrelevant modality gradually declined in ACC after an initial transient. Our analytical proof and a recurrent neural network model of the task revealed mutually inhibiting connections that produced context-gated suppression as observed in mice. Using this RNN model we predicted a correlation between contextual modulation of individual neurons and their stimulus drive, which we confirmed in ACC but not in V1.},
  author       = {Hajnal, Márton Albert and Tran, Duy and Szabó, Zsombor and Albert, Andrea and Safaryan, Karen and Einstein, Michael and Vallejo Martelo, Mauricio and Polack, Pierre-Olivier and Golshani, Peyman and Orbán, Gergő},
  issn         = {2041-1723},
  journal      = {Nature Communications},
  publisher    = {Springer Nature},
  title        = {{Shifts in attention drive context-dependent subspace encoding in anterior cingulate cortex in mice during decision making}},
  doi          = {10.1038/s41467-024-49845-2},
  volume       = {15},
  year         = {2024},
}

@inproceedings{18156,
  abstract     = {Privately counting distinct elements in a stream is a fundamental data analysis problem with many applications in machine learning. In the turnstile model, Jain et al. [NeurIPS2023] initiated the study of this problem parameterized by the maximum flippancy of any element, i.e., the number of times that the count of an element changes from 0 to above 0 or vice versa. They give an item-level (ε,δ)-differentially private algorithm whose additive error is tight with respect to that parameterization. In this work, we show that a very simple algorithm based on the sparse vector technique achieves a tight additive error for item-level (ε,δ)-differential privacy and item-level ε-differential privacy with regards to a different parameterization, namely the sum of all flippancies. Our second result is a bound which shows that for a large class of algorithms, including all existing differentially private algorithms for this problem, the lower bound from item-level differential privacy extends to event-level differential privacy. This partially answers an open question by Jain et al. [NeurIPS2023].},
  author       = {Henzinger, Monika H and Sricharan, A. R. and Steiner, Teresa Anna},
  booktitle    = {International Conference on Approximation Algorithms for Combinatorial Optimization Problems },
  isbn         = {9783959773485},
  issn         = {1868-8969},
  location     = {London, United Kingdom},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Private counting of distinct elements in the turnstile model and extensions}},
  doi          = {10.4230/LIPIcs.APPROX/RANDOM.2024.40},
  volume       = {317},
  year         = {2024},
}

@article{18158,
  abstract     = {We study the geometry of Poisson point processes from the point of view of optimal transport and Ricci lower bounds. We construct a Riemannian structure on the space of point processes and the associated distance W that corresponds to the Benamou–Brenier variational formula. Our main tool is a non-local continuity equation formulated with the difference operator. The closure of the domain of the relative entropy is a complete geodesic space, when endowed with 
W. The geometry of this non-local infinite-dimensional space is analogous to that of spaces with positive Ricci curvature. Among others: (a) the Ornstein–Uhlenbeck semi-group is the gradient flow of the relative entropy; (b) the Poisson space has an entropic Ricci curvature bounded from below by 1; (c) W satisfies an HWI inequality.},
  author       = {Dello Schiavo, Lorenzo and Herry, Ronan and Suzuki, Kohei},
  issn         = {2270-518X},
  journal      = {Journal de l'Ecole Polytechnique - Mathematiques},
  pages        = {957--1010},
  publisher    = {Ecole Polytechnique},
  title        = {{Wasserstein geometry and Ricci curvature bounds for Poisson spaces}},
  doi          = {10.5802/jep.270},
  volume       = {11},
  year         = {2024},
}

@inproceedings{18159,
  abstract     = {Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defned with respect to paths over MDP states. An increasingly
popular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states. For instance, reachability and safety properties in modeling robot swarms or chemical reaction networks are naturally defned in terms of probability distributions over states. Verifying such distributional properties is known to be hard and often beyond the reach of classical state-based verifcation techniques. In this work, we consider the problems of certifed policy (i.e. controller) verifcation and synthesis in MDPs under distributional reach-avoidance specifcations. By certifed we mean that, along with a policy, we also aim to synthesize a (checkable) certifcate ensuring that the MDP indeed satisfes the property. Thus, given the target set of distributions and an unsafe set of distributions over MDP states, our goal is to either synthesize a certifcate for a given policy or synthesize a policy along with a certifcate, proving that the target distribution can be reached while avoiding unsafe distributions. To solve this problem, we introduce the novel notion of distributional reach-avoid certifcates and present automated procedures for (1) synthesizing a certifcate for a given policy, and (2) synthesizing a policy together with the certifcate, both providing formal guarantees on certifcate correctness. Our experimental evaluation demonstrates the ability of our method to solve several non-trivial examples, including a multi-agent robot-swarm model, to synthesize certifed policies and to certify existing policies. },
  author       = {Akshay, S and Chatterjee, Krishnendu and Meggendorfer, Tobias and Zikelic, Dorde},
  booktitle    = {Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence},
  isbn         = {9781956792041},
  issn         = {1045-0823},
  location     = {Jeju, Korea},
  pages        = {3--12},
  publisher    = {International Joint Conferences on Artificial Intelligence},
  title        = {{Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties}},
  doi          = {10.24963/ijcai.2024/1},
  year         = {2024},
}

@inproceedings{18160,
  abstract     = {Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities into account. Robust Markov decision processes (RMDPs) address this shortcoming of MDPs by assigning to each transition an uncertainty set rather than a single probability value. In this work, we consider polytopic RMDPs in which all uncertainty sets are polytopes and study the problem of solving long-run average reward polytopic RMDPs. We present a novel perspective on this problem and show that it can be reduced to solving long-run average reward turn-based stochastic games with finite state and action spaces. This reduction allows us to derive several important consequences that were hitherto not known to hold for polytopic RMDPs. First, we derive new computational complexity bounds for solving long-run average reward polytopic RMDPs, showing for the first time that the threshold decision problem for them is in NP∩CONP and that they admit a randomized algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is much more efficient in solving long-run average reward polytopic RMDPs compared to state-of-the-art methods based on value iteration. },
  author       = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Karrabi, Mehrdad and Novotný, Petr and Zikelic, Dorde},
  booktitle    = {33rd International Joint Conference on Artificial Intelligence},
  isbn         = {9781956792041},
  issn         = {1045-0823},
  location     = {Jeju, South Korea},
  pages        = {6707--6715},
  publisher    = {International Joint Conferences on Artificial Intelligence},
  title        = {{Solving long-run average reward robust MDPs via stochastic games}},
  doi          = {10.24963/ijcai.2024/741},
  year         = {2024},
}

