Search arXiv⌕ Search

arXiv subjects

Zhengfeng Ji

Publications and source records attributed to Zhengfeng Ji.

At least 19 recordsLinked to original sources
arXiv2026

FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq

Quantum key distribution (QKD), whose security is derived from quantum mechanics rather than computational assumptions, is moving into standardization and commercial deployment. Yet its security guarantees rest on technically delicate proofs checked by hand. Formal verification closes this gap, establishing a two-factor assurance: unconditional security from physical principles, and machine-checked proofs against reasoning errors. We present FVQKD, a Rocq library for machine-checking QKD security proofs. Its first result is a complete, end-to-end machine-checked proof of composable, finite-key security for BB84. The mechanization reconstructs the complete proof infrastructure from first principles, including the smooth entropy framework, the entropic uncertainty relation, and the Quantum Leftover Hash Lemma. It uncovers necessary side conditions that the published argument leaves unstated, one of which reveals a missing proof branch, and it grounds the information-theoretic bound in a formal semantics of protocol execution, which the pen-and-paper analysis lacks. The proof is entirely admit-free, relying only on the Rocq kernel and standard foundational axioms. To our knowledge, this is the first end-to-end formal verification of a QKD security proof. Built on MathComp, MathComp-Analysis, and CoqQ, the development provides quantum-information infrastructure designed for reuse across broader QKD variants and quantum cryptography applications.

quant-ph↗
arXiv2026

Long-horizon autoformalization of a core theorem underlying MIP* = RE

Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization. Drawing on software-engineering principles and practices, it uses a shared blueprint to guide nested planning, proving, and review loops. Using FormalFlow, we completed a machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test, a core theorem underlying MIP* = RE, in 63 days. The final library contains 126,367 lines of Lean code, all generated by agents. Beyond providing a verified foundation for quantum complexity, the formalization corrects side conditions and intermediate error bounds in the published proof and improves the error exponent of the main theorem. The development record shows what it takes to trust proofs written by AI agents and provides reusable tools for verifying research mathematics at scale.

quant-ph↗
arXiv2026

Near-Optimal Quantum Algorithm and Complexity Analysis for Riccati Problems

We develop quantum algorithms that construct block-encodings of solution matrices for continuous- and discrete-time algebraic Riccati equations (CAREs and DAREs), differential Riccati equations (DREs), and finite Riccati recursions. The Quantum Weighted Riesz Method, unifying four kinds of Riccati problems, constructs projectors onto the solution graphs using weighted Riesz branching operators and recovers the solution matrices. Under the stated access and normalization assumptions, our algorithms for CAREs and DAREs have near-optimal query complexity $Θ(\mathcal Rα)$ up to logarithmic factors, with the generalized singularity factor $\mathcal R$ that reflects spectral separation, and the output normalization $α$. For DREs and finite-horizon problems, the query complexity has an additional initialization conditioning factor $κ_{\rm init}$. We establish product query lower bounds for specified input-oracle families, demonstrating necessary joint dependence on spectral separation and initialization or output scale. We also prove that selected-value promise problems are BQP-complete on explicit circuit-generated families of single-control discrete-time algebraic and zero-terminal differential Riccati equations. Applications include classical feedback evaluation for linear-quadratic control, a query-complexity comparison for stable random-phase approximation Riccati equations in quantum chemistry, and heated boundary control with numerical validation.

quant-ph↗
arXiv2026

MIP*=RE

We show that the class MIP* of languages that can be decided by a classical verifier interacting with multiple all-powerful quantum provers sharing entanglement is equal to the class RE of recursively enumerable languages. Our proof builds upon the quantum low-degree test of (Natarajan and Vidick, FOCS 2018) and the classical low-individual degree test of (Ji, et al., 2020) by integrating recent developments from (Natarajan and Wright, FOCS 2019) and combining them with the recursive compression framework of (Fitzsimons et al., STOC 2019). An immediate byproduct of our result is that there is an efficient reduction from the Halting Problem to the problem of deciding whether a two-player nonlocal game has entangled value $1$ or at most $1/2$. Using a known connection, undecidability of the entangled value implies a negative answer to Tsirelson's problem: we show, by providing an explicit example, that the closure $C_{qa}$ of the set of quantum tensor product correlations is strictly included in the set $C_{qc}$ of quantum commuting correlations. Following work of (Fritz, Rev. Math. Phys. 2012) and (Junge et al., J. Math. Phys. 2011) our results provide a refutation of Connes' embedding conjecture from the theory of von Neumann algebras.

quant-ph↗
arXiv2026

Quantum Query Advantage Requires Space

Hao, Huang, and Liu (STOC'26) recently showed that optimal quantum query complexity may require large workspace even for short-output problems, and asked whether a quantum query advantage over classical computation can itself require space. We resolve this question by exhibiting an explicit total Boolean function with quantum query complexity $Q=\widetildeΘ(M)$, and randomized query complexity $R=Θ(M^{21/20})$, whereas, for every fixed $0<η<1/100$ and $S\le O(M^{1/100-η})$, its $S$-space quantum query complexity satisfies $Q_S=ω(M^{21/20})$. Consequently, $$ Q<R<Q_S, $$ so the unrestricted quantum query advantage disappears under sufficiently small workspace. The separation is obtained through a one-bit filtered-parity construction and a space-sensitive quantum lower bound based on compressed-oracle capacity and a new parity-to-capacity inequality, which may be of independent interest.

quant-ph↗
arXiv2026

Simultaneously Query-Optimal Quantum Linear-System Algorithm

Quantum linear-system algorithms access the coefficient matrix through a block-encoding oracle $U_A$ and the right-hand side through a state-preparation oracle $U_b$. The optimal query complexities of these two oracles are known separately: $O(κ\log(1/\varepsilon))$ queries to $U_A$ and $O(κ/s)$ queries to $U_b$, where $s=α\|A^{-1}b\|$. Whether a single algorithm can achieve both bounds simultaneously has remained open. We resolve this question affirmatively. Given a constant-factor estimate of $s$, we give a quantum linear-system algorithm that prepares the normalized solution to error $\varepsilon$ using simultaneously $ O\left(κ\log\frac1\varepsilon\right)$ queries to $U_A$ and $O\left(κ/{s}\right)$ queries to $U_b$. The algorithm separates state preparation from precision refinement, so only the matrix-query count depends on the target accuracy. We also prove a matching same-instance worst-case lower bound: for every quantum linear-system algorithm and every solution-norm scale, there exists a single Hermitian instance on which that algorithm requires both $Ω(κ\log(1/\varepsilon))$ matrix queries and $Ω(κ/s)$ state-preparation queries. Thus the two oracle complexities can be optimized simultaneously, and the resulting bounds are jointly optimal.

quant-ph↗
arXiv2026

A Generalized Stein Lemma for Quantum Channels

We prove a generalized quantum Stein lemma for parallel discrimination of an arbitrary finite-dimensional channel against families of alternative channels. The alternatives are compact and convex, closed under tensor products, and contain a faithful replacer. At every fixed type-I error tolerance, the optimal type-II error exponent equals the regularized Umegaki channel relative entropy minimized over the alternatives, and both defining limits exist. Inputs may be entangled across channel uses and with a reference system. The main technical result constructs exactly trace-preserving approximations with exponentially small diamond error, dominated in completely positive order by free channels at every rate above the common exponent. The proof combines uniform auxiliary map approximation, iterative reduction of the domination rate, and tensor amplification. It yields asymptotic equipartition with trace-preserving smoothing at every subexponentially vanishing error, an exponential strong converse, and stability under vanishing diamond-norm perturbations. Under additional permutation invariance and closure under insertion of a fixed faithful input state and discarding of its output, we also prove an explicit finite-block completion bound. This quantitative construction uses weighted discarding, local operator corrections, and comparison with auxiliary extensions. Applications include state-preserving, coherence-restricted, covariant, entanglement-breaking, and positive-partial-transpose channels. For isometric targets against entanglement-breaking or positive-partial-transpose alternatives, we obtain exact finite-block testing and smoothing formulas.

quant-ph↗
arXiv2026

DQC1-completeness of normalized trace estimation for functions of log-local Hamiltonians

We study the computational complexity of estimating the normalized trace $2^{-n}\mathrm{Tr}[f(A)]$ for a log-local Hamiltonian $A$ acting on $n$ qubits. This problem arises naturally in the DQC1 model, yet its complexity is only understood for a limited class of functions $f(x)$. We show that if $f(x)$ is a continuous function with approximate degree $Ω(\mathrm{poly}(n))$, then estimating $2^{-n}\mathrm{Tr}[f(A)]$ up to constant additive error is DQC1-complete, under a technical condition on the polynomial approximation error of $f(x)$. This condition holds for a broad class of functions, including exponentials, trigonometric functions, logarithms, and inverse-type functions. We further prove that when $A$ is sparse, the classical query complexity of this problem is exponential in the approximate degree. Together, these results identify the approximate degree as the key parameter governing the complexity of normalized trace estimation: it characterizes both the quantum complexity (via efficient DQC1 algorithms) and the classical hardness, yielding an exponential quantum-classical separation. Our proof develops a unified framework that cleanly combines circuit-to-Hamiltonian constructions, periodic Jacobi operators, and tools from polynomial approximation theory, including the Chebyshev equioscillation theorem.

quant-ph↗
arXiv2026

Quantum Channel Stein's Lemma with an Exponential Strong Converse

We establish the quantum channel Stein lemma at every fixed type-I error tolerance in $(0,1)$ and prove an exponential strong converse under arbitrary adaptive strategies. For any finite-dimensional channel pair, the optimal type-II exponent equals the regularized channel relative entropy and is attained by parallel strategies. When this divergence is finite, every strictly larger type-II rate forces the probability of accepting the null hypothesis to decay exponentially, uniformly over strategies and quantum memories. The proof rests on a uniform Stinespring approximation: tensor powers of the null dilation are approximated by tensor powers of the alternative dilation after applying an auxiliary linear map to the environment. The operator-norm error is exponentially small under a squared-norm bound at any rate above the regularized relative entropy. We construct the approximation from a weak testing bound by iterative rate reduction and a fixed-block tensor expansion with an exact residual. It implies right continuity at order one of the regularized sandwiched Rényi channel divergence, which yields the adaptive converse through the channel chain rule. We also obtain a sharp hockey-stick threshold and a subchannel smoothing asymptotic equipartition property for fixed and subexponentially vanishing diamond-norm errors.

quant-ph↗
arXiv2026

Quantum Behaviors Are Not Semialgebraic

The conditional probabilities achievable by local measurements on a shared quantum state in a Bell scenario form the set of quantum behaviors, whose structure was studied by Tsirelson. In 1993, Tsirelson asked whether this set is semialgebraic, that is, describable by finite Boolean combinations of polynomial equations and inequalities. This question has remained open. We answer it in the negative: with four binary measurements per party, the set of finite-dimensional quantum behaviors, its closure, and the commuting-operator set are all nonsemialgebraic. More strongly, none admits a finite real-analytic description even locally near a particular classical behavior. These results rule out exact finite semidefinite representations and show that no finite level of the Navascués-Pironio-Acín hierarchy characterizes these sets exactly.

quant-ph↗
arXiv2026

Optimal Covariance Inflation under Gaussian Tilts

Covariance-sensitive analyses of Gaussian annealing for sampling from a convex body require controlling how much covariance can grow under a radial Gaussian tilt. For an isotropic convex body $K\subseteq\mathbb{R}^n$, let $μ_{K,t} (\mathrm{d} x) \propto e^{-t\| x \| ^2} \mathbb{1}_K(x)\,\mathrm{d} x$, and let $Q_n$ be the supremum of $\|\operatorname{Cov}(μ_{K,t})\|_{\mathrm{op}}$ over all such $K$ and all $t>0$. We prove the sharp bound $Q_n=Θ(n^{2/5})$, closing the gap between the known $Ω(n^{1/3})$ lower bound and the $O(\sqrt{n\log(en)})$ upper bound. The upper bound applies not only to uniform measures on convex bodies but to every compactly supported isotropic logconcave probability measure. It combines a dimension-free variance bound for quadratic forms with a Rényi comparison at a nearby time, projected moment estimates, and relative-entropy control along the Gaussian-tilt path. For the matching lower bound, we construct an explicit unconditional convex body whose axial coordinate is coupled to the transverse quadratic energy. Moderate-deviation estimates show that an appropriate tilt creates directional variance $Ω(n^{2/5})$.

math.PR↗
arXiv2026

Gate-Efficient Implementation of the Query-Optimal Time-Dependent Hamiltonian Simulation

The query-optimal algorithm of [CGWZ26] for general time-dependent Hamiltonian simulation uses $$ q = O\left( αT + \frac{\log(1/\varepsilon)}{\log\left(e + \log(1/\varepsilon)/(αT) \right)} \right) $$ queries to $\mathrm{HAM\mbox{-}T}$ within $\varepsilon$ error for a Lipschitz-continuous time-dependent Hamiltonian $H(t)$ on $[0,T]$ satisfying $\left\lVert H(t)\right\rVert\leqα$. However, its direct circuit implementation incurs a substantially larger gate overhead. In this note, we give an implementation of the same algorithm that retains its optimal query complexity and uses $$ O\left[ q \left( a + \log\left(1 + \frac{T(α+ βT)}{\varepsilon} \right) \right) \right] $$ one- and two-qubit gates, where $a$ is the number of block-encoding ancilla qubits and $β$ is the Lipschitz constant of $H$. The main ingredient is an exact dyadic factorization of the ordered update product in the underlying one-query transducer.

quant-ph↗
arXiv2026

Quantum Maximum Entropy Inference and Hamiltonian Learning

Maximum entropy inference and learning of graphical models are pivotal tasks in learning theory and optimization. This work extends algorithms for these problems, including generalized iterative scaling (GIS) and gradient descent (GD), to the quantum realm. While the generalization, known as quantum iterative scaling (QIS), is straightforward, the key challenge lies in the non-commutative nature of quantum problem instances, rendering the convergence rate analysis significantly more challenging than the classical case. Our principal technical contribution centers on a rigorous analysis of the convergence rates, involving the establishment of both lower and upper bounds on the spectral radius of the Jacobian matrix for each iteration of these algorithms. Furthermore, we explore quasi-Newton methods to enhance the performance of QIS and GD. Specifically, we propose using Anderson mixing and the L-BFGS method for QIS and GD, respectively. These quasi-Newton techniques exhibit remarkable efficiency gains, resulting in orders of magnitude improvements in performance. As an application, our algorithms provide a viable approach to designing Hamiltonian learning algorithms.

cs.LG↗
arXiv2026

Quantum Speedups for Log-Concave Sampling from Local Structure

For a convex function $f \colon \mathbb{R}^d \to \mathbb{R}$, the problem of sampling from a distribution proportional to $e^{-f(x)}$ is called log-concave sampling. In many practical scenarios, the function $f(x)$ turns out to admit a local decomposition $f(x) = \sum_{a=1}^R ψ_a(x_{S_a})$. In this paper, we consider log-concave sampling using local queries, i.e., evaluation and gradient queries to each clause $ψ_a(\cdot)$, which can be computationally much cheaper than the queries to $f(x)$ itself. We show that if each coordinate appears in only a small number of clauses, there is a quantum algorithm for strongly log-concave sampling using $\widetilde{O}(\sqrtκd)$ local queries, where $κ$ is the condition number. This improves the prior best classical result $\widetilde{O}(κd)$ due to Ascolani, Lavenant, and Zanella (Ann. Probab. 2026) and the quantum result $\widetilde{O}(\sqrtκ d^2)$ implied by Childs et al. (NeurIPS 2022). Our quantum sampler applies to a broad class of locally structured models from statistical computing and machine learning, with representative examples including Gaussian Markov random fields, finite-element latent Gaussian models, and sparse generalized linear models. These results demonstrate that local structure is not merely an implementation detail, but a quantum algorithmic resource for high-dimensional sampling.

quant-ph↗
arXiv2026

No-Go Theorems for Quantum Transport Metrics from Fixed Cost Operators

Coupling-based quantum optimal transport generalizes classical optimal transport by representing transport plans as bipartite states with prescribed marginals and evaluating their cost as the expectation of a fixed Hermitian operator. Friedland et al. [Phys. Rev. Lett. 129, 110402 (2022)] conjectured that the square root of the optimal cost associated with the SWAP projector is a metric in every dimension and that this property persists for nearby quantum cost matrices. Miller [arXiv:2607.07764] disproved both conjectures by constructing explicit diagonal qutrit counterexamples. Building on his analysis, we prove a uniform no-go theorem for standard couplings. In every dimension $d\geq3$, no fixed cost operator makes either the optimal cost or its square root a metric, with violations occurring already among commuting states. The obstruction persists under stabilization of the SWAP cost. For channel-induced couplings, global nonnegativity and vanishing self-cost force the cost operator to be zero, precluding point separation when $d\geq2$. Taken together, these no-go results show that fixed-cost coupling formulations do not lead to metrics on the full quantum state space.

quant-ph↗
arXiv2026

Quantum Nonlocality under Latency Constraints

Bell inequalities are bounds on the correlations between different parties obeying a local hidden variable theory. Here, "local" refers to spacetime locality: the parties cannot communicate their inputs because they must produce their outputs faster than the speed-of-light delay between them. In other words, the parties must satisfy a certain latency constraint. In this work, we explicitly incorporate spacetime locality into the formulation of Bell inequalities by imposing such a latency constraint. When the latency constraint is sufficiently tight such that no parties can communicate, this becomes a standard Bell scenario. When the latency constraint is relaxed such that a subset of the parties can communicate, we no longer have a Bell scenario, but we can again find a divide between classical and quantum behaviors. Hence, we observe that the classical-quantum gap should actually be a function of time. To study these more general scenarios, we introduce the mathematical framework of latency-constrained games, which models time-evolving input and output processes for spatially separated parties subject to finite communication speeds. This framework allows us to systematically study the weirdness of quantum mechanics in the "low-latency regime" where the speed-of-light delay is non-negligible. Latency-constrained games can describe real-time decision-making in real-world settings that are latency-sensitive, such as high-frequency trading and distributed systems, and can reveal the utility of quantum correlations in these settings.

quant-ph↗
arXiv2026

A Correlation-Gap Bound for Nonlinear Gaussian PCA

Principal component analysis (PCA) is optimal for the linear reconstruction of Gaussian data, a foundational property underlying its central role in algorithms and signal processing. Its nonlinear analogue, however, is notoriously subtle: in 2011, Mallat and Zeitouni conjectured that the Karhunen--Loève (KL) basis remains optimal even when the retained coordinates are chosen adaptively per sample, a property that would theoretically justify the ubiquitous pipeline of PCA followed by sparse thresholding. In this paper, we establish a $1+O(1/\sqrt{d})$-approximate version of the retained-energy form of the Mallat--Zeitouni conjecture, showing that the KL basis is within this factor of the optimal basis. This dimension-free comparison depends only on the number of retained coordinates and shows that the possible advantage of optimizing over all orthonormal bases vanishes as $d$ grows. It complements the universal-constant reconstruction-error comparison of Litvak and Tikhomirov (Ann. Appl. Probab., 2018), while providing a comparison naturally suited for algorithmic analysis. Our proof rests on a clean, conceptual reduction: we relax arbitrary rotations to a deterministic threshold bound via Schur--Horn majorization, and identify the remaining loss with the correlation gap of the rank-$d$ uniform matroid over Gaussian level sets.

cs.DS↗
arXiv2026

On the Complexity of the Circuit Width Problem

Montanaro's polynomial representation expresses amplitudes of quantum circuits over the gates $H$, $Z$, $CZ$, and $CCZ$ as normalized gaps of degree-three polynomials over $\mathbb{F}_2$. The normalization is governed by the circuit width $w(f)$, the minimum number of qubits in any circuit realizing a polynomial $f$. Thus, efficient width minimization would give an approximate-counting route toward a combinatorial characterization of $BQP$. We study the computational complexity of this parameter. For degree-three polynomials with no constant term, deciding whether $w(f)\le k$ is $NP$-complete, resolving Montanaro's open question. We also prove $NP$-hardness of approximation within any factor $49/48-ε$, and show via a twin-copy construction that the exact and approximation hardness results also hold for degree-two polynomials. Under the Exponential Time Hypothesis, the exact problem admits no $2^{o(n)}$-time algorithm when $k=Θ(n)$. Complementing these hardness results, we give a nondeterministic polynomial-time search algorithm using $2\log_2\binom{n}{k}=O(k\log(en/k))$ witness bits, and a constructive fixed-parameter algorithm parameterized by $k$ with running time $k^{6k+o(k)}n+O(m)$.

cs.CC↗