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

看板Math作者 (靠近邊緣)時間1月前 (2025/11/06 11:24), 編輯推噓7(7推 0噓 25→)
留言32則, 4人參與, 3周前最新討論串2/3 (看更多)
※ 引述 《ginstein (邁向學術之路)》 之銘言： : 　 : 本文為前沿數學探索，是數普文非學術文、非公認理論， : 　 : 盼能促進 AI 數學家早日到來。 : 　 現在當然有的數學家引入AI 像是Terence Tao自己就玩的不亦樂乎，還有Timothy Gowers也是 偶爾會分享自己用AI 搞定了什麼 但是最大的問題是，你看這倆菲爾茲獎得主，AI的證明有沒有了唬爛或是跳步之類的 他們兩個稍微排查很快就能得出結果了 但是對於其他人門檻不夠的，最多只能當為輔助工具來用 主要步驟還是得靠自己，不然有時候被AI騙了都不知道 -- ※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 106.64.112.48 (臺灣) ※ 文章網址: https://www.ptt.cc/bbs/Math/M.1762399478.A.967.html
→
11/06 14:27, 1月前 , 1F
AI不斷快速嘗試各種思路，然後可以自己初步排除掉
11/06 14:27, 1F
→
11/06 14:27, 1月前 , 2F
一些明顯錯誤的，剩下的candidate再給數學家去檢查
11/06 14:27, 2F
→
11/06 14:27, 1月前 , 3F
。問題是AI提供的解答中黃金：垃圾的比率是否足夠
11/06 14:27, 3F
→
11/06 14:27, 1月前 , 4F
高，如果垃圾比率太高也是形同浪費數學家檢查的時
11/06 14:27, 4F
→
11/06 14:27, 1月前 , 5F
間。
11/06 14:27, 5F
推
11/06 20:35, 1月前 , 6F
話說回來, 我看到有一篇論文是他們用 ChatGPT 產生
11/06 20:35, 6F
→
11/06 20:36, 1月前 , 7F
了 Lean 程式碼並且成功編過了, 這種應該算是生成式
11/06 20:36, 7F
→
11/06 20:36, 1月前 , 8F
AI 的一種意外應用方式吧 (Lean 程式碼能編過表示
11/06 20:36, 8F
→
11/06 20:36, 1月前 , 9F
邏輯推理是通的)
11/06 20:36, 9F
→
11/06 20:38, 1月前 , 10F
這是那篇論文, 做的是 Erdos 曾經懸賞一千元的猜想
11/06 20:38, 10F
→
11/06 20:39, 1月前 , 11F
11/06 20:39, 11F
推
11/06 22:13, 1月前 , 12F
謝謝L大分享的論文
11/06 22:13, 12F
推
11/07 06:54, 1月前 , 13F
LLM靠的還是機率吧，能編過不代表邏輯是通的（回L大
11/07 06:54, 13F
→
11/07 06:54, 1月前 , 14F
），至於機率是否能產生邏輯，見人見智，但有些人認
11/07 06:54, 14F
→
11/07 06:54, 1月前 , 15F
為無法，所以AI可能還需要基本架構的革新
11/07 06:54, 15F
→
11/07 07:44, 1月前 , 16F
編譯過，只代表compile 會過，不代表執行結果正確或
11/07 07:44, 16F
→
11/07 07:44, 1月前 , 17F
邏輯通
11/07 07:44, 17F
推
11/07 08:50, 1月前 , 18F
那是其他程式語言, 但這篇論文用的是專門用於證明的
11/07 08:50, 18F
→
11/07 08:50, 1月前 , 19F
Lean, 就我所知 Lean 程式編過就表示邏輯推論是通的
11/07 08:50, 19F
→
11/07 08:52, 1月前 , 20F
這篇論文的作者有說他們在這之前不會 Lean
11/07 08:52, 20F
→
11/07 08:54, 1月前 , 21F
但經 ChatGPT 的輔助他們能夠將整篇論文的多數結果
11/07 08:54, 21F
→
11/07 08:54, 1月前 , 22F
(特別是主要定理) 全部都用 Lean 驗證過
11/07 08:54, 22F
推
11/07 13:48, 1月前 , 23F
回樓上，受教了，謝謝。
11/07 13:48, 23F
→
11/07 14:00, 1月前 , 24F
11/07 14:00, 24F
→
11/11 07:14, 4周前 , 25F
LLM很擅長翻譯，把論文的定理轉化成Lean再去檢查推
11/11 07:14, 25F
→
11/11 07:14, 4周前 , 26F
論是否通過應該辦得到，不過如果使用的數學家本身
11/11 07:14, 26F
→
11/11 07:14, 4周前 , 27F
也不是很熟悉Lean，有沒有可能在LLM輔助下寫出的Le
11/11 07:14, 27F
→
11/11 07:14, 4周前 , 28F
an跟本來要證的定理其實是不等價的
11/11 07:14, 28F
推
11/12 22:58, 3周前 , 29F
原論文也有討論到這個問題, 但恰巧他們這個問題
11/12 22:58, 29F
→
11/12 22:59, 3周前 , 30F
比較著名 (Erdos 懸賞過的問題) 有其他人已經做好了
11/12 22:59, 30F
→
11/12 22:59, 3周前 , 31F
這種「翻譯」
11/12 22:59, 31F
推
11/18 09:12, 3周前 , 32F
創作不易，感謝回文評論！
11/18 09:12, 32F
‣ 更多 Bugquan 的文章
文章代碼(AID): #1f31Jsbd (Math)
‣ 更多 Bugquan 的文章
文章代碼(AID): #1f31Jsbd (Math)