Profesor | Armando Solar Lezama | lu mi vi | 13 a 14 | 105 (Yelizcalli) |
Ayudante | ma ju | 13 a 14 | ||
Ayud. Lab. |
Este curso provee una introducción a la síntesis de programas, un nuevo campo de estudio en la intersección de lenguajes de programación, métodos formales e inteligencia artificial.
El curso estará dividido en cinco unidades:
• Inductive synthesis: Esta unidad se enfoca en técnicas para generar programas cuyo comportamiento se define a base de ejemplos. En esta unidad se describirán diferentes mecanismos para representar espacios de posibles programas, así como mecanismos de búsqueda eficientes y mecanismos de ranking.
• Functional synthesis: Esta unidad cubrirá técnicas para sintetizar funciones que satisfacen especificaciones formales. En esta unidad se cubrirán algunos mecanismos de verificación, así como técnicas de síntesis por deducción.
• Quantitative synthesis: En esta unidad se cubrirán técnicas para sintetizar funciones bajo objetivos cuantitativos o probabilísticos. También se explorarán técnicas basadas en aprendizaje de máquinas y "Deep learning" para aprender distribuciones de programas que se pueden utilizar como parte del proceso de síntesis.
Requisitos: El curso asume una base solida en Matematicas Discretas y Algoritmos, pero el resto del materiál necesario se cubrirá como parte del curso.
El curso se calificará en base a tres ejercicios individuales y un proyecto final en equipo:
Tarea 1: 20%
Tarea 2: 20%
Tarea 3: 20%
Proyecto final: 40%