Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/2814270.2814310acmconferencesArticle/Chapter ViewAbstractPublication PagessplashConference Proceedingsconference-collections
research-article

FlashMeta: a framework for inductive program synthesis

Published: 23 October 2015 Publication History

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.

References

[1]
R. Alur, R. Bodik, G. Juniwal, M. M. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided synthesis. In FMCAD, pages 1– 17. IEEE, 2013.
[2]
E. Andersen, S. Gulwani, and Z. Popovi´c. Programming by demonstration framework applied to procedural math problems. Technical Report MSR-TR-2014-61, Microsoft Research, 2014.
[3]
D. W. Barowy, S. Gulwani, T. Hart, and B. Zorn. FlashRelate: Extracting relational data from semi-structured spreadsheets using examples. In PLDI, 2015.
[4]
T. Celik, E. J. Etemad, D. Glazman, I. Hickson, P. Linss, and J. Williams. Selectors level 3. W3C recommendation. World Wide Web Consortium, page 76, 2011.
[5]
J. Feser, S. Chaudhuri, and I. Dillig. Synthesizing data structure transformations from input-output examples. In PLDI, 2015.
[6]
S. Gulwani. Dimensions in program synthesis. In PPDP, pages 13–24. ACM, 2010.
[7]
S. Gulwani. Automating string processing in spreadsheets using input-output examples. In POPL, 2011.
[8]
W. R. Harris and S. Gulwani. Spreadsheet table transformations from examples. In PLDI, 2011.
[9]
C. A. R. Hoare. Algorithm 65: Find. Commun. ACM, 4(7): 321–322, July 1961. ISSN 0001-0782.
[10]
W. Hodges. A shorter model theory. Cambridge university press, 1997.
[11]
J. E. Hopcroft. Introduction to automata theory, languages, and computation. Pearson Education India, 1979.
[12]
T. Hottelier and R. Bodik. Synthesis of layout engines from relational constraints. Technical Report UCB/EECS-2014-181, University of California at Berkeley, 2014.
[13]
S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari. Oracle-guided component-based program synthesis. In ICSE, volume 1, pages 215–224. IEEE, 2010.
[14]
S. C. Johnson. Yacc: Yet another compiler-compiler, volume 32. Bell Laboratories Murray Hill, NJ, 1975.
[15]
S. Katayama. Systematic search for lambda expressions. Trends in functional programming, 6:111–126, 2005.
[16]
D. Kini and S. Gulwani. FlashNormalize: Programming by examples for text normalization. IJCAI, 2015.
[17]
E. Kitzelmann. A combined analytical and search-based approach for the inductive synthesis of functional programs. KI-Künstliche Intelligenz, 25(2):179–182, 2011.
[18]
A. S. Koksal, Y. Pu, S. Srivastava, R. Bodik, J. Fisher, and N. Piterman. Synthesis of biological models from mutation experiments. In POPL, 2013.
[19]
V. Kuncak, M. Mayer, R. Piskac, and P. Suter. Software synthesis procedures. CACM, 55(2):103–111, 2012.
[20]
Y. Kuniyoshi, M. Inaba, and H. Inoue. Learning by watching: Extracting reusable task knowledge from visual observation of human performance. IEEE Transactions on Robotics and Automation, 10(6):799–822, 1994.
[21]
T. A. Lau, P. Domingos, and D. S. Weld. Version space algebra and its application to programming by demonstration. In ICML, pages 527–534, 2000.
[22]
V. Le and S. Gulwani. FlashExtract: A framework for data extraction by examples. In PLDI, page 55. ACM, 2014.
[23]
H. Lieberman. Your wish is my command: Programming by example. Morgan Kaufmann, 2001.
[24]
E. Lu and R. Bodik. Quicksilver: Automatic synthesis of relational queries. Master’s thesis, EECS Department, University of California, Berkeley, May 2013.
[25]
Z. Manna and R. Waldinger. A deductive approach to program synthesis. TOPLAS, 2(1):90–121, 1980.
[26]
M. Mayer, G. Soares, M. Grechkin, V. Le, M. Marron, O. Polozov, R. Singh, B. Zorn, and S. Gulwani. User interaction models for disambiguation in programming by example. UIST, 2015.
[27]
T. M. Mitchell. Generalization as search. Artificial intelligence, 18(2):203–226, 1982.
[28]
P.-M. Osera and S. Zdancewic. Type-and-example-directed program synthesis. In PLDI, 2015.
[29]
P. Panchekha, A. Sanchez-Stern, J. R. Wilcox, and Z. Tatlock. Automatically improving accuracy for floating point expressions. PLDI, 2015.
[30]
M. Püschel, J. M. Moura, J. R. Johnson, D. Padua, M. M. Veloso, B. W. Singer, J. Xiong, F. Franchetti, A. Gaˇcic, Y. Voronenko, et al. SPIRAL: Code generation for DSP transforms. Proceedings of the IEEE, 93(2):232–275, 2005.
[31]
E. Schkufza, R. Sharma, and A. Aiken. Stochastic superoptimization. In ACM SIGARCH Computer Architecture News, volume 41, pages 305–316. ACM, 2013.
[32]
R. Singh and S. Gulwani. Synthesizing number transformations from input-output examples. In Computer Aided Verification, pages 634–651. Springer, 2012.
[33]
R. Singh and S. Gulwani. Learning semantic string transformations from examples. VLDB, 5(8):740–751, 2012.
[34]
R. Singh and S. Gulwani. Predicting a correct program in programming by example. CAV, 2015.
[35]
A. Solar-Lezama. Program synthesis by sketching. ProQuest, 2008.
[36]
E. Torlak and R. Bodik. Growing solver-aided languages with Rosette. In Onward!, pages 135–152. ACM, 2013.
[37]
A. Udupa, A. Raghavan, J. V. Deshmukh, S. Mador-Haim, M. M. Martin, and R. Alur. Transit: specifying protocols with concolic snippets. In PLDI, pages 287–296. ACM, 2013.
[38]
K. Yessenov, S. Tulsiani, A. Menon, R. C. Miller, S. Gulwani, B. Lampson, and A. Kalai. A colorful approach to text processing by example. In UIST, pages 495–504. ACM, 2013.
[39]
L. Zhang, C. F. Madigan, M. H. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In ICCAD, pages 279–285. IEEE Press, 2001.
[40]
Y. Zheng, X. Zhang, and V. Ganesh. Z3-str: A Z3-based string solver for web application analysis. In FSE, pages 114–124. ACM, 2013.

Cited By

View all
  • (2025)QURE: AI-Assisted and Automatically Verified UDF InliningProceedings of the ACM on Management of Data10.1145/37097163:1(1-26)Online publication date: 11-Feb-2025
  • (2024)CFLOBDDs: Context-Free-Language Ordered Binary Decision DiagramsACM Transactions on Programming Languages and Systems10.1145/3651157Online publication date: 4-Mar-2024
  • (2024)PBE-Based Selective Abstraction and Refinement for Efficient Property Falsification of Embedded SoftwareProceedings of the ACM on Software Engineering10.1145/36437401:FSE(293-315)Online publication date: 12-Jul-2024
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
October 2015
953 pages
ISBN:9781450336895
DOI:10.1145/2814270
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 10
    OOPSLA '15
    October 2015
    953 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2858965
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 October 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Inductive program synthesis
  2. deductive inference
  3. domain-specific languages
  4. frameworks
  5. programming by examples
  6. search-based synthesis

Qualifiers

  • Research-article

Funding Sources

Conference

SPLASH '15
Sponsor:

Acceptance Rates

Overall Acceptance Rate 268 of 1,244 submissions, 22%

Upcoming Conference

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)148
  • Downloads (Last 6 weeks)13
Reflects downloads up to 14 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)QURE: AI-Assisted and Automatically Verified UDF InliningProceedings of the ACM on Management of Data10.1145/37097163:1(1-26)Online publication date: 11-Feb-2025
  • (2024)CFLOBDDs: Context-Free-Language Ordered Binary Decision DiagramsACM Transactions on Programming Languages and Systems10.1145/3651157Online publication date: 4-Mar-2024
  • (2024)PBE-Based Selective Abstraction and Refinement for Efficient Property Falsification of Embedded SoftwareProceedings of the ACM on Software Engineering10.1145/36437401:FSE(293-315)Online publication date: 12-Jul-2024
  • (2024)Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector ManipulationsProceedings of the ACM on Programming Languages10.1145/36329138:POPL(2129-2159)Online publication date: 5-Jan-2024
  • (2024)Data Formulator: AI-Powered Concept-Driven Visualization AuthoringIEEE Transactions on Visualization and Computer Graphics10.1109/TVCG.2023.332658530:1(1128-1138)Online publication date: 1-Jan-2024
  • (2024)Automated discovery of algorithms from dataNature Computational Science10.1038/s43588-024-00593-94:2(110-118)Online publication date: 19-Feb-2024
  • (2024)Leveraging pre-trained language models for code generationComplex & Intelligent Systems10.1007/s40747-024-01373-8Online publication date: 29-Feb-2024
  • (2024)Parallel Assembly SynthesisLogic-Based Program Synthesis and Transformation10.1007/978-3-031-71294-4_1(3-26)Online publication date: 9-Sep-2024
  • (2024)The SemGuS ToolkitComputer Aided Verification10.1007/978-3-031-65633-0_2(27-40)Online publication date: 26-Jul-2024
  • (2024)Tree-Based Synthesis of Web Test Sequences from Manual ActionsTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_14(242-260)Online publication date: 14-Jul-2024
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media