More Like this

1. Grammar Filtering for Syntax-Guided Synthesis

   https://doi.org/10.1609/aaai.v34i02.5522  

   Morton, Kairo; Hallahan, William; Shum, Elven; Piskac, Ruzica; Santolucito, Mark (June 2020, Proceedings of the AAAI Conference on Artificial Intelligence)

   Programming-by-example (PBE) is a synthesis paradigm that allows users to generate functions by simply providing input-output examples. While a promising interaction paradigm, synthesis is still too slow for realtime interaction and more widespread adoption. Existing approaches to PBE synthesis have used automated reasoning tools, such as SMT solvers, as well as works applying machine learning techniques. At its core, the automated reasoning approach relies on highly domain specific knowledge of programming languages. On the other hand, the machine learning approaches utilize the fact that when working with program code, it is possible to generate arbitrarily large training datasets. In this work, we propose a system for using machine learning in tandem with automated reasoning techniques to solve Syntax Guided Synthesis (SyGuS) style PBE problems. By preprocessing SyGuS PBE problems with a neural network, we can use a data driven approach to reduce the size of the search space, then allow automated reasoning-based solvers to more quickly find a solution analytically. Our system is able to run atop existing SyGuS PBE synthesis tools, decreasing the runtime of the winner of the 2019 SyGuS Competition for the PBE Strings track by 47.65% to outperform all of the competing tools. 

   more » « less
2. The unitary dependence theory for characterizing quantum circuits and states

   https://doi.org/10.1038/s42005-023-01188-y  

   Hu, Zixuan; Kais, Sabre (April 2023, Communications Physics)

   Abstract Most existing quantum algorithms are discovered accidentally or adapted from classical algorithms, and there is the need for a systematic theory to understand and design quantum circuits. Here we develop a unitary dependence theory to characterize the behaviors of quantum circuits and states in terms of how quantum gates manipulate qubits and determine their measurement probabilities. Compared to the conventional entanglement description of quantum circuits and states, the unitary dependence picture offers more practical information on the measurement and manipulation of qubits, easier generalization to many-qubit systems, and better robustness upon partitioning of the system. The unitary dependence theory can be applied to systematically understand existing quantum circuits and design new quantum algorithms. 

   more » « less
3. Statistical assertions for validating patterns and finding bugs in quantum programs

   https://doi.org/10.1145/3307650.3322213  

   Huang, Yipeng; Martonosi, Margaret (June 2019, Proceedings of the 46th International Symposium on Computer Architecture (ISCA ’19))

   In support of the growing interest in quantum computing experimentation, programmers need new tools to write quantum algorithms as program code. Compared to debugging classical programs, debugging quantum programs is difficult because programmers have limited ability to probe the internal states of quantum programs; those states are difficult to interpret even when observations exist; and programmers do not yet have guidelines for what to check for when building quantum programs. In this work, we present quantum program assertions based on statistical tests on classical observations. These allow programmers to decide if a quantum program state matches its expected value in one of classical, superposition, or entangled types of states. We extend an existing quantum programming language with the ability to specify quantum assertions, which our tool then checks in a quantum program simulator. We use these assertions to debug three benchmark quantum programs in factoring, search, and chemistry. We share what types of bugs are possible, and lay out a strategy for using quantum programming patterns to place assertions and prevent bugs. 

   more » « less
4. Preparing Hamiltonians for quantum simulation: A computational framework for Cartan decomposition via Lax dynamics

   https://doi.org/10.1090/mcom/4056  

   Chu, Moody (February 2025, Mathematics of Computation)

   Quantum algorithms usually are described via quantum circuits representable as unitary operators. Synthesizing the unitary operators described mathematically in terms of the unitary operators recognizable as quantum circuits is essential. One such a challenge lies in the Hamiltonian simulation problem, where the matrix exponential of a large-scale skew-Hermitian matrix is to be computed. Most current techniques are prone to approximation errors, whereas the parametrization of the underlying Hamiltonian via the Cartan decomposition is more promising. To prepare for such a simulation, this work proposes to tackle the Cartan decomposition by means of the Lax dynamics. The advantages include not only that it is numerically feasible with no matrices involved, but also that this approach offers a genuine unitary synthesis within the integration errors. This work contributes to the theoretic and algorithmic foundations in three aspects: exploiting the quaternary representation of Hamiltonian subalgebras; describing a common mechanism for deriving the Lax dynamics; and providing a mathematical theory of convergence. 

   more » « less
5. The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation

   https://doi.org/10.1145/3656397  

   Yuan, Charles; Carbin, Michael (June 2024, Proceedings of the ACM on Programming Languages)

   Numerous quantum algorithms require the use of quantum error correction to overcome the intrinsic unreliability of physical qubits. However, quantum error correction imposes a unique performance bottleneck, known asT-complexity, that can make an implementation of an algorithm as a quantum program run more slowly than on idealized hardware. In this work, we identify that programming abstractions for control flow, such as the quantum if-statement, can introduce polynomial increases in theT-complexity of a program. If not mitigated, this slowdown can diminish the computational advantage of a quantum algorithm. To enable reasoning about the costs of control flow, we present a cost model that a developer can use to accurately analyze theT-complexity of a program under quantum error correction and pinpoint the sources of slowdown. To enable the mitigation of these costs, we present a set of program-level optimizations that a developer can use to rewrite a program to reduce itsT-complexity, predict theT-complexity of the optimized program using the cost model, and then compile it to an efficient circuit via a straightforward strategy. We implement the program-level optimizations in Spire, an extension of the Tower quantum compiler. Using a set of 11 benchmark programs that use control flow, we empirically show that the cost model is accurate, and that Spire’s optimizations recover programs that are asymptotically efficient, meaning their runtimeT-complexity under error correction is equal to their time complexity on idealized hardware. Our results show that optimizing a program before it is compiled to a circuit can yield better results than compiling the program to an inefficient circuit and then invoking a quantum circuit optimizer found in prior work. For our benchmarks, only 2 of 8 tested quantum circuit optimizers recover circuits with asymptotically efficientT-complexity. Compared to these 2 optimizers, Spire uses 54×–2400× less compile time. 

   more » « less