arXiv subjects

Thomas Reps

Publications and source records attributed to Thomas Reps.

At least 19 recordsLinked to original sources

arXiv2026

The Best of Times, the Worst of Times: Moment-Based Analysis of Probabilistic Cost Structures

This paper studies how to compute the moments -- mean, variance, and beyond -- of the cost (e.g., running time) of certain probabilistic programs, in which local costs combine not only additively but also via the extremal operations $\max$ and $\min$. Such costs arise naturally -- for instance, the number of rounds of a contention-resolution protocol, the waiting time of a quantum repeater, and the completion time of a fork-join computation -- but fall outside the scope of moment-based analyses developed for additive costs. The difficulty is that $\max$ and $\min$ are nonlinear: the moments of $\max(X, Y)$ are not determined by those of $X$ and $Y$, so propagating moments alone fails. In contrast, propagating full distributions would suffice, but is computationally intractable. We present a compositional cost analysis for a family of probabilistic programs whose cost structure can be represented as a hierarchical cost expression. The analysis proceeds bottom-up through the hierarchical structure, solving local recurrence equations at each node and summarizing each subproblem with a surrogate distribution. Each surrogate consists of an exact short-time prefix and a compact parametric tail. Our approach computes the mean of the cost distribution with a sound error bound, and systematically lifts to second and higher moments. In addition, precision can be increased by refining the surrogate representation, trading additional computation for tighter bounds. We implemented our method in a tool, called DICKENS, and evaluated its capabilities on three problems: quantum repeater waiting times, RFID collision resolution, and completion times of fork-join computations.

cs.PL↗

arXiv2026

Counterexample Guided Learning in the Large using Reasoning Agents

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 control. We approach this challenge by asking LLMs to perform regular-expression induction, a classical symbolic learning problem where precise mechanisms for feedback exist in the form of counterexamples. In counterexample-guided learning, a learner (LLM) proposes candidate regular expressions from positive/negative-labeled strings, and the teacher (verifier) returns counterexamples showcasing the difference between the candidate and target languages. We identify novel counterexample-guided refinement strategies that enable effective regex learning, such as regularization and symbolic counterexample clusters. We also explore agentic strategies such as reflection and repair loops. Empirically, we find that verifier feedback substantially improves sample efficiency on challenging regex-induction tasks, reducing the number of labeled examples required and enabling learning of complex target expressions where standard prompting fails. For example, on the hardest task groups, our counterexample-guided framework improves success from 3.2% to 38.1% and from 38.9% to 74.1% on two different regex domains. These results suggest that LLMs can benefit from rich feedback beyond treating it as additional data, opening the door for robust verifier-guided methods for LLM-based program synthesis and formal reasoning.

cs.LG↗

arXiv2026

Manjushri: A Tool for Equivalence Checking of Quantum Circuits

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 automated framework for scalable quantum-circuit equivalence checking. \textsc{Manjushri} uses local projections as discriminative circuit fingerprints, implemented with weighted binary decision diagrams (WBDDs), yielding a compact and efficient symbolic representation of quantum behavior. We present an extensive experimental evaluation that, for random 1D Clifford+$T$ circuits, explores the trade-off between \textsc{Manjushri} and \textsc{ECMC}, a tool for equivalence checking based on a much different approach. \textsc{Manjushri} is much faster up to depth 30 (with the crossover point varying from 39--49, depending on the number of qubits and whether the input circuits are equivalent or inequivalent): when inputs are equivalent, \textsc{Manjushri} is about 10$\times$ faster (or more); when inputs are inequivalent, \textsc{Manjushri} is about 8$\times$ faster (or more). For both kinds of equivalence-checking outcomes, \textsc{ECMC}'s success rate out to depth 50 is impressive on 32- and 64-qubit circuits: on such circuits, \textsc{ECMC} is almost uniformly successful. However, \textsc{ECMC} struggled on 128-qubit circuits for some depths. \textsc{Manjushri} is almost uniformly successful out to about depth 38, before tailing off to about 75\% at depth 50 (falling to 0\% at depth 48 for 128-qubit circuits that are equivalent). These results establish that \textsc{Manjushri} is a practical and scalable solution for large-scale quantum-circuit verification, and would be the preferred choice unless clients need to check equivalence of circuits of depth $>$38.

quant-ph↗

arXiv2025

On The Finetuning of MLIPs Through the Lens of Iterated Maps With BPTT

Accurate structural relaxation is critical for advanced materials design. Traditional approaches built on physics-derived first-principles calculations are computationally expensive, motivating the creation of machine-learning interatomic potentials (MLIPs), which strive to faithfully reproduce first-principles computed forces. We propose a fine-tuning method to be used on a pretrained MLIP in which we create a fully-differentiable end-to-end simulation loop that optimizes the predicted final structures directly. Trajectories are unrolled and gradients are tracked through the entire relaxation. We show that this method consistently improves performance across all evaluated pretrained models; resulting in an average of roughly 32% reduction in prediction error. Interestingly, we show the process is robust to substantial variation in the relaxation setup, achieving negligibly different results across varied hyperparameter and procedural modifications.

cond-mat.mtrl-sci↗

arXiv2025

MHA-RAG: Improving Efficiency, Accuracy, and Consistency by Encoding Exemplars as Soft Prompts

Adapting Foundation Models to new domains with limited training data is challenging and computationally expensive. While prior work has demonstrated the effectiveness of using domain-specific exemplars as in-context demonstrations, we investigate whether representing exemplars purely as text is the most efficient, effective, and stable approach. We explore an alternative: representing exemplars as soft prompts with an exemplar order invariant model architecture. To this end, we introduce Multi-Head Attention Retrieval-Augmented Generation (MHA-RAG), a framework with the number of attention heads serving as a simple hyperparameter to control soft prompt-generation across different tasks. Across multiple question-answering benchmarks and model scales, MHA-RAG achieves a 20-point performance gain over standard RAG, while cutting inference costs by a factor of 10X GFLOPs-delivering both higher accuracy and greater efficiency, invariant to exemplar order.

cs.AI↗

arXiv2025

ADAPT: Lightweight, Long-Range Machine Learning Force Fields Without Graphs

Point defects play a central role in driving the properties of materials. First-principles methods are widely used to compute defect energetics and structures, including at scale for high-throughput defect databases. However, these methods are computationally expensive, making machine-learning force fields (MLFFs) an attractive alternative for accelerating structural relaxations. Most existing MLFFs are based on graph neural networks (GNNs), which can suffer from oversmoothing and poor representation of long-range interactions. Both of these issues are especially of concern when modeling point defects. To address these challenges, we introduce the Accelerated Deep Atomic Potential Transformer (ADAPT), an MLFF that replaces graph representations with a direct coordinates-in-space formulation and explicitly considers all pairwise atomic interactions. Atoms are treated as tokens, with a Transformer encoder modeling their interactions. Applied to a dataset of silicon point defects, ADAPT achieves a roughly 33 percent reduction in both force and energy prediction errors relative to a state-of-the-art GNN-based model, while requiring only a fraction of the computational cost.

cs.LG↗

arXiv2025

Efficient Cost Bounds with Linear Maps

The Automatic Amortized Resource Analysis (AARA) derives program-execution cost bounds using types. To do so, AARA often makes use of cost-free types, which are critical for the composition of types and cost bounds. However, inferring cost-free types using the current state-of-the-art algorithm is expensive due to recursive dependence on additional cost-free types. Furthermore, that algorithm uses a heuristic only applicable to polynomial cost bounds, and not, e.g., exponential bounds. This paper presents a new approach to these problems by representing the cost-free types of a function in a new way: with a linear map, which can stand for infinitely many cost-free types. Such maps enable an algebraic flavor of reasoning about cost bounds (including non-polynomial bounds) via matrix inequalities. These inequalities can be solved with off-the-shelf linear-programming tools for many programs, so that types can always be efficiently checked and often be efficiently inferred. An experimental evaluation with a prototype implementation shows that-when it is applicable-the inference of linear maps is exponentially more efficient than the state-of-the-art algorithm.

cs.PL↗

arXiv2025

Software Model Checking via Summary-Guided Search (Extended Version)

In this work, we describe a new software model-checking algorithm called GPS. GPS treats the task of model checking a program as a directed search of the program states, guided by a compositional, summary-based static analysis. The summaries produced by static analysis are used both to prune away infeasible paths and to drive test generation to reach new, unexplored program states. GPS can find both proofs of safety and counter-examples to safety (i.e., inputs that trigger bugs), and features a novel two-layered search strategy that renders it particularly efficient at finding bugs in programs featuring long, input-dependent error paths. To make GPS refutationally complete (in the sense that it will find an error if one exists, if it is allotted enough time), we introduce an instrumentation technique and show that it helps GPS achieve refutation-completeness without sacrificing overall performance. We benchmarked GPS on a diverse suite of benchmarks including programs from the Software Verification Competition (SV-COMP), from prior literature, as well as synthetic programs based on examples in this paper. We found that our implementation of GPS outperforms state-of-the-art software model checkers (including the top performers in SV-COMP ReachSafety-Loops category), both in terms of the number of benchmarks solved and in terms of running time.

cs.PL↗

arXiv2025

SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits

Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Despite extensive research, existing verification techniques are insufficient -- even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents a logic for reasoning in such settings, called SAQR-QC. The logic supports {S}calable but {A}pproximate {Q}uantitative {R}easoning about {Q}uantum {C}ircuits, whence the name. SAQR-QC has three characteristics: (i) some (deliberate) loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) most importantly, to make reasoning scalable, every reasoning step is local -- i.e., it involves just a small number of qubits. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation -- a core subroutine in Shor's factoring algorithm.

quant-ph↗

arXiv2025

Scalable Equivalence Checking and Verification of Shallow Quantum Circuits

This paper concerns the problem of checking if two shallow (i.e., constant-depth) quantum circuits perform equivalent computations. Equivalence checking is a fundamental correctness question -- needed, e.g., for ensuring that transformations applied to a quantum circuit do not alter its behavior. For quantum circuits, the problem is challenging because a straightforward representation on a classical computer of each circuit's quantum state can require time and space that are exponential in the number of qubits $n$. The paper presents decision procedures for two variants of the equivalence-checking problem. Both can be carried out on a classical computer in time and space that, for any fixed depth, is linear in $n$. Our critical insight is that local projections are precise enough to completely characterize the output state of a shallow quantum circuit. Instead of explicitly computing the output state of a circuit, we generate a set of local projections that serve as constraints on the output state. Moreover, the circuit's output state is the unique quantum state that satisfies all the constraints. Beyond equivalence checking, we show how to use the constraint representation to check a class of assertions, both statically and at run time. Our assertion-checking methods are sound and complete for assertions expressed as conjunctions of local projections. Our experiments show that on a server equipped with 2 x Intel\textsuperscript{\textregistered} Xeon\textsuperscript{\textregistered} Gold 6338 CPUs (128 threads total) and 1.0~TiB of RAM, running Ubuntu 20.04.6 LTS, the constraint representation of a random 100-qubit circuit of depth 6 can be computed in 19.8 seconds. For fixed inputs $\ket{0}^{\otimes 100}$, equivalence checking of {random} 100-qubit circuits of depth 3 takes 4.46 seconds; for arbitrary inputs, it takes no more than 31.96 seconds.

quant-ph↗

arXiv2024

Semantics of Sets of Programs

Applications like program synthesis sometimes require proving that a property holds for all of the infinitely many programs described by a grammar - i.e., an inductively defined set of programs. Current verification frameworks overapproximate programs' behavior when sets of programs contain loops, including two Hoare-style logics that fail to be relatively complete when loops are allowed. In this work, we prove that compositionally verifying simple properties for infinite sets of programs requires tracking distinct program behaviors over unboundedly many executions. Tracking this information is both necessary and sufficient for verification. We prove this fact in a general, reusable theory of denotational semantics that can model the expressivity and compositionality of verification techniques over infinite sets of programs. We construct the minimal compositional semantics that captures simple properties of sets of programs and use it to derive the first sound and relatively complete Hoare-style logic for infinite sets of programs. Thus, our methods can be used to design minimally complex, compositional verification techniques for sets of programs.

cs.PL↗

arXiv2024

Verifying Solutions to Semantics-Guided Synthesis Problems

Semantics-Guided Synthesis (SemGuS) provides a framework to specify synthesis problems in a solver-agnostic and domain-agnostic way, by allowing a user to provide both the syntax and semantics of the language in which the desired program should be synthesized. Because synthesis and verification are closely intertwined, the SemGuS framework raises the problem of how to verify programs in a solver and domain-agnostic way. We prove that the problem of verifying whether a program is a valid solution to a SemGuS problem can be reduced to proving validity of a query in the `CLP calculus, a fixed-point logic that generalizes Constrained Horn Clauses and co-Constrained Horn Clauses. Our encoding into `CLP allows us to further classify the SemGuS verification problems into ones that are reducible to validity of (i) first-order-logic formulas, (ii) Constrained Horn Clauses, (iii) co-Constrained Horn Clauses, and (iv) `CLP queries. Furthermore, our encoding shines light on some limitations of the SemGuS framework, such as its inability to model nondeterminism and reactive synthesis. We thus propose a modification to SemGuS that makes it more expressive, and for which verifying solutions is exactly equivalent to proving validity of a query in the `CLP calculus. Our implementation of SemGuS verifiers based on the above encoding can verify instances that were not even encodable in previous work. Furthermore, we use our SemGuS verifiers within an enumeration-based SemGuS solver to correctly synthesize solutions to SemGuS problems that no previous SemGuS synthesizer could solve.

cs.PL↗

arXiv2024

Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics

In top-down enumeration for program synthesis, abstraction-based pruning uses an abstract domain to approximate the set of possible values that a partial program, when completed, can output on a given input. If the set does not contain the desired output, the partial program and all its possible completions can be pruned. In its general form, abstraction-based pruning requires manually designed, domain-specific abstract domains and semantics, and thus has only been used in domain-specific synthesizers. This paper provides sufficient conditions under which a form of abstraction-based pruning can be automated for arbitrary synthesis problems in the general-purpose Semantics-Guided Synthesis (SemGuS) framework without requiring manually-defined abstract domains. We show that if the semantics of the language for which we are synthesizing programs exhibits some monotonicity properties, one can obtain an abstract interval-based semantics for free from the concrete semantics of the programming language, and use such semantics to effectively prune the search space. We also identify a condition that ensures such abstract semantics can be used to compute a precise abstraction of the set of values that a program derivable from a given hole in a partial program can produce. These precise abstractions make abstraction-based pruning more effective. We implement our approach in a tool, Moito, which can tackle synthesis problems defined in the SemGuS framework. Moito can automate interval-based pruning without any a-priori knowledge of the problem domain, and solve synthesis problems that previously required domain-specific, abstraction-based synthesizers -- e.g., synthesis of regular expressions, CSV file schema, and imperative programs from examples.

cs.PL↗

arXiv2024

Synthesizing Formal Semantics from Executable Interpreters

Program verification and synthesis frameworks that allow one to customize the language in which one is interested typically require the user to provide a formally defined semantics for the language. Because writing a formal semantics can be a daunting and error-prone task, this requirement stands in the way of such frameworks being adopted by non-expert users. We present an algorithm that can automatically synthesize inductively defined syntax-directed semantics when given (i) a grammar describing the syntax of a language and (ii) an executable (closed-box) interpreter for computing the semantics of programs in the language of the grammar. Our algorithm synthesizes the semantics in the form of Constrained-Horn Clauses (CHCs), a natural, extensible, and formal logical framework for specifying inductively defined relations that has recently received widespread adoption in program verification and synthesis. The key innovation of our synthesis algorithm is a Counterexample-Guided Synthesis (CEGIS) approach that breaks the hard problem of synthesizing a set of constrained Horn clauses into small, tractable expression-synthesis problems that can be dispatched to existing SyGuS synthesizers. Our tool Synantic synthesized inductively-defined formal semantics from 14 interpreters for languages used in program-synthesis applications. When synthesizing formal semantics for one of our benchmarks, Synantic unveiled an inconsistency in the semantics computed by the interpreter for a language of regular expressions; fixing the inconsistency resulted in a more efficient semantics and, for some cases, in a 1.2x speedup for a synthesizer solving synthesis problems over such a language.

cs.PL↗

arXiv2024

Synthesizing Abstract Transformers for Reduced-Product Domains

Recently, we showed how to apply program-synthesis techniques to create abstract transformers in a user-provided domain-specific language (DSL) L (i.e., ''L-transformers"). However, we found that the algorithm of Kalita et al. does not succeed when applied to reduced-product domains: the need to synthesize transformers for all of the domains simultaneously blows up the search space. Because reduced-product domains are an important device for improving the precision of abstract interpretation, in this paper, we propose an algorithm to synthesize reduced L-transformers $\langle f_1^{\sharp R}, f_2^{\sharp R},..., f_n^{\sharp R}\rangle$ for a product domain $A_1 \times A_2 \times \ldots \times A_n$ , using multiple DSLs: $\mathcal{L} = \langle \mathcal{L}_1 , \mathcal{L}_2, ... , \mathcal{L}_n \rangle$. Synthesis of reduced-product transformers is quite challenging: first, the synthesis task has to tackle an increased ''feature set" because each component transformer now has access to the abstract inputs from all component domains in the product. Second, to ensure that the product transformer is maximally precise, the synthesis task needs to arrange for the component transformers to cooperate with each other. We implemented our algorithm in a tool, Amurth2, and used it to synthesize abstract transformers for two product domains -- SAFE and JSAI -- available within the SAFEstr framework for JavaScript program analysis. For four of the six operations supported by SAFEstr, Amurth2 synthesizes more precise abstract transformers than the manually written ones available in SAFEstr.

cs.PL↗

arXiv2024

Polynomial Bounds of CFLOBDDs against BDDs

Binary Decision Diagrams (BDDs) are widely used for the representation of Boolean functions. Context-Free-Language Ordered Decision Diagrams (CFLOBDDs) are a plug-compatible replacement for BDDs -- roughly, they are BDDs augmented with a certain form of procedure call. A natural question to ask is, ``For a given family of Boolean functions $F$, what is the relationship between the size of a BDD for $f \in F$ and the size of a CFLOBDD for $f$?'' Sistla et al. established that there are best-case families of functions, which demonstrate an inherently exponential separation between CFLOBDDs and BDDs. They showed that there are families of functions $\{ f_n \}$ for which, for all $n = 2^k$, the CFLOBDD for $f_n$ (using a particular variable order) is exponentially more succinct than any BDD for $f_n$ (i.e., using any variable order). However, they did not give a worst-case bound -- i.e., they left open the question, ``Is there a family of functions $\{ g_i \}$ for which the size of a CFLOBDD for $g_i$ must be substantially larger than a BDD for $g_i$?'' For instance, it could be that there is a family of functions for which the BDDs are exponentially more succinct than any corresponding CFLOBDDs. This paper studies such questions, and answers the second question posed above in the negative. In particular, we show that by using the same variable ordering in the CFLOBDD that is used in the BDD, the size of a CFLOBDD for any function $h$ cannot be far worse than the size of the BDD for $h$. The bound that relates their sizes is polynomial: If BDD $B$ for function $h$ is of size $|B|$ and uses variable ordering $\textit{Ord}$, then the size of the CFLOBDD $C$ for $h$ that also uses $\textit{Ord}$ is bounded by $O(|B|^3)$. The paper also shows that the bound is tight: there is a family of functions for which $|C|$ grows as $\Omega(|B|^3)$.

cs.SC↗

arXiv2024

The SemGuS Toolkit

Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS format, together with an open-source toolkit that provides a parser, a verifier, and enumerative SemGuS solvers. The paper also describes an initial set of SemGuS benchmarks, which form the basis for comparing SemGuS solvers, and presents an evaluation of the baseline enumerative solvers.

cs.PL↗

arXiv2024

Prompt Tuning Strikes Back: Customizing Foundation Models with Low-Rank Prompt Adaptation

Parameter-Efficient Fine-Tuning (PEFT) has become the standard for customising Foundation Models (FMs) to user-specific downstream tasks. However, typical PEFT methods require storing multiple task-specific adapters, creating scalability issues as these adapters must be housed and run at the FM server. Traditional prompt tuning offers a potential solution by customising them through task-specific input prefixes, but it under-performs compared to other PEFT methods like LoRA. To address this gap, we propose Low-Rank Prompt Adaptation (LoPA), a prompt-tuning-based approach that performs on par with state-of-the-art PEFT methods and full fine-tuning while being more parameter-efficient and not requiring a server-based adapter. LoPA generates soft prompts by balancing between sharing task-specific information across instances and customization for each instance. It uses a low-rank decomposition of the soft-prompt component encoded for each instance to achieve parameter efficiency. We provide a comprehensive evaluation on multiple natural language understanding and code generation and understanding tasks across a wide range of foundation models with varying sizes.

cs.LG↗