arXiv subjects

Zhe Hou

Publications and source records attributed to Zhe Hou.

At least 55 records · Page 3Linked to original sources

arXiv2023

Second-order topology and supersymmetry in two-dimensional topological insulators

We unravel a fundamental connection between supersymmetry and a wide class of two dimensional second-order topological insulators (SOTI). This particular supersymmetry is induced by applying a half-integer Aharonov-Bohm flux $f=Φ/Φ_0=1/2$ through a hole in the system. Here, three symmetries are essential to establish this fundamental link: chiral symmetry, inversion symmetry, and mirror symmetry. At such a flux of half-integer value the mirror symmetry anticommutes with the inversion symmetry leading to a nontrivial $n=1$-SUSY representation for the absolute value of the Hamiltonian in each chiral sector, separately. This implies that a unique zero-energy state and an exact twofold degeneracy of all eigenstates with non-zero energy is found even at finite system size. For arbitrary smooth surfaces the link between 2D-SOTI and SUSY can be described within a universal low-energy theory in terms of an effective surface Hamiltonian which encompasses the whole class of supersymmetric periodic Witten models. Applying this general link to the prototypical example of a Bernevig-Hughes-Zhang(BHZ)-model with an in-plane Zeeman field, we analyze the entire phase diagram and identify a gapless Weyl phase separating the topological from the non-topological gapped phase. Surprisingly, we find that topological states localized at the outer surface remain in the Weyl phase, whereas topological hole states move to the outer surface and change their spatial symmetry upon approaching the Weyl phase. Therefore, the topological hole states can be tuned in a versatile manner opening up a route towards magnetic-field-induced topological engineering in multi-hole systems. Finally, we demonstrate the stability of localized states against deviation from half-integer flux, flux penetration into the sample, surface distortions, and random impurities for impurity strengths up to the order of the surface gap.

cond-mat.mes-hall↗

arXiv2022

Realization of a three-dimensional quantum Hall effect in a Zeeman-induced second order topological insulator on a torus

We propose a realization of a quantum Hall effect (QHE) in a second-order topological insulator (SOTI) in three dimensions (3D), which is mediated by hinge states on a torus surface. It results from the nontrivial interplay of the material structure, Zeeman effect, and the surface curvature. In contrast to the conventional 2D- and 3D-QHE, we show that the 3D-SOTI QHE is not affected by orbital effects of the applied magnetic field and exists in the presence of a Zeeman term only, induced e.g. by magnetic doping. To explain the 3D-SOTI QHE, we analyze the boundary charge for a 3D-SOTI and establish its universal dependence on the Aharonov-Bohm flux threading through the torus hole. Exploiting the fundamental relation between the boundary charge and the Hall conductance, we demonstrate the universal quantization of the latter, as well as its stability against random disorder potentials and continuous deformations of the torus surface.

cond-mat.mes-hall↗

arXiv2022

Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective

Neural networks have been widely applied in security applications such as spam and phishing detection, intrusion prevention, and malware detection. This black-box method, however, often has uncertainty and poor explainability in applications. Furthermore, neural networks themselves are often vulnerable to adversarial attacks. For those reasons, there is a high demand for trustworthy and rigorous methods to verify the robustness of neural network models. Adversarial robustness, which concerns the reliability of a neural network when dealing with maliciously manipulated inputs, is one of the hottest topics in security and machine learning. In this work, we survey existing literature in adversarial robustness verification for neural networks and collect 39 diversified research works across machine learning, security, and software engineering domains. We systematically analyze their approaches, including how robustness is formulated, what verification techniques are used, and the strengths and limitations of each technique. We provide a taxonomy from a formal verification perspective for a comprehensive understanding of this topic. We classify the existing techniques based on property specification, problem reduction, and reasoning strategies. We also demonstrate representative techniques that have been applied in existing studies with a sample model. Finally, we discuss open questions for future research.

cs.CR↗

arXiv2022

Geometric Theory for Program Testing

Formal methods for verification of programs are extended to testing of programs. Their combination is intended to lead to benefits in reliable program development, testing, and evolution. Our geometric theory of testing is intended to serve as the specification of a testing environment, included as the last stage of a toolchain that assists professional programmers, amateurs, and students of Computer Science. The testing environment includes an automated algorithm which locates errors in a test that has been run, and assists in correcting them. It does this by displaying, on a monitor screen, a stick diagram of causal chains in the execution of the program under test. The diagram can then be navigated backwards in the familiar style of a satnav following roads on a map. This will reveal selections of places at which the program should be modified to remove the error.

cs.SE↗

arXiv2022

MUC-driven Feature Importance Measurement and Adversarial Analysis for Random Forest

The broad adoption of Machine Learning (ML) in security-critical fields demands the explainability of the approach. However, the research on understanding ML models, such as Random Forest (RF), is still in its infant stage. In this work, we leverage formal methods and logical reasoning to develop a novel model-specific method for explaining the prediction of RF. Our approach is centered around Minimal Unsatisfiable Cores (MUC) and provides a comprehensive solution for feature importance, covering local and global aspects, and adversarial sample analysis. Experimental results on several datasets illustrate the high quality of our feature importance measurement. We also demonstrate that our adversarial analysis outperforms the state-of-the-art method. Moreover, our method can produce a user-centered report, which helps provide recommendations in real-life applications.

cs.LG↗

arXiv2022

An Executable Formal Model of the VHDL in Isabelle/HOL

In the hardware design process, hardware components are usually described in a hardware description language. Most of the hardware description languages, such as Verilog and VHDL, do not have mathematical foundation and hence are not fit for formal reasoning about the design. To enable formal reasoning in one of the most commonly used description language VHDL, we define a formal model of the VHDL language in Isabelle/HOL. Our model targets the functional part of VHDL designs used in industry, specifically the design of the LEON3 processor's integer unit. We cover a wide range of features in the VHDL language that are usually not modelled in the literature and define a novel operational semantics for it. Furthermore, our model can be exported to OCaml code for execution, turning the formal model into a VHDL simulator. We have tested our simulator against simple designs used in the literature, as well as the div32 module in the LEON3 design. The Isabelle/HOL code is publicly available: https://zhehou.github.io/apps/VHDLModel.zip

cs.CL↗

arXiv2021

Zero-energy Andreev bound states in iron-based superconductor Fe(Te,Se)

Majorana bound states have been predicted to exist in vortices of topological superconductors (SC). A realization of the Fu-Kane model, based on a three-dimensional topological insulator brought into proximity to an $s$-wave SC, in iron-based SC Fe(Te,Se) has attracted strong interest after pronounced zero-energy bias peaks were observed in several experiments. Here, we show that, by taking into account inhomogeneities of the chemical potential or the presence of potential impurities on the surface of Fe(Te,Se), the emergence of these zero-energy bias peaks can be explained by trivial Andreev bound states (ABSs) whose energies are close to zero. Our numerical simulations reveal that the ABSs behave similarly to Majorana bound states. ABSs are localized only on the, say, top surface and cannot be distinguished from their topological counterparts in transport experiments performed with STM tips. Thus, such ABSs deserve a careful investigation of their own.

cond-mat.mes-hall↗

arXiv2021

Extracting Optimal Explanations for Ensemble Trees via Logical Reasoning

Ensemble trees are a popular machine learning model which often yields high prediction performance when analysing structured data. Although individual small decision trees are deemed explainable by nature, an ensemble of large trees is often difficult to understand. In this work, we propose an approach called optimised explanation (OptExplain) that faithfully extracts global explanations of ensemble trees using a combination of logical reasoning, sampling and optimisation. Building on top of this, we propose a method called the profile of equivalent classes (ProClass), which uses MAX-SAT to simplify the explanation even further. Our experimental study on several datasets shows that our approach can provide high-quality explanations to large ensemble trees models, and it betters recent top-performers.

cs.LO↗

arXiv2020

Double Andreev reflections and double normal reflections in nodal-line semimetal-superconductor junctions

We study systematically the scattering processes and the conductance spectra in nodal-line semimetalsuperconductor junctions using the extended Blonder-Tinkham-Klapwijk theory. The coexistence of peculiar quadruple reflections are found, which are the specular normal reflection, the retro-normal reflection, the specular Andreev reflection and the retro-Andreev reflection. The incident angle dependence and the quasiparticle energy dependence of the double normal reflections and the double Andreev reflections are investigated under various values of parameters such as the interfacial barrier height, the chemical potentials, and the orbital coupling strength. It is found that the appearance and the disappearance of the reflections and their magnitudes can be controlled through tuning these parameters. The scattering mechanism for the reflections are analyzed in details from the viewpoint of the band structure. We also investigate the conductance spectra for the junctions, which show distinctive features and strong anisotropy about the orientation relationships of the nodal line and interface. The unique scattering processes and conductance spectra found in the junctions are helpful in designing superconducting electronic devices and searching for the nodal line in materials experimentally.

cond-mat.supr-con↗

arXiv2020

Electron interactions in strain-induced zero-energy flat band in twisted bilayer graphene near the magic angle

In the vicinity of the magic angle in twisted bilayer graphene (TBG), the two low-energy van Hove singularities (VHSs) become exceedingly narrow1-10 and many exotic correlated states, such as superconductivity, ferromagnetism, and topological phases, are observed11-16. Heterostrain, which is almost unavoidable in the TBG, can modify its single-particle band structure and lead to novel properties of the TBG that have never been considered so far. Here, we show that heterostrain in a TBG near the magic angle generates a new zero-energy flat band between the two VHSs. Doping the TBG to partially fill the zero-energy flat band, we observe a correlation-induced gap of about 10 meV that splits the flat band. By applying perpendicular magnetic fields, a large and linear response of the gap to magnetic fields is observed, attributing to the emergence of large orbital magnetic moments in the TBG when valley degeneracy of the flat band is lifted by electron-electron interactions. The orbital magnetic moment per moire supercell is measured as about 15 uB in the TBG.

cond-mat.str-el↗

arXiv2020

Nonlocal Correlation Mediated by Weyl Orbits

Nonlocality is an interesting topic in quantum physics and is usually mediated by some unique quantum states. Here we investigate a Weyl semimetal slab and find an exotic nonlocal correlation effect when placing two potential wells merely on the top and bottom surfaces. This correlation arises from the peculiar Weyl orbit in Weyl semimetals and is a consequence of the bulk-boundary correspondence in topological band theory. A giant nonlocal transport signal and a body breakdown by Weyl fermions are further uncovered, which can serve as signatures for verifying this nonlocal correlation effect experimentally. Our results extend a new member in the nonlocality family and have potential applications for designing new electric devices with fancy functions.

cond-mat.mes-hall↗

arXiv2019

A Movable Valley Switch Driven by Berry Phase in Bilayer Graphene Resonators

Since its discovery, Berry phase has been demonstrated to play an important role in many quantum systems. In gapped Bernal bilayer graphene, the Berry phase can be continuously tuned from zero to 2pi, which offers a unique opportunity to explore the tunable Berry phase on the physical phenomena. Here, we report experimental observation of Berry phases-induced valley splitting and crossing in moveable bilayer graphene p-n junction resonators. In our experiment, the bilayer graphene resonators are generated by combining the electric field of scanning tunneling microscope tip with the gap of bilayer graphene. A perpendicular magnetic field changes the Berry phase of the confined bound states in the resonators from zero to 2pi continuously and leads to the Berry phase difference for the two inequivalent valleys in the bilayer graphene. As a consequence, we observe giant valley splitting and unusual valley crossing of the lowest bound states. Our results indicate that the bilayer graphene resonators can be used to manipulate the valley degree of freedom in valleytronics.

cond-mat.mes-hall↗

arXiv2019

GRAVITAS: A Model Checking Based Planning and Goal Reasoning Framework for Autonomous Systems

While AI techniques have found many successful applications in autonomous systems, many of them permit behaviours that are difficult to interpret and may lead to uncertain results. We follow the "verification as planning" paradigm and propose to use model checking techniques to solve planning and goal reasoning problems for autonomous systems. We give a new formulation of Goal Task Network (GTN) that is tailored for our model checking based framework. We then provide a systematic method that models GTNs in the model checker Process Analysis Toolkit (PAT). We present our planning and goal reasoning system as a framework called Goal Reasoning And Verification for Independent Trusted Autonomous Systems (GRAVITAS) and discuss how it helps provide trustworthy plans in an uncertain environment. Finally, we demonstrate the proposed ideas in an experiment that simulates a survey mission performed by the REMUS-100 autonomous underwater vehicle.

cs.AI↗

arXiv2019

Silas: High Performance, Explainable and Verifiable Machine Learning

This paper introduces a new classification tool named Silas, which is built to provide a more transparent and dependable data analytics service. A focus of Silas is on providing a formal foundation of decision trees in order to support logical analysis and verification of learned prediction models. This paper describes the distinct features of Silas: The Model Audit module formally verifies the prediction model against user specifications, the Enforcement Learning module trains prediction models that are guaranteed correct, the Model Insight and Prediction Insight modules reason about the prediction model and explain the decision-making of predictions. We also discuss implementation details ranging from programming paradigm to memory management that help achieve high-performance computation.

cs.LG↗

arXiv2019

A formalisation of the SPARC TSO memory model for multi-core machine code

SPARC processors have many applications in mission-critical industries such as aviation and space engineering. Hence, it is important to provide formal frameworks that facilitate the verification of hardware and software that run on or interface with these processors. This paper presents the first mechanised SPARC Total Store Ordering (TSO) memory model which operates on top of an abstract model of the SPARC Instruction Set Architecture (ISA) for multi-core processors. Both models are specified in the theorem prover Isabelle/HOL. We formalise two TSO memory models: one is an adaptation of the axiomatic SPARC TSO model, the other is a novel operational TSO model which is suitable for verifying execution results. We prove that the operational model is sound and complete with respect to the axiomatic model. Finally, we give verification examples with two case studies drawn from the SPARCv9 manual.

cs.LO↗

arXiv2019

Anomalous spin Nernst effect in Weyl semimetals

The spin Nernst effect describes a transverse spin current induced by the longitudinal thermal gradient in a system with the spin-orbit coupling. Here we study the spin Nernst effect in a mesoscopic four-terminal cross-bar Weyl semimetal device under a perpendicular magnetic field. By using the tight-binding Hamiltonian combining with the nonequilibrium Green's function method, the three elements of the spin current in the transverse leads and then spin Nernst coefficients are obtained. The results show that the spin Nernst effect in the Weyl semimetal has the essential difference with the traditional one: The z direction spin currents is zero without the magnetic field while it appears under the magnetic field, and the x and y direction spin currents in the two transverse leads flows out or flows in together, in contrary to the traditional spin Nernst effect, in which the spin current is induced by the spin-orbit coupling and flows out from one lead and flows in on the other. So we call it the anomalous spin Nernst effect. In addition, we show that the Weyl semimetals have the center-reversal-type symmetry, the mirror-reversal-type symmetry and the electron-hole-type symmetry, which lead to the spin Nernst coefficients being odd function or even function of the Fermi energy, the magnetic field and the transverse terminals. Moreover, the spin Nernst effect in the Weyl semimetals are strongly anisotropic and its coefficients are strongly dependent on both the direction of thermal gradient and the direction of the transverse lead connection. Three non-equivalent connection modes (x-z, z-x and x-y modes) are studied in detail, and the spin Nernst coefficients for three different modes exhibit very different behaviors. These strongly anisotropic behaviors of the spin Nernst effect can be used as the characterization of magnetic Weyl semimetals.

cond-mat.mes-hall↗

arXiv2018

Non-Abelian Braiding of Chiral Majorana Fermions by Quantum Dots

The non-Abelian braiding of Majorana fermions is one of the most promising operations providing a key building block for the realization of topological quantum computation. Recently, the chiral Majorana fermions were observed in a hybrid junction btween a quantum anomalous Hall insulator and an s-wave superconductor. Here we show that if a quantum dot or Majorana zero mode couples to the chiral Majorana fermions, the resulting resonant exchange of chiral Majorana fermions can lead to the non-Abelian braiding. Remarkably, any operation in the braid group can be achieved by this scheme. We further propose electrical transport experiments to observe the braiding of four chiral Majorana fermions and demonstrate the non-Abelian braiding statistics in four-terminal devices of the hybrid junctions. Both a conductance peak due to the braiding and the braiding-order dependent conductance are predicted. These findings pave a way to perform any braiding operation of chiral Majorana fermions by electrically controllable quantum dots.

cond-mat.mes-hall↗

arXiv2018

Configuration-Sensitive Transport on Domain Walls of a Magnetic Topological Insulator

We study the transport on the domain wall (DW) in a magnetic topological insulator. The low-energy behaviors of the magnetic topological insulator are dominated by the chiral edge states (CESs). Here, we find that the spectrum and transport of the CESs at the DW are strongly dependent on the DW configuration. For a Bloch wall, two co-propagating CESs at the DW are doubly degenerate and the incoming electron is totally reflected. However, for a Néel wall, the two CESs are split and the transmission is determined by the interference between the CESs. Moreover, the effective Hamiltonian for the CESs indicates that the component of magnetization perpendicular to the wall leads to the distinct transport behavior. These findings may pave a way to realize the low-power-dissipation spintronics devices based on magnetic DWs.

cond-mat.mes-hall↗