6 ms·

Building a Program Synthesizer

132 points by sidereal 8y ago

arnioxux 8y ago
His previous post was probably the best overview on program synthesis paradigms (circa 2015): https://homes.cs.washington.edu/~bornholt/post/synthesis-explained.html https://homes.cs.washington.edu/~bornholt/post/synthesis-exp... It's a much broader overview of the field so read that first if you need an intro!
- apskim 8y ago
  And if you want a deeper dive after that, here's a 100-page survey of all the techniques, principles, and applications of program synthesis circa 2017: https://www.microsoft.com/en-us/research/publication/program-synthesis/ https://www.microsoft.com/en-us/research/publication/program...
jbattle 8y ago
With these techniques - how complex a program can practically be created in 2018? A lot of the example programs mentioned feel more like functions (stateless + deterministic mapping of a tuple of inputs to a single output). In contrast, I think of a 'program' as having a longish lifecycle comprising a stream of inputs and outputs. Relatedly, I'm not clear how well the approaches detailed here actually would scale with complexity - is this a meaningful building block in building more complex applications? Or is some higher-order framework needed that 'knows' how to apply this in a rich context?
- jarmitage 8y ago
  The higher-order framework is you! Most of the recent work in this field seems to be based around the idea of program "sketching", i.e. the programmer sketches a high-level specification, and the algorithms progressively synthesise and evaluate small functions / programs to efficiently implement the sketch. No doubt machine learning researchers will have something to say about this though...
- saurabh20n 8y ago
  10-50 lines of code. You have to pick the right domain. Sumit is doing a lot of work [1] on integrating these ideas into Microsoft's products, e.g., Excel's flash fill. Ras [2] is synthesizing biology models and architecture design. Sanjit, Armando, Emina, Rishabh, are all doing excellent work getting them to scale. [1] https://www.microsoft.com/en-us/research/video/flash-fill-flashextract/ https://www.microsoft.com/en-us/research/video/flash-fill-fl... [2] https://www.frontiersin.org/articles/10.3389/fbioe.2014.00075/full https://www.frontiersin.org/articles/10.3389/fbioe.2014.0007...
- Y_Y 8y ago
  Barliman is pretty neat for filling in functions given a few examples: https://youtube.com/watch?v=5vtC7WEN76w https://youtube.com/watch?v=5vtC7WEN76w
- cf 8y ago
  Incidentally there is a workshop this Sunday at ICML about program synthesis https://uclmr.github.io/nampi/ https://uclmr.github.io/nampi/
jnurmine 8y ago
Once upon a time I thought of this and came to a conclusion that in the future software is not written, it is grown. A big hall with computers, churning on calculations to end up with reusable modules/components for some predescribed purpose. These are combined and eventually larger systems emerge. The inputs to the calculations were to be descriptions of what the program should do, no details on the "how". For instance, "make an input box for name and snailmail address, with cancel and ok buttons". It was obviously warp engine level stuff when it comes to feasibility and I thought it would be very far away, like 100 years away... But maybe it is closer than that.
- deleted 8y ago
  [deleted]
- iancmceachern 8y ago
  This is happening now for mechanical design. They call it generative design. You give inputs (volume/shape, loading cases, other parameters) and then the software iteratively solves for the optimum geometry to meet the goals.
  - jbattle 8y ago
    Example: antennas have been evolved to meet specific special criteria ... https://en.wikipedia.org/wiki/Evolved_antenna https://en.wikipedia.org/wiki/Evolved_antenna
  - deleted 8y ago
    [deleted]
  - tobmlt 8y ago
    And there is also ``form parameter design'' for ship hull geometry. It is also generative, but perhaps it more typically makes use of deterministic (nonlinear optimization) solvers to generate the geometry itself. (Implementations vary - I show my bias (or just inability to shut up) here as I am trying to finish a PhD in this as we speak) The main similarity I'm going for in this comment is that the user specifies design constraints and the program generates ship hull shapes that meet those requirements. Tie generative methods in with solvers for hydrodynamics, motions, structures, stability, etc, and one can conceive of automating the ship hull design spiral, or sections of it anyway. That's not to say that some of this is not already out there in commercial software.
opless 8y ago
Of course, being a new old thing, it's not complete without referencing it by it's actual name ... Genetic Programming. http://www.genetic-programming.com/johnkoza.html http://www.genetic-programming.com/johnkoza.html
- seanmcdirmid 8y ago
  Well, genetic programming is a subset of program synthesis, not a same set. I’m not sure how the use of an SMT solver could be considered a genetic programming method.
  - opless 8y ago
    Ah, I read the first link in the comments first, which really does imply they're using GP methods. https://homes.cs.washington.edu/~bornholt/post/synthesis-explained.html https://homes.cs.washington.edu/~bornholt/post/synthesis-exp... However they're using a SMT solver as part of the fitness function of the program. You know - it needs the correct output, but you need to prevent overfitting, and if you have a formal proof of the program generated you can expend greater effort into reducing its complexity and optimising. Again, it's an old new thing and possibly going to start getting hyped like neural networks have been of late.
    - seanmcdirmid 8y ago
      I’m sure the term program synthesis precedes the term genetic programming. Neither of these are new things. This (https://www.sri.com/sites/default/files/uploads/publications/pdf/1426.pdf https://www.sri.com/sites/default/files/uploads/publications...) is from 1971, for example. The earliest reference I can find to genetic programming is in the early 90s. There are plenty of program synthesis techniques (maybe not this one) that do not use fitness functions and get the program straight from a solver. If they have anything written up, I’m sure the related work section would make the context more clear. As for the accusation of band wagoning, it seems to come straight from the community that has been doing synthesis for years, not the ones that do GP.
    - ychen306 8y ago
tobmlt 8y ago
In case anybody is reading this post and wants an idea of how to get started with the basics of logic programming (upon which one might build toy constraint solvers) I recommend this: https://codon.com/hello-declarative-world#programming-paradigms https://codon.com/hello-declarative-world#programming-paradi...

132 points by sidereal 8y ago

His previous post was probably the best overview on program synthesis paradigms (circa 2015): https://homes.cs.washington.edu/~bornholt/post/synthesis-explained.html https://homes.cs.washington.edu/~bornholt/post/synthesis-exp... It's a much broader overview of the field so read that first if you need an intro!

apskim 8y ago
And if you want a deeper dive after that, here's a 100-page survey of all the techniques, principles, and applications of program synthesis circa 2017: https://www.microsoft.com/en-us/research/publication/program-synthesis/ https://www.microsoft.com/en-us/research/publication/program...

jbattle 8y ago

With these techniques - how complex a program can practically be created in 2018? A lot of the example programs mentioned feel more like functions (stateless + deterministic mapping of a tuple of inputs to a single output). In contrast, I think of a 'program' as having a longish lifecycle comprising a stream of inputs and outputs. Relatedly, I'm not clear how well the approaches detailed here actually would scale with complexity - is this a meaningful building block in building more complex applications? Or is some higher-order framework needed that 'knows' how to apply this in a rich context?

jarmitage 8y ago
The higher-order framework is you! Most of the recent work in this field seems to be based around the idea of program "sketching", i.e. the programmer sketches a high-level specification, and the algorithms progressively synthesise and evaluate small functions / programs to efficiently implement the sketch. No doubt machine learning researchers will have something to say about this though...
saurabh20n 8y ago
10-50 lines of code. You have to pick the right domain. Sumit is doing a lot of work [1] on integrating these ideas into Microsoft's products, e.g., Excel's flash fill. Ras [2] is synthesizing biology models and architecture design. Sanjit, Armando, Emina, Rishabh, are all doing excellent work getting them to scale. [1] https://www.microsoft.com/en-us/research/video/flash-fill-flashextract/ https://www.microsoft.com/en-us/research/video/flash-fill-fl... [2] https://www.frontiersin.org/articles/10.3389/fbioe.2014.00075/full https://www.frontiersin.org/articles/10.3389/fbioe.2014.0007...
Y_Y 8y ago
Barliman is pretty neat for filling in functions given a few examples: https://youtube.com/watch?v=5vtC7WEN76w https://youtube.com/watch?v=5vtC7WEN76w
cf 8y ago
Incidentally there is a workshop this Sunday at ICML about program synthesis https://uclmr.github.io/nampi/ https://uclmr.github.io/nampi/

jnurmine 8y ago

Once upon a time I thought of this and came to a conclusion that in the future software is not written, it is grown. A big hall with computers, churning on calculations to end up with reusable modules/components for some predescribed purpose. These are combined and eventually larger systems emerge. The inputs to the calculations were to be descriptions of what the program should do, no details on the "how". For instance, "make an input box for name and snailmail address, with cancel and ok buttons". It was obviously warp engine level stuff when it comes to feasibility and I thought it would be very far away, like 100 years away... But maybe it is closer than that.

deleted 8y ago
[deleted]
iancmceachern 8y ago
This is happening now for mechanical design. They call it generative design. You give inputs (volume/shape, loading cases, other parameters) and then the software iteratively solves for the optimum geometry to meet the goals.
- jbattle 8y ago
  Example: antennas have been evolved to meet specific special criteria ... https://en.wikipedia.org/wiki/Evolved_antenna https://en.wikipedia.org/wiki/Evolved_antenna
- deleted 8y ago
  [deleted]
- tobmlt 8y ago
  And there is also ``form parameter design'' for ship hull geometry. It is also generative, but perhaps it more typically makes use of deterministic (nonlinear optimization) solvers to generate the geometry itself. (Implementations vary - I show my bias (or just inability to shut up) here as I am trying to finish a PhD in this as we speak) The main similarity I'm going for in this comment is that the user specifies design constraints and the program generates ship hull shapes that meet those requirements. Tie generative methods in with solvers for hydrodynamics, motions, structures, stability, etc, and one can conceive of automating the ship hull design spiral, or sections of it anyway. That's not to say that some of this is not already out there in commercial software.

opless 8y ago

Of course, being a new old thing, it's not complete without referencing it by it's actual name ... Genetic Programming. http://www.genetic-programming.com/johnkoza.html http://www.genetic-programming.com/johnkoza.html

seanmcdirmid 8y ago
Well, genetic programming is a subset of program synthesis, not a same set. I’m not sure how the use of an SMT solver could be considered a genetic programming method.
- opless 8y ago
  Ah, I read the first link in the comments first, which really does imply they're using GP methods. https://homes.cs.washington.edu/~bornholt/post/synthesis-explained.html https://homes.cs.washington.edu/~bornholt/post/synthesis-exp... However they're using a SMT solver as part of the fitness function of the program. You know - it needs the correct output, but you need to prevent overfitting, and if you have a formal proof of the program generated you can expend greater effort into reducing its complexity and optimising. Again, it's an old new thing and possibly going to start getting hyped like neural networks have been of late.
  - seanmcdirmid 8y ago
    I’m sure the term program synthesis precedes the term genetic programming. Neither of these are new things. This (https://www.sri.com/sites/default/files/uploads/publications/pdf/1426.pdf https://www.sri.com/sites/default/files/uploads/publications...) is from 1971, for example. The earliest reference I can find to genetic programming is in the early 90s. There are plenty of program synthesis techniques (maybe not this one) that do not use fitness functions and get the program straight from a solver. If they have anything written up, I’m sure the related work section would make the context more clear. As for the accusation of band wagoning, it seems to come straight from the community that has been doing synthesis for years, not the ones that do GP.
  - ychen306 8y ago

tobmlt 8y ago

In case anybody is reading this post and wants an idea of how to get started with the basics of logic programming (upon which one might build toy constraint solvers) I recommend this: https://codon.com/hello-declarative-world#programming-paradigms https://codon.com/hello-declarative-world#programming-paradi...