arXiv subjects

Teng Zhang

Publications and source records attributed to Teng Zhang.

At least 19 recordsLinked to original sources

arXiv2026

Scaling Alternating-Bias-Assisted Annealing for Precision Transmon Frequency Targeting on Superconducting Quantum Processors

Recent advances in the alternating-bias-assisted annealing (ABAA) technique have successfully mitigated intrinsic Josephson-junction (JJ) fabrication variations. This new technique enables precision qubit frequency tuning alongside simplicity. However, it is critical to enhance tuning throughput and yield while investigating the factors that drive targeting performance as the technology scales. Here, we characterize ABAA tuning performance within a 150-mm wafer process flow and extend this technique to simultaneous, multi-channel tuning, demonstrating that a wafer-scale JJ resistance tuning precision of $\sigma=0.50\pm0.05\%$ alongside a component-level yield of $\ge 98.8\%$ can be achieved. Furthermore, we demonstrate a strong correlation between yield, tuning speed, and junction breakdown voltage, establishing the latter as a vital process control parameter for meeting production goals. Finally, we demonstrate a successful implementation of ABAA tuning on a quad-module quantum processor (Rigetti Cepheus-1-36Q), where we achieve an empirical frequency targeting precision of $\sigma \sim 30\text{ MHz}$ in both qubit and qubit-qubit detuning frequencies, contributing to high median two-qubit gate fidelities. These results confirm the efficacy and scalability of ABAA for high-precision Hamiltonian targeting, a critical enabler for modular superconducting quantum processor technology.

quant-ph↗

arXiv2026

A counterexample to Nevanlinna's century-old half-plane problem

Let $\mathbb{H}=\{z\in\mathbb{C}:\operatorname{Im}z>0\}$, and let $N(\mathbb{H})$ denote the Nevanlinna class in $\mathbb{H}$, consisting of meromorphic functions representable as quotients of two bounded analytic functions in $\mathbb{H}$. We construct a nonconstant meromorphic function $F$ on $\mathbb{C}$ such that $F^{-1}(\{0,1,\infty\})\subset\mathbb{R}$ and $F|_{\mathbb{H}}\notin N(\mathbb{H})$. Thus, omitting three distinct values of the Riemann sphere in a half-plane does not force a meromorphic function on $\mathbb{C}$ to be of bounded type there. This provides a counterexample to Nevanlinna's century-old half-plane problem.

math.CV↗

arXiv2026

The nonseparable case of Kadison's problem on orthonormal bases of unitaries for type $\mathrm{II}_1$ factors

In 1967, Kadison asked ``does every type $\mathrm{II}_1$ factor have an orthonormal (with respect to the trace) basis consisting of unitaries?''In a previous paper \cite{HTZ26}, He, Tang, and Zhang resolved Kadison's problem in the separable case. We prove the complementary nonseparable case and thereby resolve Kadison's problem in full. In fact, the basis may be chosen to consist of self-adjoint unitaries. The proof combines a relative norming lemma under small-density constraints, a finite-layer certification scheme ensuring that the relevant Hilbert-space projections are represented by bounded elements of the ambient factor, and a transfinite extension along the density character of $L^2(M,\tau)$.

math.OA↗

arXiv2026

KILVO: Kinematic-Inertial-LiDAR-Visual Odometry with Robust Multimodal Adaptation for Humanoid Robots

This article presents a kinematic-inertial-LiDAR-visual odometry for humanoid robots, called KILVO. Tailored to the platform features, requirements, and real-world complexity, it fully utilizes the sensors commonly equipped on humanoid robots, including joint encoders, IMU, LiDAR, and camera, within an asynchronous-sequential hybrid error-state iterated Kalman filter (ESIKF). Specifically, inertial data are used for prediction, leg kinematics are processed asynchronously at a high rate and provide proprioceptive constraints, while exteroception is updated sequentially, first by registering LiDAR points for geometric priors and then by updating the visual component via photometric errors. Moreover, the framework is elaborately designed with multimodal adaptation for resilience to sensor failures. A compact contact estimation module is also developed, sharing information with state estimation without additional sensors. Extensive experiments on public datasets and in the real world across multiple humanoid robots, gait patterns, and scenarios demonstrate that KILVO achieves highly competitive accuracy, efficiency, and output rates, with strong robustness against sensor degradation and failures, making it more suitable for humanoid robots than state-of-the-art fusion methods. Our code and datasets are released on GitHub.

cs.RO↗

arXiv2026

On the embedding rigidity problem for uniformly locally finite coarse spaces

In this paper, we construct countable uniformly locally finite metric spaces $X$ and $Y$ such that $C_u^*(X)$ is isomorphic to a hereditary $C^*$-subalgebra of $C_u^*(Y)$, while $X$ does not coarsely embed into$Y$. This gives a negative answer to the embedding rigidity problem for uniformly locally finite coarse spaces. On the positive side, we prove that, if every sparse subspace of $Y$ yields only compact ghost projections, then any isomorphism of $C_u^*(X)$ onto a hereditary $C^*$-subalgebra of $C_u^*(Y)$ induces an injective coarse embedding $X\to Y$. This strengthens a main result in \cite{BFV20} by upgrading coarse embeddability to injective coarse embeddability under the same hypothesis.

math.OA↗

arXiv2026

Isomorphism rigidity of uniform Roe algebras over arbitrary uniformly locally finite coarse spaces

Let $(X,\mathcal E)$ and $(Y,\mathcal F)$ be uniformly locally finite coarse spaces. We prove that every $C^*$-algebra isomorphism $C_u^*(X,\mathcal E)\cong C_u^*(Y,\mathcal F)$ forces $(X,\mathcal E)$ and $(Y,\mathcal F)$ to be bijectively coarsely equivalent. This completely resolves the isomorphism rigidity problem for uniform Roe algebras over arbitrary uniformly locally finite coarse spaces.

math.OA↗

arXiv2026

Impurity-Preserved Density Matrix Embedding Theory for Local Electronic Excitations

Density matrix embedding theory (DMET), which is usually based on a Schmidt decomposition of Slater determinants by partitioning the full system into impurity and environment in terms of local orthogonal orbitals (LOs), has demonstrated considerable promise in electronic structure studies because it enables the extraction of local properties using a high-level solver within an embedded impurity subsystem with greatly reduced degrees of freedom, thereby achieving a balance between accuracy and computational cost. However, its application to excited states of strongly correlated systems, such as lanthanide complexes, remains challenging because the errors relative to all-electron results can still be significant. Motivated by the success of the previously developed atomic orbitals (AOs) based DMET framework (Ai, Li, and Jiang, Phys. Rev. Lett. 2025, 135, 026502.), termed AO-DMET, which attains improved accuracy by constructing the embedded subspace based on a non-orthogonal decomposition of the Slater determinant in terms of AOs, we propose a new LO-based partitioning scheme that fully preserves the impurity space spanned by corresponding AOs and can achieve accuracy closely matching that of AO-DMET while retaining the orthogonal partition and its associated computational efficiency. The performance of the proposed method is demonstrated through excitation energy calculations for several representative lanthanide complexes. These results establish an efficient and accurate partitioning scheme for describing excited states in strongly correlated systems within the DMET framework.

physics.chem-ph↗

arXiv2026

Defense-in-Depth Runtime Safety in Move

Move is a smart-contract language used to execute transactions on the Aptos blockchain. Move programs execute in a sandboxed VM as typed bytecode. The VM statically verifies foundational safety properties like type safety and reference safety at code loading time. In principle, this design gives strong guarantees for Move. However, the static verification logic is complex and continually evolving with the language; like any software, it is not immune to bugs. In a live blockchain setting, a missed rule violation can translate directly into loss of assets, forged authority, or unrecoverable corruption of on-chain state. For this reason, Aptos relies on defense-in-depth runtime safety checks that independently verify the critical invariants during execution, providing protection against latent verifier bugs and malicious bytecode. This paper motivates and describes the runtime safety checks for Move on Aptos.

cs.PL↗

arXiv2026

The Sharp Phase Transition of Tyler's M-Estimator for Robust Subspace Recovery

Robust Subspace Recovery (RSR) aims to identify an underlying d-dimensional subspace from a dataset heavily corrupted by outliers. Complexity-theoretic results establish a threshold for the problem's computational hardness based on the dimension-scaled signal-to-noise ratio (DS-SNR): the problem is SSE-hard when the DS-SNR is strictly less than 1, and solvable via practical algorithms when it is greater than 1 under general position assumptions. However, the exact behavior of practical algorithms at the critical boundary DS-SNR = 1 has remained unknown. This work resolves the behavior of Tyler's M-estimator (TME) at this critical boundary, consequently establishing a sharp phase transition. Specifically, we prove that TME converges exactly to the true subspace for DS-SNR \geq 1 under a new stability condition, which is less restrictive than the general position assumptions used in prior literature. Our analysis utilizes a decomposition of the TME iterates within a majorization-minimization framework.

cs.IT↗

arXiv2026

The separable case of Kadison's problem on orthonormal bases of unitaries for type $\mathrm{II}_1$ factors

In 1967, Kadison asked ``does every type $\mathrm{II}_1$ factor have an orthonormal (with respect to the trace) basis consisting of unitaries?'' Using a noncommutative Lyapunov theorem of Akemann and Weaver, we prove that if $M$ is a separable diffuse finite von Neumann algebra with a normal faithful trace $\tau$, then $L^2(M,\tau)$ admits an orthonormal basis consisting of self-adjoint unitaries in $M$. Consequently, we affirm the separable case of the Kadison problem.

math.OA↗

arXiv2026

A Bayesian Adaptive Latent Mixture Model for Zero-Inflated Weighted Brain Connectome Analysis

Replicated weighted networks often exhibit many structural zeros alongside heterogeneous non-zero edge strengths. In structural connectomics, this zero-inflation coincides with subjects expressing overlapping, rather than discrete, connectivity patterns. To address these features, we propose a Bayesian adaptive latent mixture model for zero-inflated weighted networks. Our approach represents each subject network as a simplex mixture of shared low-rank latent score matrices, integrated with a hurdle likelihood that separates edge existence from conditional edge strength. A sparsity-coupling parameter enables absent edges to be either independent of, or informative about, the latent connectivity. For computation, we employ transformed Hamiltonian Monte Carlo on unconstrained coordinates, selecting the number of templates via predictive fit, held-out link prediction, and template stability. Theoretically, we establish posterior consistency, local asymptotic normality, a Bernstein--von Mises approximation, and predictive consistency for an identifiable quotient-space estimand under a fixed-template scenario. Simulations demonstrate performance gains over topology-only baselines in settings with mixed memberships or structure-informed sparsity. Applied to Human Connectome Project data, the model recovers stable latent score patterns and heterogeneous subject-level mixtures, with behavioural analyses serving strictly as exploratory annotations rather than confirmatory biomarker claims.

stat.ME↗

arXiv2026

Combining Mechanical and Agentic Specification Inference for Move

In this paper, we describe early work on a specification inference tool for the Move Prover that combines a weakest-precondition (WP) analysis over Move bytecode with an agentic coding CLI such as Claude Code. Specification inference reduces the boilerplate of writing specifications in Move: in order to verify a high-level property such as a global state invariant, pre- and post-conditions for the supporting functions typically have to be written by hand, which is tedious. In our setting, a Model Context Protocol (MCP) service exposes the WP analysis and the prover itself to the coding agent. The WP analysis provides a sound, mechanical baseline for inference; the AI is used precisely where WP is weakest -- for loop invariants and high-level idiomatic specifications such as monotonicity, conservation, and structural invariants. The Move Prover serves as the oracle that decides whether the generated specs are valid, and the agent is equipped to generate proof hints and to refine the inferred specification until verification succeeds. The tool has been applied to a corpus of canonical Move code, including code that uses higher-order functions, dynamic dispatch, global state, references, and various forms of loops.

cs.PL↗

arXiv2026

Formal Verification of Imperative First-Class Functions in Move

The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. Recently, Move on Aptos was extended with higher-order functions: imperative functions as first-class values that can be passed around, stored in data structs, and kept in persistent storage, enabling dynamic dispatch. This paper describes the representation of function values in the Move specification language and their implementation in MVP. We introduce behavioral predicates which characterize Move functions (aborts and pre/post conditions) by single-state or two-state predicates. We also introduce state labels for naming intermediate memory states in which expressions are evaluated and which allow to compose behavioral predicates to describe sequences of state transitions. On SMT level, function values are encoded by discriminating over the possible function values reaching a call site: when the concrete function is known, its effect is accounted for directly; when it is unknown (for example, a function parameter, or a closure loaded from storage), its behavioral predicates describe the effect. Our approach goes beyond, for example, Dafny, by supporting imperative first-class functions which can modify state via Rust-style references and global variables, and leads to more efficient SMT encodings than separation logic because of the static separation of memory enabled by Move. We further extend MVP's specification inference tool to work with function values: given arbitrary higher-order Move code, weakest-precondition analysis semi-automatically derives behavioral-predicate-based specifications, reducing the annotation burden and providing a validation pipeline for the new specification constructs.

cs.PL↗

arXiv2026

Dynamic Skill Lifecycle Management for Agentic Reinforcement Learning

Large language model agents increasingly rely on external skills to solve complex tasks, where skills act as modular units that extend their capabilities beyond what parametric memory alone supports. Existing methods assume external skills either accumulate as persistent guidance or internalized into the policy, eventually leading to zero-skill inference. We argue this assumption is overly restrictive, since with limited parametric capacity and uneven marginal contribution across skills, the optimal active skill set is non-monotonic, task- and stage-dependent. In this work, we propose SLIM, a framework of dynamic Skill LIfecycle Management for agentic reinforcement learning (RL), which treats the active external skill set as a dynamic optimization variable jointly updated with policy learning. Specifically, SLIM estimates each active skill's marginal external contribution through leave-one-skill-out validation, then applies three lifecycle operations: retaining high-value skills, retiring skills whose contribution becomes negligible after sufficient exposure, and expanding the skill bank when persistent failures reveal missing capability coverage. Experiments show that SLIM outperforms the best baselines by an average of 7.1% points across ALFWorld and SearchQA. Results further indicate that policy learning and external skill retention are not mutually exclusive: some skills are absorbed into the policy, while others continue to provide external value, supporting SLIM as a more general paradigm for skill-based agentic RL.

cs.LG↗

arXiv2026

ReflectDrive-2: Reinforcement-Learning-Aligned Self-Editing for Discrete Diffusion Driving

We introduce ReflectDrive-2, a masked discrete diffusion planner with separate action expert for autonomous driving that represents plans as discrete trajectory tokens and generates them through parallel masked decoding. This discrete token space enables in-place trajectory revision: AutoEdit rewrites selected tokens using the same model, without requiring an auxiliary refinement network. To train this capability, we use a two-stage procedure. First, we construct structure-aware perturbations of expert trajectories along longitudinal progress and lateral heading directions and supervise the model to recover the original expert trajectory. We then fine-tune the full decision--draft--reflect rollout with reinforcement learning (RL), assigning terminal driving reward to the final post-edit trajectory and propagating policy-gradient credit through full-rollout transitions. Full-rollout RL proves crucial for coupling drafting and editing: under supervised training alone, inference-time AutoEdit improves PDMS by at most $0.3$, whereas RL increases its gain to $1.9$. We also co-design an efficient reflective decoding stack for the decision--draft--reflect pipeline, combining shared-prefix KV reuse, Alternating Step Decode, and fused on-device unmasking. On NAVSIM, ReflectDrive-2 achieves $91.0$ PDMS with camera-only input and $94.8$ PDMS in a best-of-6 oracle setting, while running at $31.8$ ms average latency on NVIDIA Thor.

cs.RO↗

arXiv2026

Proof of the Agler--McCarthy entropy conjecture

In 2021, J.~Agler and J.~E. McCarthy proposed a two-step programme toward the celebrated Krzy\.z conjecture. The first step is to prove an entropy conjecture for polynomials whose zeros all lie on the unit circle; the second is to establish a full degree condition for extremal functions in the Krzy\.z conjecture. The purpose of this paper is to complete the first step. More precisely, we establish the sharp homogeneous entropy inequality for all non-constant polynomials with zeros on the unit circle and determine the equality cases.

math.CV↗

arXiv2026

Multistable energy landscapes for adaptive microscopic machines

The past few years have seen great strides in our ability to build synthetic microscopic machines. However, the function of such machines is often controlled directly by externally applied fields that deterministically specify the instantaneous machine dynamics. A crucial step towards machines that can respond adaptively to changes in their environment is the ability to program multiple functions that actuate under the same external driving field, so that their internal state dictates which function is executed. Here, we demonstrate that energy landscapes with designed multistability enable the same externally applied field to drive multiple configurations and dynamic responses in microscopic machines, enabling increasing levels of autonomy. We show three examples. First, we write a bistable energy landscape into a microscopic device, enabling the device to exhibit two stable mechanical configurations under the same external magnetic field. Next, adding a second degree of freedom enables differing dynamic responses to the same external magnetic field, which we direct into net displacement of the environment. Finally, we demonstrate how a microscopic machine with a continuous symmetry autonomously channels a single degree-of-freedom magnetic actuation into locomotion and adaptively responds to forces induced by other machines.

cond-mat.soft↗

arXiv2026

Colored Stallings graphs and Counterexamples to Stallings equalizer conjecture

The famous Stallings equalizer conjecture has remained open for more than 40 years, which states that, for any free group $F_n$ of rank $n\ge 2$, any free group $F$, and any two monomorphisms $g,h:F_n\to F,$ the equalizer $\Eq(g,h)=\{w\in F_n\mid g(w)=h(w)\}$ satisfies $\rk \Eq(g,h)\le n.$ The only known case is $n=2$, due to A. D. Logan in 2022. By introducing the notion of colored Stallings graphs, we show that for every integer $n\ge 2$ there exist monomorphisms $g,h:F_n\longrightarrow F_2$ such that$\rk\Eq(g,h)\ge 2n-2.$ This disproves Stallings equalizer conjecture for $n\ge 3$.

math.GR↗