Overview of PROSE Framework for DSL Creation and PBE Applications
The PROSE Framework enables the creation of Domain-Specific Languages (DSLs) and Program Synthesis applications through Programming by Examples (PBE). Explore the architecture, syntax, and applications of PROSE showcased at the UC Berkeley Hackathon. Witness the innovative approach to synthesizing programs based on examples and intent specifications.
Uploaded on Mar 03, 2025 | 1 Views
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Using the PROSE Framework Programming by Examples Tutorial Alex Polozov polozov@cs.washington.edu January 21, 2017 UC Berkeley PROSE Hackathon 1
Hackathon https://tiny.cc/prose-hack https://microsoft.github.io/prose prose-hackathon@googlegroups.com PROSE SDK: 1. A framework for creating DSLs and PBE applications 2. A suite of existing data wranglingDSLs: text/JSON, extraction/transformation/split Follow the installation instructions on the PROSE website Projects: a) Extend/improve/replace an existing DSL b) Use existing DSLs for some arbitrary cool purpose c) [Advanced] Create a completely new DSL and a PBE application January 21, 2017 UC Berkeley PROSE Hackathon 2
PBE Architecture Refined intent Intended program ? Example-based intent spec ? Ranked program set ? Debugging Program Synthesizer Translator DSL Test inputs ? Ranking function Intended program in Python/C#/C++/ January 21, 2017 UC Berkeley PROSE Hackathon 3
PROSE I/O Specification Input Meta-synthesizer framework Synthesis Strategies Programs PROSE App Synthesizer Output DSL Definition January 21, 2017 UC Berkeley PROSE Hackathon 4
Outline Version space algebra Deductive synthesis in PROSE Live session: creating FlashFill & FlashExtract Q&A January 21, 2017 UC Berkeley PROSE Hackathon 5
Outline Version space algebra Deductive synthesis in PROSE Live session: creating FlashFill & FlashExtract Q&A January 21, 2017 UC Berkeley PROSE Hackathon 6
VSA is a sub-DSL data structure Encodes a set of programs in a compact DAG representation ? Three kinds of nodes: Union VSA ?1, ,?? encodes a union of constituent sets Compare: CFG alternatives ? ? ? Join VSA ? ?1, ,?? encodes all applications of ? to a Cartesian product of possible parameter combinations Compare: CFG operators ? ?(?,?) Direct VSA {?1, ,??} encodes an explicit set of programs Compare: CFG terminal symbols January 21, 2017 UC Berkeley PROSE Hackathon 7
int position := AbsPos(s, k) | RegPos(s, Pair(r, r), k); January 21, 2017 UC Berkeley PROSE Hackathon 8
VSA operations: clustering ?/? Given an input ?, partition the programs in ? based on their output on ? Drastically reduces search space due to partial semantic equivalence We can reason about program outputs instead of syntax Enables efficient branching in deductive synthesis Enables interactive ambiguity resolution Recursively defined: In direct VSAs: straightforward In union VSAs: cluster the constituents and merge the resulting partitions with In join VSAs: cluster the parameter sets, build a Cartesian product of the clusters, apply ?, and merge the resulting partitions with January 21, 2017 UC Berkeley PROSE Hackathon 10
VSA operations: ranking Top(?,?) Enables ranking-based ambiguity resolution Assume a monotonicranking function :DSL Most syntactic ranking functions are monotonic (e.g. program size) Can be machine-learned [Singh & Gulwani, CAV 2015] Recursively defined through Top (?,?) of constituents Time complexity: ? V ? ?w ? log? VSA volume (# of nodes) Usually 103 104 VSA width (max arity) Usually 3 5 January 21, 2017 UC Berkeley PROSE Hackathon 11
VSA operations: filtering Filter ?,? Filter a VSA ? to the subset of programs that satisfy spec ? Implementation 1: Idea: A spec can be easily verified given a program output Cluster ? on the inputs from ?; return a union of clusters that satisfy ? Implementation 2: Idea: A VSA is isomorphic to a sub-DSL (in a context-free form) Thus, Filter ?,? is the same as Learn ,? Invoke deductive synthesis on ?, propagating ? down Enables fast incrementalsynthesis January 21, 2017 UC Berkeley PROSE Hackathon 12
Outline Version space algebra Deductive synthesis in PROSE Live session: creating FlashFill & FlashExtract Q&A January 21, 2017 UC Berkeley PROSE Hackathon 13
Backpropagation in one slide Examples for Substring(s, P1, P2) Seattle, WA Examples for P2 Examples for P1 Seattle, WA Seattle, WA [Polozov & Gulwani 15] January 21, 2017 UC Berkeley PROSE Hackathon 14
How search interacts with witness functions Witness functions Search Follows the grammar top-down ??1? = ??1??2? ?1 ??1 = ??2 Strategy-agnostic at each level Encode backpropagation: decomposition of expression specs into subexpression specs E.g.: at the lowest levels enumeration is faster than deduction Alternatively: inverse semantics of ? w.r.t. ? Dynamic programming: caching subtask results ? ? Modular: define once for ?,? , reuse in all DSLs Efficient branching via VSA clustering January 21, 2017 UC Berkeley PROSE Hackathon 15
string transform := atom | Concat(atom, transform); string atom := ConstStr(s) | let string x = Kth(inputs, k) in Substring(x, position, position); ? ?1 ?21 ?22 2 20 (202) 555-0126 202 (202) 555-0126 (202) 555-0126 02 (202) 555-0126 2 transform,? ?1= "2" ?21 ?transform? "2" ?21 Learn transform, ?21 atom,?1 ?1 Concat( ),? ?1 ?atom? ?1 Learn atom, ?1 ?1 ?1 transform,?21 Concat ?2= "20" ,?2 ?2 ?1/? ?22 ?transform? "20" ?22 Learn transform, ?22 ?2 Cached! atom,? transform,?22 Concat January 21, 2017 UC Berkeley PROSE Hackathon 16
Outline Version space algebra Deductive synthesis in PROSE Live session: creating FlashFill & FlashExtract Q&A January 21, 2017 UC Berkeley PROSE Hackathon 17
Demo January 21, 2017 UC Berkeley PROSE Hackathon 18
Outline Version space algebra Deductive synthesis in PROSE Live session: creating FlashFill & FlashExtract Q&A January 21, 2017 UC Berkeley PROSE Hackathon 19
