The overarching goal of the DELPHI project is to simplify the development of correct and reliable software. Existing methodologies require significant human expertise, such as in the design of appropriate abstract domains and environment models, or suffer from significant barriers to adoption, such as limited scalability and flexibility. This project is leveraging data-driven and learning-based approaches to verify existing programs or synthesize new programs automatically from high-level human intent.
In this context, the project aims to develop end-to-end learning frameworks for program reasoning tasks such as verification and synthesis. The two key observations underlying the DELPHI system are: 1) deep learning provides a powerful mechanism to automatically learn program features which previously required tedious human engineering; and 2) reinforcement learning overcomes the challenges of limited or no training data, and enables the discovery of transferable policies that are usually better than manually crafted heuristics.
On the other hand, this research also raises fundamental challenges for deep learning and reinforcement learning: first, concerning good representations for highly structured data like programs, and second, regarding ways to combine neural inference and complex symbolic reasoning required by tasks such as program verification and program synthesis. The DELPHI project is exploring the use of graph embeddings and continuous reward mechanisms to address these challenges.
Collaborators:
- Mayur Naik (Penn)
- Le Song (Georgia Tech)
Funding:
- DARPA, NSF, Facebook
Students and Postdocs:
- Xujie Si (Penn)
- Hanjun Dai (Georgia Tech)
- Mukund Raghothaman (Penn)
