@inproceedings{9040, abstract = {Machine learning and formal methods have complimentary benefits and drawbacks. In this work, we address the controller-design problem with a combination of techniques from both fields. The use of black-box neural networks in deep reinforcement learning (deep RL) poses a challenge for such a combination. Instead of reasoning formally about the output of deep RL, which we call the wizard, we extract from it a decision-tree based model, which we refer to as the magic book. Using the extracted model as an intermediary, we are able to handle problems that are infeasible for either deep RL or formal methods by themselves. First, we suggest, for the first time, a synthesis procedure that is based on a magic book. We synthesize a stand-alone correct-by-design controller that enjoys the favorable performance of RL. Second, we incorporate a magic book in a bounded model checking (BMC) procedure. BMC allows us to find numerous traces of the plant under the control of the wizard, which a user can use to increase the trustworthiness of the wizard and direct further training.}, author = {Alamdari, Par Alizadeh and Avni, Guy and Henzinger, Thomas A and Lukina, Anna}, booktitle = {Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design}, isbn = {9783854480426}, issn = {2708-7824}, location = {Online Conference}, pages = {138--147}, publisher = {TU Wien Academic Press}, title = {{Formal methods with a touch of magic}}, doi = {10.34727/2020/isbn.978-3-85448-042-6_21}, year = {2020}, } @inbook{9096, author = {Schmid-Hempel, Paul and Cremer, Sylvia M}, booktitle = {Encyclopedia of Social Insects}, editor = {Starr, C}, isbn = {9783319903064}, publisher = {Springer Nature}, title = {{Parasites and Pathogens}}, doi = {10.1007/978-3-319-90306-4_94-1}, year = {2020}, } @inproceedings{9103, abstract = {We introduce LRT-NG, a set of techniques and an associated toolset that computes a reachtube (an over-approximation of the set of reachable states over a given time horizon) of a nonlinear dynamical system. LRT-NG significantly advances the state-of-the-art Langrangian Reachability and its associated tool LRT. From a theoretical perspective, LRT-NG is superior to LRT in three ways. First, it uses for the first time an analytically computed metric for the propagated ball which is proven to minimize the ball’s volume. We emphasize that the metric computation is the centerpiece of all bloating-based techniques. Secondly, it computes the next reachset as the intersection of two balls: one based on the Cartesian metric and the other on the new metric. While the two metrics were previously considered opposing approaches, their joint use considerably tightens the reachtubes. Thirdly, it avoids the "wrapping effect" associated with the validated integration of the center of the reachset, by optimally absorbing the interval approximation in the radius of the next ball. From a tool-development perspective, LRT-NG is superior to LRT in two ways. First, it is a standalone tool that no longer relies on CAPD. This required the implementation of the Lohner method and a Runge-Kutta time-propagation method. Secondly, it has an improved interface, allowing the input model and initial conditions to be provided as external input files. Our experiments on a comprehensive set of benchmarks, including two Neural ODEs, demonstrates LRT-NG’s superior performance compared to LRT, CAPD, and Flow*.}, author = {Gruenbacher, Sophie and Cyranka, Jacek and Lechner, Mathias and Islam, Md Ariful and Smolka, Scott A. and Grosu, Radu}, booktitle = {Proceedings of the 59th IEEE Conference on Decision and Control}, isbn = {9781728174471}, issn = {07431546}, location = {Jeju Islang, Korea (South)}, pages = {1556--1563}, publisher = {IEEE}, title = {{Lagrangian reachtubes: The next generation}}, doi = {10.1109/CDC42340.2020.9304042}, volume = {2020}, year = {2020}, } @article{9104, abstract = {We consider the free additive convolution of two probability measures μ and ν on the real line and show that μ ⊞ v is supported on a single interval if μ and ν each has single interval support. Moreover, the density of μ ⊞ ν is proven to vanish as a square root near the edges of its support if both μ and ν have power law behavior with exponents between −1 and 1 near their edges. In particular, these results show the ubiquity of the conditions in our recent work on optimal local law at the spectral edges for addition of random matrices [5].}, author = {Bao, Zhigang and Erdös, László and Schnelli, Kevin}, issn = {15658538}, journal = {Journal d'Analyse Mathematique}, pages = {323--348}, publisher = {Springer Nature}, title = {{On the support of the free additive convolution}}, doi = {10.1007/s11854-020-0135-2}, volume = {142}, year = {2020}, } @article{9114, abstract = {Microwave photonics lends the advantages of fiber optics to electronic sensing and communication systems. In contrast to nonlinear optics, electro-optic devices so far require classical modulation fields whose variance is dominated by electronic or thermal noise rather than quantum fluctuations. Here we demonstrate bidirectional single-sideband conversion of X band microwave to C band telecom light with a microwave mode occupancy as low as 0.025 ± 0.005 and an added output noise of less than or equal to 0.074 photons. This is facilitated by radiative cooling and a triply resonant ultra-low-loss transducer operating at millikelvin temperatures. The high bandwidth of 10.7 MHz and total (internal) photon conversion efficiency of 0.03% (0.67%) combined with the extremely slow heating rate of 1.1 added output noise photons per second for the highest available pump power of 1.48 mW puts near-unity efficiency pulsed quantum transduction within reach. Together with the non-Gaussian resources of superconducting qubits this might provide the practical foundation to extend the range and scope of current quantum networks in analogy to electrical repeaters in classical fiber optic communication.}, author = {Hease, William J and Rueda Sanchez, Alfredo R and Sahu, Rishabh and Wulf, Matthias and Arnold, Georg M and Schwefel, Harald G.L. and Fink, Johannes M}, issn = {2691-3399}, journal = {PRX Quantum}, number = {2}, publisher = {American Physical Society}, title = {{Bidirectional electro-optic wavelength conversion in the quantum ground state}}, doi = {10.1103/prxquantum.1.020315}, volume = {1}, year = {2020}, } @inbook{9123, abstract = {Inversions are chromosomal rearrangements where the order of genes is reversed. Inversions originate by mutation and can be under positive, negative or balancing selection. Selective effects result from potential disruptive effects on meiosis, gene disruption at inversion breakpoints and, importantly, the effects of inversions as modifiers of recombination rate: Recombination is strongly reduced in individuals heterozygous for an inversion, allowing for alleles at different loci to be inherited as a ‘block’. This may lead to a selective advantage whenever it is favourable to keep certain combinations of alleles associated, for example under local adaptation with gene flow. Inversions can cover a considerable part of a chromosome and contain numerous loci under different selection pressures, so that the resulting overall effects may be complex. Empirical data from various systems show that inversions may have a prominent role in local adaptation, speciation, parallel evolution, the maintenance of polymorphism and sex chromosome evolution.}, author = {Westram, Anja M and Faria, Rui and Butlin, Roger and Johannesson, Kerstin}, booktitle = {eLS}, isbn = {9780470016176}, publisher = {Wiley}, title = {{Inversions and Evolution}}, doi = {10.1002/9780470015902.a0029007}, year = {2020}, } @article{9156, abstract = {The morphometric approach [11, 14] writes the solvation free energy as a linear combination of weighted versions of the volume, area, mean curvature, and Gaussian curvature of the space-filling diagram. We give a formula for the derivative of the weighted Gaussian curvature. Together with the derivatives of the weighted volume in [7], the weighted area in [4], and the weighted mean curvature in [1], this yields the derivative of the morphometric expression of solvation free energy.}, author = {Akopyan, Arseniy and Edelsbrunner, Herbert}, issn = {2544-7297}, journal = {Computational and Mathematical Biophysics}, number = {1}, pages = {74--88}, publisher = {De Gruyter}, title = {{The weighted Gaussian curvature derivative of a space-filling diagram}}, doi = {10.1515/cmb-2020-0101}, volume = {8}, year = {2020}, } @article{9157, abstract = {Representing an atom by a solid sphere in 3-dimensional Euclidean space, we get the space-filling diagram of a molecule by taking the union. Molecular dynamics simulates its motion subject to bonds and other forces, including the solvation free energy. The morphometric approach [12, 17] writes the latter as a linear combination of weighted versions of the volume, area, mean curvature, and Gaussian curvature of the space-filling diagram. We give a formula for the derivative of the weighted mean curvature. Together with the derivatives of the weighted volume in [7], the weighted area in [3], and the weighted Gaussian curvature [1], this yields the derivative of the morphometric expression of the solvation free energy.}, author = {Akopyan, Arseniy and Edelsbrunner, Herbert}, issn = {2544-7297}, journal = {Computational and Mathematical Biophysics}, number = {1}, pages = {51--67}, publisher = {De Gruyter}, title = {{The weighted mean curvature derivative of a space-filling diagram}}, doi = {10.1515/cmb-2020-0100}, volume = {8}, year = {2020}, } @article{9160, abstract = {Auxin is a key hormonal regulator, that governs plant growth and development in concert with other hormonal pathways. The unique feature of auxin is its polar, cell-to-cell transport that leads to the formation of local auxin maxima and gradients, which coordinate initiation and patterning of plant organs. The molecular machinery mediating polar auxin transport is one of the important points of interaction with other hormones. Multiple hormonal pathways converge at the regulation of auxin transport and form a regulatory network that integrates various developmental and environmental inputs to steer plant development. In this review, we discuss recent advances in understanding the mechanisms that underlie regulation of polar auxin transport by multiple hormonal pathways. Specifically, we focus on the post-translational mechanisms that contribute to fine-tuning of the abundance and polarity of auxin transporters at the plasma membrane and thereby enable rapid modification of the auxin flow to coordinate plant growth and development.}, author = {Semeradova, Hana and Montesinos López, Juan C and Benková, Eva}, issn = {2590-3462}, journal = {Plant Communications}, number = {3}, publisher = {Elsevier}, title = {{All roads lead to auxin: Post-translational regulation of auxin transport by multiple hormonal pathways}}, doi = {10.1016/j.xplc.2020.100048}, volume = {1}, year = {2020}, } @article{9194, abstract = {Quantum transduction, the process of converting quantum signals from one form of energy to another, is an important area of quantum science and technology. The present perspective article reviews quantum transduction between microwave and optical photons, an area that has recently seen a lot of activity and progress because of its relevance for connecting superconducting quantum processors over long distances, among other applications. Our review covers the leading approaches to achieving such transduction, with an emphasis on those based on atomic ensembles, opto-electro-mechanics, and electro-optics. We briefly discuss relevant metrics from the point of view of different applications, as well as challenges for the future.}, author = {Lauk, Nikolai and Sinclair, Neil and Barzanjeh, Shabir and Covey, Jacob P and Saffman, Mark and Spiropulu, Maria and Simon, Christoph}, issn = {2058-9565}, journal = {Quantum Science and Technology}, number = {2}, publisher = {IOP Publishing}, title = {{Perspectives on quantum transduction}}, doi = {10.1088/2058-9565/ab788a}, volume = {5}, year = {2020}, } @article{9195, abstract = {Quantum information technology based on solid state qubits has created much interest in converting quantum states from the microwave to the optical domain. Optical photons, unlike microwave photons, can be transmitted by fiber, making them suitable for long distance quantum communication. Moreover, the optical domain offers access to a large set of very well‐developed quantum optical tools, such as highly efficient single‐photon detectors and long‐lived quantum memories. For a high fidelity microwave to optical transducer, efficient conversion at single photon level and low added noise is needed. Currently, the most promising approaches to build such systems are based on second‐order nonlinear phenomena such as optomechanical and electro‐optic interactions. Alternative approaches, although not yet as efficient, include magneto‐optical coupling and schemes based on isolated quantum systems like atoms, ions, or quantum dots. Herein, the necessary theoretical foundations for the most important microwave‐to‐optical conversion experiments are provided, their implementations are described, and the current limitations and future prospects are discussed.}, author = {Lambert, Nicholas J. and Rueda Sanchez, Alfredo R and Sedlmeir, Florian and Schwefel, Harald G. L.}, issn = {2511-9044}, journal = {Advanced Quantum Technologies}, number = {1}, publisher = {Wiley}, title = {{Coherent conversion between microwave and optical photons - An overview of physical implementations}}, doi = {10.1002/qute.201900077}, volume = {3}, year = {2020}, } @article{9196, abstract = {In order to provide a local description of a regular function in a small neighbourhood of a point x, it is sufficient by Taylor’s theorem to know the value of the function as well as all of its derivatives up to the required order at the point x itself. In other words, one could say that a regular function is locally modelled by the set of polynomials. The theory of regularity structures due to Hairer generalizes this observation and provides an abstract setup, which in the application to singular SPDE extends the set of polynomials by functionals constructed from, e.g., white noise. In this context, the notion of Taylor polynomials is lifted to the notion of so-called modelled distributions. The celebrated reconstruction theorem, which in turn was inspired by Gubinelli’s \textit {sewing lemma}, is of paramount importance for the theory. It enables one to reconstruct a modelled distribution as a true distribution on Rd which is locally approximated by this extended set of models or “monomials”. In the original work of Hairer, the error is measured by means of Hölder norms. This was then generalized to the whole scale of Besov spaces by Hairer and Labbé. It is the aim of this work to adapt the analytic part of the theory of regularity structures to the scale of Triebel–Lizorkin spaces.}, author = {Hensel, Sebastian and Rosati, Tommaso}, issn = {1730-6337}, journal = {Studia Mathematica}, keywords = {General Mathematics}, number = {3}, pages = {251--297}, publisher = {Instytut Matematyczny}, title = {{Modelled distributions of Triebel–Lizorkin type}}, doi = {10.4064/sm180411-11-2}, volume = {252}, year = {2020}, } @article{9197, abstract = {In this paper we introduce and study all-pay bidding games, a class of two player, zero-sum games on graphs. The game proceeds as follows. We place a token on some vertex in the graph and assign budgets to the two players. Each turn, each player submits a sealed legal bid (non-negative and below their remaining budget), which is deducted from their budget and the highest bidder moves the token onto an adjacent vertex. The game ends once a sink is reached, and Player 1 pays Player 2 the outcome that is associated with the sink. The players attempt to maximize their expected outcome. Our games model settings where effort (of no inherent value) needs to be invested in an ongoing and stateful manner. On the negative side, we show that even in simple games on DAGs, optimal strategies may require a distribution over bids with infinite support. A central quantity in bidding games is the ratio of the players budgets. On the positive side, we show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation for the optimal strategy for that ratio. We also implement it, show that it performs well, and suggests interesting properties of these games. Then, given an outcome c, we show an algorithm for finding the necessary and sufficient initial ratio for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally, while the general case has not previously been studied, solving the specific game in which Player 1 wins iff he wins the first two auctions, has been long stated as an open question, which we solve.}, author = {Avni, Guy and Ibsen-Jensen, Rasmus and Tkadlec, Josef}, isbn = {9781577358350}, issn = {2374-3468}, journal = {Proceedings of the AAAI Conference on Artificial Intelligence}, location = {New York, NY, United States}, number = {02}, pages = {1798--1805}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{All-pay bidding games on graphs}}, doi = {10.1609/aaai.v34i02.5546}, volume = {34}, year = {2020}, } @inproceedings{9198, abstract = {The optimization of multilayer neural networks typically leads to a solution with zero training error, yet the landscape can exhibit spurious local minima and the minima can be disconnected. In this paper, we shed light on this phenomenon: we show that the combination of stochastic gradient descent (SGD) and over-parameterization makes the landscape of multilayer neural networks approximately connected and thus more favorable to optimization. More specifically, we prove that SGD solutions are connected via a piecewise linear path, and the increase in loss along this path vanishes as the number of neurons grows large. This result is a consequence of the fact that the parameters found by SGD are increasingly dropout stable as the network becomes wider. We show that, if we remove part of the neurons (and suitably rescale the remaining ones), the change in loss is independent of the total number of neurons, and it depends only on how many neurons are left. Our results exhibit a mild dependence on the input dimension: they are dimension-free for two-layer networks and depend linearly on the dimension for multilayer networks. We validate our theoretical findings with numerical experiments for different architectures and classification tasks.}, author = {Shevchenko, Alexander and Mondelli, Marco}, booktitle = {Proceedings of the 37th International Conference on Machine Learning}, pages = {8773--8784}, publisher = {ML Research Press}, title = {{Landscape connectivity and dropout stability of SGD solutions for over-parameterized neural networks}}, volume = {119}, year = {2020}, } @inproceedings{9202, abstract = {We propose a novel hybridization method for stability analysis that over-approximates nonlinear dynamical systems by switched systems with linear inclusion dynamics. We observe that existing hybridization techniques for safety analysis that over-approximate nonlinear dynamical systems by switched affine inclusion dynamics and provide fixed approximation error, do not suffice for stability analysis. Hence, we propose a hybridization method that provides a state-dependent error which converges to zero as the state tends to the equilibrium point. The crux of our hybridization computation is an elegant recursive algorithm that uses partial derivatives of a given function to obtain upper and lower bound matrices for the over-approximating linear inclusion. We illustrate our method on some examples to demonstrate the application of the theory for stability analysis. In particular, our method is able to establish stability of a nonlinear system which does not admit a polynomial Lyapunov function.}, author = {Garcia Soto, Miriam and Prabhakar, Pavithra}, booktitle = {2020 IEEE Real-Time Systems Symposium}, issn = {2576-3172}, location = {Houston, TX, USA }, pages = {244--256}, publisher = {IEEE}, title = {{Hybridization for stability verification of nonlinear switched systems}}, doi = {10.1109/RTSS49844.2020.00031}, year = {2020}, } @article{9208, abstract = {Bending-active structures are able to efficiently produce complex curved shapes from flat panels. The desired deformation of the panels derives from the proper selection of their elastic properties. Optimized panels, called FlexMaps, are designed such that, once they are bent and assembled, the resulting static equilibrium configuration matches a desired input 3D shape. The FlexMaps elastic properties are controlled by locally varying spiraling geometric mesostructures, which are optimized in size and shape to match specific bending requests, namely the global curvature of the target shape. The design pipeline starts from a quad mesh representing the input 3D shape, which defines the edge size and the total amount of spirals: every quad will embed one spiral. Then, an optimization algorithm tunes the geometry of the spirals by using a simplified pre-computed rod model. This rod model is derived from a non-linear regression algorithm which approximates the non-linear behavior of solid FEM spiral models subject to hundreds of load combinations. This innovative pipeline has been applied to the project of a lightweight plywood pavilion named FlexMaps Pavilion, which is a single-layer piecewise twisted arch that fits a bounding box of 3.90x3.96x3.25 meters. This case study serves to test the applicability of this methodology at the architectural scale. The structure is validated via FE analyses and the fabrication of the full scale prototype.}, author = {Laccone, Francesco and Malomo, Luigi and Perez Rodriguez, Jesus and Pietroni, Nico and Ponchio, Federico and Bickel, Bernd and Cignoni, Paolo}, issn = {25233971}, journal = {SN Applied Sciences}, number = {9}, publisher = {Springer Nature}, title = {{A bending-active twisted-arch plywood structure: Computational design and fabrication of the FlexMaps Pavilion}}, doi = {10.1007/s42452-020-03305-w}, volume = {2}, year = {2020}, } @inproceedings{9221, abstract = {Recent works have shown that gradient descent can find a global minimum for over-parameterized neural networks where the widths of all the hidden layers scale polynomially with N (N being the number of training samples). In this paper, we prove that, for deep networks, a single layer of width N following the input layer suffices to ensure a similar guarantee. In particular, all the remaining layers are allowed to have constant widths, and form a pyramidal topology. We show an application of our result to the widely used LeCun’s initialization and obtain an over-parameterization requirement for the single wide layer of order N2. }, author = {Nguyen, Quynh and Mondelli, Marco}, booktitle = {34th Conference on Neural Information Processing Systems}, location = {Vancouver, Canada}, pages = {11961–11972}, publisher = {Curran Associates}, title = {{Global convergence of deep networks with one wide layer followed by pyramidal topology}}, volume = {33}, year = {2020}, } @misc{9222, author = {Katsaros, Georgios}, publisher = {Institute of Science and Technology Austria}, title = {{Transport data for: Site‐controlled uniform Ge/Si Hut wires with electrically tunable spin–orbit coupling}}, doi = {10.15479/AT:ISTA:9222}, year = {2020}, } @article{9249, abstract = {Rhombic dodecahedron is a space filling polyhedron which represents the close packing of spheres in 3D space and the Voronoi structures of the face centered cubic (FCC) lattice. In this paper, we describe a new coordinate system where every 3-integer coordinates grid point corresponds to a rhombic dodecahedron centroid. In order to illustrate the interest of the new coordinate system, we propose the characterization of 3D digital plane with its topological features, such as the interrelation between the thickness of the digital plane and the separability constraint we aim to obtain. We also present the characterization of 3D digital lines and study it as the intersection of multiple digital planes. Characterization of 3D digital sphere with relevant topological features is proposed as well along with the 48-symmetry appearing in the new coordinate system.}, author = {Biswas, Ranita and Largeteau-Skapin, Gaëlle and Zrour, Rita and Andres, Eric}, issn = {2353-3390}, journal = {Mathematical Morphology - Theory and Applications}, number = {1}, pages = {143--158}, publisher = {De Gruyter}, title = {{Digital objects in rhombic dodecahedron grid}}, doi = {10.1515/mathm-2020-0106}, volume = {4}, year = {2020}, } @inproceedings{9299, abstract = {We call a multigraph non-homotopic if it can be drawn in the plane in such a way that no two edges connecting the same pair of vertices can be continuously transformed into each other without passing through a vertex, and no loop can be shrunk to its end-vertex in the same way. It is easy to see that a non-homotopic multigraph on n>1 vertices can have arbitrarily many edges. We prove that the number of crossings between the edges of a non-homotopic multigraph with n vertices and m>4n edges is larger than cm2n for some constant c>0 , and that this bound is tight up to a polylogarithmic factor. We also show that the lower bound is not asymptotically sharp as n is fixed and m⟶∞ .}, author = {Pach, János and Tardos, Gábor and Tóth, Géza}, booktitle = {28th International Symposium on Graph Drawing and Network Visualization}, isbn = {9783030687656}, issn = {1611-3349}, location = {Virtual, Online}, pages = {359--371}, publisher = {Springer Nature}, title = {{Crossings between non-homotopic edges}}, doi = {10.1007/978-3-030-68766-3_28}, volume = {12590}, year = {2020}, }