Experiencias de Generación de Pruebas Formales con LLMs

▶︎ Tema: Experiencias de Generación de Pruebas Formales con LLMsEn los últimos años, la IA/LLM se ha desarrollado rápidamente, capaz de generar no solo texto e imágenes sino también código estable. Hace unos meses, modelos de vanguardia como GPT 5.4 y Claude Opus 4.6 comenzaron a generar pruebas matemáticas formales relativamente complejas, incluso para la corrección compleja de transformaciones de representación intermedia de compiladores, simplemente proporcionando una "plantilla" de prueba similar para producir pruebas formales redactadas correspondientemente.Esta charla explorará la experiencia de usar la serie GPT 5 y Agda para escribir programas de tipos dependientes y pruebas de teoremas formales, demostrando cómo los modelos de lenguaje, a través de las garantías de los probadores de teoremas, generan pruebas matemáticamente sólidas de corrección que son casi perfectas.▶︎ Presentador: Chen Liang-Ting, investigador asistente en la Academia Sinica, disfruta probar varias cosas nuevas. Sus intereses recientes incluyen teoría de tipos, modelos categóricos y pruebas con significado computacional.*¡Esta vez el evento comienza más temprano! ¡Comienza a las siete en punto!----------------La entrada es gratuita y se aceptan donaciones para el lugar g0v. Simplemente entra.¡Eres bienvenido a venir para交流、交朋友！