Опыт генерации формальных доказательств с помощью LLM

▶︎ Тема: Опыт генерации формальных доказательств с помощью LLMВ последние годы ИИ/LLM развивались стремительно, способные генерировать не только тексты и изображения, но и стабильный код. Несколько месяцев назад передовые модели, такие как GPT 5.4 и Claude Opus 4.6, начали генерировать относительно сложные формальные математические доказательства, даже для сложной правильности преобразований промежуточного представления компилятора, просто предоставив аналогичный "шаблон" доказательства для получения соответствующим образом сформулированных формальных доказательств.В этой лекции будет рассмотрен опыт использования серии GPT 5 и Agda для написания программ с зависимыми типами и формальных доказательств теорем, демонстрируя, как языковые модели, через гарантии доказателей теорем, генерируют математически обоснованные доказательства правильности, которые почти безупречны.▶︎ Докладчик: Чен Лянг-Тин, научный сотрудник Академии Синика, любит пробовать различные новшества. Его недавние интересы включают теорию типов, категориальные модели и доказательства с вычислительной значимостью.*На этот раз мероприятие начинается раньше! Оно начнется в семь часов!----------------Вход свободный, пожертвования на площадку g0v приветствуются. Просто заходите.Добро пожаловать для交流、交朋友！