圖源：Terence Tao|AMS Notice

作者：陶哲軒（加州大學(xué)洛杉磯分校數(shù)學(xué)教授）AMS Notice 202501

譯者：zzllrr小樂（數(shù)學(xué)科普公眾號(hào)）2024-12-25

幾個(gè)世紀(jì)以來，數(shù)學(xué)家一直依靠計(jì)算機(jī)（人類、機(jī)械或電子）和機(jī)器來協(xié)助他們的研究（如果考慮到算盤等早期計(jì)算工具，甚至幾千年）。例如，自從納皮爾（John Napier，1550 - 1617）等人的早期對(duì)數(shù)表以來，數(shù)學(xué)家就知道構(gòu)建數(shù)學(xué)對(duì)象的大型數(shù)據(jù)集來執(zhí)行計(jì)算和做出猜想的價(jià)值。勒讓德（Adrien-Marie Legendre，1752 - 1833）和高斯（Carl Friedrich Gauss，1777 - 1855）使用人類計(jì)算機(jī)編制的大素?cái)?shù)表來猜想現(xiàn)在所謂的素?cái)?shù)定理（PNT）；一個(gè)半世紀(jì)后，伯奇（Bryan John Birch，1931 -）和斯溫納頓-戴爾（Peter Swinnerton-Dyer，1927 - 2018）同樣使用早期電子計(jì)算機(jī)生成有限域上橢圓曲線的足夠數(shù)據(jù)，以提出他們自己對(duì)這些對(duì)象的著名猜想（即BSD猜想）。毫無疑問，許多讀者已經(jīng)利用了最廣泛的數(shù)學(xué)數(shù)據(jù)集之一——整數(shù)數(shù)列在線百科全書（OEIS），它產(chǎn)生了無數(shù)猜想以及在不同數(shù)學(xué)領(lǐng)域之間意想不到的聯(lián)系，并為研究人員提供了一個(gè)有價(jià)值的數(shù)學(xué)對(duì)象的文獻(xiàn)搜索引擎。他們不知道該數(shù)學(xué)對(duì)象的名稱，但可以將其與整數(shù)序列相關(guān)聯(lián)。在21世紀(jì)，此類大型數(shù)據(jù)庫還可以作為機(jī)器學(xué)習(xí)算法的關(guān)鍵訓(xùn)練數(shù)據(jù)，這些算法有望實(shí)現(xiàn)自動(dòng)化或者至少大大簡化數(shù)學(xué)猜想和聯(lián)系的生成過程。

除了數(shù)據(jù)生成之外，計(jì)算機(jī)的另一個(gè)重要用途是科學(xué)計(jì)算，如今科學(xué)計(jì)算被大量用于數(shù)值求解微分方程和動(dòng)力系統(tǒng)，或計(jì)算大型矩陣或線性算子的統(tǒng)計(jì)數(shù)據(jù)。這種計(jì)算的早期例子出現(xiàn)在1920年代，當(dāng)時(shí)亨德里克·洛倫茲（Hendrik Lorentz，1853 - 1928）組建了一組人類計(jì)算機(jī)來模擬阿夫魯戴克大壩（Afsluitdijk，當(dāng)時(shí)荷蘭正在建設(shè)的一座水壩）周圍的流體流動(dòng)；除其他外，該計(jì)算因開創(chuàng)了現(xiàn)在標(biāo)準(zhǔn)的浮點(diǎn)運(yùn)算裝置而聞名。但現(xiàn)代計(jì)算機(jī)代數(shù)系統(tǒng)（CAS，例如Magma、SAGEMath、Mathematica、Maple等）以及更通用的編程語言可以遠(yuǎn)遠(yuǎn)超出傳統(tǒng)的“數(shù)字運(yùn)算”；它們現(xiàn)在通常用于執(zhí)行代數(shù)、分析、幾何、數(shù)論和許多其他數(shù)學(xué)分支中的符號(hào)計(jì)算。由于舍入誤差和不穩(wěn)定性，某些形式的科學(xué)計(jì)算是眾所周知的不可靠，但人們通?？梢杂酶鼑?yán)格的方法來代替這些方法（例如，用區(qū)間算術(shù)代替浮點(diǎn)算術(shù)），這可能會(huì)增加運(yùn)行時(shí)間或內(nèi)存使用量。

計(jì)算機(jī)代數(shù)系統(tǒng)的近親是可滿足性（SAT，satisfiability）求解器和可滿足性模理論 (SMT，satisfiability modulo theory) 求解器，它們可以根據(jù)某些受限制的假設(shè)集合對(duì)結(jié)論進(jìn)行復(fù)雜的邏輯推導(dǎo)，并為每個(gè)此類推導(dǎo)生成證明證書。當(dāng)然，可滿足性是一個(gè) NP完全問題，因此這些求解器的規(guī)模不會(huì)超過某個(gè)臨界點(diǎn)。以下是使用SAT求解器證明結(jié)果的典型示例：

定理 0.1 （布爾勾股數(shù)三元組定理【HKM16】）

集合{1, ? ,7824}的元素可以分為兩類，使得每一類中都不包含勾股數(shù)三元組——滿足a2+b2=c2的(a,b,c)；然而，對(duì)于集合{1, ? ,7825}這是不可能的。

該證明需要4個(gè)CPU年的計(jì)算并生成200TB的命題證明，后來被壓縮到68GB。

當(dāng)然，數(shù)學(xué)家也經(jīng)常使用計(jì)算機(jī)來完成日常任務(wù)，例如撰寫論文以及與合作者交流。但近幾十年來，出現(xiàn)了幾種利用計(jì)算機(jī)輔助數(shù)學(xué)研究的有前途的新方法：

• 機(jī)器學(xué)習(xí)算法可用于發(fā)現(xiàn)新的數(shù)學(xué)關(guān)系，或生成數(shù)學(xué)問題的潛在示例或反例。

• 形式證明助手可用于驗(yàn)證證明（以及大語言模型的輸出），允許真正大規(guī)模的數(shù)學(xué)協(xié)作，并幫助構(gòu)建數(shù)據(jù)集來訓(xùn)練上述機(jī)器學(xué)習(xí)算法。

• ChatGPT等大語言模型（有可能）被用來使其他工具更容易、更快速地使用；它們還可以建議證明策略或相關(guān)工作，甚至直接生成（簡單的）證明。

這些類型的工具中的每一種都已經(jīng)在不同的數(shù)學(xué)領(lǐng)域找到了合適的應(yīng)用，但我發(fā)現(xiàn)特別有趣的是將這些工具組合在一起的可能性，用一種工具抵消另一種工具的弱點(diǎn)。例如，形式證明助手和計(jì)算機(jī)代數(shù)包可以過濾掉現(xiàn)在臭名昭著的大語言模型看似合理的廢話的“幻覺”傾向，而反之，這些模型可以幫助自動(dòng)化證明形式化中更繁瑣的方面，并提供用于運(yùn)行復(fù)雜符號(hào)或機(jī)器學(xué)習(xí)算法的自然語言界面。其中許多組合仍僅處于概念驗(yàn)證開發(fā)階段，該技術(shù)需要一定的時(shí)間才能變得成熟起來成為數(shù)學(xué)家真正有用且可靠的工具。然而，早期的實(shí)驗(yàn)似乎確實(shí)令人鼓舞，我們應(yīng)該期待在不久的將來會(huì)出現(xiàn)一些令人驚訝的新數(shù)學(xué)研究模式的演示；它不是科幻小說中可以自主解決復(fù)雜數(shù)學(xué)問題的超級(jí)智能人工智能，而是一個(gè)有價(jià)值的助手，可以提出新想法、過濾錯(cuò)誤、執(zhí)行例行案例檢查、數(shù)值實(shí)驗(yàn)和文獻(xiàn)評(píng)審任務(wù)，讓人類數(shù)學(xué)家能夠在項(xiàng)目中注重對(duì)高層概念的探索。

1. 證明助手

當(dāng)然，計(jì)算是使用計(jì)算機(jī)執(zhí)行的這一事實(shí)并不能自動(dòng)保證其正確。計(jì)算可能會(huì)產(chǎn)生數(shù)值誤差，例如由于用離散近似值替換連續(xù)變量或方程而引起的誤差。代碼中可能會(huì)無意中引入錯(cuò)誤，或者輸入數(shù)據(jù)本身可能包含不準(zhǔn)確之處。即使計(jì)算機(jī)用來運(yùn)行代碼的編譯器也可能存在缺陷。最后，即使代碼完美執(zhí)行，代碼正確計(jì)算的表達(dá)式也可能不是數(shù)學(xué)論證真正想要的表達(dá)式。

早期的計(jì)算機(jī)輔助證明遇到了許多這樣的問題。例如，凱尼斯·阿佩爾（Kenneth Appel，1932 - 2013）和沃夫?qū)す希╓olfgang Haken，1928 - 2022）在1976年對(duì)四色定理【AH89】的原始證明圍繞著一系列1834個(gè)需要遵守兩個(gè)性質(zhì)稱為“可歸約性”（reducibility）和“不可避免性”（unavoidability）的圖?？梢酝ㄟ^每次將每個(gè)圖輸入一個(gè)定制的軟件來檢查可歸約性；但不可避免的是，需要進(jìn)行繁瑣的計(jì)算，包括數(shù)百頁的縮微膠片——通過哈肯的女兒Dorothea Blostein（多蘿西婭·布洛斯坦）的英勇努力手工驗(yàn)證——最終包含多個(gè)（可修復(fù)的）錯(cuò)誤。1994年，Robertson、Sanders、Seymour和 Thomas【RSST96】試圖使Appel–Haken證明的計(jì)算部分完全可由計(jì)算機(jī)驗(yàn)證，但最終卻產(chǎn)生了一個(gè)更簡單的論證（僅涉及633個(gè)圖，以及驗(yàn)證不可避免性的更簡單的程序），可以通過用任意數(shù)量的標(biāo)準(zhǔn)編程語言編寫的計(jì)算機(jī)代碼更有效地驗(yàn)證。

證明助手將這種形式化更進(jìn)一步，作為一種特殊類型的計(jì)算機(jī)語言，其設(shè)計(jì)目的不是執(zhí)行純粹的計(jì)算任務(wù)，而是驗(yàn)證邏輯或數(shù)學(xué)論證結(jié)論的正確性。粗略地說，數(shù)學(xué)證明中的每個(gè)步驟都對(duì)應(yīng)于該語言中的多行代碼，并且只有在證明有效的情況下才能編譯整個(gè)代碼?，F(xiàn)代證明助手，例如Coq、Isabelle或Lean，有意嘗試模仿數(shù)學(xué)寫作的語言和結(jié)構(gòu)，盡管它們?cè)谠S多方面通常更加挑剔。舉一個(gè)簡單的例子，為了解釋一個(gè)數(shù)學(xué)表達(dá)式，例如a?,形式的證明助手可能需要精確指定基礎(chǔ)變量a,b的“類型”（例如，自然數(shù)、實(shí)數(shù)、復(fù)數(shù)），以便確定正在使用哪種求冪運(yùn)算（這對(duì)于諸如0?的表達(dá)式尤其重要，在不同的求冪概念下，其解釋略有不同）。人們投入了大量精力來開發(fā)自動(dòng)化工具和廣泛的數(shù)學(xué)結(jié)果庫來管理形式證明的這些低級(jí)方面，但在實(shí)踐中，數(shù)學(xué)論證的“明顯”部分通常比“重要”部分需要更長的時(shí)間才能形式化。舉一個(gè)例子：給定三個(gè)集合A?,A?,A?，數(shù)學(xué)家可能會(huì)相互切換使用笛卡爾積(A?×A?)×A?, A?×(A?×A?)和∏_{i∈{1,2,3}}A?，因?yàn)樗鼈儭帮@然”是“同一”對(duì)象；但在大多數(shù)數(shù)學(xué)形式化中，這些乘積實(shí)際上并不相同，并且論證的形式化版本可能需要投入一部分證明來在這些空間之間建立適當(dāng)?shù)牡葍r(jià)性，并確保涉及該乘積的一個(gè)版本的陳述對(duì)于另一個(gè)版本繼續(xù)成立。

由于這個(gè)和其它的原因，將人類數(shù)學(xué)家（即使是非常仔細(xì)的數(shù)學(xué)家）編寫的證明轉(zhuǎn)換為在形式證明助手中編譯的形式證明的任務(wù)相當(dāng)耗時(shí)，盡管隨著時(shí)間的推移，這個(gè)過程逐漸變得更加高效。上述四色定理由Werner和Gonthier于2005年【Gon08】在Coq中形式化。關(guān)于3中對(duì)單位球最密堆積的臭名昭著的開普勒猜想的證明由Hales和Ferguson在1998年【Hal05】的一個(gè)非常復(fù)雜的（計(jì)算機(jī)輔助的）證明中證明。2003年，Hales啟動(dòng)了Flyspeck項(xiàng)目來形式化地驗(yàn)證證明，預(yù)計(jì)需要20年才能完成，盡管最終通過Hales和其他21位貢獻(xiàn)者的合作，“僅”用了11年就實(shí)現(xiàn)了這一目標(biāo)【HAB?17】。最近，舒爾茨（Peter Scholze，1987 -）于2019年啟動(dòng)了“液體張量實(shí)驗(yàn)” 【Com22】，形式驗(yàn)證了他和克勞森（Dustin Clausen）關(guān)于凝聚態(tài)數(shù)學(xué)理論中“液體向量空間”的某個(gè)Ext群消失的基本定理。人類寫的證明“只有”十頁長，盡管包含大量凝聚態(tài)數(shù)學(xué)的先決材料；盡管如此，通過大量的協(xié)作努力，Lean的形式化花費(fèi)了大約18個(gè)月的時(shí)間。我本人領(lǐng)導(dǎo)了一項(xiàng)關(guān)于高爾斯、格林、曼納斯和我自己的加性組合猜想【GGMT23】最近證明的形式化工作【Tao23】；人工編寫的證明長達(dá)33頁，但基本上是自給自足的，大約20名合作者組成的小組在三周內(nèi)將其形式化。有些數(shù)學(xué)領(lǐng)域比其他領(lǐng)域更難以形式化；凱文·巴扎德（Kevin Buzzard，1968 -）最近宣布了一項(xiàng)形式化費(fèi)馬大定理證明的項(xiàng)目，他估計(jì)至少需要五年時(shí)間完成。

考慮到所需的所有努力，數(shù)學(xué)證明的形式化工作對(duì)數(shù)學(xué)的價(jià)值是什么？最明顯的是，它為給定結(jié)果的正確性提供了極高的置信度，這對(duì)于有爭議或因強(qiáng)烈吸引虛假證明而臭名昭著的結(jié)果特別有價(jià)值，或者對(duì)于審閱人愿意逐行驗(yàn)證此類特別冗長的證明的領(lǐng)域尤其供不應(yīng)求。（理論上，證明助手編譯器中仍然可能存在隱藏的缺陷 - 故意將其保持得盡可能小以減少這種可能性 - 或者結(jié)果的形式聲明中使用的定義可能在微妙但重要的方面與人類可讀的陳述有所不同，但這種情況不太可能發(fā)生，特別是如果形式證明密切跟蹤人類編寫的證明的前提下。）形式化過程通常會(huì)發(fā)現(xiàn)人類證明中的小問題，有時(shí)可以揭示論證的簡化或強(qiáng)化，例如通過揭示一個(gè)看似重要的假設(shè)在引理中實(shí)際上是不必要的，或者可以使用低功效但更通用的工具來代替高級(jí)但專門的工具。采用現(xiàn)代語言（例如Lean）的形式化項(xiàng)目通常會(huì)將項(xiàng)目過程中生成的許多基本數(shù)學(xué)結(jié)果貢獻(xiàn)到公共數(shù)學(xué)庫中，這使得未來形式化項(xiàng)目更容易進(jìn)行。

但形式證明助手也可以實(shí)現(xiàn)數(shù)學(xué)教育和協(xié)作的新模式。幾個(gè)實(shí)驗(yàn)項(xiàng)目正在進(jìn)行中，以獲取形式證明并將其轉(zhuǎn)換為更易于人類理解的形式，例如一段交互式文本，其中論證中的各個(gè)步驟可以擴(kuò)展為更詳細(xì)的內(nèi)容或折疊為高級(jí)摘要；這可能是一種特別適合未來數(shù)學(xué)教科書的格式。傳統(tǒng)的數(shù)學(xué)合作很少涉及超過五個(gè)左右的共同作者，部分原因是每個(gè)共同作者都需要信任和驗(yàn)證其他人的工作；但形式化項(xiàng)目通常會(huì)涉及數(shù)十名之前沒有互動(dòng)過的人，這正是因?yàn)樾问阶C明助手允許項(xiàng)目中的各個(gè)子任務(wù)獨(dú)立于其他子任務(wù)進(jìn)行精確定義和驗(yàn)證?？梢韵胂?，這些證明助手還可以允許類似的分工來生成新的數(shù)學(xué)結(jié)果，從而允許比以前的在線協(xié)作（例如“Polymath”項(xiàng)目【Gow10】，其規(guī)模由于需要對(duì)討論進(jìn)行人工審核而受到限制）規(guī)模大得多的高度并行和眾包協(xié)作。隨著時(shí)間的推移，其他科學(xué)或軟件工程項(xiàng)目中已經(jīng)建立的大型合作也可能在研究數(shù)學(xué)中變得司空見慣。一些貢獻(xiàn)者可能扮演“項(xiàng)目經(jīng)理”的角色，例如專注于建立精確的“藍(lán)圖”，將項(xiàng)目分解為更小的部分，而其他貢獻(xiàn)者則可以專門研究項(xiàng)目的各個(gè)組成部分，而不必具備理解整個(gè)項(xiàng)目所需的所有專業(yè)知識(shí)。

然而，在此之前，形式化過程需要變得更加高效?！癲e Bruijn因子”（編寫正確的形式證明與正確的非形式證明的難度之間的比率）仍然遠(yuǎn)高于1（我估計(jì)約為20)，但在下降中。我相信將該比率降至1以下不存在根本障礙，尤其是因?yàn)锳I、SMT求解器和其他工具的集成度不斷提高；這將給我們的領(lǐng)域帶來變革。

2. 機(jī)器學(xué)習(xí)

機(jī)器學(xué)習(xí)是指訓(xùn)練計(jì)算機(jī)執(zhí)行復(fù)雜任務(wù)的一系列技術(shù)，例如預(yù)測與來自非常廣泛的類別的給定輸入相對(duì)應(yīng)的輸出，或者辨別數(shù)據(jù)集中的相關(guān)性和其他關(guān)系。許多流行的機(jī)器學(xué)習(xí)模型使用某種形式的神經(jīng)網(wǎng)絡(luò)來編碼計(jì)算機(jī)如何執(zhí)行任務(wù)。這些網(wǎng)絡(luò)是由大量簡單運(yùn)算（線性和非線性）組合在一起形成的許多變量的函數(shù)；通常，人們會(huì)為這樣的網(wǎng)絡(luò)分配某種獎(jiǎng)勵(lì)函數(shù)（或損失函數(shù)），例如通過根據(jù)訓(xùn)練數(shù)據(jù)集憑經(jīng)驗(yàn)測量其性能，然后執(zhí)行計(jì)算密集型優(yōu)化以找到該網(wǎng)絡(luò)的參數(shù)選擇使得獎(jiǎng)勵(lì)函數(shù)盡可能大（或損失函數(shù)盡可能?。?。這些模型具有無數(shù)的實(shí)際應(yīng)用，例如圖像和語音識(shí)別、推薦系統(tǒng)或欺詐檢測。然而，它們通常不能提供強(qiáng)有力的準(zhǔn)確性保證，特別是當(dāng)應(yīng)用于與訓(xùn)練數(shù)據(jù)集顯著不同的輸入時(shí)，或者當(dāng)訓(xùn)練數(shù)據(jù)集有噪聲或不完整時(shí)。此外，模型通常是不透明的，因?yàn)楹茈y從模型中提取人類可以理解的解釋來說明模型為什么做出特定的預(yù)測，或者理解模型的一般行為。因此，這些工具乍一看似乎不適合研究數(shù)學(xué)，因?yàn)槿藗兗认Ｍ玫絿?yán)格的證明，又希望對(duì)論證有直觀的理解。

盡管如此，最近出現(xiàn)了一些有前景的用例，即適當(dāng)選擇的機(jī)器學(xué)習(xí)工具可以產(chǎn)生或至少提出新的嚴(yán)格數(shù)學(xué)，特別是與其他可以驗(yàn)證這些工具輸出的更可靠技術(shù)相結(jié)合時(shí)。例如，流體方程數(shù)學(xué)理論（例如歐拉方程或納維-斯托克斯N-S方程）的一個(gè)基本問題是能夠嚴(yán)格證明解u在有限時(shí)間內(nèi)從光滑的初始數(shù)據(jù)開始有限時(shí)間內(nèi)爆破。最臭名昭著的例子涉及三維不可壓縮納維-斯托克斯方程，該方程的解是（未解決的）千禧年獎(jiǎng)問題之一；這仍然遙不可及，但最近在其他流體方程方面取得了進(jìn)展，例如二維的Boussinesq方程（三維不可壓縮歐拉方程的簡化模型）。建立這種奇點(diǎn)（singularity）的一種途徑是構(gòu)建自相似的爆破解u，由解出一個(gè)更簡單的偏微分方程（PDE）的低維函數(shù)U描述。該偏微分方程的封閉形式解似乎不可用；但如果能夠產(chǎn)生這個(gè)偏微分方程的足夠高質(zhì)量的近似解?（近似服從某些邊界條件），可以通過應(yīng)用微擾理論嚴(yán)格證明精確解U（例如基于不動(dòng)點(diǎn)定理的理論）。傳統(tǒng)上，人們會(huì)使用數(shù)值PDE方法來嘗試產(chǎn)生這些近似解?，例如，通過將偏微分方程離散化為差分方程（difference equation），但使用此類方法獲得具有所需精度水平的解的計(jì)算成本可能很高。Wang、Lai、Gómez-Serrano和Buckmaster【W(wǎng)LGSB23】于2019年提出了另一種方法，他們使用經(jīng)過訓(xùn)練的物理信息神經(jīng)網(wǎng)絡(luò)（PINN，Physics Informed Neural Network）來生成函數(shù)?，可以最小化一個(gè)合適的損失函數(shù)，該函數(shù)度量了近似遵守所需偏微分方程和邊界條件的程度。由于這些函數(shù)?通過神經(jīng)網(wǎng)絡(luò)而不是方程的離散版本生成，它們可以更快地生成，并且可能不易受到數(shù)值不穩(wěn)定的影響。事實(shí)證明，Chen和Hou的同期工作【CH22】能夠使用更傳統(tǒng)的數(shù)值方法為該方程建立有限時(shí)間爆破解；然而，機(jī)器學(xué)習(xí)范式顯示出作為此類偏微分方程問題的補(bǔ)充方法的巨大潛力。例如，我們可以設(shè)想一種混合方法，其中人類數(shù)學(xué)家首先提出一個(gè)爆破模擬，然后神經(jīng)網(wǎng)絡(luò)嘗試找到一個(gè)粗略的近似解，然后使用更傳統(tǒng)的數(shù)值方法將該解細(xì)化得足夠準(zhǔn)確，使得可以對(duì)其應(yīng)用嚴(yán)格的穩(wěn)定性分析。

機(jī)器學(xué)習(xí)在數(shù)學(xué)中應(yīng)用的另一個(gè)例子是紐結(jié)理論（knot theory）領(lǐng)域。結(jié)具有極其多樣化的拓?fù)洳蛔兞浚航Y(jié)的符號(hào)差（signature）是與以結(jié)為邊界的表面（Siefert曲面）的同調(diào)性相關(guān)的整數(shù)；結(jié)的Jones瓊斯多項(xiàng)式可以使用辮子（braid）的表示理論來描述；大多數(shù)結(jié)（不包括環(huán)面結(jié)torus knot）其補(bǔ)（complement）具有典范雙曲幾何，可用于描述許多雙曲不變量，例如雙曲體積等等。先驗(yàn)地，這些來自不同數(shù)學(xué)領(lǐng)域的不變量之間的相互關(guān)系并不明顯。然而，2021年，Davies、Juhász、Lackenby和Tomasev【DJLT21】通過機(jī)器學(xué)習(xí)研究了這個(gè)問題。通過在現(xiàn)有的近200萬個(gè)結(jié)（加上100萬個(gè)隨機(jī)生成的額外的結(jié)）的數(shù)據(jù)庫上訓(xùn)練神經(jīng)網(wǎng)絡(luò)，他們能夠使該神經(jīng)網(wǎng)絡(luò)模型從大約兩打雙曲不變量中高精度地預(yù)測結(jié)的符號(hào)差。然而，生成的預(yù)測函數(shù)非常不透明，并且最初并沒有揭示出關(guān)于符號(hào)差和雙曲不變量之間的精確關(guān)系的更多見解。然而，可以通過一種稱為顯著性分析（saliency analysis）的簡單工具進(jìn)一步進(jìn)行，粗略地說，該工具測量每個(gè)單獨(dú)的雙曲不變量對(duì)預(yù)測函數(shù)的影響。該分析表明，在使用的兩打雙曲不變量中，只有其中三個(gè)（縱向平移以及子午平移的實(shí)部和復(fù)數(shù)部分）對(duì)預(yù)測函數(shù)有顯著影響。通過視覺上檢查這三個(gè)不變量的符號(hào)差散點(diǎn)圖，作者能夠推測出這些數(shù)量之間更容易理解的關(guān)系。進(jìn)一步的數(shù)值反駁了他們最初的猜想，但提出了他們能夠嚴(yán)格證明的猜想的修改版本。機(jī)器生成的猜想與人類使用理論進(jìn)行驗(yàn)證（和修改）之間的相互作用是一個(gè)有前途的范式，似乎適用于許多其他數(shù)學(xué)領(lǐng)域。

機(jī)器學(xué)習(xí)的許多應(yīng)用需要大量的訓(xùn)練數(shù)據(jù)，理想情況下以某種標(biāo)準(zhǔn)化格式（例如數(shù)字向量）表示，以便現(xiàn)有的機(jī)器學(xué)習(xí)算法可以相對(duì)輕松地應(yīng)用于其中。數(shù)據(jù)的精確表示至關(guān)重要；機(jī)器學(xué)習(xí)算法可以很容易地在一種數(shù)據(jù)表示中發(fā)現(xiàn)數(shù)據(jù)不同組成部分之間的相關(guān)性，但在另一種數(shù)據(jù)表示中幾乎不可能找到。雖然數(shù)學(xué)的一些領(lǐng)域開始編制有用對(duì)象的大型數(shù)據(jù)庫（例如，結(jié)、圖或橢圓曲線），但仍然有許多重要類別的更模糊定義的數(shù)學(xué)概念尚未系統(tǒng)地放入可用于機(jī)器學(xué)習(xí)的形式中。例如，回到偏微分方程的例子，文獻(xiàn)中研究了數(shù)千種不同的偏微分方程，但通常在符號(hào)和項(xiàng)的代數(shù)排列方面具有很大的可變性，而且沒有什么類似于通常所研究的偏微分方程的標(biāo)準(zhǔn)數(shù)據(jù)庫（例如，研究它們是橢圓形、拋物線形還是雙曲形；解的存在性和唯一性、守恒定律等已知的信息）。這樣的數(shù)據(jù)庫可能有助于根據(jù)其他偏微分方程的結(jié)果對(duì)一個(gè)偏微分方程的行為進(jìn)行推測性預(yù)測，或者建議從一種偏微分方程到另一種偏微分方程的可能類比或化簡；但由于缺乏任何規(guī)范范式來表示此類方程（或至少缺乏識(shí)別它們的“指紋” 【BT13】），因此目前構(gòu)建這樣的數(shù)據(jù)庫都非常困難，更不用說將其輸入神經(jīng)網(wǎng)絡(luò)了?？梢韵胂螅磥淼淖C明形式化和人工智能的進(jìn)步可能會(huì)使生成和利用此類數(shù)據(jù)庫（可能包含“真實(shí)世界”和“合成”數(shù)據(jù)集）變得更加可行。

3. 大語言模型

大語言模型（LLM）是一種相對(duì)較新的機(jī)器學(xué)習(xí)模型，適合對(duì)極其廣泛和大型的自然語言文本數(shù)據(jù)集進(jìn)行訓(xùn)練。一種流行的大語言模型是GPT（Generative Pre-trained Transformer生成式預(yù)訓(xùn)練轉(zhuǎn)換器），顧名思義，它是圍繞Transformer模型（一種神經(jīng)網(wǎng)絡(luò)變體，旨在預(yù)測字符串中的下一個(gè)單詞即“token詞元”，并保留對(duì)字符串早期單詞的一些長期“注意力”，以模擬句子的上下文）構(gòu)建的。通過迭代該模型，人們可以對(duì)給定的文本提示（prompt）生成冗長的文本響應(yīng)。當(dāng)使用少量數(shù)據(jù)進(jìn)行訓(xùn)練時(shí)，此類模型的輸出并不令人印象深刻，例如，并不比嘗試在智能手機(jī)上迭代“自動(dòng)完成”文本輸入功能復(fù)雜多少，但經(jīng)過對(duì)極大且多樣化的數(shù)據(jù)集進(jìn)行大量訓(xùn)練后，這些模型的輸出可以令人驚訝地連貫，甚至具有創(chuàng)造性，并且可以生成乍一看很難與人類書寫區(qū)分開的文本，盡管仔細(xì)檢查后，輸出通常是無意義的，并且與任何基本事實(shí)沒有聯(lián)系，這種現(xiàn)象被認(rèn)為是“幻覺”（hallucination）。

人們當(dāng)然可以嘗試應(yīng)用這種通用的LLM來嘗試直接解決數(shù)學(xué)問題。有時(shí)，結(jié)果可能相當(dāng)令人印象深刻；例如布貝克（Bubeck）等人記錄了一個(gè)案例，其中強(qiáng)大的大語言模型GPT-4能夠提供2022年國際數(shù)學(xué)奧林匹克問題的完整且正確的證明，該問題并不在該模型的訓(xùn)練數(shù)據(jù)集中。相反，該模型不太適合執(zhí)行精確計(jì)算，甚至基本算術(shù)；在一個(gè)例子【BCE?23】中，當(dāng)要求計(jì)算表達(dá)式7×4 + 8×8時(shí)，GPT-4立即給出了錯(cuò)誤答案120，然后繼續(xù)通過分步過程來證明計(jì)算的合理性返回正確答案92。當(dāng)被問及這一差異時(shí)，GPT-4只表示其最初的猜測是一個(gè)“拼寫錯(cuò)誤”（typo）。這些問題可以通過使用GPT-4的“插件”得到一定程度的補(bǔ)償，其中GPT-4被訓(xùn)練為向外部工具（例如Wolfram Alpha）發(fā)送特定類型的查詢（例如數(shù)學(xué)計(jì)算），而不是通過其內(nèi)部模型猜測答案，盡管目前工具之間的集成還不是無縫的。類似地，最近的概念驗(yàn)證【RPBN?23】已經(jīng)表明，LLM可用于查找組合學(xué)和計(jì)算機(jī)科學(xué)中各種問題的示例，這些示例優(yōu)于以前的人類生成的示例，方法是要求這些模型生成程序來創(chuàng)建此類示例，而不是嘗試直接構(gòu)建示例，然后使用另一種語言執(zhí)行該程序來可靠地驗(yàn)證輸出的質(zhì)量，然后將其發(fā)送回原始模型以提示其對(duì)猜測進(jìn)行改進(jìn)。最近在使用LLM來增強(qiáng)現(xiàn)有符號(hào)證明引擎以解決狹窄類別的數(shù)學(xué)問題（例如奧林匹克幾何問題【TWL?24】）方面也取得了進(jìn)展.

在我自己的GPT-4實(shí)驗(yàn)中（可以在 https://terrytao.wordpress.com/mastodon-posts/ 找到），我發(fā)現(xiàn)最高效的用例是生成各種語言的基本計(jì)算機(jī)代碼（Python、SAGE、LaTeX、Lean、正則表達(dá)式等），或者清理凌亂且無組織的數(shù)據(jù)集（例如，在起初提供GPT-4一些所需參考書目條目格式的示例后，讓它將互聯(lián)網(wǎng)上抓取的一堆參考文獻(xiàn)整理成連貫的LaTeX參考書目）。在這種情況下，它通常會(huì)在第一次嘗試時(shí)產(chǎn)生令人滿意或接近令人滿意的輸出，只需進(jìn)行少量修改即可獲得我正在尋求的輸出類型。我在讓GPT-4為實(shí)際數(shù)學(xué)問題推薦相關(guān)文獻(xiàn)或技術(shù)方面也取得了一些有限的成功。在一個(gè)測試用例中，我問它如何計(jì)算獨(dú)立隨機(jī)變量之和的尾部概率的指數(shù)衰減率，以在不給它提供大偏差理論（large deviation theory）等關(guān)鍵詞前提下，評(píng)估它是否知道這方面的相關(guān)定理（Cramér定理）。事實(shí)證明，GPT-4并沒有準(zhǔn)確定位這個(gè)定理，而是產(chǎn)生了一串?dāng)?shù)學(xué)廢話，但奇怪的是，它確實(shí)引用了對(duì)數(shù)矩生成函數(shù)（logarithmic moment generating function），這是Cramér定理陳述中的一個(gè)關(guān)鍵概念，即使它似乎并不確切地“知道”這個(gè)函數(shù)與問題的相關(guān)性。在另一個(gè)實(shí)驗(yàn)中，我向GPT-4詢問如何證明我正在研究的組合恒等式的建議。它給出了一些我已經(jīng)考慮過的建議（漸近分析、歸納、數(shù)值）以及一些通用建議（簡化表達(dá)式、尋找類似問題、理解問題），而且還提出了一種技術(shù)（生成函數(shù)）我只是忽略了這一點(diǎn)，最終很容易地解決了這個(gè)問題。另一方面，這樣的建議列表對(duì)于新手?jǐn)?shù)學(xué)家來說可能沒什么用，因?yàn)樗麄儧]有足夠的經(jīng)驗(yàn)來獨(dú)立評(píng)估每個(gè)建議的有用性。盡管如此，我看到這些工具在提取用戶對(duì)一個(gè)問題的潛在知識(shí)方面的作用，只需成為一個(gè)好的傾聽者并提出足夠用戶給出專業(yè)評(píng)估的合理相關(guān)的想法即可。

Github Copilot（副駕駛）是另一個(gè)GPT模型，已集成到多個(gè)流行的代碼編輯器中。它經(jīng)過不同語言的大型代碼數(shù)據(jù)集的訓(xùn)練，旨在利用上下文線索（例如代碼中其他地方要執(zhí)行的任務(wù)的非形式描述）為部分編寫的代碼提供自動(dòng)完成建議。我發(fā)現(xiàn)它對(duì)于編寫數(shù)學(xué)LaTeX以及在Lean中形式化非常有效；事實(shí)上，它在我寫作時(shí)建議了幾句話，從而幫助我寫了這篇文章，其中許多句子我在最終版本中保留著或進(jìn)行了輕微編輯。雖然其建議的質(zhì)量差異很大，但有時(shí)它可以表現(xiàn)出對(duì)文本意圖的模擬理解的不可思議的水平。例如，在編寫另一篇關(guān)于如何估計(jì)積分的闡述性LaTeX筆記時(shí)，我描述了如何將積分分解為三個(gè)部分，然后詳細(xì)說明了如何估計(jì)第一部分。然后Copilot立即建議如何通過類似的方法來估計(jì)第二部分，并以完全正確的方式改變變量。這些頻繁經(jīng)歷使我在LaTeX和Lean的寫作中獲得了小幅但明顯的加速，我預(yù)計(jì)這些工具在未來會(huì)變得更加有用，因?yàn)榭梢愿鶕?jù)個(gè)人寫作風(fēng)格和喜好“微調(diào)”這些模型。

4. 這些工具可以組合使用嗎？

上面討論的各種技術(shù)都有非常不同的優(yōu)點(diǎn)和缺點(diǎn)，而且就其目前的發(fā)展水平而言，沒有一種技術(shù)適合作為數(shù)學(xué)家的通用工具，能與LaTeX或arXiv等無處不在的平臺(tái)相媲美。然而，最近有一些有希望的實(shí)驗(yàn)可以通過將兩種或多種單獨(dú)的技術(shù)結(jié)合在一起來創(chuàng)建更令人滿意的工具。例如，在生成證明時(shí)對(duì)抗LLM的幻覺性質(zhì)的一種可行方法是要求模型以形式證明助手的語言格式化其輸出，并將助手生成的任何錯(cuò)誤作為反饋發(fā)送回模型。這個(gè)組合系統(tǒng)似乎適合生成簡單命題的簡短證明【YSG?23】；由于此類任務(wù)通常是有效形式化證明的限制因素，因此這種范式可以大大加快這種形式化的速度，特別是如果這些模型在形式化證明（而不是一般文本）上進(jìn)行微調(diào)，并與更傳統(tǒng)的自動(dòng)化定理證明方法集成，例如SMT求解器的部署。

由于能夠接受自然語言輸入，LLM還可能是一個(gè)用戶友好的界面，允許沒有特定軟件專業(yè)知識(shí)的數(shù)學(xué)家使用高級(jí)工具。如前所述，我和許多其他人已經(jīng)經(jīng)常使用此類模型來生成各種語言的簡單代碼（包括符號(hào)代數(shù)包），或創(chuàng)建復(fù)雜的圖表和圖像；似乎可以合理地預(yù)期，在不久的將來，人們還可以通過此類模型進(jìn)行通信，僅使用高級(jí)會(huì)話指令來設(shè)計(jì)和操作像機(jī)器學(xué)習(xí)模型這樣復(fù)雜的東西。更雄心勃勃的是，人們可能希望最終能夠通過用自然語言向人工智能解釋結(jié)果來生成完整的研究論文（初稿），并完成形式驗(yàn)證，人工智能將嘗試形式化結(jié)果的每一步并在需要澄清時(shí)詢問作者。

當(dāng)前形式的形式化證明驗(yàn)證的人力密集性質(zhì)意味著當(dāng)前研究論文的很大一部分實(shí)時(shí)完全形式化是不可行的。然而，許多已經(jīng)用于驗(yàn)證研究論文中特定計(jì)算密集型部分的工具（例如數(shù)值積分或 PDE求解器、符號(hào)代數(shù)計(jì)算或使用SMT求解器建立的結(jié)果）似乎可以進(jìn)行修改之后出具形式證明證書。此外，可以以這種方式形式化的計(jì)算類別可以從當(dāng)前實(shí)踐中大大擴(kuò)展。僅舉一個(gè)例子，在偏微分方程領(lǐng)域，通常會(huì)使用大量計(jì)算來估計(jì)涉及一個(gè)或多個(gè)未知函數(shù)（例如一個(gè)偏微分方程的解）的某些積分表達(dá)式，并使用各種函數(shù)空間范數(shù)中此類函數(shù)的界限（例如Sobolev索博列夫空間范數(shù)），以及標(biāo)準(zhǔn)不等式（例如，H?lder霍爾德不等式和Sobolev索博列夫不等式），以及各種恒等式，例如分部積分或積分符號(hào)下的微分。此類計(jì)算雖然是常規(guī)計(jì)算，但可能包含不同嚴(yán)重程度的拼寫錯(cuò)誤（例如符號(hào)錯(cuò)誤），并且仔細(xì)審閱可能會(huì)很乏味，因?yàn)橛?jì)算本身除了驗(yàn)證最終估計(jì)值是否成立之外幾乎沒有提供任何見解。可以想象，可以開發(fā)工具來以自動(dòng)或半自動(dòng)的方式建立此類估計(jì)，并且當(dāng)前此類估計(jì)的冗長且無啟發(fā)性的證明可以由形式證明證書的鏈接取代。更雄心勃勃的是，人們可能能夠要求未來的AI人工智能工具在給定一組初始假設(shè)和方法的情況下產(chǎn)生最佳估計(jì)，而無需首先進(jìn)行一些紙筆計(jì)算來猜測估計(jì)值是什么。目前，可能估計(jì)的狀態(tài)空間太復(fù)雜，無法以這種方式自動(dòng)探索；但我認(rèn)為隨著技術(shù)的進(jìn)步，這種自動(dòng)化沒有理由無法實(shí)現(xiàn)。當(dāng)這種情況成為現(xiàn)實(shí)時(shí)，目前尚不可行的大規(guī)模的數(shù)學(xué)探索就成為可能。繼續(xù)以偏微分方程為例，該領(lǐng)域的論文通常一次研究一兩個(gè)方程；但在未來，人們可能能夠同時(shí)研究數(shù)百個(gè)方程，也許只為一個(gè)方程給出完整的論證，然后讓人工智能工具將論證適應(yīng)一大族的相關(guān)方程，在推廣的論點(diǎn)非常規(guī)時(shí)詢問作者是否有必要擴(kuò)展。這種大規(guī)模數(shù)學(xué)探索的一些提示開始在數(shù)學(xué)的其他領(lǐng)域出現(xiàn)，例如圖論中猜想的自動(dòng)探索【W(wǎng)ag21】。

目前尚不清楚這些實(shí)驗(yàn)中哪一個(gè)最終將最成功地為典型的數(shù)學(xué)家?guī)硐冗M(jìn)的計(jì)算機(jī)輔助。一些概念證明目前無法擴(kuò)展，特別是那些依賴于計(jì)算極其密集（且通常是專有）的人工智能模型，或需要大量專家人工輸入和監(jiān)督的證明。然而，我對(duì)探索可能性空間的各種努力感到鼓舞，并相信在不久的將來會(huì)有更多執(zhí)行機(jī)器輔助數(shù)學(xué)的新方法的例子。

5. 進(jìn)一步閱讀

機(jī)器輔助證明的主題相當(dāng)廣泛，分布在數(shù)學(xué)、計(jì)算機(jī)科學(xué)甚至工程學(xué)的各個(gè)領(lǐng)域；雖然每個(gè)單獨(dú)的子領(lǐng)域都有大量的活動(dòng)，但直到最近才努力建立一個(gè)更加統(tǒng)一的社區(qū)，將此處列出的所有主題匯集在一起。因此，目前很少有地方可以找到對(duì)這些快速發(fā)展的數(shù)學(xué)模式的全面調(diào)查。一個(gè)起點(diǎn)是2023年6月美國國家科學(xué)院“人工智能輔助數(shù)學(xué)推理”研討會(huì)的會(huì)議記錄【Kor23】（作者是該研討會(huì)的聯(lián)合組織者之一）；作為該研討會(huì)的成果之一，Talia Ringer領(lǐng)導(dǎo)了一項(xiàng)為數(shù)學(xué)資源編譯AI的工作，其結(jié)果可以在https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0 中找到。

例如，該文檔中有一個(gè)指向“自然數(shù)字游戲”的鏈接，這是一種開始熟悉Lean證明輔助語言的易于訪問和交互的方式。這里討論的許多例子也取自2023年2月的IPAM研討會(huì)“機(jī)器輔助證明”（作者也參與共同組織），該研討會(huì)的演講可以在網(wǎng)上找到。

感謝匿名審稿人的指正和建議。

參考資料

[AH89]

Kenneth Appel and Wolfgang Haken, Every planar map is four colorable, Contemporary Mathematics, vol. 98, American Mathematical Society, Providence, RI, 1989. With the collaboration of J. Koch, DOI 10.1090/conm/098. MR1025335

[BT13]

Sara C. Billey and Bridget E. Tenner, Fingerprint databases for theorems, Notices Amer. Math. Soc. 60 (2013), no. 8, 1034–1039, DOI 10.1090/noti1029. MR3113227

[BCE?23]

Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, Harsha Nori, Hamid Palangi, Marco Tulio Ribeiro, and Yi Zhang, Sparks of artificial general intelligence: Early experiments with GPT-4, Preprint, arXiv:2303.12712, 2023.

[CH22]

Jiajie Chen and Thomas Y. Hou, Stable nearly self-similar blowup of the 2D Boussinesq and 3D Euler equations with smooth data, parts I and II, 2022. arXiv:2210.07191; arXiv:2305.05660.

[Com22]

Johan Commelin, Liquid tensor experiment (German, with German summary), Mitt. Dtsch. Math.-Ver. 30 (2022), no. 3, 166–170, DOI 10.1515/dmvm-2022-0058. MR4469845

[DJLT21]

Alex Davies, András Juhász, Marc Lackenby, and Nenad Tomasev, The signature and cusp geometry of hyperbolic knots, Preprint, arXiv:2111.15323, 2021.

[Gon08]

Georges Gonthier, Formal proof—the four-color theorem, Notices Amer. Math. Soc. 55 (2008), no. 11, 1382–1393. MR2463991

[Gow10]

W. T. Gowers, Polymath and the density Hales-Jewett theorem, An irregular mind, Bolyai Soc. Math. Stud., vol. 21, János Bolyai Math. Soc., Budapest, 2010, pp. 659–687, DOI 10.1007/978-3-642-14444-8_21. MR2815619

[GGMT23]

W. T. Gowers, Ben Green, Freddie Manners, and Terence Tao, On a conjecture of Marton, Preprint, arXiv:2311.05762, 2023.

[HAB?17]

Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller, A formal proof of the Kepler conjecture, Forum Math. Pi 5 (2017), e2, 29, DOI 10.1017/fmp.2017.1. MR3659768

[Hal05]

Thomas C. Hales, A proof of the Kepler conjecture, Ann. of Math. (2) 162 (2005), no. 3, 1065–1185, DOI 10.4007/annals.2005.162.1065. MR2179728

[HKM16]

Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek, Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer, Theory and applications of satisfiability testing—SAT 2016, 2016, pp. 228–245, DOI 10.1007/978-3-319-40970-2_15. MR3534782

[Kor23]

Samantha Koretsky (ed.), Artificial intelligence to assist mathematical reasoning: Proceedings of a workshop, National Academies Press, 2023, DOI 10.17226/27241.

[RSST96]

Neil Robertson, Daniel P. Sanders, Paul Seymour, and Robin Thomas, A new proof of the four-colour theorem, Electron. Res. Announc. Amer. Math. Soc. 2 (1996), no. 1, 17–25, DOI 10.1090/S1079-6762-96-00003-0. MR1405965

[RPBN?23]

Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi, Mathematical discoveries from program search with large language models, Nature 625 (December 2023), no. 7995, 468–475, DOI 10.1038/s41586-023-06924-6.

[Tao23]

Terence Tao, Formalizing the proof of PFR in Lean4 using Blueprint: a short tour, 2023. https://terrytao.wordpress.com/2023/11/18

[TWL?24]

Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong, Solving olympiad geometry without human demonstrations, Nature 625 (January 2024), no. 7995, 476–482, DOI 10.1038/s41586-023-06747-5.

[Wag21]

Adam Zsolt Wagner, Constructions in combinatorics via neural networks, Preprint, arXiv:2104.14516, 2021.

[WLGSB23]

Y. Wang, C.-Y. Lai, J. Gómez-Serrano, and T. Buckmaster, Asymptotic self-similar blow-up profile for three-dimensional axisymmetric Euler equations using neural networks, Phys. Rev. Lett. 130 (2023), no. 24, Paper No. 244002, 6, DOI 10.1103/physrevlett.130.244002. MR4608987

[YSG?23]

Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar, LeanDojo: Theorem proving with retrieval-augmented language models, Preprint, arXiv:2306.15626, 2023.

https://www.ams.org/journals/notices/202501/noti3041/noti3041.html

https://terrytao.wordpress.com/mastodon-posts/

https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0

科普薦書

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評(píng)論、點(diǎn)贊、在看、在聽

收藏、分享、轉(zhuǎn)載、投稿

查看原始文章出處

點(diǎn)擊zzllrr小樂

公眾號(hào)主頁

右上角

數(shù)學(xué)科普不迷路！