Researcher profile

Teng Zhang

Teng Zhang contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
7works
0followers
16topics
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

7 published item(s)

preprint2026arXiv

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.

preprint2026arXiv

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.

preprint2026arXiv

Schur--Horn type inequalities for hyperbolic polynomials

We establish a Schur--Horn type inequality for symmetric hyperbolic polynomials. As an immediate consequence, we resolve a conjecture of Nam Q. Le on Hadamard-type inequalities for hyperbolic polynomials. Our argument is based on the Schur--Horn theorem, the Birkhoff theorem, and Gårding's concavity theorem for hyperbolicity cones. Beyond the eigenvalue level, we develop a symmetrization principle on hyperbolicity cones: if a hyperbolic polynomial is invariant under a finite group action, then its value increases under the associated Reynolds operator (group averaging). Applied to the sign-flip symmetries of linear principal minor polynomials introduced by Blekherman et al., this yields a short proof of the hyperbolic Fischer--Hadamard inequalities for PSD-stable lpm polynomials.

preprint2026arXiv

Weak majorization inequalities for the cubic and quartic coefficients of $e^{(A+B)t}$ versus $e^{At}e^{Bt}$

Let $A,B\in\mathbb{H}_n$ and set $H=A+B$. For each integer $k\ge 1$ define $$ Q_k:=\sum_{p=0}^k \binom{k}{p} A^pB^{k-p}, R_k:=\Re\,Q_k=\frac{Q_k+Q_k^*}{2}. $$ Then $H^k=\left.\frac{d^k}{dt^k}e^{Ht}\right|_{t=0}$ and $Q_k=\left.\frac{d^k}{dt^k}(e^{At}e^{Bt})\right|_{t=0}$. We prove that, for $k=3,4,$ $$ λ(H^k)\prec_w σ(Q_k). $$ Equivalently, the eigenvalues of the cubic and quartic Taylor coefficients of $e^{(A+B)t}$ are weakly majorized by the singular values of the corresponding coefficients of the Golden--Thompson product $e^{At}e^{Bt}$. Our argument combines Ky Fan variational principles with explicit commutator identitiesfor $R_k-H^k$ at orders $k=3,4$, reducing the problem to the positivity of certain double-commutator trace forms tested against Ky Fan maximizing projections. We also record a general sufficient condition for higher orders based on commutator decompositions.

preprint2025arXiv

Beijing Normal University 12-meter Interferometric kHz GW Detector Prototype: Design and Scientific Prospects

Current gravitational-wave detectors have achieved remarkable sensitivity around 100 Hz, enabling ground-breaking discoveries. Enhancing sensitivity at higher frequencies in the kilohertz (kHz) range promises access to rich physics, particularly the extreme conditions during the merger stage of binary neutron stars. However, the high-frequency sensitivity of Michelson-based interferometers is fundamentally limited by their linear optical cavities, which are optimized for low-frequency signal enhancement. In [Phys. Rev. X 13, 021019 (2023)], a new configuration employing an L-shaped optical resonator was proposed to overcome this limitation, offering exceptional sensitivity in the kHz band. As a pathfinder, the 12-meter prototype at Beijing Normal University is designed to demonstrate the sensing and control schemes of this new kHz detector configuration and to explore its performance in the high-power regime with suspended optics. Beyond its primary scientific goal, the prototype also offers potential sensitivity in the megahertz (MHz) range, potentially enabling constraints on exotic sources. This paper presents an overview of the prototype, including its optical design and current development status of key components.

preprint2024arXiv

When $D$-companion matrix meets incomplete polynomials

In this paper, we provide a simple proof of a generalization of the Gauss-Lucas theorem. By using methods of D-companion matrix, we get the majorization relationship between the zeros of convex combinations of incomplete polynomials and an origin polynomial. Moreover, we prove that the set of all zeros of all convex combinations of incomplete polynomials coincides with the closed convex hull of zeros of the original polynomial. The location of zeros of convex combinations of incomplete polynomials is determined.

preprint2021arXiv

Enhancing high frequency sensitivity of gravitational wave detectors with sloshing-Sagnac interferometer

Sensitivity of gravitational-wave detectors is limited in the high-frequency band by quantum shot noise and eventually limited by the optical loss in signal recycling cavity. This limit is the main obstacle on the way to detect gravitational waves from the binary neutron star mergers in the current and the future generation detectors, as it does not depend on either the arm length, or the injected squeezing level. In this paper, we come up with the sloshing Sagnac interferometer topology, which can be obtained from the Michelson interferometer by optically connecting the end mirrors into an additional optical cavity. This transforms the interferometer into a triply-coupled cavity system capable of beating the loss-induced high-frequency limit of the signal-recycled Michelson interferometer. With advanced LIGO+ comparable parameters, a sloshing-Sagnac scheme can achieve 7 times better sensitivity at 2.5\,kHz or 4 times better signal to noise ratio for a typical waveform of binary neutron post merge. Being an evolution of Michelson interferometer, the sloshing-Sagnac interferometer can possibly be used as a topology for the future generation detectors and upgrade of current detectors.