-
Cost Analysis for Import and Export Using an Abstract Machine
Authors:
Benjamin Bennetzen,
Daniel Vang Kleist,
Emilie Sonne Steinmann,
Loke Walsted,
Nikolaj Rossander Kristensen,
Peter Buus Steffensen
Abstract:
This paper presents the syntax and reduction rules for an abstract machine based on the JavaScript XML language. We incorporate the notion of cost into our reduction rules, and create a type system that over-approximate this cost. This over-approximation results in an equation that may contain unknowns originating from while loops. We conclude with a formal proof of soundness of the type system fo…
▽ More
This paper presents the syntax and reduction rules for an abstract machine based on the JavaScript XML language. We incorporate the notion of cost into our reduction rules, and create a type system that over-approximate this cost. This over-approximation results in an equation that may contain unknowns originating from while loops. We conclude with a formal proof of soundness of the type system for our abstract machine, demonstrating that it over-approximates the cost of any terminating program. An implementation of the type system, constraint gathering, and the abstract machine is also presented
△ Less
Submitted 23 October, 2024;
originally announced October 2024.
-
A Type System to Ensure Non-Interference in ReScript
Authors:
Benjamin Bennetzen,
Daniel Vang Kleist,
Emilie Sonne Steinmann,
Loke Walsted,
Nikolaj Rossander Kristensen,
Peter Buus Steffensen
Abstract:
Protecting confidential data from leaking is a critical challenge in computer systems, particularly given the growing number of observers on the internet. Therefore, limiting information flow using robust security policies becomes increasingly vital. We focus on the non-interference policy, where the goal is to ensure that confidential data can not impact public data. This paper presents a type sy…
▽ More
Protecting confidential data from leaking is a critical challenge in computer systems, particularly given the growing number of observers on the internet. Therefore, limiting information flow using robust security policies becomes increasingly vital. We focus on the non-interference policy, where the goal is to ensure that confidential data can not impact public data. This paper presents a type system, for a subset of the ReScript syntax, designed to enforce non-interference. We conclude with a proof of soundness for the type system, demonstrating that if an expression is type-able, it is inherently non-interferent. In addition, we provide a brief overview of a type checker that implements the previously mentioned type system.
△ Less
Submitted 23 October, 2024;
originally announced October 2024.
-
Learning Generative Factors of EEG Data with Variational auto-encoders
Authors:
Maksim Zhdanov,
Saskia Steinmann,
Nico Hoffmann
Abstract:
Electroencephalography produces high-dimensional, stochastic data from which it might be challenging to extract high-level knowledge about the phenomena of interest. We address this challenge by applying the framework of variational auto-encoders to 1) classify multiple pathologies and 2) recover the neurological mechanisms of those pathologies in a data-driven manner. Our framework learns generat…
▽ More
Electroencephalography produces high-dimensional, stochastic data from which it might be challenging to extract high-level knowledge about the phenomena of interest. We address this challenge by applying the framework of variational auto-encoders to 1) classify multiple pathologies and 2) recover the neurological mechanisms of those pathologies in a data-driven manner. Our framework learns generative factors of data related to pathologies. We provide an algorithm to decode those factors further and discover how different pathologies affect observed data. We illustrate the applicability of the proposed approach to identifying schizophrenia, either followed or not by auditory verbal hallucinations. We further demonstrate the ability of the framework to learn disease-related mechanisms consistent with current domain knowledge. We also compare the proposed framework with several benchmark approaches and indicate its classification performance and interpretability advantages.
△ Less
Submitted 17 August, 2022; v1 submitted 4 June, 2022;
originally announced June 2022.
-
Investigating Brain Connectivity with Graph Neural Networks and GNNExplainer
Authors:
Maksim Zhdanov,
Saskia Steinmann,
Nico Hoffmann
Abstract:
Functional connectivity plays an essential role in modern neuroscience. The modality sheds light on the brain's functional and structural aspects, including mechanisms behind multiple pathologies. One such pathology is schizophrenia which is often followed by auditory verbal hallucinations. The latter is commonly studied by observing functional connectivity during speech processing. In this work,…
▽ More
Functional connectivity plays an essential role in modern neuroscience. The modality sheds light on the brain's functional and structural aspects, including mechanisms behind multiple pathologies. One such pathology is schizophrenia which is often followed by auditory verbal hallucinations. The latter is commonly studied by observing functional connectivity during speech processing. In this work, we have made a step toward an in-depth examination of functional connectivity during a dichotic listening task via deep learning for three groups of people: schizophrenia patients with and without auditory verbal hallucinations and healthy controls. We propose a graph neural network-based framework within which we represent EEG data as signals in the graph domain. The framework allows one to 1) predict a brain mental disorder based on EEG recording, 2) differentiate the listening state from the resting state for each group and 3) recognize characteristic task-depending connectivity. Experimental results show that the proposed model can differentiate between the above groups with state-of-the-art performance. Besides, it provides a researcher with meaningful information regarding each group's functional connectivity, which we validated on the current domain knowledge.
△ Less
Submitted 4 June, 2022;
originally announced June 2022.
-
Efficient recursive least squares solver for rank-deficient matrices
Authors:
Ruben Staub,
Stephan N. Steinmann
Abstract:
Updating a linear least squares solution can be critical for near real-time signalprocessing applications. The Greville algorithm proposes a simple formula for updating the pseudoinverse of a matrix A $\in$ R nxm with rank r. In this paper, we explicitly derive a similar formula by maintaining a general rank factorization, which we call rank-Greville. Based on this formula, we implemented a recurs…
▽ More
Updating a linear least squares solution can be critical for near real-time signalprocessing applications. The Greville algorithm proposes a simple formula for updating the pseudoinverse of a matrix A $\in$ R nxm with rank r. In this paper, we explicitly derive a similar formula by maintaining a general rank factorization, which we call rank-Greville. Based on this formula, we implemented a recursive least squares algorithm exploiting the rank-deficiency of A, achieving the update of the minimum-norm least-squares solution in O(mr) operations and, therefore, solving the linear least-squares problem from scratch in O(nmr) operations. We empirically confirmed that this algorithm displays a better asymptotic time complexity than LAPACK solvers for rank-deficient matrices. The numerical stability of rank-Greville was found to be comparable to Cholesky-based solvers. Nonetheless, our implementation supports exact numerical representations of rationals, due to its remarkable algebraic simplicity.
△ Less
Submitted 22 June, 2021;
originally announced June 2021.
-
Comparing Popular Simulation Environments in the Scope of Robotics and Reinforcement Learning
Authors:
Marian Körber,
Johann Lange,
Stephan Rediske,
Simon Steinmann,
Roland Glück
Abstract:
This letter compares the performance of four different, popular simulation environments for robotics and reinforcement learning (RL) through a series of benchmarks. The benchmarked scenarios are designed carefully with current industrial applications in mind. Given the need to run simulations as fast as possible to reduce the real-world training time of the RL agents, the comparison includes not o…
▽ More
This letter compares the performance of four different, popular simulation environments for robotics and reinforcement learning (RL) through a series of benchmarks. The benchmarked scenarios are designed carefully with current industrial applications in mind. Given the need to run simulations as fast as possible to reduce the real-world training time of the RL agents, the comparison includes not only different simulation environments but also different hardware configurations, ranging from an entry-level notebook up to a dual CPU high performance server. We show that the chosen simulation environments benefit the most from single core performance. Yet, using a multi core system, multiple simulations could be run in parallel to increase the performance.
△ Less
Submitted 8 March, 2021;
originally announced March 2021.
-
Implicit self-consistent electrolyte model in plane-wave density-functional theory
Authors:
Kiran Mathew,
V. S. Chaitanya Kolluru,
Srinidhi Mula,
Stephan N. Steinmann,
Richard G. Hennig
Abstract:
The ab-initio computational treatment of electrochemical systems requires an appropriate treatment of the solid/liquid interfaces. A fully quantum mechanical treatment of the interface is computationally demanding due to the large number of degrees of freedom involved. In this work, we describe a computationally efficient model where the electrode part of the interface is described at the density-…
▽ More
The ab-initio computational treatment of electrochemical systems requires an appropriate treatment of the solid/liquid interfaces. A fully quantum mechanical treatment of the interface is computationally demanding due to the large number of degrees of freedom involved. In this work, we describe a computationally efficient model where the electrode part of the interface is described at the density-functional theory (DFT) level, and the electrolyte part is represented through an implicit solvation model based on the Poisson-Boltzmann equation. We describe the implementation of the linearized Poisson-Boltzmann equation into the Vienna Ab-initio Simulation Package (VASP), a widely used DFT code, followed by validation and benchmarking of the method. To demonstrate the utility of the implicit electrolyte model, we apply it to study the surface energy of Cu crystal facets in an aqueous electrolyte as a function of applied electric potential. We show that the applied potential enables the control of the shape of nanocrystals from an octahedral to a truncated octahedral morphology with increasing potential.
△ Less
Submitted 24 October, 2019; v1 submitted 13 January, 2016;
originally announced January 2016.
-
Layer-dependent Electrocatalysis of MoS2 for Hydrogen Evolution
Authors:
Yifei Yu,
Shengyang Huang,
Yanpeng Li,
Stephan Steinmann,
Weitao Yang,
Linyou Cao
Abstract:
The quantitative correlation of the catalytic activity with microscopic structure of heterogeneous catalysts is a major challenge for the field of catalysis science. It requests synergistic capabilities to tailor the structure with atomic scale precision and to control the catalytic reaction to proceed through well-defined pathways. Here we leverage on the controlled growth of MoS2 atomically thin…
▽ More
The quantitative correlation of the catalytic activity with microscopic structure of heterogeneous catalysts is a major challenge for the field of catalysis science. It requests synergistic capabilities to tailor the structure with atomic scale precision and to control the catalytic reaction to proceed through well-defined pathways. Here we leverage on the controlled growth of MoS2 atomically thin films to demonstrate that the catalytic activity of MoS2 for the hydrogen evolution reaction decreases by a factor of ~4.47 for the addition of every one more layer. Similar layer dependence is also found in edge-riched MoS2 pyramid platelets. This layer-dependent electrocatalysis can be correlated to the hopping of electrons in the vertical direction of MoS2 layers over an interlayer potential barrier, which is found to be 0.119V and consistent with theoretical calculations. Our results point out that increasing the hopping efficiency of electrons in the vertical direction is a key for the development of high-efficiency two-dimensional material catalysts.
△ Less
Submitted 14 September, 2013;
originally announced September 2013.
-
Equivalence of Particle-Particle Random Phase Approximation Correlation Energy and Ladder-Coupled-Cluster-Double
Authors:
Degao Peng,
Stephan N. Steinmann,
Helen van Aggelen,
Weitao Yang
Abstract:
We present an analytical proof and numerical demonstrations of the equivalence of the correlation energy from particle-particle random phase approximation (pp-RPA) and ladder-couple-cluster-doubles (ladder-CCD). These two theories reduce to the identical algebraic matrix equation and correlation energy expressions, under the assumption that the pp-RPA equation is stable. The numerical examples ill…
▽ More
We present an analytical proof and numerical demonstrations of the equivalence of the correlation energy from particle-particle random phase approximation (pp-RPA) and ladder-couple-cluster-doubles (ladder-CCD). These two theories reduce to the identical algebraic matrix equation and correlation energy expressions, under the assumption that the pp-RPA equation is stable. The numerical examples illustrate that the correlation energy missed by pp-RPA in comparison with couple-cluster single and double is largely canceled out when considering reaction energies. This theoretical connection will be beneficial to future pp-RPA studies based on the well established couple cluster theory.
△ Less
Submitted 24 June, 2013;
originally announced June 2013.
