#math
2026-08-10
chewei 哲瑋 _
[協助轉貼] 8/13 週四晚上 F4: <#C09ACNRUES1> 社群活動
▶︎ 主題：用 LLM 生成形式證明經驗談
• 近年來 AI/LLM 發展迅速，不僅能生成文字和圖片，還能穩定生成程式碼。幾個月前，GPT 5.4 和 Claude Opus 4.6 等前沿模型開始能生成相對複雜的形式化數學證明，甚至複雜如編譯器中介表示轉換的正確性，只需提供類似的證明「範本」即可生成相近敘述的形式證明。
• 本次分享將探討使用 GPT 5 系列與 Agda 撰寫依值型別程式和形式定理證明的經驗，並說明語言模型如何透過定理證明器的保證，生成正確性近乎無懈可擊的數學證明。
▶︎ 分享者：陳亮廷
• 在中央研究院擔任助理研究員，喜歡嘗試各種新事物。最近的興趣是型別論、範疇模型，還有具備計算意義的證明。
facebook.com/groups/functioanl.thursday/posts/4447561422225517
[協助轉貼] 8/13 週四晚上 F4: <#C09ACNRUES1> 社群活動
▶︎ 主題：用 LLM 生成形式證明經驗談
• 近年來 AI/LLM 發展迅速，不僅能生成文字和圖片，還能穩定生成程式碼。幾個月前，GPT 5.4 和 Claude Opus 4.6 等前沿模型開始能生成相對複雜的形式化數學證明，甚至複雜如編譯器中介表示轉換的正確性，只需提供類似的證明「範本」即可生成相近敘述的形式證明。
• 本次分享將探討使用 GPT 5 系列與 Agda 撰寫依值型別程式和形式定理證明的經驗，並說明語言模型如何透過定理證明器的保證，生成正確性近乎無懈可擊的數學證明。
▶︎ 分享者：陳亮廷
• 在中央研究院擔任助理研究員，喜歡嘗試各種新事物。最近的興趣是型別論、範疇模型，還有具備計算意義的證明。
facebook.com/groups/functioanl.thursday/posts/4447561422225517