Live data from Hacker News

Building a Program Synthesizer

homes.cs.washington.edu

11–20 of 27 posts

Re: Building a Program Synthesizer

#12
post #11

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

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.

Re: Building a Program Synthesizer

#13
post #5

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 insta…

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.

Example: antennas have been evolved to meet specific special criteria ...

https://en.wikipedia.org/wiki/Evolved_antenna

Re: Building a Program Synthesizer

#14
post #5

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 insta…

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.

[deleted]

Re: Building a Program Synthesizer

#15
post #11

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

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.

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-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.

Re: Building a Program Synthesizer

#16
post #15

Earlier quoted context omitted.

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.

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-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 reduci…

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...) 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.

Re: Building a Program Synthesizer

#17
post #2

His previous post was probably the best overview on program synthesis paradigms (circa 2015): 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!

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...

Re: Building a Program Synthesizer

#18
post #15

Earlier quoted context omitted.

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.

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-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 reduci…

    Ah, I read the first link in the comments first, which really does imply they're using GP methods.
No, it doesn't.

Re: Building a Program Synthesizer

#19
post #15

Earlier quoted context omitted.

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-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 reduci…

Ah, I read the first link in the comments first, which really does imply they're using GP methods. No, it doesn't.

And the evidence to back up your assertion, is where?

Here's mine... (excuse my lack of formatting.)

The synthesis step of stochastic superoptimisation finds the next candidate program P’ by drawing an MCMC sample based on the previous candidate program P. It proposes P’ by randomly applying one of a few mutations to P:

* changing the opcode of a randomly selected instruction

* changing a random operand of a randomly selected instruction

* inserting a new random instruction

* swapping two randomly selected instructions

* deleting an existing randomly selected instruction

The MCMC sampler uses the cost function, which measures how “close” to the target program P’ is and how fast P’ is, to decide whether to accept the candidate P’. A candidate is more likely to be accepted if it is close to the target or very fast. But even programs that are slow or distant from the target have some probability of being accepted, ensuring we explore novel programs

Post reply on HN