UC Santa Barbara engineering
Explore the need for specification languages in quantum algorithms, correctness verification methods, programmer assertions, success probabilities, scalable compilation techniques, and language design ideas. Emphasizing the importance of tracking precision, error bounds, and optimizing quantum operations for successful quantum programs.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Quantum Programming Languages for Specification and Optimization Fred Chong UC Santa Barbara Ken Brown, Ravi Chugh, Margaret Martonosi, John Reppy and Wim van Dam GaTech, Princeton, U Chicago, UCSB
IARPA Algorithms Algorithm Boolean Formula Linear Systems Binary Welded Tree Class Number Triangle Finding Shortest Vector Problem Ground State Estimation Lines of Code 479 1741 608 226 1231 539 554 Started with algorithms specified in English prose, some pseudocode 2
Correctness? Need a specification language for algorithms Check implementation against the specification Simulation for small problem sizes (~30 qubits) Type systems Model checking Symbolic execution Certified compilation passes General quantum properties No-cloning, entanglement, uncomputation Programmer assertions 3
Programmer Assertion Example b_eig_U = Eigenvalue(b,U) CascadeU(a,b,U) if not(b_eig_U) assert(Entangled(a,b)) 4
Success Probabilities / Error Bounds measure(a) assert(precision(a, 8)) /*precision of a is at least 10-8 */ assert(error(a, 0.5)) /*probability of error in a < 0.5 */ Quantum operations are approximate (eg rotations) Need to track achieved precision Quantum programs often involve multiple trials Assume error probability is low enough for success in small number of trials Type system that tracks probabilities Static analysis when possible Symbolic execution when necessary 5
Scalable Compilation Need deep optimization given known inputs Constant propagation Function cloning Loop unrolling Need to optimize parallelism and communication Constraints such as SIMD control Need to optimize success probabilities and error correction 6
Language Design Ideas Embedded, high-level front-end language Lower-level backend language with industrial- strength, scalable analysis tools Type system for verifying quantum properties and calculating success probabilities / errors Longer term: Verification or direct code generation using Unitary Transforms ORAQL/NQCS 7
