[madPL] Synthesis / SemGuS Reading Group - Prose - Friday at 1:10


Date: Thu, 7 Oct 2021 15:57:05 +0000
From: Keith Jens Carl Johnson <keith.johnson@xxxxxxxx>
Subject: [madPL] Synthesis / SemGuS Reading Group - Prose - Friday at 1:10

Good morning,

 

I will be presenting at this week’s Synthesis / SemGuS reading group on Prose (a.k.a. FlashMeta), which is Microsoft’s program synthesis toolkit that is used in Excel, PowerShell, and more.

 

Everyone is welcome; the paper discussion will start at 1:10pm tomorrow (Friday) at the Zoom link below. Wiley will be discussing the productivity tool Notion from 1 to 1:10 or so.

https://uwmadison.zoom.us/j/96450343227?pwd=emtGcHROSVZoOWsyWEFhN2wyazA2Zz09

 

 

Link:

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/oopsla15-pbe.pdf

 

Title:

FlashMeta: A Framework for Inductive Program Synthesis

 

Abstract:

Inductive synthesis, or programming-by-examples (PBE) is gaining prominence with disruptive applications for automating repetitive tasks in end-user programming. However, designing, developing, and maintaining an effective industrial-quality inductive synthesizer is an intellectual and engineering challenge, requiring 1-2 man-years of effort. Our novel observation is that many PBE algorithms are a natural fall-out of one generic meta-algorithm and the domain-specific properties of the operators in the underlying domain-specific language (DSL). The meta-algorithm propagates example-based constraints on an _expression_ to its subexpressions by leveraging associated witness functions, which essentially capture the inverse semantics of the underlying operator. This observation enables a novel program synthesis methodology called data-driven domain-specific deduction (D4), where domain-specific insight, provided by the DSL designer, is separated from the synthesis algorithm. Our FlashMeta framework implements this methodology, allowing synthesizer developers to generate an efficient synthesizer from the mere DSL definition (if properties of the DSL operators have been modeled). In our case studies, we found that 10+ existing industrial-quality mass-market applications based on PBE can be cast as instances of D4. Our evaluation includes reimplementation of some prior works, which in FlashMeta become more efficient, maintainable, and extensible. As a result, FlashMeta-based PBE tools are deployed in several industrial products, including Microsoft PowerShell 3.0 for Windows 10, Azure Operational Management Suite, and Microsoft Cortana digital assistant.

 

“Homework” Question:

Prose gets much of its power from expert domain-specific knowledge, tailored to the specific synthesis problem at hand. Conversely, other approaches (e.g., SyGuS or SemGuS) provide only generic knowledge such as the grammar and semantics of operators, having general applicability to many problems. What domain-specific knowledge would you have liked to have in synthesis problems you have looked in the past? Examples might include ranges of values (“x is always between 0 and 5”), expected inputs and outputs (“this term only produces odd numbers”), and data sources (“the output should pull substrings from this input text”).

 

-Keith

[← Prev in Thread] Current Thread [Next in Thread→]
  • [madPL] Synthesis / SemGuS Reading Group - Prose - Friday at 1:10, Keith Jens Carl Johnson <=