用 LLM 生成形式證明經驗談

▶︎ 主題：用 LLM 生成形式證明經驗談

近年來 AI/LLM 發展迅速，不僅能生成文字和圖片，還能穩定生成程式碼。幾個月前，GPT 5.4 和 Claude Opus 4.6 等前沿模型開始能生成相對複雜的形式化數學證明，甚至複雜如編譯器中介表示轉換的正確性，只需提供類似的證明「範本」即可生成相近敘述的形式證明。

本次分享將探討使用 GPT 5 系列與 Agda 撰寫依值型別程式和形式定理證明的經驗，並說明語言模型如何透過定理證明器的保證，生成正確性近乎無懈可擊的數學證明。

▶︎ 分享者：陳亮廷
在中央研究院擔任助理研究員，喜歡嘗試各種新事物。最近的興趣是型別論、範疇模型，還有具備計算意義的證明。

*這次時間有提早喔！七點開講！

活動免費，隨喜樂捐給場地 g0v
直接推門進來就可以。

歡迎來交流、交朋友！