Using a novel formal methods approach, we have generated computer-veri ed proofs of major theorems pertinent to the quantum phase estimation algorithm. This was accomplished using our Prove-It software package in Python. While many formal methods tools are available, their practical utility is limited. Translating a problem of interest into these systems and working through the steps of a proof is an art form that requires much expertise. One must surrender to the preferences and restrictions of the tool regarding how mathematical notions are expressed and what deductions are allowed. Automation is a major driver that forces restrictions. Our focus, on the other hand, is to produce a tool that allows users the ability to con rm proofs that are essentially known already. This goal is valuable in itself. We demonstrate the viability of our approach that allows the user great exibility in expressing state- ments and composing derivations. There were no major obstacles in following a textbook proof of the quantum phase estimation algorithm. There were tedious details of algebraic manipulations that we needed to implement (and a few that we did not have time to enter into our system) and some basic components that we needed to rethink, but there were no serious roadblocks. In the process, we made a number of convenient additions to our Prove-It package that will make certain algebraic manipulations easier to perform in the future. In fact, our intent is for our system to build upon itself in this manner.
In this paper, we present a strategy for producing multiqubit gates that promise high fidelity with minimal tuning requirements. Our strategy combines gap protection from the adiabatic theorem with dynamical decoupling in a complementary manner. Energy-level transition errors are protected by adiabaticity and remaining phase errors are mitigated via dynamical decoupling. This is a powerful way to divide and conquer the various error channels. In order to accomplish this without violating a no-go theorem regarding black-box dynamically corrected gates [Phys. Rev. A 80, 032314 (2009)], we require a robust operating point (sweet spot) in control space where the qubits interact with little sensitivity to noise. There are also energy gap requirements for effective adiabaticity. We apply our strategy to an architecture in Si with P donors where we assume we can shuttle electrons between different donors. Electron spins act as mobile ancillary qubits and P nuclear spins act as long-lived data qubits. Furthermore, this system can have a very robust operating point where the electron spin is bound to a donor in the quadratic Stark shift regime. High fidelity single qubit gates may be performed using well-established global magnetic resonance pulse sequences. Single electron-spin preparation and measurement has also been demonstrated. Thus, putting this all together, we present a robust universal gate set for quantum computation.
The construction of high-fidelity control fields that are robust to control, system, and/or surrounding environment uncertainties is a crucial objective for quantum information processing. Using the two-state Landau-Zener model for illustrative simulations of a controlled qubit, we generate optimal controls for π/2 and π pulses and investigate their inherent robustness to uncertainty in the magnitude of the drift Hamiltonian. Next, we construct a quantum-control protocol to improve system-drift robustness by combining environment-decoupling pulse criteria and optimal control theory for unitary operations. By perturbatively expanding the unitary time-evolution operator for an open quantum system, previous analysis of environment-decoupling control pulses has calculated explicit control-field criteria to suppress environment-induced errors up to (but not including) third order from π/2 and π pulses. We systematically integrate this criteria with optimal control theory, incorporating an estimate of the uncertain parameter to produce improvements in gate fidelity and robustness, demonstrated via a numerical example based on double quantum dot qubits. For the qubit model used in this work, postfacto analysis of the resulting controls suggests that realistic control-field fluctuations and noise may contribute just as significantly to gate errors as system and environment fluctuations.