Scalable
Neo outperforms state-of-the-art synthesizers in PL (i.e., Morpheus) and ML (i.e., DeepCoder).
Neo is a novel synthesis framework based on the idea of conflict-driven learning. Given a spurious partial program that violates the specification, the idea is to infer a lemma that can be used to prevent similar mistakes in the future. Our synthesis algorithm infers these lemmas by identifying DSL constructs that are equivalent modulo conflict, meaning that replacing one component with the other results in an another infeasible program.
Neo outperforms state-of-the-art synthesizers in PL (i.e., Morpheus) and ML (i.e., DeepCoder).
Neo can synthesize most tasks in a few seconds.
Neo can solve problems from different domains and supports arbitrary DSLs.
For technical details see our PLDI'18 publication: Program Synthesis using Conflict-Driven Learning. Yu Feng, Ruben Martins, Osbert Bastani, and Isil Dillig.
Neo was developed by the UToPiA research group lead by Isil Dillig at UT Austin.
Neo is maintained by Ruben Martins at CMU and Yu Feng at UT Austin.