Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Springer eBooks

On the Simulation and Verification of Noisy Quantum Circuits

Seiichiro Tani

Published Jan 1, 2025• 0 citations
Publisher

Abstract

Abstract Noise is the most serious obstacle to developing quantum computers. This article reviews two recently published results that answer the essential questions on noisy quantum circuits in particular meaningful situations expected in the near future. The purpose of the article is not to provide comprehensive surveys but to introduce how to apply some essential state-of-the-art techniques to the simulation and verification of noisy quantum circuits. The first part reveals that even slight noise at the end of computation spoils the quantum advantage under a particular noise model. This raises the question of verifying that a given quantum circuit is not significantly affected by noise. The second part shows an efficient verification method of a given quantum circuit with the help of a smaller verified quantum circuit when the circuit to be verified is sparse and shallow.

DOI
10.1007/978-981-96-0668-9_18

Related papers

Dilemma between Quantum Speedup and Computational Reliability--Overcoming Errors with Efficient Verification Methods for Quantum Computing

Yuki Takeuchi, Seiichiro Tani

Quantum computers are expected to solve several problems faster than any classical computer.However, they may sometimes output incorrect answers because they are prone to errors.Therefore, to develop reliable quantum computers, it is essential to develop methods of verifying whether the outputs of quantum computers are correct.In this article, we introduce our recent research results on our verification methods.

NTT technical review•Oct 1, 2023•2 citations

Mitigating errors by quantum verification and postselection

Rawad Mezher, James K. Mills, Elham Kashefi

Correcting errors due to noise in quantum circuits run on current and near-term quantum hardware is essential for any convincing demonstration of quantum advantage. Indeed, in many cases it has been shown that noise renders quantum circuits efficiently classically simulable, thereby destroying any quantum advantage potentially offered by an ideal (noiseless) implementation of these circuits. Although the technique of quantum error correction (QEC) allows correcting these errors very accurately, QEC usually requires a large overhead of physical qubits which is not reachable with currently available quantum hardware. This has been the motivation behind the field of quantum error mitigation, which aims at developing techniques to correct an important part of the errors in quantum circuits, while also being compatible with current and near-term quantum hardware. In this work, we present a technique for quantum error mitigation which is based on a technique from quantum verification, the so-called accreditation protocol, together with postselection. Our technique allows for correcting the expectation value of an observable $O$, which is the output of multiple runs of noisy quantum circuits, where the noise in these circuits is at the level of preparations, gates, and measurements. We discuss the sample complexity of our procedure and provide rigorous guarantees of errors being mitigated under some realistic assumptions on the noise. Our technique is tailored to time-dependent behaviors, as we allow for the output states to be different between different runs of the accreditation protocol. We validate our findings by running our technique on currently available quantum hardware.

arXiv:2109.14329•Physical Review A•May 27, 2022•14 citations

A Review of Formal Methods in Quantum Circuit Verification

Arun Govindankutty

Quantum computing uses the laws of quantum mechanics to perform computation. Information is stored in qubits and processed using quantum gates arranged as quantum circuits. As quantum hardware grows in size and complexity, verifying these systems becomes increasingly difficult. Traditional verification methods do not scale well and quickly become computationally infeasible. This creates a strong need for more powerful and scalable verification techniques. Formal methods provide a potential solution to this problem. Techniques such as theorem proving, model checking, and symbolic reasoning offer mathematically rigorous ways to verify correctness, equivalence, and implementation. They also help detect design errors early in the development process. This review examines how formal methods are applied to quantum circuit verification. It focuses on barrier certificates, abstract interpretation, model checking, theorem proving approaches. The review discusses both the theoretical foundations and practical applications of these techniques. Their strengths and limitations are analysed through representative case studies. Finally, the review highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.

Qeios•Jan 24, 2026•0 citations

A Review of Formal Methods in Quantum Circuit Verification

Arun Govindankutty

Quantum computing uses the laws of quantum mechanics to perform computation. Information is stored in qubits and processed using quantum gates arranged as quantum circuits. As quantum hardware grows in size and complexity, verifying these systems becomes increasingly difficult. Traditional verification methods do not scale well and quickly become computationally infeasible. This creates a strong need for more powerful and scalable verification techniques. Formal methods provide a potential solution to this problem. Techniques such as theorem proving, model checking, and symbolic reasoning offer mathematically rigorous ways to verify correctness, equivalence, and implementation. They also help detect design errors early in the development process. This review examines how formal methods are applied to quantum circuit verification. It focuses on barrier certificates, abstract interpretation, model checking, theorem proving, and emerging hybrid approaches. The review discusses both the theoretical foundations and practical applications of these techniques. Their strengths and limitations are analysed through representative case studies. Finally, the review highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.

Qeios•Jan 8, 2026•0 citations

Noisy Random Quantum Circuit Sampling and its Classical Simulation

Meng Zhang, Chao Wang, Yong‐Jian Han

Abstract Demonstrating quantum advantage on noisy quantum devices is one of the most important tasks of quantum computing research in the near future. Random quantum circuit sampling is proposed as the most promising approach to the task and has been implemented in experiments for achieving quantum advantage. A series of encouraging computational complexity results, based on some plausible assumptions, show that this task is impossible to complete efficiently by classical computers. However, in practical experiments on noisy quantum devices, the approximate average‐case hardness and the effects of the noise need to be further checked. The competition between the classical simulation algorithm (mainly based on tensor network algorithms) and noisy quantum devices is the explicit way to understand quantum advantage in practice. This review briefly overviews the computational complexity arguments for the hardness of classical simulation of random quantum circuits sampling, then focus on various methods of classical simulation of quantum circuits based on tensor network method.

Advanced Quantum Technologies•May 9, 2023•4 citations

A Comprehensive Review of Quantum Circuit Optimization: Current Trends and Future Directions

Krishnageetha Karuppasamy, Varun Puram, Stevens Johnson +1 more

Optimizing quantum circuits is critical for enhancing computational speed and mitigating errors caused by quantum noise. Effective optimization must be achieved without compromising the correctness of the computations. This survey explores recent advancements in quantum circuit optimization, encompassing both hardware-independent and hardware-dependent techniques. It reviews state-of-the-art approaches, including analytical algorithms, heuristic strategies, machine learning-based methods, and hybrid quantum-classical frameworks. The paper highlights the strengths and limitations of each method, along with the challenges they pose. Furthermore, it identifies potential research opportunities in this evolving field, offering insights into the future directions of quantum circuit optimization.

arXiv:2408.08941•Quantum Reports•Jan 1, 2025•43 citations
Abstract Noise is the most serious obstacle to developing quantum computers. This article reviews two recently published results that answer the essential questions on noisy quantum circuits in particular meaningful situations expected in the near future. The purpose of the article is not to provide comprehensive surveys but to introduce how to apply some essential state-of-the-art techniques to the simulation and verification of noisy quantum circuits. The first part reveals that even slight noise at the end of computation spoils the quantum advantage under a particular noise model. This raises the question of verifying that a given quantum circuit is not significantly affected by noise. The second part shows an efficient verification method of a given quantum circuit with the help of a smaller verified quantum circuit when the circuit to be verified is sparse and shallow.
Correcting errors due to noise in quantum circuits run on current and near-term quantum hardware is essential for any convincing demonstration of quantum advantage. Indeed, in many cases it has been shown that noise renders quantum circuits efficiently classically simulable, thereby destroying any quantum advantage potentially offered by an ideal (noiseless) implementation of these circuits. Although the technique of quantum error correction (QEC) allows correcting these errors very accurately, QEC usually requires a large overhead of physical qubits which is not reachable with currently available quantum hardware. This has been the motivation behind the field of quantum error mitigation, which aims at developing techniques to correct an important part of the errors in quantum circuits, while also being compatible with current and near-term quantum hardware. In this work, we present a technique for quantum error mitigation which is based on a technique from quantum verification, the so-called accreditation protocol, together with postselection. Our technique allows for correcting the expectation value of an observable OOO, which is the output of multiple runs of noisy quantum circuits, where the noise in these circuits is at the level of preparations, gates, and measurements. We discuss the sample complexity of our procedure and provide rigorous guarantees of errors being mitigated under some realistic assumptions on the noise. Our technique is tailored to time-dependent behaviors, as we allow for the output states to be different between different runs of the accreditation protocol. We validate our findings by running our technique on currently available quantum hardware.
Quantum computing uses the laws of quantum mechanics to perform computation. Information is stored in qubits and processed using quantum gates arranged as quantum circuits. As quantum hardware grows in size and complexity, verifying these systems becomes increasingly difficult. Traditional verification methods do not scale well and quickly become computationally infeasible. This creates a strong need for more powerful and scalable verification techniques. Formal methods provide a potential solution to this problem. Techniques such as theorem proving, model checking, and symbolic reasoning offer mathematically rigorous ways to verify correctness, equivalence, and implementation. They also help detect design errors early in the development process. This review examines how formal methods are applied to quantum circuit verification. It focuses on barrier certificates, abstract interpretation, model checking, theorem proving approaches. The review discusses both the theoretical foundations and practical applications of these techniques. Their strengths and limitations are analysed through representative case studies. Finally, the review highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.
Quantum computing uses the laws of quantum mechanics to perform computation. Information is stored in qubits and processed using quantum gates arranged as quantum circuits. As quantum hardware grows in size and complexity, verifying these systems becomes increasingly difficult. Traditional verification methods do not scale well and quickly become computationally infeasible. This creates a strong need for more powerful and scalable verification techniques. Formal methods provide a potential solution to this problem. Techniques such as theorem proving, model checking, and symbolic reasoning offer mathematically rigorous ways to verify correctness, equivalence, and implementation. They also help detect design errors early in the development process. This review examines how formal methods are applied to quantum circuit verification. It focuses on barrier certificates, abstract interpretation, model checking, theorem proving, and emerging hybrid approaches. The review discusses both the theoretical foundations and practical applications of these techniques. Their strengths and limitations are analysed through representative case studies. Finally, the review highlights open challenges and identifies promising directions for future research. An extensive set of references is included to support further study and exploration.
Abstract Demonstrating quantum advantage on noisy quantum devices is one of the most important tasks of quantum computing research in the near future. Random quantum circuit sampling is proposed as the most promising approach to the task and has been implemented in experiments for achieving quantum advantage. A series of encouraging computational complexity results, based on some plausible assumptions, show that this task is impossible to complete efficiently by classical computers. However, in practical experiments on noisy quantum devices, the approximate average‐case hardness and the effects of the noise need to be further checked. The competition between the classical simulation algorithm (mainly based on tensor network algorithms) and noisy quantum devices is the explicit way to understand quantum advantage in practice. This review briefly overviews the computational complexity arguments for the hardness of classical simulation of random quantum circuits sampling, then focus on various methods of classical simulation of quantum circuits based on tensor network method.
Optimizing quantum circuits is critical for enhancing computational speed and mitigating errors caused by quantum noise. Effective optimization must be achieved without compromising the correctness of the computations. This survey explores recent advancements in quantum circuit optimization, encompassing both hardware-independent and hardware-dependent techniques. It reviews state-of-the-art approaches, including analytical algorithms, heuristic strategies, machine learning-based methods, and hybrid quantum-classical frameworks. The paper highlights the strengths and limitations of each method, along with the challenges they pose. Furthermore, it identifies potential research opportunities in this evolving field, offering insights into the future directions of quantum circuit optimization.