5 ms·

Introduction To Program Synthesis (2018)

132 points by optimalsolver 5y ago

deleted 5y ago
[deleted]
LondonGeorge 5y ago
Is there a set of program synthesis problems (or a source of problems) accepted by academics as a reasonable benchmark for measuring progress these days? Or does each new approach find its own example problems to demonstrate their particular differences on?
- daralthus 5y ago
  Perhaps https://ml4code.github.io/tags.html#benchmark https://ml4code.github.io/tags.html#benchmark
- mechtaev 5y ago
  SyGuS competition (SyGuS-Comp)[1] is a widely-used collection of such problems, but of course there will always be problem domains that are not well-represented by standard benchmarks. 1. https://sygus.org/ https://sygus.org/
Darmani 5y ago
I was the TA for this course at MIT last time it was taught in 2020. Ask me anything.
- gnulinux 5y ago
  In what ways program synthesis different than code generation taught in compiler and/or PLT courses? Is the goal here get ad high level ss possible, or be able to create as much code as possible?
  - Darmani 5y ago
    One word: search. Most of the traditional compilation pipeline can be expressed using deterministic rewrite rules. Synthesizers of all families generate and consider a large number of possibilities. Flipping it around, there's an old joke that "a synthesizer is just a compiler that sometimes doesn't work." But the first thing to learn is that, the deeper you go, the blurrier the lines get. There certainly exists a compiler out there that does more search than a good chunk of things done under the name of synthesis. (Especially because "synthesis" has become a bit of a buzzword in PL circles, and often gets slapped where it doesn't really belong.) I've discussed this briefly before in my blog: http://www.pathsensitive.com/2021/03/why-programmers-shouldnt-learn-theory.html http://www.pathsensitive.com/2021/03/why-programmers-shouldn...
- agumonkey 5y ago
  How do you feel about the topic, is it lively ? dormant but potentially great ? Any other source to read about ? thanks :)
  - Darmani 5y ago
    It's a very lively field. Lots of groups working on it. Last year, the big 3 PL conferences (PLDI, POPL, OOPSLA) all had tracks dedicated to it. A few years ago, Armando (my advisor and the professor of this course) taught a weekend seminar on the nitty-gritty internals of how his tool, Sketch, works ---- and had commercial users flying in. Most recent summaries off the top of my head: https://alexpolozov.com/blog/program-synthesis-2018/ https://alexpolozov.com/blog/program-synthesis-2018/ https://www.microsoft.com/en-us/research/wp-content/uploads/2017/10/program_synthesis_now.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
    - srvmshr 5y ago
      Fun fact: My elder brother was Armando's TA in TAMU. Armanda probably was the brightest and most fun guy to work with. There were extra credit for building a fully functional software CPU and its vector pipeline supporting VLIW (mid 90s duh). Your advisor guy did it in a breeze. The instructor privately confided to my brother he was a legend in the making. Ask him about Sid in Lawrence Rawschberger's class for good old anecdotes! :)
- archibaldJ 5y ago
  Would knowledge in automated theorem proving (e.g. knowing how coq works) be somehow transferable to research in this field? What are some existing open-source program synthesis libraries/frameworks where we can tinker around and maybe make something with it? Thanks! I'm super curious about this field and it's somewhat related to what I'm working on so I'm pretty interested to learn more!
  - Darmani 5y ago
    > Would knowledge in automated theorem proving (e.g. knowing how coq works) be somehow transferable to research in this field? Possibly. First, Coq is not an automated theorem proving tool; it's an interactive theorem prover. If by automated theorem proving, you're thinking of a tool like Z3 or CVC4 which find models of statements in a decidable theory (which are pretty much always mathematically uninteresting), then...absolutely! SAT/SMT are at the core of constraint-based synthesis. Heck, CVC4 has a SyGuS mode that won the synthesis competition one year. If you're referring to actually searching for interesting theorems, as done by tools like Vampire and Otter, then probably not. Last month, I was discussing the matching algorithm used in the paper "egg: Fast and Flexible Equality Saturation" with a collaborator. It uses code trees, which I read about a few months earlier in the Handbook of Automated Reasoning. It stands out because I had pretty much never encountered a mention of any of that stuff in the preceding several years. I touch on this slightly in this blog post, about the benefits of learning Coq towards synthesis: http://www.pathsensitive.com/2021/03/why-programmers-shouldnt-learn-theory.html http://www.pathsensitive.com/2021/03/why-programmers-shouldn... . (And the benefits I mention are in understanding the type theory, not the innards.) > What are some existing open-source program synthesis libraries/frameworks where we can tinker around and maybe make something with it? https://github.com/microsoft/prose https://github.com/microsoft/prose Sketch: Download and manual from https://people.csail.mit.edu/asolar/ https://people.csail.mit.edu/asolar/ https://egraphs-good.github.io/ https://egraphs-good.github.io/ I searched for a few others, but they're either tools rather than frameworks, not directly synthesis, or I couldn't find a download. Though I may as well plug my own Cubix framework: http://cubix-framework.com/ http://cubix-framework.com/ > Thanks! I'm super curious about this field and it's somewhat related to what I'm working on so I'm pretty interested to learn more! Awesome! I hope to see great things coming from you.
- YeGoblynQueenne 5y ago
  Not so much a question as a complaint: I can't find anything about Inductive Logic Programming in the course material. ILP is the field that studies the inductive synthesis of logic programs, it should fit right in with the rest of the material, particulary in the parts about constraint based synthesis and verification. If ILP is discussed and I missed it, apologies- I've only read through very quickly to get a general idea of the curriculum and bookmarked the top level for reference.
  - Darmani 5y ago
    I'm barely familiar with Inductive Logic Programming and never hear anyone talk about it. I came in prepared to dismiss the field's relevance to synthesis, but decided to do a bunch of reading first so that I could do so from an informed perspective. I knew ILP to be "constructing a classifier from a conjunction of literals," which is very much not synthesis. It turns out there's a lot more done under the name of ILP. I think the real answer is largely that logic programming as a whole fell out of favor in the US sometime in the 90's, whereas the program synthesis renaissance started in the 2000's -- and is still US-dominated. Not to say there still aren't tons of people doing logic programming, but, personal anecdote: I encountered a ton of logic programming papers during the lit review for one of my other project, which has some overlap in the symbolic techniques used, and....they're all from the period 1988-1995. Mukund's work is the most relevant from a synthesis perspective that I know of, as one of the only people doing synthesis of a logic language (unless you count SQL). (Note: This is distinct from people like William Byrd doing synthesis using a logic programming language.) Have a look at the bottom of page 23 of "Provenance-Guided Synthesis of Datalog Programs" https://dl.acm.org/doi/pdf/10.1145/3371130 https://dl.acm.org/doi/pdf/10.1145/3371130 . It does a good job explaining the distinction between the goals of ILP things done under the umbrella of synthesis. But note that this work is still considered niche in the synthesis world. There's also the question about what techniques belong to what field; I expect that, were I to dig into thy synthesis-relevant parts of ILP further, I'd find a lot of techniques that are familiar and that I learned with no connection to ILP. Paul Graham has said that philosophy is not useful because everything useful it discovers was spun out into a different field. ( http://www.paulgraham.com/philosophy.html http://www.paulgraham.com/philosophy.html ) The philosophy of computer science in that perspective is AI. 40 years ago, garbage collection, term rewriting, logic programming, and programming assistants were all AI. Even just 20 years ago, Tessa Lau's work on inductive synthesis was AI. Today, all of those are things likely to be rejected from a top AI conference, but welcome at a PL conference. Thus, you might find in the synthesis world techniques that would be familiar to an old-school ILP researcher, but without shared context. (Two recent exceptions are neural synthesis and probabilistic programming, where you do see a lot of crossover between PL and ML. This is very recent. [Insert harsh judgments here about the attempts from 2016 and earlier to learn programs.])
agumonkey 5y ago
I also tried to read mathematics of program construction (similar spirit I assume) with Gibbons et al. https://duckduckgo.com/?q=mathematics+program+construction&t=ffab&ia=web https://duckduckgo.com/?q=mathematics+program+construction&t...

132 points by optimalsolver 5y ago

deleted 5y ago

[deleted]

Is there a set of program synthesis problems (or a source of problems) accepted by academics as a reasonable benchmark for measuring progress these days? Or does each new approach find its own example problems to demonstrate their particular differences on?

daralthus 5y ago
Perhaps https://ml4code.github.io/tags.html#benchmark https://ml4code.github.io/tags.html#benchmark
mechtaev 5y ago
SyGuS competition (SyGuS-Comp)[1] is a widely-used collection of such problems, but of course there will always be problem domains that are not well-represented by standard benchmarks. 1. https://sygus.org/ https://sygus.org/

Darmani 5y ago

I was the TA for this course at MIT last time it was taught in 2020. Ask me anything.

gnulinux 5y ago
In what ways program synthesis different than code generation taught in compiler and/or PLT courses? Is the goal here get ad high level ss possible, or be able to create as much code as possible?
- Darmani 5y ago
  One word: search. Most of the traditional compilation pipeline can be expressed using deterministic rewrite rules. Synthesizers of all families generate and consider a large number of possibilities. Flipping it around, there's an old joke that "a synthesizer is just a compiler that sometimes doesn't work." But the first thing to learn is that, the deeper you go, the blurrier the lines get. There certainly exists a compiler out there that does more search than a good chunk of things done under the name of synthesis. (Especially because "synthesis" has become a bit of a buzzword in PL circles, and often gets slapped where it doesn't really belong.) I've discussed this briefly before in my blog: http://www.pathsensitive.com/2021/03/why-programmers-shouldnt-learn-theory.html http://www.pathsensitive.com/2021/03/why-programmers-shouldn...
agumonkey 5y ago
How do you feel about the topic, is it lively ? dormant but potentially great ? Any other source to read about ? thanks :)
- Darmani 5y ago
  It's a very lively field. Lots of groups working on it. Last year, the big 3 PL conferences (PLDI, POPL, OOPSLA) all had tracks dedicated to it. A few years ago, Armando (my advisor and the professor of this course) taught a weekend seminar on the nitty-gritty internals of how his tool, Sketch, works ---- and had commercial users flying in. Most recent summaries off the top of my head: https://alexpolozov.com/blog/program-synthesis-2018/ https://alexpolozov.com/blog/program-synthesis-2018/ https://www.microsoft.com/en-us/research/wp-content/uploads/2017/10/program_synthesis_now.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
  - srvmshr 5y ago
    Fun fact: My elder brother was Armando's TA in TAMU. Armanda probably was the brightest and most fun guy to work with. There were extra credit for building a fully functional software CPU and its vector pipeline supporting VLIW (mid 90s duh). Your advisor guy did it in a breeze. The instructor privately confided to my brother he was a legend in the making. Ask him about Sid in Lawrence Rawschberger's class for good old anecdotes! :)
archibaldJ 5y ago
Would knowledge in automated theorem proving (e.g. knowing how coq works) be somehow transferable to research in this field? What are some existing open-source program synthesis libraries/frameworks where we can tinker around and maybe make something with it? Thanks! I'm super curious about this field and it's somewhat related to what I'm working on so I'm pretty interested to learn more!
- Darmani 5y ago
  > Would knowledge in automated theorem proving (e.g. knowing how coq works) be somehow transferable to research in this field? Possibly. First, Coq is not an automated theorem proving tool; it's an interactive theorem prover. If by automated theorem proving, you're thinking of a tool like Z3 or CVC4 which find models of statements in a decidable theory (which are pretty much always mathematically uninteresting), then...absolutely! SAT/SMT are at the core of constraint-based synthesis. Heck, CVC4 has a SyGuS mode that won the synthesis competition one year. If you're referring to actually searching for interesting theorems, as done by tools like Vampire and Otter, then probably not. Last month, I was discussing the matching algorithm used in the paper "egg: Fast and Flexible Equality Saturation" with a collaborator. It uses code trees, which I read about a few months earlier in the Handbook of Automated Reasoning. It stands out because I had pretty much never encountered a mention of any of that stuff in the preceding several years. I touch on this slightly in this blog post, about the benefits of learning Coq towards synthesis: http://www.pathsensitive.com/2021/03/why-programmers-shouldnt-learn-theory.html http://www.pathsensitive.com/2021/03/why-programmers-shouldn... . (And the benefits I mention are in understanding the type theory, not the innards.) > What are some existing open-source program synthesis libraries/frameworks where we can tinker around and maybe make something with it? https://github.com/microsoft/prose https://github.com/microsoft/prose Sketch: Download and manual from https://people.csail.mit.edu/asolar/ https://people.csail.mit.edu/asolar/ https://egraphs-good.github.io/ https://egraphs-good.github.io/ I searched for a few others, but they're either tools rather than frameworks, not directly synthesis, or I couldn't find a download. Though I may as well plug my own Cubix framework: http://cubix-framework.com/ http://cubix-framework.com/ > Thanks! I'm super curious about this field and it's somewhat related to what I'm working on so I'm pretty interested to learn more! Awesome! I hope to see great things coming from you.
YeGoblynQueenne 5y ago
Not so much a question as a complaint: I can't find anything about Inductive Logic Programming in the course material. ILP is the field that studies the inductive synthesis of logic programs, it should fit right in with the rest of the material, particulary in the parts about constraint based synthesis and verification. If ILP is discussed and I missed it, apologies- I've only read through very quickly to get a general idea of the curriculum and bookmarked the top level for reference.
- Darmani 5y ago
  I'm barely familiar with Inductive Logic Programming and never hear anyone talk about it. I came in prepared to dismiss the field's relevance to synthesis, but decided to do a bunch of reading first so that I could do so from an informed perspective. I knew ILP to be "constructing a classifier from a conjunction of literals," which is very much not synthesis. It turns out there's a lot more done under the name of ILP. I think the real answer is largely that logic programming as a whole fell out of favor in the US sometime in the 90's, whereas the program synthesis renaissance started in the 2000's -- and is still US-dominated. Not to say there still aren't tons of people doing logic programming, but, personal anecdote: I encountered a ton of logic programming papers during the lit review for one of my other project, which has some overlap in the symbolic techniques used, and....they're all from the period 1988-1995. Mukund's work is the most relevant from a synthesis perspective that I know of, as one of the only people doing synthesis of a logic language (unless you count SQL). (Note: This is distinct from people like William Byrd doing synthesis using a logic programming language.) Have a look at the bottom of page 23 of "Provenance-Guided Synthesis of Datalog Programs" https://dl.acm.org/doi/pdf/10.1145/3371130 https://dl.acm.org/doi/pdf/10.1145/3371130 . It does a good job explaining the distinction between the goals of ILP things done under the umbrella of synthesis. But note that this work is still considered niche in the synthesis world. There's also the question about what techniques belong to what field; I expect that, were I to dig into thy synthesis-relevant parts of ILP further, I'd find a lot of techniques that are familiar and that I learned with no connection to ILP. Paul Graham has said that philosophy is not useful because everything useful it discovers was spun out into a different field. ( http://www.paulgraham.com/philosophy.html http://www.paulgraham.com/philosophy.html ) The philosophy of computer science in that perspective is AI. 40 years ago, garbage collection, term rewriting, logic programming, and programming assistants were all AI. Even just 20 years ago, Tessa Lau's work on inductive synthesis was AI. Today, all of those are things likely to be rejected from a top AI conference, but welcome at a PL conference. Thus, you might find in the synthesis world techniques that would be familiar to an old-school ILP researcher, but without shared context. (Two recent exceptions are neural synthesis and probabilistic programming, where you do see a lot of crossover between PL and ML. This is very recent. [Insert harsh judgments here about the attempts from 2016 and earlier to learn programs.])

agumonkey 5y ago

I also tried to read mathematics of program construction (similar spirit I assume) with Gibbons et al. https://duckduckgo.com/?q=mathematics+program+construction&t=ffab&ia=web https://duckduckgo.com/?q=mathematics+program+construction&t...