-
Verifying Quantum Phase Estimation (QPE) using Prove-It
Authors:
Wayne M. Witzel,
Warren D. Craft,
Robert Carr,
Deepak Kapur
Abstract:
The general-purpose interactive theorem-proving assistant called Prove-It was used to verify the Quantum Phase Estimation (QPE) algorithm, specifically claims about its outcome probabilities. Prove-It is unique in its ability to express sophisticated mathematical statements, including statements about quantum circuits, integrated firmly within its formal theorem-proving framework. We demonstrate o…
▽ More
The general-purpose interactive theorem-proving assistant called Prove-It was used to verify the Quantum Phase Estimation (QPE) algorithm, specifically claims about its outcome probabilities. Prove-It is unique in its ability to express sophisticated mathematical statements, including statements about quantum circuits, integrated firmly within its formal theorem-proving framework. We demonstrate our ability to follow a textbook proof to produce a formally certified proof, highlighting useful automation features to fill in obvious steps and make formal proving nearly as straightforward as informal theorem proving. Finally, we make comparisons with formal theorem-proving in other systems where similar claims about QPE have been proven.
△ Less
Submitted 4 April, 2023;
originally announced April 2023.
-
Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge
Authors:
Wayne M. Witzel,
Warren D. Craft,
Robert D. Carr,
Joaquín E. Madrid Larrañaga
Abstract:
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps using LaTeX. We review Prove-It's highly expressive representati…
▽ More
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps using LaTeX. We review Prove-It's highly expressive representation of expressions, judgments, theorems, and proofs; demonstrate the system by constructing a traditional proof-by-contradiction that $\sqrt{2}\notin\mathbb{Q}$; and discuss how the system avoids inconsistencies such as Russell's and Curry's paradoxes. Extensive documentation is provided in the appendices about core elements of the system. Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.
△ Less
Submitted 26 December, 2020; v1 submitted 20 December, 2020;
originally announced December 2020.
-
Fractional Decomposition Tree Algorithm: A tool for studying the integrality gap of Integer Programs
Authors:
Robert D. Carr,
Arash Haddadan,
Cynthia A. Phillips
Abstract:
We present a new algorithm, Fractional Decomposition Tree (FDT) for finding a feasible solution for an integer program (IP) where all variables are binary. FDT runs in polynomial time and is guaranteed to find a feasible integer solution provided the integrality gap is bounded. The algorithm gives a construction for Carr and Vempala's theorem that any feasible solution to the IP's linear-programmi…
▽ More
We present a new algorithm, Fractional Decomposition Tree (FDT) for finding a feasible solution for an integer program (IP) where all variables are binary. FDT runs in polynomial time and is guaranteed to find a feasible integer solution provided the integrality gap is bounded. The algorithm gives a construction for Carr and Vempala's theorem that any feasible solution to the IP's linear-programming relaxation, when scaled by the instance integrality gap, dominates a convex combination of feasible solutions. FDT is also a tool for studying the integrality gap of IP formulations. We demonstrate that with experiments studying the integrality gap of two problems: optimally augmenting a tree to a 2-edge-connected graph and finding a minimum-cost 2-edge-connected multi-subgraph (2EC). We also give a simplified algorithm, Dom2IP, that more quickly determines if an instance has an unbounded integrality gap. We show that FDT's speed and approximation quality compare well to that of feasibility pump on moderate-sized instances of the vertex cover problem. For a particular set of hard-to-decompose fractional 2EC solutions, FDT always gave a better integer solution than the best previous approximation algorithm (Christofides).
△ Less
Submitted 11 August, 2020; v1 submitted 12 June, 2020;
originally announced June 2020.
-
A New Integer Programming Formulation of the Graphical Traveling Salesman Problem
Authors:
Robert D. Carr,
Neil Simonetti
Abstract:
In the Traveling Salesman Problem (TSP), a salesman wants to visit a set of cities and return home. There is a cost $c_{ij}$ of traveling from city $i$ to city $j$, which is the same in either direction for the Symmetric TSP. The objective is to visit each city exactly once, minimizing total travel costs. In the Graphical TSP, a city may be visited more than once, which may be necessary on a spars…
▽ More
In the Traveling Salesman Problem (TSP), a salesman wants to visit a set of cities and return home. There is a cost $c_{ij}$ of traveling from city $i$ to city $j$, which is the same in either direction for the Symmetric TSP. The objective is to visit each city exactly once, minimizing total travel costs. In the Graphical TSP, a city may be visited more than once, which may be necessary on a sparse graph. We present a new integer programming formulation for the Graphical TSP requiring only two classes of constraints that are either polynomial in number or polynomially separable, while addressing an open question proposed by Denis Naddef.
△ Less
Submitted 8 June, 2020;
originally announced June 2020.
-
Symmetric Linear Programming Formulations for Minimum Cut with Applications to TSP
Authors:
Robert D. Carr,
Jennifer Iglesias,
Giuseppe Lanciac,
Benjamin Moseley
Abstract:
We introduce multiple symmetric LP relaxations for minimum cut problems. The relaxations give optimal and approximate solutions when the input is a Hamiltonian cycle. We show that this leads to one of two interesting results. In one case, these LPs always give optimal and near optimal solutions, and then they would be the smallest known symmetric LPs for the problems considered. Otherwise, these L…
▽ More
We introduce multiple symmetric LP relaxations for minimum cut problems. The relaxations give optimal and approximate solutions when the input is a Hamiltonian cycle. We show that this leads to one of two interesting results. In one case, these LPs always give optimal and near optimal solutions, and then they would be the smallest known symmetric LPs for the problems considered. Otherwise, these LP formulations give strictly better LP relaxations for the traveling salesperson problem than the subtour relaxation. We have the smallest known LP formulation that is a 9/8-approximation or better for min-cut. In addition, the LP relaxation of min-cut investigated in this paper has interesting constraints; the LP contains only a single typical min-cut constraint and all other constraints are typically only used for max-cut relaxations.
△ Less
Submitted 24 May, 2020;
originally announced May 2020.
-
Machine Learning at Microsoft with ML .NET
Authors:
Zeeshan Ahmed,
Saeed Amizadeh,
Mikhail Bilenko,
Rogan Carr,
Wei-Sheng Chin,
Yael Dekel,
Xavier Dupre,
Vadim Eksarevskiy,
Eric Erhardt,
Costin Eseanu,
Senja Filipi,
Tom Finley,
Abhishek Goswami,
Monte Hoover,
Scott Inglis,
Matteo Interlandi,
Shon Katzenberger,
Najeeb Kazmi,
Gleb Krivosheev,
Pete Luferenko,
Ivan Matantsev,
Sergiy Matusevych,
Shahab Moradi,
Gani Nazirov,
Justin Ormont
, et al. (9 additional authors not shown)
Abstract:
Machine Learning is transitioning from an art and science into a technology available to every developer. In the near future, every application on every platform will incorporate trained models to encode data-based decisions that would be impossible for developers to author. This presents a significant engineering challenge, since currently data science and modeling are largely decoupled from stan…
▽ More
Machine Learning is transitioning from an art and science into a technology available to every developer. In the near future, every application on every platform will incorporate trained models to encode data-based decisions that would be impossible for developers to author. This presents a significant engineering challenge, since currently data science and modeling are largely decoupled from standard software development processes. This separation makes incorporating machine learning capabilities inside applications unnecessarily costly and difficult, and furthermore discourage developers from embracing ML in first place. In this paper we present ML .NET, a framework developed at Microsoft over the last decade in response to the challenge of making it easy to ship machine learning models in large software applications. We present its architecture, and illuminate the application demands that shaped it. Specifically, we introduce DataView, the core data abstraction of ML .NET which allows it to capture full predictive pipelines efficiently and consistently across training and inference lifecycles. We close the paper with a surprisingly favorable performance study of ML .NET compared to more recent entrants, and a discussion of some lessons learned.
△ Less
Submitted 15 May, 2019; v1 submitted 14 May, 2019;
originally announced May 2019.
-
A Deep Neural Network for Pixel-Level Electromagnetic Particle Identification in the MicroBooNE Liquid Argon Time Projection Chamber
Authors:
MicroBooNE collaboration,
C. Adams,
M. Alrashed,
R. An,
J. Anthony,
J. Asaadi,
A. Ashkenazi,
M. Auger,
S. Balasubramanian,
B. Baller,
C. Barnes,
G. Barr,
M. Bass,
F. Bay,
A. Bhat,
K. Bhattacharya,
M. Bishai,
A. Blake,
T. Bolton,
L. Camilleri,
D. Caratelli,
I. Caro Terrazas,
R. Carr,
R. Castillo Fernandez,
F. Cavanna
, et al. (148 additional authors not shown)
Abstract:
We have developed a convolutional neural network (CNN) that can make a pixel-level prediction of objects in image data recorded by a liquid argon time projection chamber (LArTPC) for the first time. We describe the network design, training techniques, and software tools developed to train this network. The goal of this work is to develop a complete deep neural network based data reconstruction cha…
▽ More
We have developed a convolutional neural network (CNN) that can make a pixel-level prediction of objects in image data recorded by a liquid argon time projection chamber (LArTPC) for the first time. We describe the network design, training techniques, and software tools developed to train this network. The goal of this work is to develop a complete deep neural network based data reconstruction chain for the MicroBooNE detector. We show the first demonstration of a network's validity on real LArTPC data using MicroBooNE collection plane images. The demonstration is performed for stop** muon and a $ν_μ$ charged current neutral pion data samples.
△ Less
Submitted 22 August, 2018;
originally announced August 2018.
-
Bayesian Learning of Clique Tree Structure
Authors:
Cetin Savkli,
J. Ryan Carr,
Philip Graff,
Lauren Kennell
Abstract:
The problem of categorical data analysis in high dimensions is considered. A discussion of the fundamental difficulties of probability modeling is provided, and a solution to the derivation of high dimensional probability distributions based on Bayesian learning of clique tree decomposition is presented. The main contributions of this paper are an automated determination of the optimal clique tree…
▽ More
The problem of categorical data analysis in high dimensions is considered. A discussion of the fundamental difficulties of probability modeling is provided, and a solution to the derivation of high dimensional probability distributions based on Bayesian learning of clique tree decomposition is presented. The main contributions of this paper are an automated determination of the optimal clique tree structure for probability modeling, the resulting derived probability distribution, and a corresponding unified approach to clustering and anomaly detection based on the probability distribution.
△ Less
Submitted 23 August, 2017;
originally announced August 2017.
-
SOCRATES: A System For Scalable Graph Analytics
Authors:
Cetin Savkli,
Ryan Carr,
Matthew Chapman,
Brant Chee,
David Minch
Abstract:
A distributed semantic graph processing system that provides locality control, indexing, graph query, and parallel processing capabilities is presented.
A distributed semantic graph processing system that provides locality control, indexing, graph query, and parallel processing capabilities is presented.
△ Less
Submitted 16 August, 2017;
originally announced August 2017.
