17 Search Results for "Wu, Xiaodi"

Document
DOI: 10.4230/LIPIcs.ESA.2024.101
Time-Efficient Quantum Entropy Estimator via Samplizer

Authors: Qisheng Wang and Zhicheng Zhang

Published in: LIPIcs, Volume 308, 32nd Annual European Symposium on Algorithms (ESA 2024)

Abstract
Entropy is a measure of the randomness of a system. Estimating the entropy of a quantum state is a basic problem in quantum information. In this paper, we introduce a time-efficient quantum approach to estimating the von Neumann entropy S(ρ) and Rényi entropy S_α(ρ) of an N-dimensional quantum state ρ, given access to independent samples of ρ. Specifically, we provide the following quantum estimators. - A quantum estimator for S(ρ) with time complexity Õ(N²), improving the prior best time complexity Õ(N⁶) by Acharya, Issa, Shende, and Wagner (2020) and Bavarian, Mehraba, and Wright (2016). - A quantum estimator for S_α(ρ) with time complexity Õ(N^{4/α-2}) for 0 < α < 1 and Õ(N^{4-2/α}) for α > 1, improving the prior best time complexity Õ(N^{6/α}) for 0 < α < 1 and Õ(N⁶) for α > 1 by Acharya, Issa, Shende, and Wagner (2020), though at a cost of a slightly larger sample complexity. Moreover, these estimators are naturally extensible to the low-rank case. We also provide a sample lower bound Ω(max{N/ε, N^{1/α-1}/ε^{1/α}}) for estimating S_α(ρ). Technically, our method is quite different from the previous ones that are based on weak Schur sampling and Young diagrams. At the heart of our construction, is a novel tool called samplizer, which can "samplize" a quantum query algorithm to a quantum algorithm with similar behavior using only samples of quantum states; this suggests a unified framework for estimating quantum entropies. Specifically, when a quantum oracle U block-encodes a mixed quantum state ρ, any quantum query algorithm using Q queries to U can be samplized to a δ-close (in the diamond norm) quantum algorithm using Θ~(Q²/δ) samples of ρ. Moreover, this samplization is proven to be optimal, up to a polylogarithmic factor.
Cite as

Qisheng Wang and Zhicheng Zhang. Time-Efficient Quantum Entropy Estimator via Samplizer. In 32nd Annual European Symposium on Algorithms (ESA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 308, pp. 101:1-101:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.ESA.2024.101,
  author =	{Wang, Qisheng and Zhang, Zhicheng},
  title =	{{Time-Efficient Quantum Entropy Estimator via Samplizer}},
  booktitle =	{32nd Annual European Symposium on Algorithms (ESA 2024)},
  pages =	{101:1--101:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-338-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{308},
  editor =	{Chan, Timothy and Fischer, Johannes and Iacono, John 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.2024.101},
  URN =		{urn:nbn:de:0030-drops-211722},
  doi =		{10.4230/LIPIcs.ESA.2024.101},
  annote =	{Keywords: Quantum computing, entropy estimation, von Neumann entropy, R\'{e}nyi entropy, sample complexity}
}
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.2024.15
Typed Compositional Quantum Computation with Lenses

Authors: Jacques Garrigue and Takafumi Saikawa

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq, currying on quantum states allows one to apply quantum gates directly inside a complex circuit. By introducing a discrete notion of lens to control this currying, we are further able to separate the combinatorics of the circuit structure from the computational content of gates. We apply our development to define quantum circuits recursively from the bottom up, and prove their correctness compositionally.
Cite as

Jacques Garrigue and Takafumi Saikawa. Typed Compositional Quantum Computation with Lenses. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{garrigue_et_al:LIPIcs.ITP.2024.15,
  author =	{Garrigue, Jacques and Saikawa, Takafumi},
  title =	{{Typed Compositional Quantum Computation with Lenses}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.15},
  URN =		{urn:nbn:de:0030-drops-207431},
  doi =		{10.4230/LIPIcs.ITP.2024.15},
  annote =	{Keywords: quantum programming, semantics, lens, currying, Coq, MathComp}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.29
Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving

Authors: Jiong Yang, Yaroslav A. Kharkov, Yunong Shi, Marijn J. H. Heule, and Bruno Dutertre

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Quantum Computing (QC) is a new computational paradigm that promises significant speedup over classical computing in various domains. However, near-term QC faces numerous challenges, including limited qubit connectivity and noisy quantum operations. To address the qubit connectivity constraint, circuit mapping is required for executing quantum circuits on quantum computers. This process involves performing initial qubit placement and using the quantum SWAP operations to relocate non-adjacent qubits for nearest-neighbor interaction. Reducing the SWAP count in circuit mapping is essential for improving the success rate of quantum circuit execution as SWAPs are costly and error-prone. In this work, we introduce a novel circuit mapping method by combining incremental and parallel solving for Boolean Satisfiability (SAT). We present an innovative SAT encoding for circuit mapping problems, which significantly improves solver-based mapping methods and provides a smooth trade-off between compilation quality and compilation time. Through comprehensive benchmarking of 78 instances covering 3 quantum algorithms on 2 distinct quantum computer topologies, we demonstrate that our method is 26× faster than state-of-the-art solver-based methods, reducing the compilation time from hours to minutes for important quantum applications. Our method also surpasses the existing heuristics algorithm by 26% in SWAP count.
Cite as

Jiong Yang, Yaroslav A. Kharkov, Yunong Shi, Marijn J. H. Heule, and Bruno Dutertre. Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.SAT.2024.29,
  author =	{Yang, Jiong and Kharkov, Yaroslav A. and Shi, Yunong and Heule, Marijn J. H. and Dutertre, Bruno},
  title =	{{Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.29},
  URN =		{urn:nbn:de:0030-drops-205517},
  doi =		{10.4230/LIPIcs.SAT.2024.29},
  annote =	{Keywords: Quantum computing, Quantum compilation, SAT solving, Incremental solving, Parallel solving}
}
Document
DOI: 10.4230/LIPIcs.CCC.2024.6
The Entangled Quantum Polynomial Hierarchy Collapses

Authors: Sabee Grewal and Justin Yirka

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)

Abstract
We introduce the entangled quantum polynomial hierarchy, QEPH, as the class of problems that are efficiently verifiable given alternating quantum proofs that may be entangled with each other. We prove QEPH collapses to its second level. In fact, we show that a polynomial number of alternations collapses to just two. As a consequence, QEPH = QRG(1), the class of problems having one-turn quantum refereed games, which is known to be contained in PSPACE. This is in contrast to the unentangled quantum polynomial hierarchy, QPH, which contains QMA(2). We also introduce DistributionQCPH, a generalization of the quantum-classical polynomial hierarchy QCPH where the provers send probability distributions over strings (instead of strings). We prove DistributionQCPH = QCPH, suggesting that only quantum superposition (not classical probability) increases the computational power of these hierarchies. To prove this equality, we generalize a game-theoretic result of Lipton and Young (1994) which says that, without loss of generality, the provers can send uniform distributions over a polynomial-size support. We also prove the analogous result for the polynomial hierarchy, i.e., DistributionPH = PH. Finally, we show that PH and QCPH are contained in QPH, resolving an open question of Gharibian et al. (2022).
Cite as

Sabee Grewal and Justin Yirka. The Entangled Quantum Polynomial Hierarchy Collapses. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{grewal_et_al:LIPIcs.CCC.2024.6,
  author =	{Grewal, Sabee and Yirka, Justin},
  title =	{{The Entangled Quantum Polynomial Hierarchy Collapses}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.6},
  URN =		{urn:nbn:de:0030-drops-204028},
  doi =		{10.4230/LIPIcs.CCC.2024.6},
  annote =	{Keywords: Polynomial hierarchy, Entangled proofs, Correlated proofs, Minimax}
}
Document
DOI: 10.4230/LIPIcs.CCC.2024.26
Dimension Independent Disentanglers from Unentanglement and Applications

Authors: Fernando Granha Jeronimo and Pei Wu

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)

Abstract
Quantum entanglement, a distinctive form of quantum correlation, has become a key enabling ingredient in diverse applications in quantum computation, complexity, cryptography, etc. However, the presence of unwanted adversarial entanglement also poses challenges and even prevents the correct behaviour of many protocols and applications. In this paper, we explore methods to "break" the quantum correlations. Specifically, we construct a dimension-independent k-partite disentangler (like) channel from bipartite unentangled input. In particular, we show: For every d,𝓁 ≥ k ∈ ℕ^+, there is an efficient channel Λ : ℂ^{d𝓁} ⊗ ℂ^{d𝓁} → ℂ^{dk} such that for every bipartite separable density operator ρ₁⊗ ρ₂, the output Λ(ρ₁⊗ρ₂) is close to a k-partite separable state. Concretely, for some distribution μ on states from C^d, ║ Λ(ρ₁⊗ρ₂) - ∫ |ψ⟩⟨ψ|^{⊗k} dμ(ψ) ║₁ ≤ Õ((k³/𝓁)^{1/4}). Moreover, Λ(|ψ⟩⟨ψ|^{⊗𝓁} ⊗ |ψ⟩⟨ψ|^{⊗𝓁}) = |ψ⟩⟨ψ|^{⊗k}. Without the bipartite unentanglement assumption, the above bound is conjectured to be impossible and would imply QMA(2) = QMA. Leveraging multipartite unentanglement ensured by our disentanglers, we achieve the following: (i) a new proof that QMA(2) admits arbitrary gap amplification; (ii) a variant of the swap test and product test with improved soundness, addressing a major limitation of their original versions. More importantly, we demonstrate that unentangled quantum proofs of almost general real amplitudes capture NEXP, thereby greatly relaxing the non-negative amplitudes assumption in the recent work of QMA^+(2) = NEXP [Jeronimo and Wu, STOC 2023]. Specifically, our findings show that to capture NEXP, it suffices to have unentangled proofs of the form |ψ⟩ = √a |ψ_{+}⟩ + √{1-a} |ψ_{-}⟩ where |ψ_{+}⟩ has non-negative amplitudes, |ψ_{-}⟩ only has negative amplitudes and |a-(1-a)| ≥ 1/poly(n) with a ∈ [0,1]. Additionally, we present a protocol achieving an almost largest possible completeness-soundness gap before obtaining QMA^ℝ(k) = NEXP, namely, a 1/poly(n) additive improvement to the gap results in this equality.
Cite as

Fernando Granha Jeronimo and Pei Wu. Dimension Independent Disentanglers from Unentanglement and Applications. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 26:1-26:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jeronimo_et_al:LIPIcs.CCC.2024.26,
  author =	{Jeronimo, Fernando Granha and Wu, Pei},
  title =	{{Dimension Independent Disentanglers from Unentanglement and Applications}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{26:1--26:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.26},
  URN =		{urn:nbn:de:0030-drops-204228},
  doi =		{10.4230/LIPIcs.CCC.2024.26},
  annote =	{Keywords: QMA(2), disentangler, quantum proofs}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.13
Learning Low-Degree Quantum Objects

Authors: Srinivasan Arunachalam, Arkopal Dutt, Francisco Escudero Gutiérrez, and Carlos Palazuelos

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
We consider the problem of learning low-degree quantum objects up to ε-error in 𝓁₂-distance. We show the following results: (i) unknown n-qubit degree-d (in the Pauli basis) quantum channels and unitaries can be learned using O(1/ε^d) queries (which is independent of n), (ii) polynomials p:{-1,1}ⁿ → [-1,1] arising from d-query quantum algorithms can be learned from O((1/ε)^d ⋅ log n) many random examples (x,p(x)) (which implies learnability even for d = O(log n)), and (iii) degree-d polynomials p:{-1,1}ⁿ → [-1,1] can be learned through O(1/ε^d) queries to a quantum unitary U_p that block-encodes p. Our main technical contributions are new Bohnenblust-Hille inequalities for quantum channels and completely bounded polynomials.
Cite as

Srinivasan Arunachalam, Arkopal Dutt, Francisco Escudero Gutiérrez, and Carlos Palazuelos. Learning Low-Degree Quantum Objects. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arunachalam_et_al:LIPIcs.ICALP.2024.13,
  author =	{Arunachalam, Srinivasan and Dutt, Arkopal and Escudero Guti\'{e}rrez, Francisco and Palazuelos, Carlos},
  title =	{{Learning Low-Degree Quantum Objects}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.13},
  URN =		{urn:nbn:de:0030-drops-201563},
  doi =		{10.4230/LIPIcs.ICALP.2024.13},
  annote =	{Keywords: Tomography}
}
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}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.25
Distributional Property Testing in a Quantum World

Authors: András Gilyén and Tongyang Li

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
A fundamental problem in statistics and learning theory is to test properties of distributions. We show that quantum computers can solve such problems with significant speed-ups. We also introduce a novel access model for quantum distributions, enabling the coherent preparation of quantum samples, and propose a general framework that can naturally handle both classical and quantum distributions in a unified manner. Our framework generalizes and improves previous quantum algorithms for testing closeness between unknown distributions, testing independence between two distributions, and estimating the Shannon / von Neumann entropy of distributions. For classical distributions our algorithms significantly improve the precision dependence of some earlier results. We also show that in our framework procedures for classical distributions can be directly lifted to the more general case of quantum distributions, and thus obtain the first speed-ups for testing properties of density operators that can be accessed coherently rather than only via sampling.
Cite as

András Gilyén and Tongyang Li. Distributional Property Testing in a Quantum World. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gilyen_et_al:LIPIcs.ITCS.2020.25,
  author =	{Gily\'{e}n, Andr\'{a}s and Li, Tongyang},
  title =	{{Distributional Property Testing in a Quantum World}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.25},
  URN =		{urn:nbn:de:0030-drops-117100},
  doi =		{10.4230/LIPIcs.ITCS.2020.25},
  annote =	{Keywords: distributional property testing, quantum algorithms, quantum query complexity}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2019.12
Formal Verification vs. Quantum Uncertainty

Authors: Robert Rand, Kesha Hietala, and Michael Hicks

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
Quantum programming is hard: Quantum programs are necessarily probabilistic and impossible to examine without disrupting the execution of a program. In response to this challenge, we and a number of other researchers have written tools to verify quantum programs against their intended semantics. This is not enough. Verifying an idealized semantics against a real world quantum program doesn't allow you to confidently predict the program’s output. In order to have verification that works, you need both an error semantics related to the hardware at hand (this is necessarily low level) and certified compilation to the that same hardware. Once we have these two things, we can talk about an approach to quantum programming where we start by writing and verifying programs at a high level, attempt to verify properties of the compiled code, and repeat as necessary.
Cite as

Robert Rand, Kesha Hietala, and Michael Hicks. Formal Verification vs. Quantum Uncertainty. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 12:1-12:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{rand_et_al:LIPIcs.SNAPL.2019.12,
  author =	{Rand, Robert and Hietala, Kesha and Hicks, Michael},
  title =	{{Formal Verification vs. Quantum Uncertainty}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{12:1--12:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.12},
  URN =		{urn:nbn:de:0030-drops-105558},
  doi =		{10.4230/LIPIcs.SNAPL.2019.12},
  annote =	{Keywords: Formal Verification, Quantum Computing, Programming Languages, Quantum Error Correction, Certified Compilation, NISQ}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2019.27
Quantum SDP Solvers: Large Speed-Ups, Optimality, and Applications to Quantum Learning

Authors: Fernando G. S. L. Brandão, Amir Kalev, Tongyang Li, Cedric Yen-Yu Lin, Krysta M. Svore, and Xiaodi Wu

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We give two new quantum algorithms for solving semidefinite programs (SDPs) providing quantum speed-ups. We consider SDP instances with m constraint matrices, each of dimension n, rank at most r, and sparsity s. The first algorithm assumes an input model where one is given access to an oracle to the entries of the matrices at unit cost. We show that it has run time O~(s^2 (sqrt{m} epsilon^{-10} + sqrt{n} epsilon^{-12})), with epsilon the error of the solution. This gives an optimal dependence in terms of m, n and quadratic improvement over previous quantum algorithms (when m ~~ n). The second algorithm assumes a fully quantum input model in which the input matrices are given as quantum states. We show that its run time is O~(sqrt{m}+poly(r))*poly(log m,log n,B,epsilon^{-1}), with B an upper bound on the trace-norm of all input matrices. In particular the complexity depends only polylogarithmically in n and polynomially in r. We apply the second SDP solver to learn a good description of a quantum state with respect to a set of measurements: Given m measurements and a supply of copies of an unknown state rho with rank at most r, we show we can find in time sqrt{m}*poly(log m,log n,r,epsilon^{-1}) a description of the state as a quantum circuit preparing a density matrix which has the same expectation values as rho on the m measurements, up to error epsilon. The density matrix obtained is an approximation to the maximum entropy state consistent with the measurement data considered in Jaynes' principle from statistical mechanics. As in previous work, we obtain our algorithm by "quantizing" classical SDP solvers based on the matrix multiplicative weight update method. One of our main technical contributions is a quantum Gibbs state sampler for low-rank Hamiltonians, given quantum states encoding these Hamiltonians, with a poly-logarithmic dependence on its dimension, which is based on ideas developed in quantum principal component analysis. We also develop a "fast" quantum OR lemma with a quadratic improvement in gate complexity over the construction of Harrow et al. [Harrow et al., 2017]. We believe both techniques might be of independent interest.
Cite as

Fernando G. S. L. Brandão, Amir Kalev, Tongyang Li, Cedric Yen-Yu Lin, Krysta M. Svore, and Xiaodi Wu. Quantum SDP Solvers: Large Speed-Ups, Optimality, and Applications to Quantum Learning. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brandao_et_al:LIPIcs.ICALP.2019.27,
  author =	{Brand\~{a}o, Fernando G. S. L. and Kalev, Amir and Li, Tongyang and Lin, Cedric Yen-Yu and Svore, Krysta M. and Wu, Xiaodi},
  title =	{{Quantum SDP Solvers: Large Speed-Ups, Optimality, and Applications to Quantum Learning}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{27:1--27:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.27},
  URN =		{urn:nbn:de:0030-drops-106036},
  doi =		{10.4230/LIPIcs.ICALP.2019.27},
  annote =	{Keywords: quantum algorithms, semidefinite program, convex optimization}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2019.35
Query-To-Communication Lifting for BPP Using Inner Product

Authors: Arkadev Chattopadhyay, Yuval Filmus, Sajin Koroth, Or Meir, and Toniann Pitassi

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We prove a new query-to-communication lifting for randomized protocols, with inner product as gadget. This allows us to use a much smaller gadget, leading to a more efficient lifting. Prior to this work, such a theorem was known only for deterministic protocols, due to Chattopadhyay et al. [Arkadev Chattopadhyay et al., 2017] and Wu et al. [Xiaodi Wu et al., 2017]. The only query-to-communication lifting result for randomized protocols, due to Göös, Pitassi and Watson [Mika Göös et al., 2017], used the much larger indexing gadget. Our proof also provides a unified treatment of randomized and deterministic lifting. Most existing proofs of deterministic lifting theorems use a measure of information known as thickness. In contrast, Göös, Pitassi and Watson [Mika Göös et al., 2017] used blockwise min-entropy as a measure of information. Our proof uses the blockwise min-entropy framework to prove lifting theorems in both settings in a unified way.
Cite as

Arkadev Chattopadhyay, Yuval Filmus, Sajin Koroth, Or Meir, and Toniann Pitassi. Query-To-Communication Lifting for BPP Using Inner Product. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 35:1-35:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chattopadhyay_et_al:LIPIcs.ICALP.2019.35,
  author =	{Chattopadhyay, Arkadev and Filmus, Yuval and Koroth, Sajin and Meir, Or and Pitassi, Toniann},
  title =	{{Query-To-Communication Lifting for BPP Using Inner Product}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{35:1--35:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.35},
  URN =		{urn:nbn:de:0030-drops-106110},
  doi =		{10.4230/LIPIcs.ICALP.2019.35},
  annote =	{Keywords: lifting theorems, inner product, BPP Lifting, Deterministic Lifting}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2019.99
Improvements in Quantum SDP-Solving with Applications

Authors: Joran van Apeldoorn and András Gilyén

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
Following the first paper on quantum algorithms for SDP-solving by Brandão and Svore [Brandão and Svore, 2017] in 2016, rapid developments have been made on quantum optimization algorithms. In this paper we improve and generalize all prior quantum algorithms for SDP-solving and give a simpler and unified framework. We take a new perspective on quantum SDP-solvers and introduce several new techniques. One of these is the quantum operator input model, which generalizes the different input models used in previous work, and essentially any other reasonable input model. This new model assumes that the input matrices are embedded in a block of a unitary operator. In this model we give a O~((sqrt{m}+sqrt{n}gamma)alpha gamma^4) algorithm, where n is the size of the matrices, m is the number of constraints, gamma is the reciprocal of the scale-invariant relative precision parameter, and alpha is a normalization factor of the input matrices. In particular for the standard sparse-matrix access, the above result gives a quantum algorithm where alpha=s. We also improve on recent results of Brandão et al. [Fernando G. S. L. Brandão et al., 2018], who consider the special case when the input matrices are proportional to mixed quantum states that one can query. For this model Brandão et al. [Fernando G. S. L. Brandão et al., 2018] showed that the dependence on n can be replaced by a polynomial dependence on both the rank and the trace of the input matrices. We remove the dependence on the rank and hence require only a dependence on the trace of the input matrices. After we obtain these results we apply them to a few different problems. The most notable of which is the problem of shadow tomography, recently introduced by Aaronson [Aaronson, 2018]. Here we simultaneously improve both the sample and computational complexity of the previous best results. Finally we prove a new Omega~(sqrt{m}alpha gamma) lower bound for solving LPs and SDPs in the quantum operator model, which also implies a lower bound for the model of Brandão et al. [Fernando G. S. L. Brandão et al., 2018].
Cite as

Joran van Apeldoorn and András Gilyén. Improvements in Quantum SDP-Solving with Applications. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 99:1-99:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{vanapeldoorn_et_al:LIPIcs.ICALP.2019.99,
  author =	{van Apeldoorn, Joran and Gily\'{e}n, Andr\'{a}s},
  title =	{{Improvements in Quantum SDP-Solving with Applications}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{99:1--99:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.99},
  URN =		{urn:nbn:de:0030-drops-106750},
  doi =		{10.4230/LIPIcs.ICALP.2019.99},
  annote =	{Keywords: quantum algorithms, semidefinite programming, shadow tomography}
}
  • Refine by Author
  • 5 Wu, Xiaodi
  • 3 Li, Liyi
  • 2 Chang, Le
  • 2 Chung, Kai-Min
  • 2 Cleaveland, Rance
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Program verification
  • 3 Theory of computation → Quantum complexity theory
  • 3 Theory of computation → Quantum information theory
  • 3 Theory of computation → Quantum query complexity
  • 2 Software and its engineering → Formal software verification
  • Show More...

  • Refine by Keyword
  • 4 Quantum Computing
  • 3 quantum algorithms
  • 2 Automated Verification
  • 2 Formal Verification
  • 2 Quantum computing
  • Show More...

  • Refine by Type
  • 17 document

  • Refine by Publication Year
  • 8 2024
  • 4 2019
  • 2 2020
  • 1 2015
  • 1 2016
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact