[pl-seminar] CS703 Project Presentations Dec 5/7 1-2 pm (COMP SCI 1257)

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

Wednesday 12/5: 1-2 (COMP SCI 1257)

Mechanical suggestions for rust lifetime compiler errors (Mark Mansi)

Rust is a new systems programming language that aims to allow low-level control and high performance, like C/C++, but with memory safety and data-race-freedom guaranteed statically. Rust accomplishes this using a compiler pass called the borrow checker. Unfortunately, the borrow checker's compile errors are sometimes difficult to understand. Beginners and advanced users alike are often not sure how to resolve them. In our work, we propose a tool that uses the compiler's analyses to mechanically produce suggestions for how to resolve borrow checker errors.

Combining I/O & Logical specifications for program synthesis (Yunchan Lee)

Programming-by-examples is a line of program synthesis where input/output examples are used as specifications for inductive synthesis. However, often simple logical constraints can more succinctly describe desired program behaviors, and/or limit its input space. Conflict-guided synthesis is a methodology in which program enumeration is guided by âlemmasâ learned during synthesis via analysis of the abstract program and specification semantics. At each step of the enumeration, the partial programâs abstract semantics is checked against the specification. On failure component properties that cause incompatibility are found in the form of minimum unsatisfiable core, and any components that have properties implied by the core are discarded for the program node.

In the previous work, study has focused on IO examples as specifications, and have shown favorable results compared to existing synthesis frameworks, such as DeepCoder. However, the frameworkâs use of logical constraints to limit the range of possible components suggest that it can be adapted to use logical specifications to supplement the IO examples.Â

The current work explores this possibility, by instantiating the framework on the Learning Inductive Program Synthesis domain, first presented on the DeepCoder research. The original conflict guided synthesis algorithm is adapted to directly use partial logical specifications in its conflict analysis phase, and encoding input constraint specifications onto the variable components and output constraints onto the output node.Â

Preliminary results comparing the performances of the current work against a re-implementation of Neo, the instantiation of the framework in the original research, and DeepCoder, its base-line comparison, is presented.

Learn JSON Schema from Positive and Negative Examples (Harrison Brewton)

JSON Schemas provide an explicit specification for data interchange that well balances human and machine readability. Without this balance, we will not have a transparent and smart web. Unfortunately, a large portion of the web's JSON follows know schemas[Bex]. This is often because of opaque APIs and fast-moving developers. Therefore we present a tool capable of learning JSON schemas from example. We first convert schemas into Symbolic Tree Automata. We then lift the Lambda* Algorithm[DDA] from Symbolic Automata to Symbolic Tree Automata, and learn schema from positive and negative examples. Converting back to JSON schema, we evaluate equivalence using both human inspection, and a probabilistic evaluation of generated member JSON objects against an API. We believe that this tool will help developers standardize unstandardized data.

Speeding up program repair under uncertainty (Shashank Rajput)

Given a property Ï and a program G0 that does not satisfy the property, program repair is

to find a new program Gâ which satisfies Ï and is âclosestâ to G0. In particular, we focus

on the problem of automating program repair in the presence of uncertainty - when the

input follows a probability distribution. A strategy to find this repair is to find a large set

of programs, check which of them satisfy the property (called post condition) and then find

the one which is closest to the original program. Typically this large set is the set of all

programs, one for each possible labelling of the training data. It can be seen that this is

exponentially large in the number of training points. In this work, we aim to reduce this large

set by selecting candidate programs which contain optimal repair with high probability. We

propose threshold based candidate selection, and provide theoretical and emipirical results

supporting our claim.

Friday 12/7: 1-2 (COMP SCI 1257)

Realizing LIME (Local Interpretable Model-agnostic Explanations) for RNNs (Samuel Jackson)

LIME (Local Interpretable Model-agnostic Explanations) is a framework for explaining explanations from a model. Given a specific word and classification from the model, LIME allows you to describe why that classification applies to the word in question by looking locally around the word and finding the best explanation that fits the local space. While LIME has traditionally been applied on neural networks using linear functions as explanations, I have tried to apply the LIME framework to recurrent neural networks using an arbitrary DSL. In this talk I will introduce LIME as a framework and explain the strategy we are using to instantiate LIME in this domain.

Programming by Examples: Example Distributions and Synthesis Loss (Xiating Ouyang)

Version Space Algebra (VSA) is often used in program synthesis onÂinput-output examples. A VSA synthesizer will maintain a list of consistent programs for each subset of the given examples, and then combine some programs from the list to form the synthesized program usingÂthe If-Then-Else construct. This process theoretically requiresÂexponential space. However in many applications, that exponentiality does not emerge since the input examples to the synthesizer follow certainÂdistributions. We introduce the notion of consistency graphs and study theÂexample distributions in the PROSE benchmark suite released by Microsoft. We find that examples do not follow the Erdos-Renyi model or the power-law graph model, and when the examples are for the same task, the exponentiality does occur, but can be controlled by reducing the input examples to the synthesizer; and when the examples are for distinct tasks, the exponentiality generally does not emerge.The VSA synthesizer incurs the loss of information over all consistent programs when an example has multiple programs consistent on it but theÂsynthesizer only selects one in the synthesized program. We introduce the enriched consistency graphs to analyze such loss of programs on differentÂset of examples. The VSA synthesizer in 93% of the samples does not lose any program for examples from the same task, but it does not lose only in 28% of the cases if examples are from different tasks. We also introduce averaged loss number, a metric to measure such loss and present the experiment results.

Programming by Example with HTML (Samuel Erickson)

HTML and CSS are used in tandem in just about every modern web application. While some of the styling offered by CSS can be expressed in HTML attributes, it is preferable to replace those attributes with CSS selectors and declarations. This project explores the realm of programming by example with HTML and CSS, with the goal of synthesizing a program that automatically generates CSS declarations based on HTML inputs. Building on top of Microsoftâs PROSE APIs for the .NET framework, a simple user interface was designed to accept HTML input and CSS output examples and synthesize a program based upon those examples. The PROSE framework is unable to synthesize programs based on a set of examples with different numbers of attributes due to its columnar structure. However, by dividing the set of examples into subsets of examples with the same number of attributes, a set of programs could be synthesized, one per subset of examples. On average, the application correctly synthesized the optimal program when given three examples with the same number of attributes. While this project successfully synthesizes the optimal program for a subset of examples efficiently, the ideal state is to synthesize a single program for all examples, even with different numbers of attributes. There is untapped potential to enhance the PROSE framework to support columnar data with differing numbers of columns, which would provide a means to synthesize a single programmatic output.

Introducing Program Synthesis through the Creation of Visual Art (Katie Zutter)
There is a substantial diversity gap in the field of computing. The composition of the fieldâs workforce does not reflect that of the countryâs population. A primary reason why women and racial and ethnic minorities are underrepresented in computer science fields is lack of exposure. The broad goal of this project is to garner interest in computer science among groups that may not otherwise be introduced to it through a series of workshops. In these workshops, which will be advertised to students from different departments on campus, attendees will use program synthesis to create some form of visual art using a tool specifically created for this purpose. This tool allows students to explore program synthesis and try out ideas through the creation of art.