Síntesis de programas
Inducir programas a partir de ejemplos
Dale a la máquina ejemplos de entrada/salida y deja que invente el programa. Flash Fill lo hizo cotidiano en las hojas de cálculo.
Intuición
Un DSL pequeño (concatenar, extraer dígitos, mayúsculas…) define el espacio de programas.
La búsqueda (enumeración, versión space, neuro-guiada) encuentra un programa consistente con los IO.
El laboratorio inventa transformaciones de strings a partir de ejemplos.
Mecanismo
FlashFill (Gulwani): DSL de strings + síntesis por versión.
Neural-guided: un modelo propone candidatos; se verifican.
Program synthesis ∩ LLMs: Codex, AlphaCode, verification loops.
Laboratorio
Flash Fill de juguete
Da ejemplos IO de strings; el sintetizador busca en un DSL (extraer, concatenar, mayúsculas) un programa consistente.
Historia
- 1971
Summers y la síntesis inductiva temprana.
Summers (1977)
- 2011
FlashFill en Excel.
Gulwani (2011), POPL
- 2017
DeepCoder: guía neural de búsqueda.
Balog et al.
- 2022
AlphaCode compite en Codeforces.
Li et al., Science
Límites
El DSL acota lo expresable.
Ambigüedad: muchos programas caben en pocos ejemplos.
Verificar corrección general es indecidible.
¿Programar es especificar o ejemplificar?
Flash Fill apuesta por el ejemplo. Los tipos y contratos, por la especificación.
¿Qué entiende un modelo que escribe código que pasa los tests?