[pl-seminar] CS703 project presentations

["Loris D'Antoni" <loris@xxxxxxxxxxx>]

Folks, Students in my 703 class are giving their project presentations this (W,F) and next week (M), at 11-12 in CS 1257. Feel free to pass by.

Wednesday 12/4

Mapping program descriptions to compositions of typed components (Scott Wang)
Type-driven component-based program synthesis is the problem of synthesising programs meeting a specification by composing together typed components. Recent work has provided an algorithm to synthesise programs of a given query type; however, this approach both requires the query type to be known in advance and does not disambiguate within the set of synthesised programs of that query type.
We extend this approach by exploring the problem of program synthesis from natural language descriptions. To do so, we endow the components with descriptions, then demonstrate that the component with the closest text description to the description of a desired program has a similar type to that desired program. In addition, we show that the text descriptions of the components of synthesised programs can correctly predict which synthesised program is the desired program in many cases.

Learning weighted finite automata via matrix completion (Owen Levin)
Weighted finite automata (WFA) are a wide class of functions mapping sequences of characters to numbers. In this presentation we will walk through what weighted finite automata are and some interpretations. Next, we will discuss some results on representability of functions as WFA and a guide on how to synthesize WFAs from examples.

Recursive completion of fractal patterns from hand-drawn images (Anant Gupta, Ankit Pensia)
Given a hand-drawn figure containing recursive patterns (such as a fractal), we synthesize a high-level (recursive) program that can render the given figure. The input figure can be assumed to be drawn only upto a small recursive depth, which means that there can be multiple recursive programs consistent with the given figure. We find the shortest such program, and then "complete" the pattern in the input by running the synthesized program upto a high recursive depth.

Friday 12/6

Code Refactoring Using Program Synthesis (Mark Powers)

Code readability and simplicity are design goals for any code base, and better refactoring tools should exist that make it easier to maintain source code. Current IDE refactoring tools are simple and require the programmer to select exact methods. Using program synthesis, this process can be made automatic, and it can utilize library methods unknown to the programmer. We employ the component-based synthesizer FrAngel, and aide in synthesis by levering knowledge of libraries and _expression_ fragments from the original code.
Refactored methods for a particular subsegment are synthesized using examples derived from the original code. This process is iterative over all subsegments from a larger code section, using the prior synthesized methods as new components in later refactoring. The synthesized methods can be spliced into the original code to generate final refactored candidates, which can be ranked according to how they improve upon the original code. This technique is shown to be effective over a set of examples, in both total time and quality of refactored methods.

Modeling parser-based interactive fiction using NuSMV (Xin Yu)
In parser-based interactive fiction (IF), players navigate a text environment using simple verb-noun commands. In most cases, the player's goal is to overcome obstacles by manipulating the state of the game world until they reach a winning ending. One important consideration in modern IF design is "cruelty", which measures the player's ability to reach a winning ending in any given state of the game world. This project presents a first attempt at automatically determining cruelty via NuSMV-based model checking.
This project focuses on Inform, the most popular authoring system for parser-based IF. Since Inform is a domain-specific language with an established model of interaction with game objects, the project combines explicit conditions (obtained through parsing if statements) with conditions derived from this default model. The project's implementation is object-focused: each room and object is modeled separately, whereas player action is abstracted using nondeterminism except where it interferes with Inform's default interactions. The possible states of each object translate readily into atomic propositions, allowing the project to convert Inform source code into NuSMV code while limiting loss of fidelity.
The project has gone through preliminary testing using handcrafted examples, and will undergo fuller testing against modified versions of Inform's standard example programs. Due to time constraints, this implementation focuses mainly on verifying winnability, though it is readily extensible to verifying program integrity and analyzing game structure.

Verification for Recurrent Neural Networks (Yuhao Zhang)
Abstracts: This project uses the Interval domain and the Zonotope domain to verify the robustness of Recurrent Neural Networks. A novel abstract interpretation is designed for a GRU cell operation. Moreover, dynamic programming is used to capture the global constraint on the number of the local modifications. Furthermore, to improve the imprecision of the verification, disjoint domains has been kept during propagation with a budget.

Synthesizing Graphics Latex Code for Hand-drawn Automata (Young Wu)
This project implements in _javascript_ an online tool that converts automata drawings to Latex code that can produce the corresponding automata diagram. Two sets of Latex codes are produced, one using the "automata" package, the other treats the drawing as a directed graph and does not use the package.

Monday 12/9

A survey of existing abstract domains towards proving unrealizability of syntax-guided synthesis problems over bitvectors (Jinwoo Kim)

We consider the problem of automatically proving that a syntax-guided synthesis (SyGuS) problem over bitvectors is unrealizable, meaning that it has no solution. Our main contribution is a primarily theoretical analysis of existing techniques towards solving this problem.ÂTo do so, we explore previously established frameworks of proving unrealizability over syntax-guided synthesis problems over linear integer arithmetic (LIA): one that encodes the unrealizability problem as a program reachability problem, and one that expresses the unrealizability problem as the solution to a set of equations over semi-linear sets. We also explore traditional abstract domains from program analysis used to model bitvectors, and see if they can be applied to the frameworks in proving unrealizabilty. Our results suggest that it is difficult to answer unrealizability questions over bitvectors based on existing methods, which is mainly due to the various operations supported by bitvectors.

NodeMatcher: Synthesizing XPath query from minimal examples (Paul Luh)
NodeMatcher is a system for data extraction that synthesizes XPath query via input examples in the format of annotated DOM HTML. Users will annotate a handful of webpages as input examples and NodeMatcher will automatically synthesize XPath queries that are consistent with the user-provided examples. These synthesized XPath queries can then be used to extract relevant data from unseen webpages. This project investigates the effectiveness and possibilities of learning XPath query from small training data examples and explores different methodologies when constructing such a system. In the presentation, I will present the motivation of the project, the applications, the naive baseline approach, the different methodologies I have explored that improved the result of the baseline, and an analysis of advantages and disadvantages of the explored methodologies.

Sheep: An Example-Driven Synthesizer for the Lambda Calculus (Zachary Susag)
This paper provides an algorithm for synthesizing terms in the pure, untyped lambda calculus. The pure, untyped lambda calculus serves as the formal system of logic for expressing computation and is the foundation for functional programming languages. However, this logic can be quite complex and confusing to students initially trying to understand expressing computation purely through function abstraction, application, and variable binding. To help ease the transition, we present Sheep, a program synthesizer for terms in the pure, untyped lambda calculus from input/output examples. Sheep inductively builds terms by consuming lambda abstractions from the input/output examples and efficiently enumerating all possible lambda terms using a heuristic that prefers abstraction over application. We evaluate Sheep by synthesizing over 30 terms in the pure lambda calculus. Our results demonstrate that Sheep can generate non-trivial, recursive terms in the lambda calculus efficiently.