Data Science Seminars

Correct-by-Construction Program Synthesis using Type Theory and Evolutionary Computation

Sala 6.3.27, Ciências ULisboa

Por Alcides Fonseca (LASIGE/DI-FCUL).

Program Synthesis (PS) consists in automatically deriving a program from a specification, examples or both. Large Language Models (like CoPilot and GPTs) have improved the state of the art in PS, but they have several limitations. In particular, they provide no guarantee that the program is correct, or even compiles. Simple Type Systems (like Java's) guarantee that you cannot use an integer where a string is expected. More complex type systems (Affine Types, Liquid Types, Dependent Types) can provide more interesting guarantees: a file handle is always closed, you do not mix training and testing data, etc..

In this talk, we will cover how type systems can be used together with evolutionary techniques (Simulated Annealing, Genetic Programming) to explore large spaces of candidate programs, aiming to find one that maximizes or minimizes some properties. These can be correctness properties (my pipeline does not shuffle time-series training data), or non-functional properties (I want to minimize the time or energy consumption of my pipeline).

Short bio: Alcides Fonseca is an Associate Professor at FCUL, where he conducts research on the intersection of Machine Learning, Programming Languages and Software Engineering. He has led the Resource-Aware Programming project, which developed techniques to be used to understand the energy consumption of programs, and the CAMELOT project at FCUL, where we developed techniques to create machine learning models that respect the constraints on real-world data. He also blogs regularly at http://alcidesfonseca.com/.

14h30
Departamento de Informática | Ciências ULisboa