33 citations · 166 across the 51 of their papers we have counts for
11 papers · 1 filter
Semantics of Sets of Programs
Jinwoo Kim, Shaan Nagy, Thomas Reps +1
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 se…
Synthesizing Formal Semantics from Executable Interpreters
Jiangyi Liu, Charlie Murphy, Anvay Grover +3
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…
Perceptions of the Fairness Impacts of Multiplicity in Machine Learning
Anna P. Meyer, Yea-Seul Kim, Aws Albarghouthi +1
Machine learning (ML) is increasingly used in high-stakes settings, yet multiplicity - the existence of multiple good models - means that some predictions are essentially arbitrary…
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
Keith J. C. Johnson, Rahul Krishnan, Thomas Reps +1
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, c…
Verifying Solutions to Semantics-Guided Synthesis Problems
Charlie Murphy, Keith Johnson, Thomas Reps +1
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 a…
LOUD: Synthesizing Strongest and Weakest Specifications
Kanghee Park, Xuanyu Peng, Loris D'Antoni
This paper tackles the problem of synthesizing specifications for nondeterministic programs. For such programs, useful specifications can capture demonic properties, which hold for…
The SemGuS Toolkit
Keith J. C. Johnson, Andrew Reynolds, Thomas Reps +1
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 fo…
A One-Layer Decoder-Only Transformer is a Two-Layer RNN: With an Application to Certified Robustness
Yuhao Zhang, Aws Albarghouthi, Loris D'Antoni
This paper reveals a key insight that a one-layer decoder-only Transformer is equivalent to a two-layer Recurrent Neural Network (RNN). Building on this insight, we propose ARC-Tra…
Grammar-Aligned Decoding
Kanghee Park, Jiayu Wang, Taylor Berg-Kirkpatrick +2
Large Language Models (LLMs) struggle with reliably generating highly structured outputs, such as program code, mathematical formulas, or well-formed markup. Constrained decoding a…
Verified Training for Counterfactual Explanation Robustness under Data Shift
Anna P. Meyer, Yuhao Zhang, Aws Albarghouthi +1
Counterfactual explanations (CEs) enhance the interpretability of machine learning models by describing what changes to an input are necessary to change its prediction to a desired…
Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
Shaan Nagy, Jinwoo Kim, Thomas Reps +1
Automated verification of all members of a (potentially infinite) set of programs has the potential to be useful in program synthesis, as well as in verification of dynamically loa…