arXiv subjects

Yuxiang Peng

Publications and source records attributed to Yuxiang Peng.

At least 19 recordsLinked to original sources

arXiv2026

Quantum-Inspired Hamiltonian Descent for Radiation Therapy Treatment Planning

Direct incorporation of dose-volume constraints into inverse radiotherapy planning leads to large mixed-integer optimization problems that accurately represent clinical requirements but are computationally challenging. We develop and evaluate a quantum-inspired approach for automated dose-volume-constrained intensity-modulated radiation therapy (IMRT) and intensity-modulated proton therapy (IMPT) planning. Clinical requirements are formulated as mixed-integer optimization problems, with binary variables representing dose-volume constraint violations. Patient-specific dose-influence matrices are generated at the photon control-point and proton spot levels, and intensities are optimized using Quantum-Inspired Hamiltonian Descent (QIHD). We evaluate QIHD on eight clinical cases: four IMRT (two prostate, one head-and-neck, and one liver) and four IMPT (two lung, one prostate, and one liver). The IMRT formulations contain 27,621 to 112,565 variables and are solved in 5 to 32 minutes, while the IMPT formulations contain 69,861 to 221,342 variables and are solved in 11 to 35 minutes on an NVIDIA RTX 4060 GPU. QIHD produces dose distributions satisfying clinical protocols without manual intervention. In comparison, a CPU implementation of Gurobi fails to solve most tested mixed-integer formulations within several hours. These results demonstrate the computational feasibility of GPU-accelerated QIHD for automated photon and proton treatment planning. Prospective clinical validation and implementation of decomposed subproblems on quantum hardware remain future directions.

math.OC↗

arXiv2026

Analog Quantum Experiments Meet Automatic Differentiation - from Programs to Atoms

Gradient-based optimization of analog quantum hardware poses a concrete programming problem: given an executable experiment P(θ) that returns only measurement samples, what executable experiment should the system run to obtain (d/dθ_ell)P(θ)? Conventional automatic differentiation cannot propagate through the inaccessible quantum state, while finite differences require a noise-sensitive step size and analytic gradient identities cover only parts of an experiment. We present DiffSimuQ, which shows that a broad class of open-loop analog quantum experiments is closed under automatic differentiation. A compositional transformation maps P(θ) to a derivative program D_ell[P(θ)] in the same language whose expected outcome is exactly the derivative. Only continuous evolution requires a strategy-specific rule, and we give two realizations. Our Nyquist shift rule (NSR) applies to general time-dependent evolution: we prove that the observable response to shifting the Hamiltonian along its tangent is band-limited even for non-commuting controls, enabling exact reconstruction from shifted executions. For involutory generators, a parameter-shift realization (PSR) inserts a parameter-independent operation at a sampled time. Because derivative programs remain ordinary programs, source and derivative experiments share one compiler, which reuses the source realization, lowers branches to device-ready neutral-atom controls, and selects between NSR and PSR based on estimated cost. Under device noise, the exact derivative programs differentiate the objective realized by the device, with hardware realization errors treated separately. In machine-level noisy emulation, NSR and PSR avoid the finite-difference error floor and improve closed-loop optimization; they win in complementary cost regimes, while each derivative branch at 1000 qubits add at most 0.3% to source compilation time.

quant-ph↗

arXiv2026

Structure-Aware Equivalence for Evaluating Autoformalized Statements

Evaluating autoformalized mathematical statements requires determining whether a candidate preserves the mathematical claim intended by a trusted reference. Existing methods approach this problem from complementary directions: reference-free learned evaluators estimate semantic agreement but are not constrained to a formal equivalence relation, while reference-based proof methods typically employ whole-statement logical equivalence to provide formal certificates, which is too coarse for translation fidelity and may identify mathematically unrelated statements. We introduce Structure-Aware Equivalence (SAE), a role-preserving formal equivalence relation between syntactic and whole-statement logical equivalence that allows formally justified reformulations while preserving translation-relevant mathematical structure. We operationalize SAE in the Autoformalization Correctness Evaluator (ACE), which provides certified equivalence or inequivalence judgments and reports Inconclusive otherwise. On ProofNetVerif, a benchmark introduced with BEq+, ACE retains substantial equivalent-case coverage while remaining highly conservative in certifying disputed or inequivalent pairs. On targeted diagnostics, BEq+ accepts 94-96% of unrelated but whole-statement logically equivalent pairs, while Mathesis LeanScorer accepts 42% of localized meaning-changing perturbations; ACE accepts none of either set as equivalent.

cs.PL↗

arXiv2026

Stateful Governance for Concurrent Agentic Systems

AI agents are moving from advisory interfaces into systems that execute consequential operations: issuing refunds, reserving scarce inventory, provisioning cloud resources, and initiating financial transfers. These workflows require governance over effects, not only over model outputs. Existing safeguards often decide whether an action is allowed from the information available when the action is requested. For stateful policies, that request-time view may be incomplete: budgets, inventory, approval status, and risk signals can change before the effect occurs, making an earlier authorization or approval stale. This paper studies stateful governance for concurrent agentic systems. We identify stale authorization as the core failure mode and define policy-state serializability, a correctness condition requiring committed effects to be explainable as authorized against the policy state immediately before they occur. We present MasuGate, a runtime architecture that keeps policies as reviewable programs while coordinating the state and effects needed to preserve their decisions. In experiments with a PostgreSQL-backed prototype of MasuGate, the system prevents stale authorizations missed by baselines that pass policy state as ordinary request context, preserves delayed approvals while unrelated work proceeds, keeps policy evolution mostly in policy text rather than trusted provider code, and avoids policy violations in a scripted, LLM-free procurement workflow where agent-governance baselines produce stale authorizations over shared budgets and inventory. More broadly, MasuGate suggests a path for integrating stateful governance boundaries into agent frameworks and provider-backed domains where agents act on shared resources.

cs.MA↗

arXiv2026

EVOREFUSE: Evolutionary Prompt Optimization for Evaluation and Mitigation of LLM Over-Refusal to Pseudo-Malicious Instructions

Large language models (LLMs) frequently refuse to respond to pseudo-malicious instructions: semantically harmless input queries triggering unnecessary LLM refusals due to conservative safety alignment, significantly impairing user experience. Collecting such instructions is crucial for evaluating and mitigating over-refusals, but existing instruction curation methods, like manual creation or instruction rewriting, either lack scalability or fail to produce sufficiently diverse and effective refusal-inducing prompts. To address these limitations, we introduce EVOREFUSE, a prompt optimization approach that generates diverse pseudo-malicious instructions consistently eliciting confident refusals across LLMs. EVOREFUSE employs an evolutionary algorithm exploring the instruction space in more diverse directions than existing methods via mutation strategies and recombination, and iteratively evolves seed instructions to maximize evidence lower bound on LLM refusal probability. Using EVOREFUSE, we create two novel datasets: EVOREFUSE-TEST, a benchmark of 582 pseudo-malicious instructions that outperforms the next-best benchmark with 85.34% higher average refusal triggering rate across 9 LLMs without a safety-prior system prompt, 34.86% greater lexical diversity, and 40.03% improved LLM response confidence scores; and EVOREFUSE-ALIGN, which provides 3,000 pseudo-malicious instructions with responses for supervised and preference-based alignment training. With supervised fine-tuning on EVOREFUSE-ALIGN, LLAMA3.1-8B-INSTRUCT achieves up to 29.85% fewer over-refusals than models trained on the second-best alignment dataset, without compromising safety. Our analysis with EVOREFUSE-TEST reveals models trigger over-refusals by overly focusing on sensitive keywords while ignoring broader context. Our code and datasets are available at https://github.com/FishT0ucher/EVOREFUSE.

cs.AI↗

arXiv2025

sqrtVINS: Robust and Ultrafast Square-Root Filter-based 3D Motion Tracking

In this paper, we develop and open-source, for the first time, a square-root filter (SRF)-based visual-inertial navigation system (VINS), termed sqrtVINS, which is ultra-fast, numerically stable, and capable of dynamic initialization even under extreme conditions (i.e., extremely small time window). Despite recent advancements in VINS, resource constraints and numerical instability on embedded (robotic) systems with limited precision remain critical challenges. A square-root covariance-based filter offers a promising solution by providing numerical stability, efficient memory usage, and guaranteed positive semi-definiteness. However, canonical SRFs suffer from inefficiencies caused by disruptions in the triangular structure of the covariance matrix during updates. The proposed method significantly improves VINS efficiency with a novel Cholesky decomposition (LLT)-based SRF update, by fully exploiting the system structure to preserve the structure. Moreover, we design a fast, robust, dynamic initialization method, which first recovers the minimal states without triangulating 3D features and then efficiently performs iterative SRF update to refine the full states, enabling seamless VINS operation. The proposed LLT-based SRF is extensively verified through numerical studies, demonstrating superior numerical stability and achieving robust efficient performance on 32-bit single-precision floats, operating at twice the speed of state-of-the-art (SOTA) methods. Our initialization method, tested on both mobile workstations and Jetson Nano computers, achieving a high success rate of initialization even within a 100 ms window under minimal conditions. Finally, the proposed sqrtVINS is extensively validated across diverse scenarios, demonstrating strong efficiency, robustness, and reliability. The full open-source implementation is released to support future research and applications.

cs.RO↗

arXiv2025

Expanding Hardware-Efficiently Manipulable Hilbert Space via Hamiltonian Embedding

Many promising quantum applications depend on the efficient quantum simulation of an exponentially large sparse Hamiltonian, a task known as sparse Hamiltonian simulation, which is fundamentally important in quantum computation. Although several theoretically appealing quantum algorithms have been proposed for this task, they typically require a black-box query model of the sparse Hamiltonian, rendering them impractical for near-term implementation on quantum devices. In this paper, we propose a technique named Hamiltonian embedding. This technique simulates a desired sparse Hamiltonian by embedding it into the evolution of a larger and more structured quantum system, allowing for more efficient simulation through hardware-efficient operations. We conduct a systematic study of this new technique and demonstrate significant savings in computational resources for implementing prominent quantum applications. As a result, we can now experimentally realize quantum walks on complicated graphs (e.g., binary trees, glued-tree graphs), quantum spatial search, and the simulation of real-space Schrödinger equations on current trapped-ion and neutral-atom platforms. Given the fundamental role of Hamiltonian evolution in the design of quantum algorithms, our technique markedly expands the horizon of implementable quantum advantages in the NISQ era.

quant-ph↗

arXiv2025

Revisiting Privacy-Utility Trade-off for DP Training with Pre-existing Knowledge

Differential privacy (DP) provides a provable framework for protecting individuals by customizing a random mechanism over a privacy-sensitive dataset. Deep learning models have demonstrated privacy risks in model exposure as an established learning model unintentionally records membership-level privacy leakage. Differentially private stochastic gradient descent (DP-SGD) has been proposed to safeguard training individuals by adding random Gaussian noise to gradient updates in the backpropagation. Researchers identify that DP-SGD causes utility loss since the injected homogeneous noise can alter the gradient updates calculated at each iteration. Namely, all elements in the gradient are contaminated regardless of their importance in updating model parameters. In this work, we argue that the utility can be optimized by involving the heterogeneity of the the injected noise. Consequently, we propose a generic differential privacy framework with heterogeneous noise (DP-Hero) by defining a heterogeneous random mechanism to abstract its property. The insight of DP-Hero is to leverage the knowledge encoded in the previously trained model to guide the subsequent allocation of noise heterogeneity, thereby leveraging the statistical perturbation and achieving enhanced utility. Atop DP-Hero, we instantiate a heterogeneous version of DP-SGD, and further extend it to federated training. We conduct comprehensive experiments to verify and explain the effectiveness of the proposed DP-Hero, showing improved training accuracy compared with state-of-the-art works. Broadly, we shed light on improving the privacy-utility space by learning the noise guidance from the pre-existing leaked knowledge encoded in the previously trained model, showing a different perspective of understanding the utility-improved DP training.

cs.CR↗

arXiv2025

Quantum Hamiltonian Descent for Non-smooth Optimization

Non-smooth optimization models play a fundamental role in various disciplines, including engineering, science, management, and finance. However, classical algorithms for solving such models often struggle with convergence speed, scalability, and parameter tuning, particularly in high-dimensional and non-convex settings. In this paper, we explore how quantum mechanics can be leveraged to overcome these limitations. Specifically, we investigate the theoretical properties of the Quantum Hamiltonian Descent (QHD) algorithm for non-smooth optimization in both continuous and discrete time. First, we propose continuous-time variants of the general QHD algorithm and establish their global convergence and convergence rate for non-smooth convex and strongly convex problems through a novel Lyapunov function design. Furthermore, we prove the finite-time global convergence of continuous-time QHD for non-smooth non-convex problems under mild conditions (i.e., locally Lipschitz). In addition, we propose discrete-time QHD, a fully digitized implementation of QHD via operator splitting (i.e., product formula). We find that discrete-time QHD exhibits similar convergence properties even with large time steps. Finally, numerical experiments validate our theoretical findings and demonstrate the computational advantages of QHD over classical non-smooth non-convex optimization algorithms.

math.OC↗

arXiv2024

QHDOPT: A Software for Nonlinear Optimization with Quantum Hamiltonian Descent

We develop an open-source, end-to-end software (named QHDOPT), which can solve nonlinear optimization problems using the quantum Hamiltonian descent (QHD) algorithm. QHDOPT offers an accessible interface and automatically maps tasks to various supported quantum backends (i.e., quantum hardware machines). These features enable users, even those without prior knowledge or experience in quantum computing, to utilize the power of existing quantum devices for nonlinear and nonconvex optimization tasks. In its intermediate compilation layer, QHDOPT employs SimuQ, an efficient interface for Hamiltonian-oriented programming, to facilitate multiple algorithmic specifications and ensure compatible cross-hardware deployment. The detailed documentation of QHDOPT is available at https://github.com/jiaqileng/QHDOPT.

quant-ph↗

arXiv2024

NeRF-VINS: A Real-time Neural Radiance Field Map-based Visual-Inertial Navigation System

Achieving efficient and consistent localization a prior map remains challenging in robotics. Conventional keyframe-based approaches often suffers from sub-optimal viewpoints due to limited field of view (FOV) and/or constrained motion, thus degrading the localization performance. To address this issue, we design a real-time tightly-coupled Neural Radiance Fields (NeRF)-aided visual-inertial navigation system (VINS). In particular, by effectively leveraging the NeRF's potential to synthesize novel views, the proposed NeRF-VINS overcomes the limitations of traditional keyframe-based maps (with limited views) and optimally fuses IMU, monocular images, and synthetically rendered images within an efficient filter-based framework. This tightly-coupled fusion enables efficient 3D motion tracking with bounded errors. We extensively compare the proposed NeRF-VINS against the state-of-the-art methods that use prior map information and demonstrate its ability to perform real-time localization, at over 10 Hz, on a resource-constrained Jetson AGX Orin embedded platform.

cs.RO↗

arXiv2023

A Case for Synthesis of Recursive Quantum Unitary Programs

Quantum programs are notoriously difficult to code and verify due to unintuitive quantum knowledge associated with quantum programming. Automated tools relieving the tedium and errors associated with low-level quantum details would hence be highly desirable. In this paper, we initiate the study of program synthesis for quantum unitary programs that recursively define a family of unitary circuits for different input sizes, which are widely used in existing quantum programming languages. Specifically, we present QSynth, the first quantum program synthesis framework, including a new inductive quantum programming language, its specification, a sound logic for reasoning, and an encoding of the reasoning procedure into SMT instances. By leveraging existing SMT solvers, QSynth successfully synthesizes ten quantum unitary programs including quantum adder circuits, quantum eigenvalue inversion circuits and Quantum Fourier Transformation, which can be readily transpiled to executable programs on major quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket.

quant-ph↗

arXiv2023

SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation

Quantum Hamiltonian simulation, which simulates the evolution of quantum systems and probes quantum phenomena, is one of the most promising applications of quantum computing. Recent experimental results suggest that Hamiltonian-oriented analog quantum simulation would be advantageous over circuit-oriented digital quantum simulation in the Noisy Intermediate-Scale Quantum (NISQ) machine era. However, programming analog quantum simulators is much more challenging due to the lack of a unified interface between hardware and software. In this paper, we design and implement SimuQ, the first framework for quantum Hamiltonian simulation that supports Hamiltonian programming and pulse-level compilation to heterogeneous analog quantum simulators. Specifically, in SimuQ, front-end users specify the target quantum system with Hamiltonian Modeling Language, and the Hamiltonian-level programmability of analog quantum simulators is specified through a new abstraction called the abstract analog instruction set (AAIS) and programmed in AAIS Specification Language by hardware providers. Through a solver-based compilation, SimuQ generates executable pulse schedules for real devices to simulate the evolution of desired quantum systems, which is demonstrated on superconducting (IBM), neutral-atom (QuEra), and trapped-ion (IonQ) quantum devices. Moreover, we demonstrate the advantages of exposing the Hamiltonian-level programmability of devices with native operations or interaction-based gates and establish a small benchmark of quantum simulation to evaluate SimuQ's compiler with the above analog quantum simulators.

cs.PL↗

arXiv2022

Differentiable Analog Quantum Computing for Optimization and Control

We formulate the first differentiable analog quantum computing framework with a specific parameterization design at the analog signal (pulse) level to better exploit near-term quantum devices via variational methods. We further propose a scalable approach to estimate the gradients of quantum dynamics using a forward pass with Monte Carlo sampling, which leads to a quantum stochastic gradient descent algorithm for scalable gradient-based training in our framework. Applying our framework to quantum optimization and control, we observe a significant advantage of differentiable analog quantum computing against SOTAs based on parameterized digital quantum circuits by orders of magnitude.

quant-ph↗

arXiv2022

Verified Compilation of Quantum Oracles

Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the largest components of a quantum program. To ease the construction of efficient, correct oracle functions, this paper presents VQO, a high-assurance framework implemented with the Coq proof assistant. The core of VQO is OQASM, the oracle quantum assembly language. OQASM operations move qubits between two different bases via the quantum Fourier transform, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM's design enabled us to prove correct VQO's compilers -- from a simple imperative language called OQIMP to OQASM, and from OQASM to SQIR, a general-purpose quantum assembly language -- and allowed us to efficiently test properties of OQASM programs using the QuickChick property-based testing framework. We have used VQO to implement a variety of arithmetic and geometric operators that are building blocks for important oracles, including those used in Shor's and Grover's algorithms. We found that VQO's QFT-based arithmetic oracles require fewer qubits, sometimes substantially fewer, than those constructed using "classical" gates; VQO's versions of the latter were nevertheless on par with or better than (in terms of both qubit and gate counts) oracles produced by Quipper, a state-of-the-art but unverified quantum programming platform.

quant-ph↗

arXiv2022

A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm

Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors -- "bugs". Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside their program, and semi-automatically proves the program correct with respect to it. The proof's validity is automatically confirmed -- certified -- by a "proof assistant". Formal methods have successfully yielded high-assurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present the first formally certified end-to-end implementation of Shor's prime factorization algorithm, developed as part of a novel framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way.

cs.PL↗

arXiv2022

Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra

We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose Non-idempotent Kleene Algebra (NKA) as a natural alternative and identify complete and sound semantic models for NKA as well as their quantum interpretations. In light of applications of KAT, we demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum while-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems.

cs.PL↗

arXiv2021

Experimental Realization of Device-Independent Quantum Randomness Expansion

Randomness expansion where one generates a longer sequence of random numbers from a short one is viable in quantum mechanics but not allowed classically. Device-independent quantum randomness expansion provides a randomness resource of the highest security level. Here, we report the first experimental realization of device-independent quantum randomness expansion secure against quantum side information established through quantum probability estimation. We generate $5.47\times10^8$ quantum-proof random bits while consuming $4.39\times10^8$ bits of entropy, expanding our store of randomness by $1.08\times10^8$ bits at a latency of about $13.1$ h, with a total soundness error $4.6\times10^{-10}$. Device-independent quantum randomness expansion not only enriches our understanding of randomness but also sets a solid base to bring quantum-certifiable random bits into realistic applications.

quant-ph↗