SearcharxivSearch

arXiv subjects

Zeguan Wu

Publications and source records attributed to Zeguan Wu.

15 recordsLinked to original sources

Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution

Designing effective Lean proof agents is a central challenge in formal mathematical reasoning. Beyond building stronger provers, recent work emphasizes the workflow around Lean: how an agent decomposes proof obligations, uses tools and compiler feedback, diagnoses failures, repairs proofs, and maintains structured proof context. Motivated by code-level self-evolving agents, we study whether such workflows can be evolved rather than hand-designed. We present a self-evolving Lean proof agent in which a small fixed, trusted runtime wraps a fully mutable workspace: the proof workflow, prompts, and tools. Unlike most self-evolving systems, which optimize against a fixed external benchmark, our system coevolves the agent and its benchmark. Between generations, the highest-scoring agent (the champion) revises the active task distribution through a mastery-throttled curriculum update that introduces harder proof obligations only after the current level is mastered, and a single-anchor recalibration re-runs the champion on the updated benchmark to keep scores comparable as difficulty rises. All evolution stays inside a Lean-grounded verification loop: however the agent rewrites itself, a success counts only when its behavior yields Lean-verified proofs under a trusted snapshot, and each attempt must emit a machine-readable, Lean-grounded proof context whose representation may evolve but whose groundedness is enforced. We run the coevolving trajectory and a fixed-benchmark baseline for 15 active generations and compare them on a held-out miniF2F test split. The best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent, showing that verifier-grounded self-evolution can improve Lean proof workflows under a coevolving benchmark.

cs.AI

When AI meets quantum information: A comprehensive review

Artificial intelligence (AI) and quantum information (QI) are rapidly co-evolving. AI is becoming a practical tool for learning, designing, controlling, and verifying quantum systems, while QI offers new computational models, representational structures, and learning-theoretic questions for AI. This survey reviews the interface from both directions. In the AI for QI direction, we organize recent progress around the central tasks of extracting information from limited measurements, training and discovering quantum algorithms, stabilizing noisy hardware, automating experimental and programming workflows, and extending learning-based methods to sensing and networking. In the QI for AI direction, we examine how quantum computation and quantum-inspired structures affect learning through algorithmic speedups, expressivity, trainability, generalization, neural-network design, and tensor-network representations. We close by identifying cross-cutting challenges in reproducibility, scalability, hardware realism, and co-design, arguing that progress will depend on tighter integration of theory, experiment, and hybrid quantum--classical systems.

quant-ph

Stab-QRAM: A Clifford-Only Quantum Oracle for Affine Boolean Data

Oracle-based quantum algorithms require coherent evaluation of classical functions on superposed inputs, and in fault-tolerant architectures this cost is dominated by non-Clifford gates: generic lookup constructions incur $T$-counts that grow with the data size. Here we show that affine Boolean functions $f(\mathbf{x})=A\mathbf{x}+\mathbf{b}$ over $\mathbb{F}_2$ -- the algebraic core of parity checks, linear feedback shift registers, and cipher linear layers -- are exactly the functions admitting computational-basis-preserving Clifford oracles, and we develop this correspondence into Stab-QRAM, a compiler mapping a specification $(A,\mathbf{b})$ to an ancilla-free circuit of CNOT and $X$ gates with zero $T$-count. Via König's edge-coloring theorem, the compiled schedule provably attains the minimum depth for its gate set. Case studies spanning Simon-type oracles, block-encodings of $X$-type coset operators, and syndrome extraction for CSS codes show one compiler serving the algorithm, primitive, and error-correction layers of the quantum stack.

quant-ph

Benchmarking and Resource Analysis for Augmented-Lagrangian Quantum Hamiltonian Descent

Quantum Hamiltonian Descent (QHD) is a continuous optimization algorithm based on simulating a time-dependent quantum Hamiltonian whose potential energy encodes the objective function and whose kinetic energy promotes exploration through quantum interference and tunneling. While QHD is formulated for unconstrained optimization, many real-world optimization problems are constrained and highly nonconvex. In this paper, we benchmark AL-QHD, a hybrid framework that embeds QHD within the Augmented Lagrangian Method (ALM), thereby solving a sequence of unconstrained subproblems while using ALM to enforce constraints. We evaluate AL-QHD on standard nonconvex test functions and use iterative refinement to improve solution accuracy at fixed per-run qubit cost. We also perform a gate-based resource analysis on ACOPF-derived power system subproblems constructed from power-network data to estimate the quantum-computer scale required for practical applications. Resource estimates on Texas7k-derived ACOPF instances show steep hard-gate scaling, reaching $\sim 4.46 \times 10^7$ entangling gates in a NISQ-oriented model and $\sim 9.42 \times 10^8$ T gates in a fault-tolerant model at $\sim 5.3 \times 10^2$ active variables. These results suggest that AL-QHD is a useful framework for studying constrained nonconvex optimization with QHD, but that practical ACOPF-scale applications would likely require large-scale fault-tolerant quantum hardware.

quant-ph

Infeasibility Aware Large Language Models for Combinatorial Optimization

Large language models (LLMs) are increasingly explored for NP-hard combinatorial optimization problems, but most existing methods emphasize feasible-instance solution generation and do not explicitly address infeasibility detection. We propose an infeasibility-aware framework that combines certifiable dataset construction, supervised fine-tuning, and LLM-assisted downstream search. For the minor-embedding problem, we introduce a new mathematical programming formulation together with provable zero-phase infeasibility screening, which enables scalable construction of training instances labeled either as feasible with structured certificates or as certifiably infeasible. Using training data generated through this exact optimization pipeline, we show that an 8B-parameter LLM can be fine-tuned to jointly perform solution generation and infeasibility detection. We further utilize LLM outputs as warm starts for downstream local search, providing a practical way to accelerate optimization even when the LLM outputs are imperfect. Experiments show that our fine-tuned model improves overall accuracy by up to 30\% over GPT-5.2; meanwhile LLM-guided warm starts provide up to $2\times$ speedup compared with starting from scratch in downstream local search.

cs.AI

Artificial Entanglement in the Fine-Tuning of Large Language Models

Large language models (LLMs) can be adapted to new tasks using parameter-efficient fine-tuning (PEFT) methods that modify only a small number of trainable parameters, often through low-rank updates. In this work, we adopt a quantum-information-inspired perspective to understand their effectiveness. From this perspective, low-rank parameterizations naturally correspond to low-dimensional Matrix Product States (MPS) representations, which enable entanglement-based characterizations of parameter structure. Thereby, we term and measure "Artificial Entanglement", defined as the entanglement entropy of the parameters in artificial neural networks (in particular the LLMs). We first study the representative low-rank adaptation (LoRA) PEFT method, alongside full fine-tuning (FFT), using LLaMA models at the 1B and 8B scales trained on the Tulu3 and OpenThoughts3 datasets, and uncover: (i) Internal artificial entanglement in the updates of query and value projection matrices in LoRA follows a volume law with a central suppression (termed as the "Entanglement Valley"), which is sensitive to hyper-parameters and is distinct from that in FFT; (ii) External artificial entanglement in attention matrices, corresponding to token-token correlations in representation space, follows an area law with logarithmic corrections and remains robust to LoRA hyper-parameters and training steps. Drawing a parallel to the No-Hair Theorem in black hole physics, we propose that although LoRA and FFT induce distinct internal entanglement signatures, such differences do not manifest in the attention outputs, suggesting a "no-hair" property that results in the effectiveness of low rank updates. We further provide theoretical support based on random matrix theory, and extend our analysis to an MPS Adaptation PEFT method, which exhibits qualitatively similar behaviors.

cs.LG

Quantum Interior Point Methods: A Review of Developments and An Optimally Scaling Framework

The growing demand for solving large-scale, data-intensive linear and conic optimization problems, particularly in applications such as artificial intelligence and machine learning, has highlighted the limitations of classical interior point methods (IPMs). Despite their favorable polynomial-time convergence, conventional IPMs often suffer from high per-iteration computational costs, especially for dense problem instances. Recent advances in quantum computing, particularly quantum linear system solvers, offer promising avenues to accelerate the most computationally intensive steps of IPMs. However, practical challenges such as quantum error, hardware noise, and sensitivity to poorly conditioned systems remain significant obstacles. In response, a series of Quantum IPMs (QIPMs) has been developed to address these challenges, incorporating techniques such as feasibility maintenance, iterative refinement, and preconditioning. In this work, we review this line of research with a focus on our recent contributions, including an almost-exact QIPM framework. This hybrid quantum-classical approach constructs and solves the Newton system entirely on a quantum computer, while performing solution updates classically. Crucially, all matrix-vector operations are executed on quantum hardware, enabling the method to achieve an optimal worst-case scalability w.r.t dimension, surpassing the scalability of existing classical and quantum IPMs.

quant-ph

Optimal Scaling Quantum Interior Point Method for Linear Optimization

The emergence of huge-scale, data-intensive linear optimization (LO) problems in applications such as machine learning has driven the need for more computationally efficient interior point methods (IPMs). While conventional IPMs are polynomial-time algorithms with rapid convergence, their per-iteration cost can be prohibitively high for dense large-scale LO problems. Quantum linear system solvers have shown potential in accelerating the solution of linear systems arising in IPMs. In this work, we introduce a novel almost-exact quantum IPM, where the Newton system is constructed and solved on a quantum computer, while solution updates occur on a classical machine. Additionally, all matrix-vector products are performed on the quantum hardware. This hybrid quantum-classical framework achieves an optimal worst-case scaling of $\mathcal{O}(n^2)$ for fully dense LO problems. To ensure high precision, despite the limited accuracy of quantum operations, we incorporate iterative refinement techniques both within and outside the proposed IPM iterations. The proposed algorithm has a quantum complexity of $\mathcal{O}(n^{1.5} κ_A \log(\frac{1}ε))$ queries to QRAM and $\mathcal{O}(n^2 \log(\frac{1}ε))$ classical arithmetic operations. Our method outperforms the worst-case complexity of prior classical and quantum IPMs, offering a significant improvement in scalability and computational efficiency.

quant-ph

Provably Efficient Quantum Algorithms for Solving Nonlinear Differential Equations Using Multiple Bosonic Modes Coupled with Qubits

Quantum computers have long been expected to efficiently solve complex classical differential equations. Most digital, fault-tolerant approaches use Carleman linearization to map nonlinear systems to linear ones and then apply quantum linear-system solvers. However, provable speedups typically require digital truncation and full fault tolerance, rendering such linearization approaches challenging to implement on current hardware. Here we present an analog, continuous-variable algorithm based on coupled bosonic modes with qubit-based adaptive measurements that avoids Hilbert-space digitization. This method encodes classical fields as coherent states and, via Kraus-channel composition derived from the Koopman-von Neumann (KvN) formalism, maps nonlinear evolution to linear dynamics. Unlike many analog schemes, the algorithm is provably efficient: advancing a first-order, $L$-grid point, $d$-dimensional, order-$K$ spatial-derivative, degree-$r$ polynomial-nonlinearity, strongly dissipative partial differential equations (PDEs) for $T$ time steps costs $\mathcal{O}\left(T(\log L + d r \log K)\right)$. The capability of the scheme is demonstrated by using it to simulate the one-dimensional Burgers' equation and two-dimensional Fisher-KPP equation. The resilience of the method to photon loss is shown under strong-dissipation conditions and an analytic counterterm is derived that systematically cancels the dominant, experimentally calibrated noise. This work establishes a continuous-variable framework for simulating nonlinear systems and identifies a viable pathway toward practical quantum speedup on near-term analog hardware.

quant-ph

An Inexact Feasible Interior Point Method for Linear Optimization with High Adaptability to Quantum Computers

The use of quantum computing to accelerate complex optimization problems is a burgeoning research field. This paper applies Quantum Linear System Algorithms (QLSAs) to Newton systems within Interior Point Methods (IPMs) to take advantage of quantum speedup in solving Linear Optimization (LO) problems. Due to their inexact nature, QLSAs can be applied only to inexact variants of IPMs. Existing IPMs with inexact Newton directions are infeasible methods due to the inexact nature of their computations. This paper proposes an Inexact-Feasible IPM (IF-IPM) for LO problems, using a novel linear system to generate inexact but feasible steps. We show that this method has $\Ocal(\sqrt{n}L)$ iteration complexity, analogous to the best exact IPMs, where $n$ is the number of variables and $L$ is the binary length of the input data. Moreover, we examine how QLSAs can efficiently solve the proposed system in an iterative refinement (IR) scheme to find the exact solution without excessive calls to QLSAs. We show that the proposed IR-IF-IPM can also be helpful to mitigate the impact of the condition number when a classical iterative method, such as a Conjugate Gradient method or a quantum solver is used at iterations of IPMs. After applying the proposed IF-IPM to the self-dual embedding formulation, we investigate the proposed IF-IPM's efficiency using the QISKIT simulator of QLSA.

math.OC

A quantum dual logarithmic barrier method for linear optimization

Quantum computing has the potential to speed up some optimization methods. One can use quantum computers to solve linear systems via Quantum Linear System Algorithms (QLSAs). QLSAs can be used as a subroutine for algorithms that require solving linear systems, such as the dual logarithmic barrier method (DLBM) for solving linear optimization (LO) problems. In this paper, we use a QLSA to solve the linear systems arising in each iteration of the DLBM. To use the QLSA in a hybrid setting, we read out quantum states via a tomography procedure which introduces considerable error and noise. Thus, this paper first proposes an inexact-feasible variant of DLBM for LO problems and then extends it to a quantum version. Our quantum approach has quadratic convergence toward the central path with inexact directions and we show that this method has the best-known $\mathcal{O}(\sqrt{n} \log (n μ_0 /ζ))$ iteration complexity, where $n$ is the number of variables, $μ_0$ is the initial duality gap, and $ζ$ is the desired accuracy. We further use iterative refinement to improve the time complexity dependence on accuracy. For LO problems with quadratically more constraints than variables, the quantum complexity of our method has a sublinear dependence on dimension.

math.OC

A preconditioned inexact infeasible quantum interior point method for linear optimization

Quantum Interior Point Methods (QIPMs) have been attracting significant interests recently due to their potential of solving optimization problems substantially faster than state-of-the-art conventional algorithms. In general, QIPMs use Quantum Linear System Algorithms (QLSAs) to substitute classical linear system solvers. However, the performance of QLSAs depends on the condition numbers of the linear systems, which are typically proportional to the square of the reciprocal of the duality gap in QIPMs. To improve conditioning, a preconditioned inexact infeasible QIPM (II-QIPM) based on optimal partition estimation is developed in this work. We improve the condition number of the linear systems in II-QIPMs from quadratic dependence on the reciprocal of the duality gap to linear, and obtain better dependence with respect to the accuracy when compared to other II-QIPMs. Our method also attains better dependence with respect to the dimension when compared to other inexact infeasible Interior Point Methods.

math.OC

An Efficient Quantum Algorithm for Linear System Problem in Tensor Format

Solving linear systems is at the foundation of many algorithms. Recently, quantum linear system algorithms (QLSAs) have attracted great attention since they converge to a solution exponentially faster than classical algorithms in terms of the problem dimension. However, low-complexity circuit implementations of the oracles assumed in these QLSAs constitute the major bottleneck for practical quantum speed-up in solving linear systems. In this work, we focus on the application of QLSAs for linear systems that are expressed as a low rank tensor sums, which arise in solving discretized PDEs. Previous works uses modified Krylov subspace methods to solve such linear systems with a per-iteration complexity being polylogarithmic of the dimension but with no guarantees on the total convergence cost. We propose a quantum algorithm based on the recent advances on adiabatic-inspired QLSA and perform a detailed analysis of the circuit depth of its implementation. We rigorously show that the total complexity of our implementation is polylogarithmic in the dimension, which is comparable to the per-iteration complexity of the classical heuristic methods.

quant-ph

Improvements to Quantum Interior Point Method for Linear Optimization

Quantum linear system algorithms (QLSA) have the potential to speed up Interior Point Methods (IPM). However, a major challenge is that QLSAs are inexact and sensitive to the condition number of the coefficient matrices of linear systems. This sensitivity is exacerbated when the Newton systems arising in IPMs converge to a singular matrix. Recently, an Inexact Feasible Quantum IPM (IF-QIPM) has been developed that addresses the inexactness of QLSAs and, in part, the influence of the condition number using iterative refinement. However, this method requires a large number of gates and qubits to be implemented. Here, we propose a new IF-QIPM using the normal equation system, which is more adaptable to near-term quantum devices. To mitigate the sensitivity to the condition number, we use preconditioning coupled with iterative refinement to obtain better gate complexity. Finally, we demonstrate the effectiveness of our approach on IBM Qiskit simulators

math.OC

An Inexact Feasible Quantum Interior Point Method for Linearly Constrained Quadratic Optimization

Quantum linear system algorithms (QLSAs) have the potential to speed up algorithms that rely on solving linear systems. Interior Point Methods (IPMs) yield a fundamental family of polynomial-time algorithms for solving optimization problems. IPMs solve a Newton linear system at each iteration to find the search direction, and thus QLSAs can potentially speed up IPMs. Due to the noise in contemporary quantum computers, such quantum-assisted IPM (QIPM) only allows an inexact solution for the Newton linear system. Typically, an inexact search direction leads to an infeasible solution. In our work, we propose an Inexact-Feasible QIPM (IF-QIPM) and show its advantage in solving linearly constrained quadratic optimization problems. We also apply the algorithm to $\ell_1$-norm soft margin support vector machine (SVM) problems and obtain the best complexity regarding dependence on dimension. This complexity bound is better than any existing classical or quantum algorithm that produces a classical solution.

math.OC