Verified Simulation for Large Quantum Systems (VSL-Q)

Programming classical computers has become a popular practice thanks to high-level programming languages and compilers which enable the running of high-level programs on different computing platforms. For critical applications, there now exist verified compilation schemes and certified compilers, which ensure the correctness of the compiled executions. This is done by reference to a mathematical model of the high-level code. 

This project will establish such a promising trajectory for quantum computing, taking into account the subtle features of quantum computers. This will be achieved by bringing together expertise in software testing and quantum simulation.  

The project has three key technical objectives: 

• To develop a compositional and expressive method for specifying the different representations of quantum systems at different layers of abstraction and the mappings between them. 
• To devise efficient algorithms for checking timed and stochastic conformance among different mappings, and devise a symbolic method to reason about data parameters that will allow for different instantiations of the mappings for quantum simulation problems and other quantum computations. 
• To evaluate the developed methodology on large-scale case studies for simulating fermionic systems via Hamiltonian time-evolution and qubitisation methods based on ideas from quantum signal processing. These will provide strong benchmarks for both NISQ and fault-tolerant algorithms. 

The results of this research will lead to verified software for quantum computing applications and, consequently, to widespread and effective exploitation of quantum computing. VSL-Q will enable popular and effective use of quantum computing by providing verified compilation schemes from high-level quantum programming languages into low-level representations.