Experiências de Geração de Provas Formais com LLMs

▶︎ Tópico: Experiências de Geração de Provas Formais com LLMsNos últimos anos, a IA/LLM se desenvolveu rapidamente, capaz de gerar não apenas texto e imagens, mas também código estável. Há alguns meses, modelos de ponta como GPT 5.4 e Claude Opus 4.6 começaram a gerar provas matemáticas formais relativamente complexas, mesmo para a complexidade da correção de transformações de representação intermediária de compiladores, simplesmente fornecendo um "template" de prova semelhante para produzir provas formais correspondentemente formuladas.Esta apresentação explorará a experiência de usar a série GPT 5 e Agda para escrever programas de tipos dependentes e provas de teoremas formais, demonstrando como modelos de linguagem, através das garantias dos provadores de teoremas, geram provas matematicamente sólidas de correção que são quase impecáveis.▶︎ Apresentador: Chen Liang-Ting, um pesquisador assistente na Academia Sinica, que gosta de experimentar várias coisas novas. Seus interesses recentes incluem teoria dos tipos, modelos categóricos e provas com significância computacional.*Desta vez, o evento começa mais cedo! Começa às sete horas!----------------O evento é gratuito e doações para o local g0v são bem-vindas. É só entrar.Você é bem-vindo para vir para交流、交朋友！