DROPS

Document

DOI: 10.4230/LIPIcs.STACS.2026.66

Computational Hardness of Estimating Quantum Entropies via Binary Entropy Bounds

Authors: Yupan Liu

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract

We investigate the computational hardness of estimating the quantum α-Rényi entropy S^𝚁_α(ρ) = (ln Tr(ρ^α))/(1-α) and the quantum q-Tsallis entropy S^𝚃_q(ρ) = (1-Tr(ρ^q))/(q-1), both converging to the von Neumann entropy as the order approaches 1. The promise problems Quantum α-Rényi Entropy Approximation (RényiQEA_α) and Quantum q-Tsallis Entropy Approximation (TsallisQEA_q) ask whether S^𝚁_α(ρ) or S^𝚃_q(ρ), respectively, is at least τ_Y or at most τ_N, where τ_Y - τ_N is typically a positive constant. Previous hardness results cover only the von Neumann entropy (order 1) and some cases of the quantum q-Tsallis entropy, while existing approaches do not readily extend to other orders. We establish that for all positive real orders, the rank-2 variants Rank2RényiQEA_α and Rank2TsallisQEA_q are BQP-hard. Combined with prior (rank-dependent) quantum query algorithms in Wang, Guan, Liu, Zhang, and Ying (TIT 2024), Wang, Zhang, and Li (TIT 2024), and Liu and Wang (SODA 2025), our results imply: - For all real order α > 0 and 0 < q ≤ 1, LowRankRényiQEA_α and LowRankTsallisQEA_q are BQP-complete, where both are restricted versions of RényiQEA_α and TsallisQEA_q with ρ of polynomial rank. - For all real order q > 1, TsallisQEA_q is BQP-complete. Our hardness results stem from reductions based on new inequalities relating the α-Rényi or q-Tsallis binary entropies of different orders, where the reductions differ substantially from previous approaches, and the inequalities are also of independent interest.

Cite as

Yupan Liu. Computational Hardness of Estimating Quantum Entropies via Binary Entropy Bounds. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 66:1-66:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{liu:LIPIcs.STACS.2026.66,
  author =	{Liu, Yupan},
  title =	{{Computational Hardness of Estimating Quantum Entropies via Binary Entropy Bounds}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{66:1--66:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.66},
  URN =		{urn:nbn:de:0030-drops-255550},
  doi =		{10.4230/LIPIcs.STACS.2026.66},
  annote =	{Keywords: computational hardness, quantum state testing, quantum R\'{e}nyi entropy, quantum Tsallis entropy, von Neumann entropy}
}

Document

Extended Abstract

DOI: 10.4230/LIPIcs.ITCS.2026.13

Fully Quantum Computational Entropies (Extended Abstract)

Authors: Noam Avidan, Thomas A. Hahn, Joseph M. Renes, and Rotem Arnon

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract

Quantum information theory has provided the formal framework for describing how information is stored, transmitted, and transformed in physical quantum systems [Renes, 2022; Tomamichel, 2015; Wilde, 2013]. Its entropic formulations underpin our understanding of quantum computation, communication, and cryptography. Yet this theory traditionally treats all quantum operations as freely available, ignoring computational restrictions. In practice, however, any manipulation of quantum information must be performed by devices of bounded complexity and runtime. Capturing such realistic constraints requires extending quantum information theory to include computational efficiency as a fundamental component. This work takes a first step toward building a computational version of quantum information theory, one that treats efficiency as part of the theory itself. The goal is to understand how the behavior of quantum information changes when the parties involved can only perform computationally efficient operations. This approach bridges the abstract, ideal setting of quantum information theory with the practical limitations of real quantum devices, offering a means to study information processing under realistic resource constraints. At the center of this work are two new quantities: the quantum computational min-entropy and the quantum computational max-entropy. These entropies extend standard quantum entropies by explicitly limiting the computational power of the observer or adversary. The quantum computational min-entropy captures how unpredictable a quantum system A remains to an observer holding system B, when that observer is restricted to quantum circuits of bounded size. Formally, for a bipartite state ρ_{AB}, we define {H^c}^s_{min}(A|B)_{ρ} ≔ -log d_A max_{ℰ^s_{B→A'}} F((𝕀_A ⊗ ℰ^s)(ρ_{AB}),|Φ_{AA'}⟩⟨Φ_{AA'}|) , where the maximization is over quantum channels that can be implemented by circuits of size at most s, and F denotes fidelity with a maximally entangled state. In the classical setting, the min-entropy can be expressed through the maximal probability of correctly guessing a random variable given some side-information. In the fully quantum setting, this idea extends to uncertainty about quantum information [König et al., 2009], quantifying how well one system can be inferred from another using local quantum operations. Our definition generalizes this operational viewpoint by restricting the computational power of the observer to efficient quantum circuits. This definition extends the operational meaning of the information-theoretic quantum min-entropy [König et al., 2009] by incorporating computational constraints, and it provides the fully quantum counterpart of the classical unpredictability entropy [Hsiao et al., 2007]. We establish fundamental properties for the computational min-entropy, including monotonicity in the circuit size and smoothing parameters, efficient data-processing inequalities, and fully quantum leakage and purification chain rules, which were left as open questions in earlier definitions of quantum computational entropies [Yi-Hsiu Chen et al., 2017; Munson et al., 2025]. For classical–quantum states, it coincides with the previously defined quantum computational unpredictability entropy [Noam Avidan and Rotem Arnon, 2025], showing that the new definition correctly generalizes known results. We also introduce the quantum computational max-entropy through a duality relation [Tomamichel et al., 2010] with the min-entropy using a fixed purification. Finally, we prove unconditional separations between the computational and information-theoretic entropies, demonstrating that computational restrictions can fundamentally alter entropic behavior even for simple states. These results establish the fundamental mathematical framework for studying quantum information within realistic computational constraints. By integrating efficiency directly into entropic quantities, they open the door to a fully developed computational quantum information theory that parallels its information-theoretic counterpart. Such a framework provides the foundation for analyzing cryptographic security against computationally bounded quantum adversaries [Noam Avidan and Rotem Arnon, 2025] and the limits of efficient quantum state manipulation. More broadly, it suggests that many core notions in quantum information theory may have refined computational analogues yet to be explored.

Cite as

Noam Avidan, Thomas A. Hahn, Joseph M. Renes, and Rotem Arnon. Fully Quantum Computational Entropies (Extended Abstract). In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 13:1-13:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{avidan_et_al:LIPIcs.ITCS.2026.13,
  author =	{Avidan, Noam and Hahn, Thomas A. and Renes, Joseph M. and Arnon, Rotem},
  title =	{{Fully Quantum Computational Entropies}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{13:1--13:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.13},
  URN =		{urn:nbn:de:0030-drops-253003},
  doi =		{10.4230/LIPIcs.ITCS.2026.13},
  annote =	{Keywords: quantum information theory, computational entropy, min-entropy, max-entropy}
}

Document

DOI: 10.4230/LIPIcs.ITCS.2026.83

The Pure-State Consistency of Local Density Matrices Problem: In PSPACE and Complete for a Class Between QMA and QMA(2)

Authors: Jonas Kamminga and Dorian Rudolph

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract

In this work we investigate the computational complexity of the pure consistency of local density matrices (PureCLDM) and pure N-representability (Pure-N-Representability; analog of PureCLDM for bosonic or fermionic systems) problems. In these problems the input is a set of reduced density matrices and the task is to determine whether there exists a global pure state consistent with these reduced density matrices. While mixed CLDM, i.e. where the global state can be mixed, was proven to be QMA-complete by Broadbent and Grilo [JoC 2022], almost nothing was known about the complexity of the pure version. Before our work the best upper and lower bounds were QMA(2) and QMA. Our contribution to the understanding of these problems is twofold. Firstly, we define a pure state analogue of the complexity class QMA^+ of Aharanov and Regev [FOCS 2003], which we call PureSuperQMA. We prove that both pure-N-Representability and PureCLDM are complete for this new class. Along the way we supplement Broadbent and Grilo by proving hardness for 2-qubit reduced density matrices and showing that mixed N-Representability is QMA-complete. Secondly, we improve the upper bound on PureCLDM. Using methods from algebraic geometry, we prove that PureSuperQMA ⊆ PSPACE. Our methods, and the PSPACE upper bound, are also valid for PureCLDM with exponential or even perfect precision, hence precisePureCLDM is not preciseQMA(2) = NEXP-complete, unless PSPACE = NEXP. We view this as evidence for a negative answer to the longstanding open question whether PureCLDM is QMA(2)-complete. The techniques we develop for our PSPACE upper bound are quite general. We are able to use them for various applications: from proving PSPACE upper bounds on other quantum problems to giving an efficient parallel (NC) algorithm for (non-convex) quadratically constrained quadratic programs with few constraints.

Cite as

Jonas Kamminga and Dorian Rudolph. The Pure-State Consistency of Local Density Matrices Problem: In PSPACE and Complete for a Class Between QMA and QMA(2). In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 83:1-83:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kamminga_et_al:LIPIcs.ITCS.2026.83,
  author =	{Kamminga, Jonas and Rudolph, Dorian},
  title =	{{The Pure-State Consistency of Local Density Matrices Problem: In PSPACE and Complete for a Class Between QMA and QMA(2)}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{83:1--83:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.83},
  URN =		{urn:nbn:de:0030-drops-253701},
  doi =		{10.4230/LIPIcs.ITCS.2026.83},
  annote =	{Keywords: Quantum Complexity Theory, PSPACE, QMA(2), Consistency of Local Density Matrices, Polynomial Optimization}
}

Document

DOI: 10.4230/LIPIcs.ITCS.2026.27

Identity Check Problem for Shallow Quantum Circuits

Authors: Sergey Bravyi, Natalie Parham, and Minh Tran

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract

Verifying that a quantum circuit correctly implements a desired transformation is essential for validating quantum algorithms. We consider the closely related identity check problem: given a quantum circuit U, estimate the diamond-norm distance between U and the identity channel. Ji and Wu showed that estimating this distance to within an additive 1/poly error is QMA-hard, even when U is constant-depth and 1D local - ruling out efficient algorithms in this regime. We show that this hardness barrier disappears if one seeks a constant multiplicative-approximation instead. We present a classical algorithm that, for shallow geometrically local D-dimensional circuits, approximates the distance to the identity within a factor α = D+1, provided that the circuit is sufficiently close to the identity. The runtime of the algorithm scales linearly with the number of qubits for any constant circuit depth and spatial dimension. We also show that the operator-norm distance to the identity ‖U-I‖ can be efficiently approximated within a factor α = 5 for shallow 1D circuits and, under a certain technical condition, within a factor α = 2D+3 for shallow D-dimensional circuits. A numerical implementation of the identity check algorithm is reported for 1D Trotter circuits with up to 100 qubits.

Cite as

Sergey Bravyi, Natalie Parham, and Minh Tran. Identity Check Problem for Shallow Quantum Circuits. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bravyi_et_al:LIPIcs.ITCS.2026.27,
  author =	{Bravyi, Sergey and Parham, Natalie and Tran, Minh},
  title =	{{Identity Check Problem for Shallow Quantum Circuits}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.27},
  URN =		{urn:nbn:de:0030-drops-253147},
  doi =		{10.4230/LIPIcs.ITCS.2026.27},
  annote =	{Keywords: Quantum computing, Identity check problem, quantum circuits, classical simulation of quantum computation, shallow circuits}
}

Document

DOI: 10.4230/LIPIcs.ESA.2025.51

Quantum Approximate k-Minimum Finding

Authors: Minbo Gao, Zhengfeng Ji, and Qisheng Wang

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract

Quantum k-minimum finding is a fundamental subroutine with numerous applications in combinatorial problems and machine learning. Previous approaches typically assume oracle access to exact function values, making it challenging to integrate this subroutine with other quantum algorithms. In this paper, we propose an (almost) optimal quantum k-minimum finding algorithm that works with approximate values for all k ≥ 1, extending a result of van Apeldoorn, Gilyén, Gribling, and de Wolf (FOCS 2017) for k = 1. As practical applications, we present efficient quantum algorithms for identifying the k smallest expectation values among multiple observables and for determining the k lowest ground state energies of a Hamiltonian with a known eigenbasis.

Cite as

Minbo Gao, Zhengfeng Ji, and Qisheng Wang. Quantum Approximate k-Minimum Finding. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 51:1-51:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gao_et_al:LIPIcs.ESA.2025.51,
  author =	{Gao, Minbo and Ji, Zhengfeng and Wang, Qisheng},
  title =	{{Quantum Approximate k-Minimum Finding}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{51:1--51:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.51},
  URN =		{urn:nbn:de:0030-drops-245192},
  doi =		{10.4230/LIPIcs.ESA.2025.51},
  annote =	{Keywords: Quantum Computing, Quantum Algorithms, Quantum Minimum Finding}
}

Document

DOI: 10.4230/LIPIcs.TQC.2025.3

Mixing Time of Quantum Gibbs Sampling for Random Sparse Hamiltonians

Authors: Akshar Ramkumar and Mehdi Soleimanifar

Published in: LIPIcs, Volume 350, 20th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2025)

Abstract

Providing evidence that quantum computers can efficiently prepare low-energy or thermal states of physically relevant interacting quantum systems is a major challenge in quantum information science. A newly developed quantum Gibbs sampling algorithm [Chen et al., 2023] provides an efficient simulation of the detailed-balanced dissipative dynamics of non-commutative quantum systems. The running time of this algorithm depends on the mixing time of the corresponding quantum Markov chain, which has not been rigorously bounded except in the high-temperature regime. In this work, we establish a polylog(n) upper bound on its mixing time for various families of random n × n sparse Hamiltonians at any constant temperature. We further analyze how the choice of the jump operators for the algorithm and the spectral properties of these sparse Hamiltonians influence the mixing time. Our result places this method for Gibbs sampling on par with other efficient algorithms for preparing low-energy states of quantumly easy Hamiltonians.

Cite as

Akshar Ramkumar and Mehdi Soleimanifar. Mixing Time of Quantum Gibbs Sampling for Random Sparse Hamiltonians. In 20th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 350, pp. 3:1-3:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ramkumar_et_al:LIPIcs.TQC.2025.3,
  author =	{Ramkumar, Akshar and Soleimanifar, Mehdi},
  title =	{{Mixing Time of Quantum Gibbs Sampling for Random Sparse Hamiltonians}},
  booktitle =	{20th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2025)},
  pages =	{3:1--3:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-392-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{350},
  editor =	{Fefferman, Bill},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2025.3},
  URN =		{urn:nbn:de:0030-drops-240520},
  doi =		{10.4230/LIPIcs.TQC.2025.3},
  annote =	{Keywords: Quantum algorithms, quantum Gibbs sampling, mixing time analysis}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2025.85

Cutoff Theorems for the Equivalence of Parameterized Quantum Circuits

Authors: Neil J. Ross and Scott Wesley

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract

Many promising quantum algorithms in economics, medical science, and material science rely on circuits that are parameterized by a large number of angles. To ensure that these algorithms are efficient, these parameterized circuits must be heavily optimized. However, most quantum circuit optimizers are not verified, so this procedure is known to be error-prone. For this reason, there is growing interest in the design of equivalence checking algorithms for parameterized quantum circuits. In this paper, we define a generalized class of parameterized circuits with arbitrary rotations and show that this problem is decidable for cyclotomic gate sets. We propose a cutoff-based procedure which reduces the problem of verifying the equivalence of parameterized quantum circuits to the problem of verifying the equivalence of finitely many parameter-free quantum circuits. Because the number of parameter-free circuits grows exponentially with the number of parameters, we also propose a probabilistic variant of the algorithm for cases when the number of parameters is intractably large. We show that our techniques extend to equivalence modulo global phase, and describe an efficient angle sampling procedure for cyclotomic gate sets.

Cite as

Neil J. Ross and Scott Wesley. Cutoff Theorems for the Equivalence of Parameterized Quantum Circuits. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 85:1-85:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ross_et_al:LIPIcs.MFCS.2025.85,
  author =	{Ross, Neil J. and Wesley, Scott},
  title =	{{Cutoff Theorems for the Equivalence of Parameterized Quantum Circuits}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{85:1--85:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.85},
  URN =		{urn:nbn:de:0030-drops-241921},
  doi =		{10.4230/LIPIcs.MFCS.2025.85},
  annote =	{Keywords: Quantum Circuits, Parameterized Equivalence Checking}
}

Document

DOI: 10.4230/LIPIcs.CP.2025.38

Reducing Quantum Circuit Synthesis to #SAT

Authors: Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, and Alfons Laarman

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract

Quantum circuit synthesis is the task of decomposing a given quantum operator into a sequence of elementary quantum gates. Since the finite target gate set cannot exactly implement any given operator, approximation is often necessary. Model counting, or #SAT, has recently been demonstrated as a promising new approach for tackling core problems in quantum circuit analysis. In this work, we show for the first time that the universal quantum circuit synthesis problem can be reduced to maximum model counting. We formulate a #SAT encoding for exact and approximate depth-optimal quantum circuit synthesis into the Clifford+T gate set. We evaluate our method with an open-source implementation that uses the maximum model counter d4Max as a backend. For this purpose, we extended d4Max with support for complex and negative weights to represent amplitudes. Experimental results show that existing classical tools have potential for the quantum circuit synthesis problem.

Cite as

Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, and Alfons Laarman. Reducing Quantum Circuit Synthesis to #SAT. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zak_et_al:LIPIcs.CP.2025.38,
  author =	{Zak, Dekel and Mei, Jingyi and Lagniez, Jean-Marie and Laarman, Alfons},
  title =	{{Reducing Quantum Circuit Synthesis to #SAT}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{38:1--38:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.38},
  URN =		{urn:nbn:de:0030-drops-238997},
  doi =		{10.4230/LIPIcs.CP.2025.38},
  annote =	{Keywords: Maximum weighted model counting, quantum circuit synthesis}
}

Document

Track A: Algorithms, Complexity and Games

DOI: 10.4230/LIPIcs.ICALP.2025.61

How to Compute the Volume in Low Dimension?

Authors: Arjan Cornelissen, Simon Apers, and Sander Gribling

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract

Estimating the volume of a convex body is a canonical problem in theoretical computer science. Its study has led to major advances in randomized algorithms, Markov chain theory, and computational geometry. In particular, determining the query complexity of volume estimation to a membership oracle has been a longstanding open question. Most of the previous work focuses on the high-dimensional limit. In this work, we tightly characterize the deterministic, randomized and quantum query complexity of this problem in the high-precision limit, i.e., when the dimension is constant.

Cite as

Arjan Cornelissen, Simon Apers, and Sander Gribling. How to Compute the Volume in Low Dimension?. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 61:1-61:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cornelissen_et_al:LIPIcs.ICALP.2025.61,
  author =	{Cornelissen, Arjan and Apers, Simon and Gribling, Sander},
  title =	{{How to Compute the Volume in Low Dimension?}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{61:1--61:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.61},
  URN =		{urn:nbn:de:0030-drops-234381},
  doi =		{10.4230/LIPIcs.ICALP.2025.61},
  annote =	{Keywords: Query complexity, computational geometry, quantum computing, volume estimation, high-precision limit}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2025.16

Quantum Data Sketches

Authors: Qin Zhang and Mohsen Heidari

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract

Recent advancements in quantum technologies, particularly in quantum sensing and simulation, have facilitated the generation and analysis of inherently quantum data. This progress underscores the necessity for developing efficient and scalable quantum data management strategies. This goal faces immense challenges due to the exponential dimensionality of quantum data and its unique quantum properties such as no-cloning and measurement stochasticity. Specifically, classical storage and manipulation of an arbitrary n-qubit quantum state requires exponential space and time. Hence, there is a critical need to revisit foundational data management concepts and algorithms for quantum data. In this paper, we propose succinct quantum data sketches to support basic database operations such as search and selection. We view our work as an initial step towards the development of quantum data management model, opening up many possibilities for future research in this direction.

Cite as

Qin Zhang and Mohsen Heidari. Quantum Data Sketches. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ICDT.2025.16,
  author =	{Zhang, Qin and Heidari, Mohsen},
  title =	{{Quantum Data Sketches}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{16:1--16:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.16},
  URN =		{urn:nbn:de:0030-drops-229570},
  doi =		{10.4230/LIPIcs.ICDT.2025.16},
  annote =	{Keywords: quantum data representation, data sketching, query execution}
}

Document

DOI: 10.4230/LIPIcs.ITCS.2025.78

Randomized Lifting to Semi-Structured Communication Complexity via Linear Diversity

Authors: Vladimir Podolskii and Alexander Shekhovtsov

Published in: LIPIcs, Volume 325, 16th Innovations in Theoretical Computer Science Conference (ITCS 2025)

Abstract

We study query-to-communication lifting. The major open problem in this area is to prove a lifting theorem for gadgets of constant size. The recent paper [Paul Beame and Sajin Koroth, 2023] introduces semi-structured communication complexity, in which one of the players can only send parities of their input bits. They have shown that for any m ≥ 4 deterministic decision tree complexity of a function f can be lifted to the so called semi-structured communication complexity of f∘Ind_m, where Ind_m is the Indexing gadget. As our main contribution we extend these results to randomized setting. Our results also apply to a substantially larger set of gadgets. More specifically, we introduce a new complexity measure of gadgets, linear diversity. For all gadgets g with non-trivial linear diversity we show that randomized decision tree complexity of f lifts to randomized semi-structured communication complexity of f∘g. In particular, this gives tight lifting results for Indexing gadget Ind_m, Inner Product gadget IP_m for all m ≥ 2, and for Majority gadget MAJ_m for all m ≥ 4. We prove the same results for deterministic case. From our result it immediately follows that deterministic/randomized decision tree complexity lifts to deterministic/randomized parity decision tree complexity. For randomized case this is the first result of this type. For deterministic case, our result improves the bound in [Arkadev Chattopadhyay et al., 2023] for Inner Product gadget. To obtain our results we introduce a new secret sets approach to simulation of semi-structured communication protocols by decision trees. It allows us to simulate (restricted classes of) communication protocols on truly uniform distribution of inputs.

Cite as

Vladimir Podolskii and Alexander Shekhovtsov. Randomized Lifting to Semi-Structured Communication Complexity via Linear Diversity. In 16th Innovations in Theoretical Computer Science Conference (ITCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 325, pp. 78:1-78:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{podolskii_et_al:LIPIcs.ITCS.2025.78,
  author =	{Podolskii, Vladimir and Shekhovtsov, Alexander},
  title =	{{Randomized Lifting to Semi-Structured Communication Complexity via Linear Diversity}},
  booktitle =	{16th Innovations in Theoretical Computer Science Conference (ITCS 2025)},
  pages =	{78:1--78:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-361-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{325},
  editor =	{Meka, Raghu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2025.78},
  URN =		{urn:nbn:de:0030-drops-227061},
  doi =		{10.4230/LIPIcs.ITCS.2025.78},
  annote =	{Keywords: communication complexity, decision trees, lifting}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2024.24

Qafny: A Quantum-Program Verifier

Authors: Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract

Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny’s automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover’s algorithm, and Shor’s algorithm.

Cite as

Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. Qafny: A Quantum-Program Verifier. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 24:1-24:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ECOOP.2024.24,
  author =	{Li, Liyi and Zhu, Mingwei and Cleaveland, Rance and Nicolellis, Alexander and Lee, Yi and Chang, Le and Wu, Xiaodi},
  title =	{{Qafny: A Quantum-Program Verifier}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{24:1--24:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.24},
  URN =		{urn:nbn:de:0030-drops-208735},
  doi =		{10.4230/LIPIcs.ECOOP.2024.24},
  annote =	{Keywords: Quantum Computing, Automated Verification, Separation Logic}
}

Document

Artifact

DOI: 10.4230/DARTS.10.2.12

Qafny: A Quantum-Program Verifier (Artifact)

Authors: Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract

This artifact contains the Coq theory files for the Qafny proof system, including the formalism of the Qafny syntax, semantics, type system, and proof system, with the theorem proofs of type soundness, proof system soundness and completeness. It also contains a the compiled Dafny example programs generated from our Qafny-to-Dafny prototype compiler. These example programs serve as the validations of our Qafny-to-Dafny prototype compiler mechanism. The main work is introduced in the Qafny paper, which develops a separation logic style verification framework for quantum programs.

Cite as

Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. Qafny: A Quantum-Program Verifier (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 12:1-12:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{li_et_al:DARTS.10.2.12,
  author =	{Li, Liyi and Zhu, Mingwei and Cleaveland, Rance and Nicolellis, Alexander and Lee, Yi and Chang, Le and Wu, Xiaodi},
  title =	{{Qafny: A Quantum-Program Verifier (Artifact)}},
  pages =	{12:1--12:2},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Li, Liyi and Zhu, Mingwei and Cleaveland, Rance and Nicolellis, Alexander and Lee, Yi and Chang, Le and Wu, Xiaodi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.12},
  URN =		{urn:nbn:de:0030-drops-209104},
  doi =		{10.4230/DARTS.10.2.12},
  annote =	{Keywords: Quantum Computing, Automated Verification, Separation Logic}
}

Document

DOI: 10.4230/LIPIcs.ITP.2021.21

Proving Quantum Programs Correct

Authors: Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract

As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Grover’s algorithm and quantum phase estimation, a key component of Shor’s algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.

Cite as

Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. Proving Quantum Programs Correct. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hietala_et_al:LIPIcs.ITP.2021.21,
  author =	{Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Li, Liyi and Hicks, Michael},
  title =	{{Proving Quantum Programs Correct}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{21:1--21:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.21},
  URN =		{urn:nbn:de:0030-drops-139160},
  doi =		{10.4230/LIPIcs.ITP.2021.21},
  annote =	{Keywords: Formal Verification, Quantum Computing, Proof Engineering}
}

Document

DOI: 10.4230/LIPIcs.ITC.2020.8

Lower Bounds for Function Inversion with Quantum Advice

Authors: Kai-Min Chung, Tai-Ning Liao, and Luowen Qian

Published in: LIPIcs, Volume 163, 1st Conference on Information-Theoretic Cryptography (ITC 2020)

Abstract

Function inversion is the problem that given a random function f: [M] → [N], we want to find pre-image of any image f^{-1}(y) in time T. In this work, we revisit this problem under the preprocessing model where we can compute some auxiliary information or advice of size S that only depends on f but not on y. It is a well-studied problem in the classical settings, however, it is not clear how quantum algorithms can solve this task any better besides invoking Grover’s algorithm [Grover, 1996], which does not leverage the power of preprocessing. Nayebi et al. [Nayebi et al., 2015] proved a lower bound ST² ≥ ̃Ω(N) for quantum algorithms inverting permutations, however, they only consider algorithms with classical advice. Hhan et al. [Minki Hhan et al., 2019] subsequently extended this lower bound to fully quantum algorithms for inverting permutations. In this work, we give the same asymptotic lower bound to fully quantum algorithms for inverting functions for fully quantum algorithms under the regime where M = O(N). In order to prove these bounds, we generalize the notion of quantum random access code, originally introduced by Ambainis et al. [Ambainis et al., 1999], to the setting where we are given a list of (not necessarily independent) random variables, and we wish to compress them into a variable-length encoding such that we can retrieve a random element just using the encoding with high probability. As our main technical contribution, we give a nearly tight lower bound (for a wide parameter range) for this generalized notion of quantum random access codes, which may be of independent interest.

Cite as

Kai-Min Chung, Tai-Ning Liao, and Luowen Qian. Lower Bounds for Function Inversion with Quantum Advice. In 1st Conference on Information-Theoretic Cryptography (ITC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 163, pp. 8:1-8:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chung_et_al:LIPIcs.ITC.2020.8,
  author =	{Chung, Kai-Min and Liao, Tai-Ning and Qian, Luowen},
  title =	{{Lower Bounds for Function Inversion with Quantum Advice}},
  booktitle =	{1st Conference on Information-Theoretic Cryptography (ITC 2020)},
  pages =	{8:1--8:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-151-1},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{163},
  editor =	{Tauman Kalai, Yael and Smith, Adam D. and Wichs, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITC.2020.8},
  URN =		{urn:nbn:de:0030-drops-121134},
  doi =		{10.4230/LIPIcs.ITC.2020.8},
  annote =	{Keywords: Cryptanalysis, Data Structures, Quantum Query Complexity}
}

22 Search Results for "Wu, Xiaodi"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message