@misc{11321, abstract = {Here are the research data underlying the publication "Effects of fine-scale population structure on the distribution of heterozygosity in a long-term study of Antirrhinum majus" Further information are summed up in the README document. }, author = {Surendranadh, Parvathy and Arathoon, Louise S and Baskett, Carina and Field, David and Pickup, Melinda and Barton, Nicholas H}, publisher = {Institute of Science and Technology Austria}, title = {{Effects of fine-scale population structure on the distribution of heterozygosity in a long-term study of Antirrhinum majus}}, doi = {10.15479/at:ista:11321}, year = {2022}, } @article{11330, abstract = {In this article we study the noncommutative transport distance introduced by Carlen and Maas and its entropic regularization defined by Becker and Li. We prove a duality formula that can be understood as a quantum version of the dual Benamou–Brenier formulation of the Wasserstein distance in terms of subsolutions of a Hamilton–Jacobi–Bellmann equation.}, author = {Wirth, Melchior}, issn = {15729613}, journal = {Journal of Statistical Physics}, number = {2}, publisher = {Springer Nature}, title = {{A dual formula for the noncommutative transport distance}}, doi = {10.1007/s10955-022-02911-9}, volume = {187}, year = {2022}, } @inproceedings{11331, abstract = {We propose separating the task of reliable transaction dissemination from transaction ordering, to enable high-performance Byzantine fault-tolerant quorum-based consensus. We design and evaluate a mempool protocol, Narwhal, specializing in high-throughput reliable dissemination and storage of causal histories of transactions. Narwhal tolerates an asynchronous network and maintains high performance despite failures. Narwhal is designed to easily scale-out using multiple workers at each validator, and we demonstrate that there is no foreseeable limit to the throughput we can achieve. Composing Narwhal with a partially synchronous consensus protocol (Narwhal-HotStuff) yields significantly better throughput even in the presence of faults or intermittent loss of liveness due to asynchrony. However, loss of liveness can result in higher latency. To achieve overall good performance when faults occur we design Tusk, a zero-message overhead asynchronous consensus protocol, to work with Narwhal. We demonstrate its high performance under a variety of configurations and faults. As a summary of results, on a WAN, Narwhal-Hotstuff achieves over 130,000 tx/sec at less than 2-sec latency compared with 1,800 tx/sec at 1-sec latency for Hotstuff. Additional workers increase throughput linearly to 600,000 tx/sec without any latency increase. Tusk achieves 160,000 tx/sec with about 3 seconds latency. Under faults, both protocols maintain high throughput, but Narwhal-HotStuff suffers from increased latency.}, author = {Danezis, George and Kokoris Kogias, Eleftherios and Sonnino, Alberto and Spiegelman, Alexander}, booktitle = {Proceedings of the 17th European Conference on Computer Systems}, isbn = {9781450391627}, location = {Rennes, France}, pages = {34--50}, publisher = {Association for Computing Machinery}, title = {{Narwhal and Tusk: A DAG-based mempool and efficient BFT consensus}}, doi = {10.1145/3492321.3519594}, year = {2022}, } @article{11332, abstract = {We show that the fluctuations of the largest eigenvalue of a real symmetric or complex Hermitian Wigner matrix of size N converge to the Tracy–Widom laws at a rate O(N^{-1/3+\omega }), as N tends to infinity. For Wigner matrices this improves the previous rate O(N^{-2/9+\omega }) obtained by Bourgade (J Eur Math Soc, 2021) for generalized Wigner matrices. Our result follows from a Green function comparison theorem, originally introduced by Erdős et al. (Adv Math 229(3):1435–1515, 2012) to prove edge universality, on a finer spectral parameter scale with improved error estimates. The proof relies on the continuous Green function flow induced by a matrix-valued Ornstein–Uhlenbeck process. Precise estimates on leading contributions from the third and fourth order moments of the matrix entries are obtained using iterative cumulant expansions and recursive comparisons for correlation functions, along with uniform convergence estimates for correlation kernels of the Gaussian invariant ensembles.}, author = {Schnelli, Kevin and Xu, Yuanyuan}, issn = {1432-0916}, journal = {Communications in Mathematical Physics}, pages = {839--907}, publisher = {Springer Nature}, title = {{Convergence rate to the Tracy–Widom laws for the largest Eigenvalue of Wigner matrices}}, doi = {10.1007/s00220-022-04377-y}, volume = {393}, year = {2022}, } @article{11333, abstract = {Adenosine triphosphate (ATP) is the energy source for various biochemical processes and biomolecular motors in living things. Development of ATP antagonists and their stimuli-controlled actions offer a novel approach to regulate biological processes. Herein, we developed azobenzene-based photoswitchable ATP antagonists for controlling the activity of motor proteins; cytoplasmic and axonemal dyneins. The new ATP antagonists showed reversible photoswitching of cytoplasmic dynein activity in an in vitro dynein-microtubule system due to the trans and cis photoisomerization of their azobenzene segment. Importantly, our ATP antagonists reversibly regulated the axonemal dynein motor activity for the force generation in a demembranated model of Chlamydomonas reinhardtii. We found that the trans and cis isomers of ATP antagonists significantly differ in their affinity to the ATP binding site.}, author = {Thayyil, Sampreeth and Nishigami, Yukinori and Islam, Muhammad J and Hashim, P. K. and Furuta, Ken'Ya and Oiwa, Kazuhiro and Yu, Jian and Yao, Min and Nakagaki, Toshiyuki and Tamaoki, Nobuyuki}, issn = {15213765}, journal = {Chemistry - A European Journal}, number = {30}, publisher = {Wiley}, title = {{Dynamic control of microbial movement by photoswitchable ATP antagonists}}, doi = {10.1002/chem.202200807}, volume = {28}, year = {2022}, } @article{11334, abstract = {Hybridization is a common evolutionary process with multiple possible outcomes. In vertebrates, interspecific hybridization has repeatedly generated parthenogenetic hybrid species. However, it is unknown whether the generation of parthenogenetic hybrids is a rare outcome of frequent hybridization between sexual species within a genus or the typical outcome of rare hybridization events. Darevskia is a genus of rock lizards with both hybrid parthenogenetic and sexual species. Using capture sequencing, we estimate phylogenetic relationships and gene flow among the sexual species, to determine how introgressive hybridization relates to the origins of parthenogenetic hybrids. We find evidence for widespread hybridization with gene flow, both between recently diverged species and deep branches. Surprisingly, we find no signal of gene flow between parental species of the parthenogenetic hybrids, suggesting that the parental pairs were either reproductively or geographically isolated early in their divergence. The generation of parthenogenetic hybrids in Darevskia is, then, a rare outcome of the total occurrence of hybridization within the genus, but the typical outcome when specific species pairs hybridize. Our results question the conventional view that parthenogenetic lineages are generated by hybridization in a window of divergence. Instead, they suggest that some lineages possess specific properties that underpin successful parthenogenetic reproduction.}, author = {Freitas, Susana and Westram, Anja M and Schwander, Tanja and Arakelyan, Marine and Ilgaz, Çetin and Kumlutas, Yusuf and Harris, David James and Carretero, Miguel A. and Butlin, Roger K.}, issn = {1558-5646}, journal = {Evolution}, number = {5}, pages = {899--914}, publisher = {Wiley}, title = {{Parthenogenesis in Darevskia lizards: A rare outcome of common hybridization, not a common outcome of rare hybridization}}, doi = {10.1111/evo.14462}, volume = {76}, year = {2022}, } @article{11336, abstract = {The generation of a correctly-sized cerebral cortex with all-embracing neuronal and glial cell-type diversity critically depends on faithful radial glial progenitor (RGP) cell proliferation/differentiation programs. Temporal RGP lineage progression is regulated by Polycomb Repressive Complex 2 (PRC2) and loss of PRC2 activity results in severe neurogenesis defects and microcephaly. How PRC2-dependent gene expression instructs RGP lineage progression is unknown. Here we utilize Mosaic Analysis with Double Markers (MADM)-based single cell technology and demonstrate that PRC2 is not cell-autonomously required in neurogenic RGPs but rather acts at the global tissue-wide level. Conversely, cortical astrocyte production and maturation is cell-autonomously controlled by PRC2-dependent transcriptional regulation. We thus reveal highly distinct and sequential PRC2 functions in RGP lineage progression that are dependent on complex interplays between intrinsic and tissue-wide properties. In a broader context our results imply a critical role for the genetic and cellular niche environment in neural stem cell behavior.}, author = {Amberg, Nicole and Pauler, Florian and Streicher, Carmen and Hippenmeyer, Simon}, issn = {2375-2548}, journal = {Science Advances}, number = {44}, publisher = {American Association for the Advancement of Science}, title = {{Tissue-wide genetic and cellular landscape shapes the execution of sequential PRC2 functions in neural stem cell lineage progression}}, doi = {10.1126/sciadv.abq1263}, volume = {8}, year = {2022}, } @article{11337, abstract = {Nonanalytic points in the return probability of a quantum state as a function of time, known as dynamical quantum phase transitions (DQPTs), have received great attention in recent years, but the understanding of their mechanism is still incomplete. In our recent work [Phys. Rev. Lett. 126, 040602 (2021)], we demonstrated that one-dimensional DQPTs can be produced by two distinct mechanisms, namely semiclassical precession and entanglement generation, leading to the definition of precession (pDQPTs) and entanglement (eDQPTs) dynamical quantum phase transitions. In this manuscript, we extend and investigate the notion of p- and eDQPTs in two-dimensional systems by considering semi-infinite ladders of varying width. For square lattices, we find that pDQPTs and eDQPTs persist and are characterized by similar phenomenology as in 1D: pDQPTs are associated with a magnetization sign change and a wide entanglement gap, while eDQPTs correspond to suppressed local observables and avoided crossings in the entanglement spectrum. However, DQPTs show higher sensitivity to the ladder width and other details, challenging the extrapolation to the thermodynamic limit especially for eDQPTs. Moving to honeycomb lattices, we also demonstrate that lattices with an odd number of nearest neighbors give rise to phenomenologies beyond the one-dimensional classification.}, author = {De Nicola, Stefano and Michailidis, Alexios and Serbyn, Maksym}, issn = {2469-9950}, journal = {Physical Review B}, publisher = {American Physical Society}, title = {{Entanglement and precession in two-dimensional dynamical quantum phase transitions}}, doi = {10.1103/PhysRevB.105.165149}, volume = {105}, year = {2022}, } @article{11339, abstract = {The interaction between a cell and its environment shapes fundamental intracellular processes such as cellular metabolism. In most cases growth rate is treated as a proximal metric for understanding the cellular metabolic status. However, changes in growth rate might not reflect metabolic variations in individuals responding to environmental fluctuations. Here we use single-cell microfluidics-microscopy combined with transcriptomics, proteomics and mathematical modelling to quantify the accumulation of glucose within Escherichia coli cells. In contrast to the current consensus, we reveal that environmental conditions which are comparatively unfavourable for growth, where both nutrients and salinity are depleted, increase glucose accumulation rates in individual bacteria and population subsets. We find that these changes in metabolic function are underpinned by variations at the translational and posttranslational level but not at the transcriptional level and are not dictated by changes in cell size. The metabolic response-characteristics identified greatly advance our fundamental understanding of the interactions between bacteria and their environment and have important ramifications when investigating cellular processes where salinity plays an important role.}, author = {Glover, Georgina and Voliotis, Margaritis and Łapińska, Urszula and Invergo, Brandon M. and Soanes, Darren and O’Neill, Paul and Moore, Karen and Nikolic, Nela and Petrov, Peter and Milner, David S. and Roy, Sumita and Heesom, Kate and Richards, Thomas A. and Tsaneva-Atanasova, Krasimira and Pagliara, Stefano}, issn = {2399-3642}, journal = {Communications Biology}, publisher = {Springer Nature}, title = {{Nutrient and salt depletion synergistically boosts glucose metabolism in individual Escherichia coli cells}}, doi = {10.1038/s42003-022-03336-6}, volume = {5}, year = {2022}, } @article{11340, abstract = {Like-charge attraction, driven by ionic correlations, challenges our understanding of electrostatics both in soft and hard matter. For two charged planar surfaces confining counterions and water, we prove that, even at relatively low correlation strength, the relevant physics is the ground-state one, oblivious of fluctuations. Based on this, we derive a simple and accurate interaction pressure that fulfills known exact requirements and can be used as an effective potential. We test this equation against implicit-solvent Monte Carlo simulations and against explicit-solvent simulations of cement and several types of clays. We argue that water destructuring under nanometric confinement drastically reduces dielectric screening, enhancing ionic correlations. Our equation of state at reduced permittivity therefore explains the exotic attractive regime reported for these materials, even in the absence of multivalent counterions.}, author = {Palaia, Ivan and Goyal, Abhay and Del Gado, Emanuela and Šamaj, Ladislav and Trizac, Emmanuel}, issn = {1520-5207}, journal = {Journal of Physical Chemistry B}, number = {16}, pages = {3143--3149}, publisher = {American Chemical Society}, title = {{Like-charge attraction at the nanoscale: Ground-state correlations and water destructuring}}, doi = {10.1021/acs.jpcb.2c00028}, volume = {126}, year = {2022}, } @article{11341, abstract = {Intragenic regions that are removed during maturation of the RNA transcript—introns—are universally present in the nuclear genomes of eukaryotes1. The budding yeast, an otherwise intron-poor species, preserves two sets of ribosomal protein genes that differ primarily in their introns2,3. Although studies have shed light on the role of ribosomal protein introns under stress and starvation4,5,6, understanding the contribution of introns to ribosome regulation remains challenging. Here, by combining isogrowth profiling7 with single-cell protein measurements8, we show that introns can mediate inducible phenotypic heterogeneity that confers a clear fitness advantage. Osmotic stress leads to bimodal expression of the small ribosomal subunit protein Rps22B, which is mediated by an intron in the 5′ untranslated region of its transcript. The two resulting yeast subpopulations differ in their ability to cope with starvation. Low levels of Rps22B protein result in prolonged survival under sustained starvation, whereas high levels of Rps22B enable cells to grow faster after transient starvation. Furthermore, yeasts growing at high concentrations of sugar, similar to those in ripe grapes, exhibit bimodal expression of Rps22B when approaching the stationary phase. Differential intron-mediated regulation of ribosomal protein genes thus provides a way to diversify the population when starvation threatens in natural environments. Our findings reveal a role for introns in inducing phenotypic heterogeneity in changing environments, and suggest that duplicated ribosomal protein genes in yeast contribute to resolving the evolutionary conflict between precise expression control and environmental responsiveness9.}, author = {Lukacisin, Martin and Espinosa-Cantú, Adriana and Bollenbach, Mark Tobias}, issn = {1476-4687}, journal = {Nature}, pages = {113--118}, publisher = {Springer Nature}, title = {{Intron-mediated induction of phenotypic heterogeneity}}, doi = {10.1038/s41586-022-04633-0}, volume = {605}, year = {2022}, } @article{11343, abstract = {Multistable systems are characterized by exhibiting domain coexistence, where each domain accounts for the different equilibrium states. In case these systems are described by vectorial fields, domains can be connected through topological defects. Vortices are one of the most frequent and studied topological defect points. Optical vortices are equally relevant for their fundamental features as beams with topological features and their applications in image processing, telecommunications, optical tweezers, and quantum information. A natural source of optical vortices is the interaction of light beams with matter vortices in liquid crystal cells. The rhythms that govern the emergence of matter vortices due to fluctuations are not established. Here, we investigate the nucleation mechanisms of the matter vortices in liquid crystal cells and establish statistical laws that govern them. Based on a stochastic amplitude equation, the law for the number of nucleated vortices as a function of anisotropy, voltage, and noise level intensity is set. Experimental observations in a nematic liquid crystal cell with homeotropic anchoring and a negative anisotropic dielectric constant under the influence of a transversal electric field show a qualitative agreement with the theoretical findings.}, author = {Aguilera, Esteban and Clerc, Marcel G. and Zambra, Valeska}, issn = {1573-269X}, journal = {Nonlinear Dynamics}, keywords = {Electrical and Electronic Engineering, Applied Mathematics, Mechanical Engineering, Ocean Engineering, Aerospace Engineering, Control and Systems Engineering}, pages = {3209--3218}, publisher = {Springer Nature}, title = {{Vortices nucleation by inherent fluctuations in nematic liquid crystal cells}}, doi = {10.1007/s11071-022-07396-5}, volume = {108}, year = {2022}, } @article{11344, abstract = {Until recently, Shigella and enteroinvasive Escherichia coli were thought to be primate-restricted pathogens. The base of their pathogenicity is the type 3 secretion system (T3SS) encoded by the pINV virulence plasmid, which facilitates host cell invasion and subsequent proliferation. A large family of T3SS effectors, E3 ubiquitin-ligases encoded by the ipaH genes, have a key role in the Shigella pathogenicity through the modulation of cellular ubiquitination that degrades host proteins. However, recent genomic studies identified ipaH genes in the genomes of Escherichia marmotae, a potential marmot pathogen, and an E. coli extracted from fecal samples of bovine calves, suggesting that non-human hosts may also be infected by these strains, potentially pathogenic to humans. We performed a comparative genomic study of the functional repertoires in the ipaH gene family in Shigella and enteroinvasive Escherichia from human and predicted non-human hosts. We found that fewer than half of Shigella genomes had a complete set of ipaH genes, with frequent gene losses and duplications that were not consistent with the species tree and nomenclature. Non-human host IpaH proteins had a diverse set of substrate-binding domains and, in contrast to the Shigella proteins, two variants of the NEL C-terminal domain. Inconsistencies between strains phylogeny and composition of effectors indicate horizontal gene transfer between E. coli adapted to different hosts. These results provide a framework for understanding of ipaH-mediated host-pathogens interactions and suggest a need for a genomic study of fecal samples from diseased animals.}, author = {Dranenko, NO and Tutukina, MN and Gelfand, MS and Kondrashov, Fyodor and Bochkareva, Olga}, issn = {2045-2322}, journal = {Scientific Reports}, publisher = {Springer Nature}, title = {{Chromosome-encoded IpaH ubiquitin ligases indicate non-human enteroinvasive Escherichia}}, doi = {10.1038/s41598-022-10827-3}, volume = {12}, year = {2022}, } @article{11351, abstract = {One hallmark of plant cells is their cell wall. They protect cells against the environment and high turgor and mediate morphogenesis through the dynamics of their mechanical and chemical properties. The walls are a complex polysaccharidic structure. Although their biochemical composition is well known, how the different components organize in the volume of the cell wall and interact with each other is not well understood and yet is key to the wall’s mechanical properties. To investigate the ultrastructure of the plant cell wall, we imaged the walls of onion (Allium cepa) bulbs in a near-native state via cryo-focused ion beam milling (cryo-FIB milling) and cryo-electron tomography (cryo-ET). This allowed the high-resolution visualization of cellulose fibers in situ. We reveal the coexistence of dense fiber fields bathed in a reticulated matrix we termed “meshing,” which is more abundant at the inner surface of the cell wall. The fibers adopted a regular bimodal angular distribution at all depths in the cell wall and bundled according to their orientation, creating layers within the cell wall. Concomitantly, employing homogalacturonan (HG)-specific enzymatic digestion, we observed changes in the meshing, suggesting that it is—at least in part—composed of HG pectins. We propose the following model for the construction of the abaxial epidermal primary cell wall: the cell deposits successive layers of cellulose fibers at −45° and +45° relative to the cell’s long axis and secretes the surrounding HG-rich meshing proximal to the plasma membrane, which then migrates to more distal regions of the cell wall.}, author = {Nicolas, William J. and Fäßler, Florian and Dutka, Przemysław and Schur, Florian KM and Jensen, Grant and Meyerowitz, Elliot}, issn = {0960-9822}, journal = {Current Biology}, keywords = {General Agricultural and Biological Sciences, General Biochemistry, Genetics and Molecular Biology}, number = {11}, pages = {P2375--2389}, publisher = {Elsevier}, title = {{Cryo-electron tomography of the onion cell wall shows bimodally oriented cellulose fibers and reticulated homogalacturonan networks}}, doi = {10.1016/j.cub.2022.04.024}, volume = {32}, year = {2022}, } @article{11353, abstract = {Micro- and nanoscale optical or microwave cavities are used in a wide range of classical applications and quantum science experiments, ranging from precision measurements, laser technologies to quantum control of mechanical motion. The dissipative photon loss via absorption, present to some extent in any optical cavity, is known to introduce thermo-optical effects and thereby impose fundamental limits on precision measurements. Here, we theoretically and experimentally reveal that such dissipative photon absorption can result in quantum feedback via in-loop field detection of the absorbed optical field, leading to the intracavity field fluctuations to be squashed or antisquashed. A closed-loop dissipative quantum feedback to the cavity field arises. Strikingly, this modifies the optical cavity susceptibility in coherent response measurements (capable of both increasing or decreasing the bare cavity linewidth) and causes excess noise and correlations in incoherent interferometric optomechanical measurements using a cavity, that is parametrically coupled to a mechanical oscillator. We experimentally observe such unanticipated dissipative dynamics in optomechanical spectroscopy of sideband-cooled optomechanical crystal cavitiess at both cryogenic temperature (approximately 8 K) and ambient conditions. The dissipative feedback introduces effective modifications to the optical cavity linewidth and the optomechanical scattering rate and gives rise to excess imprecision noise in the interferometric quantum measurement of mechanical motion. Such dissipative feedback differs fundamentally from a quantum nondemolition feedback, e.g., optical Kerr squeezing. The dissipative feedback itself always results in an antisqueezed out-of-loop optical field, while it can enhance the coexisting Kerr squeezing under certain conditions. Our result applies to cavity spectroscopy in both optical and superconducting microwave cavities, and equally applies to any dissipative feedback mechanism of different bandwidth inside the cavity. It has wide-ranging implications for future dissipation engineering, such as dissipation enhanced sideband cooling and Kerr squeezing, quantum frequency conversion, and nonreciprocity in photonic systems.}, author = {Qiu, Liu and Huang, Guanhao and Shomroni, Itay and Pan, Jiahe and Seidler, Paul and Kippenberg, Tobias J.}, issn = {26913399}, journal = {PRX Quantum}, number = {2}, publisher = {American Physical Society}, title = {{Dissipative quantum feedback in measurements using a parametrically coupled microcavity}}, doi = {10.1103/PRXQuantum.3.020309}, volume = {3}, year = {2022}, } @article{11354, abstract = {We construct a recurrent diffusion process with values in the space of probability measures over an arbitrary closed Riemannian manifold of dimension d≥2. The process is associated with the Dirichlet form defined by integration of the Wasserstein gradient w.r.t. the Dirichlet–Ferguson measure, and is the counterpart on multidimensional base spaces to the modified massive Arratia flow over the unit interval described in V. Konarovskyi and M.-K. von Renesse (Comm. Pure Appl. Math. 72 (2019) 764–800). Together with two different constructions of the process, we discuss its ergodicity, invariant sets, finite-dimensional approximations, and Varadhan short-time asymptotics.}, author = {Dello Schiavo, Lorenzo}, issn = {2168-894X}, journal = {Annals of Probability}, number = {2}, pages = {591--648}, publisher = {Institute of Mathematical Statistics}, title = {{The Dirichlet–Ferguson diffusion on the space of probability measures over a closed Riemannian manifold}}, doi = {10.1214/21-AOP1541}, volume = {50}, year = {2022}, } @inproceedings{11355, abstract = {Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees. Although there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory that is designed for ensuring system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. We illustrate the applicability of our framework with an example inspired from the automotive domain.}, author = {Bartocci, Ezio and Ferrere, Thomas and Henzinger, Thomas A and Nickovic, Dejan and Da Costa, Ana Oliveira}, booktitle = {Fundamental Approaches to Software Engineering}, isbn = {9783030994280}, issn = {1611-3349}, location = {Munich, Germany}, pages = {3--22}, publisher = {Springer Nature}, title = {{Information-flow interfaces}}, doi = {10.1007/978-3-030-99429-7_1}, volume = {13241}, year = {2022}, } @article{11356, author = {Chang, Cheng and Qin, Bingchao and Su, Lizhong and Zhao, Li Dong}, issn = {2095-9281}, journal = {Science Bulletin}, number = {11}, pages = {1105--1107}, publisher = {Elsevier}, title = {{Distinct electron and hole transports in SnSe crystals}}, doi = {10.1016/j.scib.2022.04.007}, volume = {67}, year = {2022}, } @phdthesis{11362, abstract = {Deep learning has enabled breakthroughs in challenging computing problems and has emerged as the standard problem-solving tool for computer vision and natural language processing tasks. One exception to this trend is safety-critical tasks where robustness and resilience requirements contradict the black-box nature of neural networks. To deploy deep learning methods for these tasks, it is vital to provide guarantees on neural network agents' safety and robustness criteria. This can be achieved by developing formal verification methods to verify the safety and robustness properties of neural networks. Our goal is to design, develop and assess safety verification methods for neural networks to improve their reliability and trustworthiness in real-world applications. This thesis establishes techniques for the verification of compressed and adversarially trained models as well as the design of novel neural networks for verifiably safe decision-making. First, we establish the problem of verifying quantized neural networks. Quantization is a technique that trades numerical precision for the computational efficiency of running a neural network and is widely adopted in industry. We show that neglecting the reduced precision when verifying a neural network can lead to wrong conclusions about the robustness and safety of the network, highlighting that novel techniques for quantized network verification are necessary. We introduce several bit-exact verification methods explicitly designed for quantized neural networks and experimentally confirm on realistic networks that the network's robustness and other formal properties are affected by the quantization. Furthermore, we perform a case study providing evidence that adversarial training, a standard technique for making neural networks more robust, has detrimental effects on the network's performance. This robustness-accuracy tradeoff has been studied before regarding the accuracy obtained on classification datasets where each data point is independent of all other data points. On the other hand, we investigate the tradeoff empirically in robot learning settings where a both, a high accuracy and a high robustness, are desirable. Our results suggest that the negative side-effects of adversarial training outweigh its robustness benefits in practice. Finally, we consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with systems over the infinite time horizon. Bayesian neural networks are probabilistic models for learning uncertainties in the data and are therefore often used on robotic and healthcare applications where data is inherently stochastic. We introduce a method for recalibrating Bayesian neural networks so that they yield probability distributions over safe decisions only. Our method learns a safety certificate that guarantees safety over the infinite time horizon to determine which decisions are safe in every possible state of the system. We demonstrate the effectiveness of our approach on a series of reinforcement learning benchmarks.}, author = {Lechner, Mathias}, isbn = {978-3-99078-017-6}, keywords = {neural networks, verification, machine learning}, pages = {124}, publisher = {Institute of Science and Technology Austria}, title = {{Learning verifiable representations}}, doi = {10.15479/at:ista:11362}, year = {2022}, } @unpublished{11366, abstract = {Adversarial training (i.e., training on adversarially perturbed input data) is a well-studied method for making neural networks robust to potential adversarial attacks during inference. However, the improved robustness does not come for free but rather is accompanied by a decrease in overall model accuracy and performance. Recent work has shown that, in practical robot learning applications, the effects of adversarial training do not pose a fair trade-off but inflict a net loss when measured in holistic robot performance. This work revisits the robustness-accuracy trade-off in robot learning by systematically analyzing if recent advances in robust training methods and theory in conjunction with adversarial robot learning can make adversarial training suitable for real-world robot applications. We evaluate a wide variety of robot learning tasks ranging from autonomous driving in a high-fidelity environment amenable to sim-to-real deployment, to mobile robot gesture recognition. Our results demonstrate that, while these techniques make incremental improvements on the trade-off on a relative scale, the negative side-effects caused by adversarial training still outweigh the improvements by an order of magnitude. We conclude that more substantial advances in robust learning methods are necessary before they can benefit robot learning tasks in practice.}, author = {Lechner, Mathias and Amini, Alexander and Rus, Daniela and Henzinger, Thomas A}, booktitle = {arXiv}, title = {{Revisiting the adversarial robustness-accuracy tradeoff in robot learning}}, doi = {10.48550/arXiv.2204.07373}, year = {2022}, }