Re: [其他] 確定性的失落？創造性的無限？(上)

看板Math作者Bugquan (靠近邊緣)時間1月前 (2025/11/07 09:47)推噓0(0推 0噓 18→)

留言18則, 3人參與討論串3/3 (看更多)

※ 引述《Bugquan (靠近邊緣)》之銘言： : 推 LPH66 : 話說回來, 我看到有一篇論文是他們用 ChatGPT 產生 11/06 20:35 : → LPH66 : 了 Lean 程式碼並且成功編過了, 這種應該算是生成式 11/06 20:36 : → LPH66 : AI 的一種意外應用方式吧 (Lean 程式碼能編過表示 11/06 20:36 : → LPH66 : 邏輯推理是通的) 11/06 20:36 : → LPH66 : 這篇論文的作者有說他們在這之前不會 Lean 11/07 08:52 https://xenaproject.wordpress.com/2025/10/22/formal-or-not-formal-that-is-the-qu estion-in-ai-for-theorem-proving/ 根據 Kevin Buzzard（倫敦帝國學院教授，https://reurl.cc/LQ0Ddx）的觀點，我們來探討 AI 證明數學猜想時的核心問題。小知識：關於 Kevin Buzzard 這位數學家正帶領團隊，試圖利用 Lean 形式化證明費馬最後定理。他甚至邀請到他的指導教授 Richard Taylor（費馬最後定理證明關鍵貢獻者之一）來協助制定一套現代化且更具可行性的形式化藍圖。 (參考：https://imperialcollegelondon.github.io/FLT/blueprint/) Kevin Buzzard 在文章中指出，AI 證明數學時面臨兩大挑戰： 1. AI 的「幻覺」與證明可靠性問題核心：像大型語言模型（LLM）這樣的 AI 存在「幻覺」（Hallucination）問題。在數學證明中，只要證明過程出現一個幻覺，就足以完全破壞整個數學論證的有效性。形式化的作用與局限：如果我們要求 AI 在提供證明的同時，也以 Lean 形式化語言呈現，是否就能高枕無憂？答案是否定的。雖然 Lean 可以以超人類水平校驗邏輯步驟，但人類仍然需要仔細檢查：定理的陳述和證明的過程是否被正確地翻譯成了 Lean 語言。確保「人類想證明的」與「Lean 實際檢查的」是同一件事，是至關重要的環節。 2. AI 配合 Lean 的發展瓶頸問題核心： AI 與 Lean 混合系統能走多遠？ Buzzard 的觀點：他認為目前的瓶頸在於，即便是最好的形式化數學函式庫（如 Lean 的 mathlib），仍不具備理解大多數現代研究級數學所需的「定義」。範例：目前的定理證明器尚不了解（或缺乏足夠形式化定義）這些複雜但又極其重要和常用的數學對象，例如： Tate-Shafarevich 群 Calabi-Yau 簇代數疊 (algebraic stacks) 自守表示 (automorphic representations) 因此，在 AI 能夠真正協助進行研究級數學證明之前，仍需要人類研究人員投入時間，為 L ean 等證明器提供和形式化這些現代數學的基礎定義。 -- ※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 27.53.161.22 (臺灣) ※ 文章網址: https://www.ptt.cc/bbs/Math/M.1762480024.A.346.html

→

xcycl

11/09 21:21, 1月前 , 1^F

11/09 21:21, 1^F

→

xcycl

11/09 21:22, 1月前 , 2^F

11/09 21:22, 2^F

→

xcycl

11/09 21:24, 1月前 , 3^F

11/09 21:24, 3^F