From the 1 of 6 linked papers with an AI index.
6 papers
The Best of Times, the Worst of Times: Moment-Based Analysis of Probabilistic Cost Structures
Chenyu Zhou, Di Wang, Thomas Reps
The paper introduces a compositional static analysis that computes mean, variance, and higher moments of cost distributions for probabilistic programs whose costs involve additive,…
Counterexample Guided Learning in the Large using Reasoning Agents
Hongyi Liu, Frederic Sala, Thomas Reps +1
LLMs and LLM agents should improve when given feedback, but identifying when they are able to do so is difficult: feedback is heterogeneous, domain-specific, and difficult to contr…
Do CFLOBDDs Actually Make Use of Linear Structure?
Meghana Aparna Sistla, Swarat Chaudhuri, Thomas W. Reps
Binary Decision Diagrams (BDDs) are a widely used data structure for efficient Boolean function representation. Context-Free-Language Ordered Binary Decision Diagrams (CFLOBDDs) ar…
SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
Nengkun Yu, Jens Palsberg, Thomas Reps
Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Despite extensive research, existing verification t…
Manjushri: A Tool for Equivalence Checking of Quantum Circuits
Xuan Du Trinh, Meghana Sistla, Nengkun Yu +1
Verifying whether two quantum circuits are equivalent is a central challenge in the compilation and optimization of quantum programs. We introduce \textsc{Manjushri}, a new automat…
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Nengkun Yu, Xuan Du Trinh, Thomas Reps
This paper concerns the problem of checking if two shallow (i.e., constant-depth) quantum circuits perform equivalent computations. Equivalence checking is a fundamental correctnes…