•• This position is filled ••
Overview
We are looking for applicants for the phd project
“Towards Zero-Defect Quantum Programs”.
The aim of the project is to develop methods for statically analysing programs intended for near-term quantum computers by combining techniques from the verification of probabilistic programs and the verification of quantum programs. This shall enable developers on quantum hardware to drastically reduce the amount of testing and simulation required, and to detect errors early in the program design and to understand them more easily, thus streamlining the software development process and significantly reducing testing and simulation costs. A particular focus will be on near-term systems with realistic error models (NISQ), and on use-cases from practice.
The project is a cooperation between the Chair of Quantum Information Systems and the Software Modeling and Verification (MOVES) group and will be jointly supervised by Joost-Pieter Katoen and Dominique Unruh.
How to apply?
Please send the following documents to both Joost-Pieter Katoen and Dominique Unruh:
- A letter of motivation including how exactly you see your connection to the project
- Curriculum vitae (please explain your scientific background)
- List of publications, if any
- A summary explaining your master thesis/thesis project (and possible connections to the position)
- At least two letters of reference (please ask for the letters to be sent directly to us)
- Masters degree (if you do not have it yet, provide whatever confirmation you can get)
- Transcript of records
All documents (except the recommendation letters) should be formatted as a single pdf-file. You should send your application ultimately by
September 25, 2023 (AoE)
by e-mail to both:
katoen@cs.rwth-aachen.de and zero.defect.j1dda8@rwth.unruh.de
Enquiries can also be directed to these e-mail addresses.
Required profile
Candidates must have (or soon obtain) a master degree in Computer Science, Mathematics, Physics or related area and have completed their studies with excellent grades. You should have interest in performing original, highly competitive scientific research, publishing your results in top conferences and scientific journals. Self-motivation and the ability to work both independently and as a team player in local and international research groups are expected. Fluency in English is required; proficiency in German is helpful but not compulsory.
What do we offer? We offer a stimulating international research environment, the possibility to participate in highly competitive and interdisciplinary research and the opportunity to involve students in your research through project work. Doctoral researchers have a status as employee with a salary according to the German federal employee scale TV-L E13; the exact salary is subject to your family situation. The duration of the position is four years.
RWTH Aachen University offers excellent facilities for professional and personal development.
Starting date of the position: early 2024.
Research plan
With accelerating development and rising importance of noisy intermediate scale quantum (NISQ) computers, the question how to program these computers becomes ever more relevant.
Developers on quantum software systems will face the need to design programs on quantum computers that have a complex, hard to predict behavior and take both quantum mechanics and noisy behavior into account.
To aid the developer, we will need systems that take as many tasks off their shoulders as possible. One aspect of this is to predict errors in the design of quantum algorithms before they happen and to understand the reason for the errors afterwards.
In classical software systems, testing and run-time debugging are powerful tools for this. While this is, to some degree, also possible on quantum systems, we face a number of challenges:
- Testing on a real quantum computer is expensive. Testing on a simulator is limited to problems that are still within the reach of classical systems; for interesting problems (in the domain of quantum advantage) this will not be feasible without scaling down the problem.
- The possibilities for debugging are limited: Inspecting data on an actual quantum system disturbs the data and disrupts the algorithm. And due to the probabilistic nature of quantum mechanics and of noisy systems, errors may not be reproducible between different runs.
This leaves a third option, the static analysis of programs. Specifically, the computer (on which we develop the quantum program) could, as part of a suitable development environment, analyze quantum algorithms, detect potential problems, determine amounts of errors, check claimed invariants (such as “this quantum register will not contain |0⟩”), determine equivalent but simpler (and thus less noisy) code, etc. Such a tool-suite will make the development more efficient, allow to reduce the reliance on expensive testing and simulation, give insight into reasons for errors beyond what testing/simulation can reveal, and can also be used in the design of future optimizing quantum compilers.
The aim of this doctoral project is to develop algorithms for verifying properties of quantum programs such as the ones listed above without having to execute the programs. These will specifically address use-cases that occur in the development of quantum algorithms on near-term quantum systems.
Due to the probabilistic nature of quantum mechanics and of the noise, we will heavily draw on existing research in the area of the analysis of probabilistic programs (and models). The supervisor Joost-Pieter Katoen will provide expertise is this area. But quantum mechanical systems also behave very differently from classical probabilistic systems; existing solutions for analyzing probabilistic systems will not carry over directly. Methods from quantum program verification will need to be combined with the probabilistic solutions. The supervisor Dominique Unruh will provide expertise in this area.
RWTH Aachen University is certified as a “Family-Friendly University”. We particularly welcome and encourage applications from women, disabled persons and ethnic minority groups, recognizing they are underrepresented across RWTH Aachen University. The principles of fair and open competition apply and appointments will be made on merit.