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