Program Synthesis through Examples and Search Methodology

Dive into the world of program synthesis through examples and explore search methodology. Discover the challenges, methodologies, and techniques involved in designing efficient search strategies for inductive program synthesis. Uncover the architecture, output properties, and problem reduction techniques to synthesize programs from specifications.

• Program Synthesis
• Search Methodology
• Inductive Programming
• Architecture
• Output Properties

grabowski_j Follow

Uploaded on Apr 17, 2025 | 0 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.

Presentation Transcript

1. Programming by Examples Sumit Gulwani Marktoberdorf Lectures August 2015

2. Lecture 3 Search Methodology 1

3. PBE Architecture Example-based specification Ordered set of Program Programs Ranking Function Search Algorithm DSL Challenge 1: Ambiguous/under-specified intent may result in unintended programs. Challenge 2: Designing efficient search strategy. FlashMeta: A Framework for Inductive Program Synthesis Alex Polozov, Sumit Gulwani; OOPSLA 2015 2

4. Search Methodology Goal:Set of expr of kind ? that satisfies spec ? [denoted ? ? ] ?: DSL (top-level) expression ?: example-based inductive specification Examples: Conjunction of (input state ? , output value ?) [denoted ? ?] Inductive Spec: Conjunction of (input state, output property) Output properties are easier to specify intent! 3

5. Output properties Task Elements belonging to the output list Elements not belonging to the output list Contiguous subsequence of the output list Prefix of the output list 4

6. Output properties Task Prefix of the output table (seq of records) We do not require explicit (magenta) record boundaries in which case the spec is: Prefixes of projections of the output table 5

7. Search Methodology Goal:Set of expr of kind ? that satisfies spec ? [denoted ? ? ] ?: DSL (top-level) expression ?: example-based inductive specification Methodology: Based on divide-and-conquer ? ? is reduced to simpler problems (over sub- expressions of e or sub-constraints of ?). Top-down (as opposed to bottom-up enumerative search). 6

8. Problem Reduction list of strings T := Map(L, S) substring fn S := ?y: list of lines L := Filter(Split(d, \n ), B) boolean fn B := ?y: Spec for L FlashExtract DSL Spec for S Spec for T 7

9. Problem Reduction substring expr E := SubStr(y, P1, P2) position expr P := K | Pos(y, R1, R2, K) SubStr grammar Spec for P1 Spec for P2 Spec for E Redmond, WA Redmond, WA 8

10. Search Methodology Goal:Set of expr of kind ? that satisfies spec ? [denoted ? ? ] ?: DSL (top-level) expression ?: example-based inductive specification Methodology: Based on divide-and-conquer ? ? is reduced to simpler problems (over sub- expressions of e or sub-constraints of ?). Top-down (as opposed to bottom-up enumerative search). Key concepts in problem reduction: VSAs & Witness functions 9

11. Version Space Algebra (VSA) AST based succinct representation for a set of programs A graph with 3 kinds of nodes and a unique start node. Each node ? represents a set of programs [?]. Leaf node: labelled with a set ? of program expressions [?] = ? Union node (with k children ?1, ,??) ? = ?1 ?? Join node (with k ordered children ?1, ,??): labelled with a k-ary operator F ? = ? ?1, ,?? ?1 ?1, ,?? [??] } 10

12. VSA Operations Union: VSA ??? ??? Intersect: VSA ??? ??? TopRank: ??? Ranking function int ? Top-? programs Cluster: ??? State ? 2??? The output is a smallest partitioning of the input VSA s.t. all programs in any output VSA produce the same output on ?. Filter: ??? Spec ? ??? Filter the input VSA to the subset that satisfies spec ?. 11

13. Problem Reduction Rules Union( ?1 ? , ?2 ? ) ? ? = where ? is a non-terminal defined as ? ?1 | ?2 ?????????( ? ?1, ? ?2) ? ?1 ?2 = 12

14. Intersect Operation Intersect: ??? ??? ??? The output VSA represents the intersection of the sets of programs represented by the input VSAs. ????????? ???? ?1,????( ?2) = ???? ?1 ?2 ?????????(???? ? ,?)) = { ? ? | ? ? } ????????? Union ?1,?2,? = ????????? ? ?1,?2,? ?1 ?(????????? ?1,?1 Union(????????? ?1,? ,????????? ?2,? ) ,?2 = ,????????? ?2,?2 ) 13

15. Problem Reduction Rules Union( ?1 ? , ?2 ? ) ? ? = where ? is a non-terminal defined as ? ?1 | ?2 ?????????( ? ?1, ? ?2) ? ?1 ?2 = ? ?1 ?2 = ??????( ? ?1,?2) 14

16. Cluster Operation Cluster: ??? ? 2??? Smallest partitioning of the input VSA s.t. programs in any output VSA are indistinguishable over the input state. Notation: Let ???????(?,?) be denoted by ? ? Union ?1,?2 ? = let ? = ?1 ? ?2 ? in ?????( ?,?) ? ?1,?2 ? = let ?1= ?1 ?, ?2= ?2 ? in let ?3= F ?1 ?2 } in ?????( ?3,?) ?1,?2 ,?2 ?1 ????? ?,? unites VSAs in ? that have same behavior on ?. 15

17. Filter Operation Filter: ??? ? ??? Filter the input VSA to the subset that satisfies ?. ?????? ?,? = let ? = set of input states that occur in ? in let ? = ? ? in Union( ? ? ? satisfies ?}) 16

18. Problem Reduction Rules Union( ?1 ? , ?2 ? ) ? ? = where ? is a non-terminal defined as ? ?1 | ?2 ?????????( ? ?1, ? ?2) ? ?1 ?2 = ? ?1 ?2 = ??????( ? ?1,?2) 17

19. Problem Reduction Rules Let F be a binary operator. Inverse set:? 1? = ?,? ? ?,? = ?} ?????? 1"Abc" = { "Abc", ,("??","c"), ("A","bc"), ( ,"Abc")} ? ?1,?2 ? ? = ?????({F e1 ? ? , ?2 ? ? | ?,? ? 1? }) [?????? ?,? (? "Abc")] = Union({ ??????( ? ? "Abc" , ? ? ? ), ?????? ? ? "Ab" , ? ? "?" ?????? ? ? "A" , ? ? "??" ?????? ? ? , ? ? "???" , , }) 18

20. Problem Reduction Rules Let F be an n-ary binary operator. Dependent Inverse Set: ? 1? ?1) = ?2, ,?? ? ?1, ,?? = ?} ?????? 1"Ab" "Ab cd Ab") = { 0,2 ,(6,8) } ? ?0,?1,?2 ? ? = let ? = VSA of ?0 in let ?1, ,?? = ? ? in let ??= ???? ??,? in ?,? ? 1? ?? ?1= ?1 ? ? ?2= ?2 ? ? ????? ? = 1..? ? ??,?1,?2 Let ? be the state ?: ?? ?? ?? . ?????? ?,?1,?2 ? "cd" ?, ?1 ? 3 , ?2 ? 5 ?????? = 19

21. Problem Reduction Rules Let F be an n-ary operator. Witness Function: ??? = ?1, ,?? ?? ??: ? ?1, ,?? ? } ?1 1 ?2 0,?1 ?1,?2 ?2, ?1 1 ?2 1,?1 ?1 ?2 ?2,1 ?????1 ?1 ?2 ?2 = ? ?1,?2 ? = ?????( F e1 ?1, ?2 ?2 ?1,?2 ??? }) ??? ?,?1,?2 ?1 ?1 ?2 ?2 ? ?1 1 ?2 0 , E1 ?1 ?1, ?2 ?2 ?2 = ?????( ? ?1 1 ?2 1 , E1 ?1 ?1 (?2 ?2) , ?2 1 ??? ,??? ) 20

22. FlashMeta Framework Provides efficient implementations of VSA operations Provides a library of witness functions Role of synthesis designer Can add new operators and witness functions. Can provide ranking strategies. Can specify tactics to resolve non-determinism in search Which witness function to use? How to order search branches? 21

23. Comparison of FlashMeta with hand-tuned implementations Lines of Code (K) Development time (months) Project FlashFill FlashExtractText FlashRelate FlashNormalize FlashExtractWeb Original 12 7 5 17 N/A FlashMeta 3 4 2 2 2.5 Original 9 8 8 7 N/A FlashMeta 1 1 1 2 1.5 Running time of FlashMeta implementations vary between 0.5- 3x of the corresponding original implementation. Faster because of some free optimizations Slower because of larger feature sets & a generalized framework 22