BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Zhe Hou

Zhe Hou contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
cond-mat.mes-hallLogic in Computer Sciencecond-mat.mtrl-sciArtificial IntelligenceComputation and Languagecond-mat.str-elcond-mat.supr-conFormal Languages and Automata TheoryMachine LearningProgramming LanguagesSoftware Engineering

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
9works
0followers
11topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

9 published item(s)

preprint2026arXiv

Vibe Coding an LLM-powered Theorem Prover

We present Isabellm, an LLM-powered theorem prover for Isabelle/HOL that performs fully automatic proof synthesis. Isabellm works with any local LLM on Ollama and APIs such as Gemini CLI, and it is designed to run on consumer grade computers. The system combines a stepwise prover, which uses large language models to propose proof commands validated by Isabelle in a bounded search loop, with a higher-level proof planner that generates structured Isar outlines and attempts to fill and repair remaining gaps. The framework includes beam search for tactics, tactics reranker ML and RL models, premise selection with small transformer models, micro-RAG for Isar proofs built from AFP, and counter-example guided proof repair. All the code is implemented by GPT 4.1 - 5.2, Gemini 3 Pro, and Claude 4.5. Empirically, Isabellm can prove certain lemmas that defeat Isabelle's standard automation, including Sledgehammer, demonstrating the practical value of LLM-guided proof search. At the same time, we find that even state-of-the-art LLMs, such as GPT 5.2 Extended Thinking and Gemini 3 Pro struggle to reliably implement the intended fill-and-repair mechanisms with complex algorithmic designs, highlighting fundamental challenges in LLM code generation and reasoning. The code of Isabellm is available at https://github.com/zhehou/llm-isabelle

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

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.

0 citations0 reviewsNo code linkedOpen access