arXiv subjects

Jie-Hong Roland Jiang

Publications and source records attributed to Jie-Hong Roland Jiang.

7 recordsLinked to original sources

arXiv2026

Quantum circuit synthesis for the preparation of arbitrary and highly sparse mixed quantum states

This paper addresses the challenge of preparing mixed quantum states -- both arbitrary states in general and highly sparse ones in particular -- an area that has received far less attention than the preparation of pure states. We present two classes of circuit-synthesis methods: one based on constructing the density matrix as a mixture of pure states and the other based on purification. To improve both preprocessing efficiency and the complexity of the resulting circuits, we propose a novel strategy based on the Cholesky decomposition, which offers significant advantages, especially when the target density matrix is highly or extremely sparse. Furthermore, by exploiting incomplete Cholesky decomposition with threshold dropping, we introduce a practical approach for constructing high-fidelity approximations of the target density matrix. This approach enables substantial reductions in circuit complexity at the cost of negligible or only mild fidelity loss.

quant-ph↗

arXiv2026

Adiabatic Quantum Simulation of the Topological Su--Schrieffer--Heeger--Hubbard Model

We develop an adiabatic quantum simulation framework on gate-based quantum computers to probe topological signatures of the one-dimensional fermionic Su--Schrieffer--Heeger--Hubbard (SSHH) model. We present explicit quantum-circuit constructions for initial-state preparation and time evolution, together with a practical measurement protocol and classical post-processing procedure for extracting the many-body Berry phase and the spatial profile of the sublattice polarization. Using classical simulations of the proposed circuits, we demonstrate -- for the first time within a genuine many-body framework -- that the topological characteristics of the SSH model remain robust against weak Hubbard interactions but eventually break down as the chiral-symmetry-breaking component of the interaction exceeds a threshold. The required qubit number, gate complexity, measurement shots, and classical pre- and post-processing costs all scale polynomially with system size. Our results provide a proof-of-concept framework for probing topological properties of interacting many-body systems via adiabatic quantum simulation on future large-scale quantum computers.

quant-ph↗

arXiv2026

Error-Tolerant Quantum State Discrimination: Optimization and Quantum Circuit Synthesis

We develop error-tolerant quantum state discrimination(QSD) strategies that maintain reliable performance under moderate noise. Two complementary approaches are proposed: CrossQSD, which generalizes unambiguous discrimination with tunable confidence bounds to balance accuracy and efficiency, and FitQSD, which optimizes the measurement outcome distribution to approximate that of the ideal noiseless case. Furthermore, we provide a unified hybrid-objective QSD framework that continuously interpolates between minimum-error discrimination (MED) and FitQSD, allowing flexible trade-offs among competing objectives. The associated optimization problems are formulated as convex programs and efficiently solved via disciplined convex programming or, in many cases, semidefinite programming. Additionally, a circuit synthesis framework based on a modified Naimark dilation and isometry synthesis enables hardware-efficient implementations with substantially reduced qubit and gate resources. An open-source toolkit automates the full optimization and synthesis workflow, providing a practical route to QSD on current quantum devices.

quant-ph↗

arXiv2026

Neuro-Symbolic Compliance: Integrating LLMs and SMT Solvers for Automated Financial Legal Analysis

Financial regulations are increasingly complex, hindering automated compliance-especially the maintenance of logical consistency with minimal human oversight. We introduce a Neuro-Symbolic Compliance Framework that integrates Large Language Models (LLMs) with Satisfiability Modulo Theories (SMT) solvers to enable formal verifiability and optimization-based compliance correction. The LLM interprets statutes and enforcement cases to generate SMT constraints, while the solver enforces consistency and computes the minimal factual modification required to restore legality when penalties arise. Unlike transparency-oriented methods, our approach emphasizes logic-driven optimization, delivering verifiable, legally consistent reasoning rather than post-hoc explanation. Evaluated on 87 enforcement cases from Taiwan's Financial Supervisory Commission (FSC), the system attains 86.2% correctness in SMT code generation, improves reasoning efficiency by over 100x, and consistently corrects violations-establishing a preliminary foundation for optimization-based compliance applications.

cs.AI↗

arXiv2025

Enhanced Quantum Circuit Cutting Framework for Sampling Overhead Reduction

The recently developed quantum circuit cutting technique greatly extends the capabilities of current noisy intermediate-scale quantum (NISQ) hardware. However, it introduces substantial overhead in both classical postprocessing and quantum resources, as the postprocessing complexity and sampling cost scale exponentially with the number of circuit cuts. In this work, we propose an enhanced circuit cutting framework, ShotQC, which effectively reduces the sampling overhead through two key optimizations: shot distribution and cut parameterization. The former employs an adaptive Monte Carlo strategy to dynamically allocate more quantum resources to subcircuit configurations that contribute more to the variance in the final outcome. The latter exploits additional degrees of freedom in postprocessing to further suppress variance. Integrating these optimizations, ShotQC significantly reduces the sampling overhead without increasing classical postprocessing complexity, as demonstrated across a range of benchmark circuits.

quant-ph↗

arXiv2025

Model Counting for Dependency Quantified Boolean Formulas

Dependency Quantified Boolean Formulas (DQBF) generalize QBF by explicitly specifying which universal variables each existential variable depends on, instead of relying on a linear quantifier order. The satisfiability problem of DQBF is NEXP-complete, and many hard problems can be succinctly encoded as DQBF. Recent work has revealed a strong analogy between DQBF and SAT: k-DQBF (with k existential variables) is a succinct form of k-SAT, and satisfiability is NEXP-complete for 3-DQBF but PSPACE-complete for 2-DQBF, mirroring the complexity gap between 3-SAT (NP-complete) and 2-SAT (NL-complete). Motivated by this analogy, we study the model counting problem for DQBF, denoted #DQBF. Our main theoretical result is that #2-DQBF is #EXP-complete, where #EXP is the exponential-time analogue of #P. This parallels Valiant's classical theorem stating that #2-SAT is #P-complete. As a direct application, we show that first-order model counting (FOMC) remains #EXP-complete even when restricted to a PSPACE-decidable fragment of first-order logic and domain size two. Building on recent successes in reducing 2-DQBF satisfiability to symbolic model checking, we develop a dedicated 2-DQBF model counter. Using a diverse set of crafted instances, we experimentally evaluated it against a baseline that expands 2-DQBF formulas into propositional formulas and applies propositional model counting. While the baseline worked well when each existential variable depends on few variables, our implementation scaled significantly better to larger dependency sets.

cs.LO↗

arXiv2013

Synthesizing Multiple Boolean Functions using Interpolation on a Single Proof

It is often difficult to correctly implement a Boolean controller for a complex system, especially when concurrency is involved. Yet, it may be easy to formally specify a controller. For instance, for a pipelined processor it suffices to state that the visible behavior of the pipelined system should be identical to a non-pipelined reference system (Burch-Dill paradigm). We present a novel procedure to efficiently synthesize multiple Boolean control signals from a specification given as a quantified first-order formula (with a specific quantifier structure). Our approach uses uninterpreted functions to abstract details of the design. We construct an unsatisfiable SMT formula from the given specification. Then, from just one proof of unsatisfiability, we use a variant of Craig interpolation to compute multiple coordinated interpolants that implement the Boolean control signals. Our method avoids iterative learning and back-substitution of the control functions. We applied our approach to synthesize a controller for a simple two-stage pipelined processor, and present first experimental results.

cs.LO↗