# [PhD proposal] A graphical approach for simulation and verification in quantum computing

## A graphical approach for simulation and verification in quantum computing.

**Supervision :** Simon Perdrix (simon.perdrix@loria.fr), Emmanuel Jeandel (emmanuel.jeandel@loria.fr)

### Context

Quantum information processing theoretically solves some computer problems beyond the reach of conventional computers. The recent announcements form Google, the European flagship on quantum technologies, the British (NQIT) and Dutch (QuTech) programs, and the commercialization of new quantum machines by D-Wave, demonstrate that quantum computing is entering a new era. The emergence of quantum machines is very promising, but also opens new concrete problems such as programming and quantum verification of these machines. Indeed, are the quantum machines marketed today really quantum? Can they be effectively simulated with a conventional computer? The emergence of the quantum computer must also be accompanied by adapted programming languages. The development of formal tools and methods for the verification and use of quantum machines is therefore essential in the development of the quantum computer.

ZX-calculus is a powerful graphical language for quantum computing. The ZX-calculus has multiple applications in quantum information theory: quantum error correcting codes, measurement-based quantum computing, but also fundamental questions of quantum mechanics.

### Objectives

ZX-calculus is a diagram language with a powerful equational theory that allows you to decide if two diagrams represent the same quantum evolution. However, deciding whether two diagrams are equivalent may require a large number of calculation steps.

- The first objective will be to develop techniques to give the necessary conditions to the equivalence of diagrams, based for example on invariants, or random evaluations of diagrams.
- The second objective will be to develop algorithms to efficiently read and simulate ZX-calculus diagrams and also to identify families of diagrams for which semantic calculation can be effective, for example using structural properties such as tree width.
- Finally, the previous points will also be addressed in the case where the diagrams are parameterized by variables: under what condition can the problem be reduced to the case without variables?

The theoretical results of these three points will be implemented and integrated into the Quantomatic tool, a diagrammatic proof assistant.