10 月 6 日OpenAI 在 GitHub 上一次性公開了 722 篇數(shù)學(xué)手稿聲稱在幾何、代數(shù)、計(jì)算機(jī)科學(xué)等方向的 372 個(gè)問題上取得進(jìn)展。第二天撤回 3 篇一個(gè)符號(hào)錯(cuò)誤讓其中一篇的論證失效另外兩篇依賴了同一個(gè)構(gòu)造一并作廢同時(shí)修訂 14 篇還改了一處過時(shí)引用。手稿總數(shù)從 722 變成 719。這批東西沒走同行評(píng)審也沒發(fā)在 arXiv而是直接傳到自家倉庫。據(jù) OpenAI 方面對(duì)媒體的說法錯(cuò)誤是內(nèi)部審計(jì)時(shí)發(fā)現(xiàn)的約一半結(jié)果在發(fā)布時(shí)并未經(jīng)過確認(rèn)合作方 AGMAI 的建議是不必等完全形式化再發(fā)。10 月下旬陶哲軒和鄧煜在一場對(duì)談里把這類產(chǎn)出稱作有毒廢料——這話針對(duì)的不是 AI 會(huì)不會(huì)做數(shù)學(xué)而是把解數(shù)學(xué)題當(dāng)基準(zhǔn)測試這種做法。技術(shù)上看變的是發(fā)布方式AI 能不能做數(shù)學(xué)兩位數(shù)學(xué)家都沒否認(rèn)甚至看好它在真正的研究里加速。爭的是產(chǎn)出和驗(yàn)證之間的順序被調(diào)換了。以前的路子是人有想法AI 補(bǔ)細(xì)節(jié)寫完自己核一遍?，F(xiàn)在的路子是AI 批量生成人來做驗(yàn)收。據(jù)報(bào)道這批手稿來自約 4000 次會(huì)話產(chǎn)出 722 篇成功率不到兩成——這個(gè)比例本身不算丟人問題是剩下那八成里有多少被當(dāng)成結(jié)論發(fā)了出來。生產(chǎn)端的邊際成本接近零驗(yàn)證端的成本一點(diǎn)沒降。甚至更高讀一份沒有思維鏈、引用不透明、符號(hào)還可能有錯(cuò)的證明比自己做一遍更累。鄧煜提的兩條邊界說的就是這個(gè)——過去有證明的問題和人類理解的問題是同一條線現(xiàn)在中間裂開了一條有證明但只有 AI 知道人不懂。這跟寫業(yè)務(wù)代碼是一回事看著離得很遠(yuǎn)其實(shí)是同一個(gè)結(jié)構(gòu)。AI 生成代碼的成本已經(jīng)很低低到不少團(tuán)隊(duì)開始用每天合入多少 PR衡量效能。但驗(yàn)證成本沒變code review 要人看測試要人寫線上出事要人背。產(chǎn)出量一旦成了 KPI被壓縮的一定是驗(yàn)證環(huán)節(jié)。表現(xiàn)是 review 從逐行看變成掃一眼 CI 綠了就過測試從覆蓋邊界變成跑通主流程。賬不會(huì)消失只是從開發(fā)階段挪到了故障復(fù)盤會(huì)上。Lean 這類形式化工具本來是條出路——證明可以機(jī)器校驗(yàn)不依賴人的耐心。但據(jù)報(bào)道這批手稿里大量文字證明和 Lean 代碼之間存在斷層形式化覆蓋并不完整。工具在覆蓋率不夠約等于沒有。三個(gè)能落地的做法一、把驗(yàn)證做成流水線別指望自覺。類型檢查、lint、單測、集成測試該卡的卡住。人一定會(huì)偷懶機(jī)器不會(huì)。二、獨(dú)立復(fù)算別讓模型自證。讓生成答案的同一個(gè)模型去檢查答案等于讓它給自己判卷。能用確定性方法驗(yàn)的就別用概率方法驗(yàn)。比如下面這段fromfractionsimportFractiondefcheck(n_max50):用精確有理數(shù)復(fù)算 sum(k^3) (n(n1)/2)^2返回第一個(gè)反例。forninrange(1,n_max1):lhssum(Fraction(k)**3forkinrange(1,n1))rhsFraction(n*(n1),2)**2iflhs!rhs:returnn,lhs,rhsreturnNoneprint(check(200))# None表示 1..200 全部成立跑 1 到 200 返回 None全部通過。這不是證明只是低成本證偽——但對(duì) AI 產(chǎn)出來說絕大多數(shù)錯(cuò)誤死在這一步就夠了。這里用 Fraction 而不是 float因?yàn)楦↑c(diǎn)誤差既會(huì)制造假陰性也會(huì)掩蓋真問題。三、留痕。記錄 prompt、模型版本、生成時(shí)間、人工改動(dòng)。出問題時(shí)這段到底是誰寫的、怎么來的必須有答案。AI 不會(huì)背鍋簽字的那個(gè)人會(huì)。幾個(gè)坑LLM 自評(píng)不可靠。讓模型輸出我已仔細(xì)檢查沒有任何信息量它對(duì)自己的錯(cuò)誤沒有感知能力語氣卻一樣篤定。形式化驗(yàn)證有成本。寫 Lean 比寫自然語言證明慢得多只值得用在高價(jià)值、高風(fēng)險(xiǎn)的斷言上全量上不現(xiàn)實(shí)?？雌饋韺?duì)是最危險(xiǎn)的信號(hào)。符號(hào)錯(cuò)誤、量詞順序、隱含假設(shè)這些地方 AI 出錯(cuò)時(shí)讀起來依然通順而人讀的時(shí)候會(huì)自動(dòng)腦補(bǔ)缺失的一步。最后陶哲軒在那場對(duì)談里用了個(gè)開車的比喻車確實(shí)比走路快但不是所有原本走路的路都該換成開車——有時(shí)候你就是想走一走。放到工程上也成立。生成成本趨近于零之后稀缺的東西不再是產(chǎn)出而是誰來驗(yàn)、驗(yàn)到什么程度、驗(yàn)不出來的時(shí)候敢不敢說不。你怎么看評(píng)論區(qū)聊聊。