saurabh20n 26 days ago [-]
I am the OP. Along with Ras and Henele, we are leading efforts in program synthesis at Synthetic Minds (YC S’18). I started working on synthesis in 2007; and Ras has been developing these techniques since the late 90s and is an ACM fellow for his work in program synthesis.

The researchers will talk about their peer-reviewed work in web automation, hardware security, operating system extensions, programming for non-programmers, automatic code translation, and superoptimization. Hopefully, this will illustrate the power and limitations. We'd love for people to extrapolate from these onto their own domain-specific automation needs.

By touching upon foundational techniques (making imperative code functional, symbolic compilation, SMT encodings, partial evaluation), hopefully the leap to "code synthesis" will seem less like magic and more like an obvious next step. In addition, open-source frameworks exist (e.g., Rosette, Sketch) that abstract away these foundations, and the program will cover those in hands-on workshops.

We’d love to hear insights into application from people for whom synthesis is new. Some problems are exciting to us (Synthetic Minds is working on smart contract synthesis); and we’d love for the community to brainstorm applications to their domains.

kyboren 25 days ago [-]
Cool! Very similar techniques can be used in the hardware domain. For these types of problems, at least, I have found SRI's yices solver to be much, much more performant than Armando's CEGIS solver. Do you have any tips on other solvers you've found to be faster for exists-forall problems?

Here's a raw example of a 32-bit adder super-optimized according to rough delay, gate complexity, and wire complexity models embedded in the 2QBF: https://share.riseup.net/#xg2ySn41zmhtHtmrlQWn5Q . According to post-PAR results from Innovus, it can actually (barely) beat DesignWare adders at some points in the trade-off space.

rbodik 22 days ago [-]
Hi, this looks like a strong result. Congratulations!

Short answer: to scale up hardware synthesis, it may be necessary to change the encoding rather than look for a better solver.

More details: I should first say that I have limited experience with synthesizing hardware. My lessons come from [1], where synthesized a small Wallace Tree multiplier. What that taught me is that hardware arithmetic circuits should perhaps not be formulated as a 2QBF problem -- because you might need too many counterexample inputs to terminate the CEGIS loop.

Instead, I believe that the circuit synthesis should use algebraic reasoning (for correctness) and combinatorial reasoning to explore the space of candidate circuits. Since one symbolic input is sufficient to show correctness, the problem simplifies from 2QBF to SAT.

This idea is briefly explained in Sec 4.1 in [3], a project that synthesizes software expressions that look very much like hardware circuits (permutations and such) [2].

I am happy to discuss this in person if it might be helpful to your work. Both Mangpo (the author of [2,3]) and I will be at the conference.

[1] https://ieeexplore.ieee.org/document/5227085

[2] https://github.com/mangpo/swizzle-inventor

[3] https://github.com/mangpo/mangpo.github.io/blob/master/paper...,

25 days ago [-]
AthLado 25 days ago [-]
This is very interesting - my eyes stuck on the programming for non-programmers as we in MOOCTORS (https://www.mooctors.com) we are building a tutoring platform for MOOC students who are not necessarily programming experts. We invite technology experts and everyone who can code to register as tutors on their free time, help students on their MOOC courses, and earn an extra income for doing that. How Synthesis could power tech/coding tutoring?

best, Athanasios

rbodik 25 days ago [-]
Hi Athanasios, program synthesis has been used to automatically repair introductory programming assignments (a sample of papers is at the end). This technology could make tutors more productive: [1] says that 81% of synthesized repairs were of high quality. This is very impressive but the tutor is still needed to check the quality. Also, synthesis cannot repair all programs (an empty submission cannot be repaired). Finally, this automatic repair allows the tutor to focus on giving guidance, rather than on finding the bug in a programming assignment.

[1] https://arxiv.org/pdf/1603.03165.pdf [2] https://rishabhmit.bitbucket.io/papers/icse18.pdf

rbodik 25 days ago [-]
I should add that Rishabh Singh, one of the lead authors of of the repair papers, will speak at the conference.
rishabhs 25 days ago [-]
Thanks Ras for the above pointers! I also wanted to add that there is a demo of the system with different levels of feedback mechanism hosted here: http://sketch2.csail.mit.edu/python-autofeedback/new-encodin...

It uses constraint-based synthesis to search for small repairs. We also did some follow up work on learning from other student's solutions to learn to correct similar mistakes: https://rishabhmit.bitbucket.io/papers/sarfgen_pldi18.pdf https://rishabhmit.bitbucket.io/papers/dyn_iclr18.pdf