@phdthesis{18766,
  abstract     = {Poxviruses are large pleomorphic double-stranded DNA viruses that include well known members such as variola virus, the causative agent of smallpox, Mpox virus, as well as Vaccinia virus (VACV), which serves as a vaccination strain for formerly mentioned viruses. VACV is a valuable model for studying large pleomorphic DNA viruses in general and poxviruses specifically, as many features, such as core morphology and structural proteins, are well conserved within this family. Despite decades of research, our understanding of the structural components and proteins that comprise the poxvirus core in mature virions remains limited. Although major core proteins were identified via indirect experimental evidence, the core's complexity, with its large size, structure and number of involved proteins, has hindered efforts to achieve high-resolution insights and to define the roles of the individual proteins. The specific protein composition of the core's individual layers, including the palisade layer and the inner core wall, has remained unclear. In this study, we have merged multiple approaches, including single particle cryo electron microscopy of purified virus cores, cryo-electron tomography and subtomogram averaging of mature virions and molecular modeling to elucidate the structural determinants of the VACV core. Due to the lack of experimentally derived structures, either in situ or reconstituted in vitro, we used Alphafold to predict models of the putative major core protein candidates, A10, 23k, A3, A4, and L4. Our results show that the VACV core is composed of several layers with varying local symmetries, forming more intricate interactions than observed previously. This allowed us to identify several molecular building blocks forming the viral core lattice. In particular, we identified trimers of protein A10 as a major core structure that forms the palisade layer of the viral core. Additionally, we revealed that six petals of a flower shaped core pore within the core wall are composed of A10 trimers. Furthermore, we obtained a cryo-EM density for the inner core wall that could potentially accommodate an A3 dimer. Integrating descriptions of protein interactions from previous studies enabled us to provide a detailed structural model of the poxvirus core wall, and our findings indicate that the interactions within A10 trimers are likely consistent across orthopox- and parapoxviruses. This combined application of cryo-SPA and cryo-ET can help overcome obstacles in studying complex virus structures in the future, including their key assembly proteins, interactions, and the formation into a core lattice. Our work provides important fundamental new insights into poxvirus core architecture, also considering the recent re-emergence of poxviruses.},
  author       = {Datler, Julia},
  isbn         = {978-3-99078-049-7},
  issn         = {2663-337X},
  keywords     = {cryo-EM, cryo-ET, cryo-SPA, Structural Virology, Poxvirus, Vaccinia Virus, Structural Biology},
  pages        = {106},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Elucidating the structural determinants of the poxvirus core using multi-modal cryo-EM}},
  doi          = {10.15479/at:ista:18766},
  year         = {2024},
}

@inproceedings{18847,
  abstract     = {Machine Learning and AI have the potential to transform data-driven
scientific discovery, enabling accurate predictions for several scientific
phenomena. As many scientific questions are inherently causal, this paper looks
at the causal inference task of treatment effect estimation, where the outcome
of interest is recorded in high-dimensional observations in a Randomized
Controlled Trial (RCT). Despite being the simplest possible causal setting and
a perfect fit for deep learning, we theoretically find that many common choices
in the literature may lead to biased estimates. To test the practical impact of
these considerations, we recorded ISTAnt, the first real-world benchmark for
causal inference downstream tasks on high-dimensional observations as an RCT
studying how garden ants (Lasius neglectus) respond to microparticles applied
onto their colony members by hygienic grooming. Comparing 6 480 models
fine-tuned from state-of-the-art visual backbones, we find that the sampling
and modeling choices significantly affect the accuracy of the causal estimate,
and that classification accuracy is not a proxy thereof. We further validated
the analysis, repeating it on a synthetically generated visual data set
controlling the causal model. Our results suggest that future benchmarks should
carefully consider real downstream scientific questions, especially causal
ones. Further, we highlight guidelines for representation learning methods to
help answer causal questions in the sciences.},
  author       = {Cadei, Riccardo and Lindorfer, Lukas and Cremer, Sylvia and Schmid, Cordelia and Locatello, Francesco},
  booktitle    = {ICML 2024 Workshop AI4Science},
  publisher    = {Curran Associates},
  title        = {{Smoke and mirrors in causal downstream tasks}},
  volume       = {38},
  year         = {2024},
}

@inproceedings{18875,
  abstract     = {Current state-of-the-art methods for differentially private model training are based on matrix factorization techniques. However, these methods suffer from high computational overhead because they require numerically solving a demanding optimization problem to determine an approximately optimal factorization prior to the actual model training. In this work, we present a new matrix factorization approach, BSR, which overcomes this computational bottleneck. By exploiting properties of the standard matrix square root, BSR allows to efficiently handle also large-scale problems. For the key scenario of stochastic gradient descent with momentum and weight decay, we even derive analytical expressions for BSR that render the computational overhead negligible. We prove bounds on the approximation quality that hold both in the centralized and in the federated learning setting. Our numerical experiments demonstrate that models trained using BSR perform on par with the best existing methods, while completely avoiding their computational overhead.},
  author       = {Kalinin, Nikita and Lampert, Christoph},
  booktitle    = {38th Annual Conference on Neural Information Processing Systems},
  issn         = {1049-5258},
  location     = {Vancouver, Canada},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{Banded square root matrix factorization for differentially private model training}},
  volume       = {37},
  year         = {2024},
}

@inproceedings{18890,
  abstract     = {Deep Neural Collapse (DNC) refers to the surprisingly rigid structure of the data representations in the final layers of Deep Neural Networks (DNNs). Though the phenomenon has been measured in a variety of settings, its emergence is typically explained via data-agnostic approaches, such as the unconstrained features model. In this work, we introduce a data-dependent setting where DNC forms due to feature learning through the average gradient outer product (AGOP). The AGOP is defined with respect to a learned predictor and is equal to the uncentered covariance matrix of its input-output gradients averaged over the training dataset. The Deep Recursive Feature Machine (Deep RFM) is a method that constructs a neural network by iteratively mapping the data with the AGOP and applying an untrained random feature map. We demonstrate empirically that DNC occurs in Deep RFM across standard settings as a consequence of the projection with the AGOP matrix computed at each layer. Further, we theoretically explain DNC in Deep RFM in an asymptotic setting and as a result of kernel learning. We then provide evidence that this mechanism holds for neural networks more generally. In particular, we show that the right singular vectors and values of the weights can be responsible for the majority of within-class variability collapse for DNNs trained in the feature learning regime. As observed in recent work, this singular structure is highly correlated with that of the AGOP.},
  author       = {Beaglehole, Daniel and Súkeník, Peter and Mondelli, Marco and Belkin, Mikhail},
  booktitle    = {38th Annual Conference on Neural Information Processing Systems},
  issn         = {1049-5258},
  location     = {Vancouver, Canada},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{Average gradient outer product as a mechanism for deep neural collapse}},
  volume       = {37},
  year         = {2024},
}

@inproceedings{18891,
  abstract     = {Deep neural networks (DNNs) exhibit a surprising structure in their final layer
known as neural collapse (NC), and a growing body of works has currently investigated the propagation of neural collapse to earlier layers of DNNs – a phenomenon
called deep neural collapse (DNC). However, existing theoretical results are restricted to special cases: linear models, only two layers or binary classification.
In contrast, we focus on non-linear models of arbitrary depth in multi-class classification and reveal a surprising qualitative shift. As soon as we go beyond two
layers or two classes, DNC stops being optimal for the deep unconstrained features
model (DUFM) – the standard theoretical framework for the analysis of collapse.
The main culprit is a low-rank bias of multi-layer regularization schemes: this bias
leads to optimal solutions of even lower rank than the neural collapse. We support
our theoretical findings with experiments on both DUFM and real data, which show
the emergence of the low-rank structure in the solution found by gradient descent.},
  author       = {Súkeník, Peter and Lampert, Christoph and Mondelli, Marco},
  booktitle    = {38th Annual Conference on Neural Information Processing Systems},
  location     = {Vancouver, Canada},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{Neural collapse versus low-rank bias: Is deep neural collapse really optimal?}},
  volume       = {37},
  year         = {2024},
}

@misc{18895,
  abstract     = {ISTAnt is a new ecological dataset for social immunity and represents the first real-world benchmark for causal inference downstream tasks on high-dimensional observations. It analyzes grooming behavior in the ant Lasius neglectus in groups of three worker ants. The workers for the experiment were obtained from their laboratory stock colony, which had been collected from the field in 2022 in the Botanical Garden Jena, Germany. Ant collection and all experimental work were performed in compliance with international, national and institutional regulations and ethical guidelines. For the experiment, the body surface of one of the three ants was treated with a suspension of either of two microparticle types (diameter ~5 µm) to induce grooming by the two nestmates, which were individually color-coded by application of a dot of blue or orange paint, respectively. The three ants were housed in small plastic containers (diameter 28mm, height 30mm) with moistened, plastered ground and the interior walls covered with PTFE (polytetrafluoroethane) to hamper climbing by the ants. Filming occurred in a temperature- and humidity-controlled room at 23°C within a custom-made filming box with controlled lighting and ventilation conditions. We set up nine ant groups at a time (always containing both treatments) and placed them randomly on positions 1-9 marked on the floor in a 3x3 grid, about 3mm from each other. The experiment was performed on two consecutive days. Videos were acquired using a USB camera (FLIR blackfly S BFS-U3-120S4C, Teledyne FLIR) with a high-performance lens (HP Series 25mm Focal Length, Edmund optics 86-572) in OBS studio 29.0.0 \citep{bailey2017obs} at a framerate of 30 FPS and a resolution of 2500x2500 pixels. From each original video (105x105 mm), we generated nine individual videos .mkv (each ~32x32 mm, 770x770 pixels) by determining exact coordinates per container from one frame in GIMP 2.10.36 and cropping of the videos with FFmpeg 6.1.1. Annotation was performed over two consecutive days by three observers who had not been involved in the experimental setup or recording and were unaware of the treatment assignments to ensure bias-free behavioral annotation. They annotated the behavior of the ants during video observations, using custom-made software that saves the start and end frames of behaviors marked in a .csv file (see 'annotations' folder). In one of the videos, one of the nestmates' legs got inadvertently stuck to its body surface during the color-coding, interfering with its behavior, so the video was discarded. This left 44 videos from 5 independent setups (n=24 of treatment 1 and n=20 of treatment 2) of 10 minutes each for a total of 792 000 annotated frames (see 'video' folder). For each video, we provide the following information: the number of the set to which it belongs (1-5); the number of the position within the set reflecting the position of the ant group under the camera (1-9), for which we also provide ‘coordinates’ in the 3x3 grid (taking values -1/0/1 for both X and Y axis); treatment (1 or 2); the hour of the day when the recording was started (in 24h CEST); experimental day (A or B); the top left coordinate of the cropping square from the original video (CropX/CropY); the person annotating the video (given as A, B, C); the date of annotation (1: first day, 2: second day) and in which order the videos were annotated by each person, both reflecting a possible training effect of the person (see 'experiments_settings.csv' file).},
  author       = {Cadei, Riccardo and Locatello, Francesco and Cremer, Sylvia M and Lindorfer, Lukas and Schmid, Cordelia},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{ISTAnt}},
  doi          = {10.6084/M9.FIGSHARE.26484934.V2},
  year         = {2024},
}

@article{18961,
  abstract     = {Automated contact tracing (ACT) emerged as a promising measure to curb the spread of Covid-19. Users enable ACT on their smartphones to automatically record contacts with other users. If a user tests positive for the disease, they report their diagnosis to alert their contacts.
Designing effective ACT protocols is challenging since they need to be efficient and secure while also ensuring users' privacy. As ACT protocols necessarily leak some information by design, defining privacy is difficult. For example, a user cannot deny having met another user. Ideally, however, the user can plausibly deny everything else, in particular, when they met. We call this privacy property contact-time deniability.
While some early works discussed contact-time deniability informally, it has received little attention since then. We investigate deniability from a rigorous, theoretical point of view and arrive at the following impossibility result:
A decentralized protocol with unidirectional communication cannot be contact-time deniable and replay-secure. This holds even if malicious users treat smartphones as black-boxes.
 Unidirectional protocols are usually very efficient and many proposals are unidirectional, e.g., the widely-deployed Google-Apple Exposure Notifications. So the impossibility result considerably constrains the design space of efficient, secure, and private ACT protocols. However, it can also be used as a guide; we discuss several possibilities to achieve contact-time deniability in practice.},
  author       = {Günther, Christoph Ullrich and Pietrzak, Krzysztof Z},
  issn         = {2299-0984},
  journal      = {Proceedings on Privacy Enhancing Technologies},
  location     = {Bristol, UK/Virtual},
  number       = {4},
  pages        = {636--648},
  publisher    = {Privacy Enhancing Technologies Symposium Advisory Board},
  title        = {{Deniability in automated contact tracing: Impossibilities and possibilities}},
  doi          = {10.56553/popets-2024-0134},
  volume       = {2024},
  year         = {2024},
}

@inproceedings{18998,
  abstract     = {Word embeddings represent language vocabularies as clouds of d-dimensional points. We investigate how information is conveyed by the general shape of these clouds, instead of representing the semantic meaning of each token. Specifically, we use the notion of persistent homology from topological data analysis (TDA) to measure the distances between language pairs from the shape of their unlabeled embeddings. These distances quantify the degree of non-isometry of the embeddings. To distinguish whether these differences are random training errors or capture real information about the languages, we use the computed distance matrices to construct language phylogenetic trees over 81 Indo-European languages. Careful evaluation shows that our reconstructed trees exhibit strong and statistically-significant similarities to the reference.},
  author       = {Draganov, Ondrej and Skiena, Steven},
  booktitle    = {Findings of the Association for Computational Linguistics: EMNLP 2024},
  location     = {Miami, FL, United States},
  pages        = {12080--12099},
  publisher    = {Association for Computational Linguistics},
  title        = {{The shape of word embeddings: Quantifying non-isometry with topological data analysis}},
  doi          = {10.18653/v1/2024.findings-emnlp.705},
  year         = {2024},
}

@unpublished{18999,
  abstract     = {Exploring the shape of point configurations has been a key driver in the evolution of TDA (short for topological data analysis) since its infancy. This survey illustrates the recent efforts to broaden these ideas to model spatial interactions among multiple configurations, each distinguished by a color. It describes advances in this area and prepares the ground for further exploration by mentioning unresolved questions and promising research avenues while focusing on the overlap with discrete geometry.},
  author       = {Cultrera di Montesano, Sebastiano and Draganov, Ondrej and Edelsbrunner, Herbert and Saghafian, Morteza},
  booktitle    = {arXiv},
  title        = {{Chromatic topological data analysis}},
  doi          = {10.48550/ARXIV.2406.04102},
  year         = {2024},
}

@unpublished{19063,
  abstract     = {Instruction-tuned Large Language Models (LLMs) show impressive results in numerous practical applications, but they lack essential safety features that are common in other areas of computer science, particularly an explicit separation of instructions and data. This makes them vulnerable to manipulations such as indirect prompt injections and generally unsuitable for safety-critical tasks. Surprisingly, there is currently no established definition or benchmark to quantify this phenomenon. In this work, we close this gap by introducing a formal measure for instruction-data separation and an empirical variant that is calculable from a model's outputs. We also present a new dataset, SEP, that allows estimating the measure for real-world models. Our results on various LLMs show that the problem of instruction-data separation is real: all models fail to achieve high separation, and canonical mitigation techniques, such as prompt engineering and fine-tuning, either fail to substantially improve separation or reduce model utility. The source code and SEP dataset are openly accessible at https://github.com/egozverev/Shold-It-Be-Executed-Or-Processed.
},
  author       = {Zverev, Egor and Abdelnabi, Sahar and Tabesh, Soroush and Fritz, Mario and Lampert, Christoph},
  booktitle    = {arXiv},
  title        = {{Can LLMs separate instructions from data? And what do we even mean by that?}},
  doi          = {10.48550/arXiv.2403.06833},
  year         = {2024},
}

@unpublished{20071,
  abstract     = {Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".},
  author       = {Dvorak, Martin and Kolmogorov, Vladimir},
  booktitle    = {arXiv},
  keywords     = {Farkas lemma, linear programming, extended reals, calculus of inductive constructions},
  title        = {{Duality theory in linear optimization and its extensions -- formally  verified}},
  doi          = {10.48550/arXiv.2409.08119},
  year         = {2024},
}

@article{17202,
  abstract     = {Gate-tunable transmons (gatemons) employing semiconductor Josephson junctions have recently emerged as building blocks for hybrid quantum circuits. In this study, 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 and Crippa, Alessandro and Valentini, Marco and Janik, Marian and Baghumyan, Levon and Fabris, Giorgio and Kapoor, Lucky and Hassani, Farid and Fink, Johannes M and Calcaterra, Stefano and Chrastina, Daniel and Isella, Giovanni and Katsaros, Georgios},
  issn         = {2041-1723},
  journal      = {Nature Communications},
  publisher    = {Springer Nature},
  title        = {{A gate tunable transmon qubit in planar Ge}},
  doi          = {10.1038/s41467-024-50763-6},
  volume       = {15},
  year         = {2024},
}

@phdthesis{17208,
  abstract     = {Can current quantum computers provide a speedup over their classical counterparts for some kinds of problems? In this thesis, with a focus on ground state search/preparation, we address some of the challenges that both quantum annealing and variational quantum algorithms suffer from, hindering any possible practical speedup in comparison to the best classical counterparts. 

In the first part of the thesis, we study the performance of quantum annealing for solving a particular combinatorial optimization problem called 3-XOR satisfability (3-XORSAT). The classical problem is mapped into a ground state search of a 3-local classical Hamiltonian $H_C$. We consider how modifying the initial problem, by adding more interaction terms to the corresponding Hamiltonian, leads to the emergence of a first-order phase transition during the annealing process. This phenomenon causes the total annealing duration, $T$, required to prepare the ground state of $H_C$ with a high probability to increase exponentially with the size of the problem. Our findings indicate that with the growing complexity of problem instances, the likelihood of encountering first-order phase transitions also increases, making quantum annealing an impractical solution for these types of combinatorial optimization problems.

In the second part, we focus on the problem of barren plateaus in generic variational quantum algorithms. Barren plateaus correspond to flat regions in the parameter space where the gradient of the cost function is zero in expectation, and with the variance decaying exponentially with the system size, thus obstructing an efficient parameter optimization.  We propose an algorithm to circumvent Barren Plateaus by monitoring the entanglement entropy of k-local reduced density matrices, alongside a method for estimating entanglement entropy via classical shadow tomography. We illustrate the approach with the paradigmatic example of the variational quantum eigensolver, and show that our algorithm effectively avoids barren plateaus in the initialization as well as during the optimization stage. 

Lastly, in the last two Chapters of this thesis, we focus on the quantum approximate optimization algorithm (QAOA), originally introduced as an algorithm for solving generic combinatorial optimization problems in near-term quantum devices. Specifically, we focus on how to develop rigorous initialization strategies with guarantee improvement. Our motivation for this study lies in that for random initialization, the optimization typically leads to local minima with poor performance. Our main result corresponds to the analytical construction of index-1 saddle points or transition states, stationary points with a single direction of descent, as a tool for systematically exploring the QAOA optimization landscape. This leads us to propose a novel greedy parameter initialization strategy that guarantees for the energy to decrease with an increasing number of circuit layers. Furthermore, with precise estimates for the negative Hessian eigenvalue and its eigenvector, we establish a lower bound for energy improvement following a QAOA iteration.},
  author       = {Medina Ramos, Raimel A},
  issn         = {2663-337X},
  keywords     = {Quantum computing, Variational Quantum Algorithms, Optimization},
  pages        = {133},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Exploring the optimization landscape of variational quantum algorithms}},
  doi          = {10.15479/at:ista:17208},
  year         = {2024},
}

@inproceedings{17214,
  abstract     = {Current numerical algorithms for simulating friction fall in one of two camps: smooth solvers sacrifice the stable treatment of static friction in exchange for fast convergence, and non-smooth solvers accurately compute friction at convergence rates that are often prohibitive for large graphics applications. We introduce a novel bridge between these two ideas that computes static and dynamic friction stably and efficiently. Our key idea is to convert the highly constrained non-smooth problem into an unconstrained smooth problem using logarithmic barriers that converges to the exact solution as accuracy increases. We phrase the problem as an interior point primal-dual problem that can be solved efficiently with Newton iteration. We observe quadratic convergence despite the non-smooth nature of the original problem, and our method is well-suited for large systems of tightly packed objects with many contact points. We demonstrate the efficacy of our method with stable piles of grains and stacks of objects, complex granular flows, and robust interlocking assemblies of rigid bodies.},
  author       = {Chen, Yi-Lu and Ly, Mickaël and Wojtan, Christopher J},
  booktitle    = {Special Interest Group on Computer Graphics and Interactive Techniques Conference Conference Papers '24},
  isbn         = {9798400705250},
  keywords     = {physical simulation, frictional contact, rigid body mechanics, non-smooth dynamics},
  location     = {Denver, United States},
  publisher    = {Association for Computing Machinery},
  title        = {{Primal-dual non-smooth friction for rigid body animation}},
  doi          = {10.1145/3641519.3657485},
  year         = {2024},
}

@article{17219,
  abstract     = {We introduce a multi-material non-manifold mesh-based surface tracking algorithm that converts self-intersections into topological changes. Our algorithm generalizes prior work on manifold surface tracking with topological changes: it preserves surface features like mesh-based methods, and it robustly handles topological changes like level set methods. Our method also offers improved efficiency and robustness over the state of the art. We demonstrate the effectiveness of the approach on a range of examples, including complex soap film simulations with thousands of interacting bubbles, and boolean unions of non-manifold meshes consisting of millions of triangles.},
  author       = {Synak, Peter and Kalinov, Aleksei and Strugaru, Irina-Malina and Etemadihaghighi, Arian and Yang, Huidong and Wojtan, Christopher J},
  issn         = {1557-7368},
  journal      = {ACM Transactions on Graphics},
  keywords     = {surface tracking, topology change, non- manifold meshes, multi-material flows, solid modeling},
  number       = {4},
  publisher    = {Association for Computing Machinery},
  title        = {{Multi-material mesh-based surface tracking with implicit topology changes}},
  doi          = {10.1145/3658223},
  volume       = {43},
  year         = {2024},
}

@article{17278,
  abstract     = {An azeotrope is a constant boiling point mixture, and its behavior is important for fluid separation processes. Predicting azeotropes from atomistic simulations is difficult due to the complexities and convergence problems of Monte Carlo and free-energy perturbation techniques. Here, we present a methodology for predicting the azeotropes of binary mixtures, which computes the compositional dependence of chemical potentials from molecular dynamics simulations using the S0 method and employs experimental boiling point and vaporization enthalpy data. Using this methodology, we reproduce the azeotropes, or lack thereof, in five case studies, including ethanol/water, ethanol/isooctane, methanol/water, hydrazine/water, and acetone/chloroform mixtures. We find that it is crucial to use the experimental boiling point and vaporization enthalpy for reliable azeotrope predictions, as empirical force fields are not accurate enough for these quantities. Finally, we use regular solution models to rationalize the azeotropes and reveal that they tend to form when the mixture components have similar boiling points and strong interactions.},
  author       = {Wang, Xiaoyu and Cheng, Bingqing},
  issn         = {1089-7690},
  journal      = {Journal of Chemical Physics},
  number       = {3},
  publisher    = {AIP Publishing},
  title        = {{Integrating molecular dynamics simulations and experimental data for azeotrope predictions in binary mixtures}},
  doi          = {10.1063/5.0217232},
  volume       = {161},
  year         = {2024},
}

@article{17283,
  abstract     = {We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.},
  author       = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Novotný, Petr and Zikelic, Dorde},
  issn         = {2475-1421},
  journal      = {Proceedings of the ACM on Programming Languages},
  publisher    = {Association for Computing Machinery},
  title        = {{Equivalence and similarity refutation for probabilistic programs}},
  doi          = {10.1145/3656462},
  volume       = {8},
  year         = {2024},
}

@phdthesis{17336,
  abstract     = {This thesis deals with the study of stochastic processes and their ergodicity properties. The
variety of problems encountered calls for a set of different approaches, ranging from classical to
modern ones: a special place is held by probabilistic methods based on couplings, by functional
inequalities, and by the theory of gradient flows in the space of measures.

The material is organized as follows. Chapter 1 contains the introduction to this thesis, starting
with a general presentation of some of the relevant topics. Section 1.1 is dedicated to the
theory of gradient flows in metric spaces, and introduces the first contribution of this thesis
[DSMP24], which is presented in detail in Chapter 2. Section 1.2 moves to the topic of
curvature of Markov chains, concluding with a brief description of our second contribution
[Ped23], which is included in Chapter 3. Section 1.3 discusses applications of stochastic
processes to the theory of sampling, in particular the recent framework of score-based diffusion
models, and our contribution [PMM24], which is contained in Chapter 4. Section 1.4 discusses
some related problems, concerning the regularization properties of the heat flow. It serves
as a motivation for the work [BP24], which we report in Chapter 5. Finally, Section 1.5
discusses the last contribution of this thesis, which can be found in Chapter 6. It deals with
the convergence to equilibrium of a particular stochastic model from quantitative genetics:
this is established via some functional inequalities, which we prove with probabilistic arguments
based on couplings.
},
  author       = {Pedrotti, Francesco},
  issn         = {2663-337X},
  pages        = {183},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Functional inequalities and convergence of stochastic processes}},
  doi          = {10.15479/at:ista:17336},
  year         = {2024},
}

@misc{17344,
  abstract     = {This file contains the Mathematica notebook associated with the paper Effect of assortative mating and sexual selection on polygenic barriers to gene flow. It contains the numerical approximations, analyses, and simulations used in the study. },
  author       = {Surendranadh, Parvathy and Sachdeva, Himani},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Mathematica notebook for 'Effect of assortative mating and sexual selection on polygenic barriers to gene flow'}},
  doi          = {10.15479/AT:ISTA:17344},
  year         = {2024},
}

@unpublished{17361,
  abstract     = {We present symplectic structures on the shape space of unparameterized space curves that generalize the classical Marsden-Weinstein structure. Our method integrates the Liouville 1-form of the Marsden-Weinstein structure with Riemannian structures that have been introduced in mathematical shape analysis. We also derive Hamiltonian vector fields for several classical Hamiltonian functions with respect to these new symplectic structures.},
  author       = {Bauer, Martin and Ishida, Sadashige and Michor, Peter W.},
  booktitle    = {arXiv},
  keywords     = {space of space curves, symplectic stuctures},
  title        = {{Symplectic structures on the space of space curves}},
  doi          = {10.48550/arXiv.2407.19908},
  year         = {2024},
}

