Find N3入網(wǎng)：最高支持16+1TB
OPPO將于近期登場的Find N3折疊屏目前已經(jīng)正式入網(wǎng)，型號為PHN110。本次Find N3在外觀方面相比前兩代有很大的變化，不再是小號的橫向折疊屏，而是跟別的廠商一樣采用了較為常見的
今年6月，陶哲軒曾在博客中預(yù)言，2026年，AI將與搜索和符號數(shù)學(xué)工具相結(jié)合，成為數(shù)學(xué)研究中值得信賴的合著者。
這個預(yù)言，如今已經(jīng)愈發(fā)成真。
就在6月底，加州理工、英偉達(dá)、MIT等機構(gòu)的學(xué)者，曾構(gòu)建了一個基于開源LLM的定理證明器。
最近，陶哲軒又發(fā)現(xiàn)，在使用Lean進(jìn)行自然數(shù)游戲研究時，GPT-4竟然也起到一些作用。
在AI的輔助下，他得到了關(guān)于有限多個實變量不等式理論的成果，論文很快就會發(fā)在arXiv上。
圖片
什么是自然數(shù)游戲？
圖片
這個游戲，神奇地展示了歸納的力量。
如圖所示，我們從藍(lán)色節(jié)點上輸入，而灰色節(jié)點上方的所有結(jié)點都完成時，灰色節(jié)點將變?yōu)樗{(lán)色。
在這個過程中，我們當(dāng)然可以隨時嘗試任何級別的節(jié)點，但如果它是灰色的，我們可能就沒有足夠的知識來完成這個節(jié)點。
引理：對于所有自然數(shù)x、y和z都有xy+z=xy+z。證明開始！
在自然數(shù)游戲中，我們就會在定理證明器Lean中，得到自己的一個自然數(shù)版本——mynat。這個自然數(shù)滿足了數(shù)學(xué)歸納定理，以及其他原理（比如皮亞諾公理）。
圖片
不過，問題在于，目前還沒有人證明這些關(guān)于自然數(shù)的定理，比如，你可以定義加法，但還沒有人證明x + y = y + x。
皮亞諾公理
而自然數(shù)游戲，就需要你解決游戲中的關(guān)卡，用Lean定理證明器來證明數(shù)學(xué)定理。
我們證明了n+0=n，這個證明被稱為add_zero。但并不能證明zero_add，0+n=n。這兩個定理不是一樣嗎？并非如此！事實上x + y = y + x，這是加法世界的BOSS級難題。
陶哲軒是出于怎樣的機緣巧合，開始玩自然數(shù)游戲的呢？
原來，他是在IPAM機器輔助證明研討會上看到過幾次Lean的演示，并且被建議玩一玩自然數(shù)游戲，來熟悉Lean中用于證明定理的基本語法和策略。
讓陶哲軒感到驚喜的是，這個游戲越玩越熟悉，因為它證明的結(jié)果和自己寫的本科實分教材前幾章的結(jié)果分成相似。
圖片
比如，從皮亞諾公理建立基本的算術(shù)事實，例如乘法的交換性和結(jié)合性。
另外，自然數(shù)游戲還讓他想起了自己編碼的邏輯游戲。
才玩了三個小時，陶哲軒就已經(jīng)到達(dá)了「高級乘法」世界。他表示，在以后的空閑時間里他會繼續(xù)玩這個游戲。
圖片
高級乘法世界：證明兩個非零自然數(shù)的乘積為非零：a≠0 → b≠0 → a*b≠0
當(dāng)然，GPT-4也知道Lean，它可以提供一些有用的回答。
不過，因為自然數(shù)游戲中可用的工具集很有限，所以GPT-4對于這個游戲沒有直接的幫助，因為它提出的解決方案中涉及的方法，通常還沒有被納入游戲中。
不過，當(dāng)他開始使用Lean的時候，GPT-4就變得非常有幫助了。
圖片
隨著關(guān)卡變得越來越難，GPT的作用開始逐漸顯現(xiàn)出來。
在Z顯而易見是X和Y的結(jié)果的情況下，如果向GPT提問——
如果我已經(jīng)知道X和Y，該如何證明Z呢？
這個過程就解決了各種微妙的語法問題，否則這些問題會十分令人沮喪。
圖片
而且，陶哲軒發(fā)現(xiàn)，自然數(shù)游戲中包含的Lean庫，似乎比文件中宣稱的要多得多。
總之，AI工具輔助研究數(shù)學(xué)的奇跡，一次次讓陶哲軒稱贊不已，甚至發(fā)展到了讓他「不安」。
前不久陶哲軒發(fā)現(xiàn)，GitHub Copilot已經(jīng)能夠預(yù)測到自己文章中數(shù)學(xué)論證的步驟了。
圖片
在10月初，陶哲軒表示，Github Copilot的能力驚艷到他了。
而且他強調(diào)，并不是它的編碼能力，而是它編碼之外的補充其他內(nèi)容的能力，經(jīng)常能讓他喜出望外。
最近，他又稱贊到——
我發(fā)現(xiàn)Github Copilot在我最近撰寫博客文章的過程中出奇地有幫助。它能夠正確預(yù)測該帖子中數(shù)學(xué)論證的幾個步驟；在下面給出的示例中，我將積分分成三部分，并描述了如何估計第一部分，然后copilot正確地說明了如何估計其余兩部分。
陶哲軒給出的例證
只要簡單說明一下如何對第一部分進(jìn)行估計，剩下的工作GitHub Copilot就能完成了，這也太驚艷了！
對此，陶哲軒的評價是：「Copilot的性能給我留下了深刻的印象（并且讓我有點不安）」。
他補充說「雖然其中的許多建議并不那么合適，我估計Copilot可能建議了十幾句話，最終以某種形式出現(xiàn)在我的博客文章中。」
而他說的博客文章就是這篇關(guān)于「非負(fù)量的和或積分的上界」。
圖片
博文地址：https://terrytao.wordpress.com/2023/09/30/bounding-sums-or-integrals-of-non-negative-quantities/
估計某個量的大小，是數(shù)分、概率論、組合學(xué)等領(lǐng)域中的常見問題，如估計函數(shù)、序列、結(jié)合等的和或積分。
因此陶哲軒這篇估計非負(fù)量的和或積分上界，探討的正是數(shù)學(xué)領(lǐng)域的重要問題。
圖片
陶哲軒在博客中總結(jié)了3種估算大量非負(fù)量和以及積分的方法，如算術(shù)平均值-幾何平均值不等式、Holder不等式、Markov不等式等。
圖片
其中的內(nèi)容和代碼沒有關(guān)系，但是Github Copilot依然給出了讓陶哲軒都感到驚嘆的內(nèi)容建議。
圖片
能讓陶哲軒都感到有點不安的Github Copilot，源于Github和OpenAI的合作。
它主要功能是利用生成式AI的能力為程序提供編碼的建議，自動補充等編碼功能。而之所以它有如此強大的功能，和背后微軟，OpenAI的大量投入是分不開的。
最近外媒報道，微軟提供的Github Copilot每月10刀的訂閱服務(wù)，在算力成本上，每個用戶要讓微軟虧損20美元/月。
圖片
文章地址：https://www.wsj.com/tech/ai/ais-costly-buildup-could-make-early-products-a-hard-sell-bdd29b9f?mod=followamazon
這些服務(wù)成本如此高昂的原因之一，是使用了最強大的AI模型，與普通的軟件或云服務(wù)相比，這些模型需要更多的電力，并對處理器的運行造成更大的壓力。
文章中甚至將現(xiàn)在的AI工具的能力和成本做了一個讓人繃不住的比喻：
「用AI去做文章總結(jié)就像開著蘭博基尼去送披薩一樣」。
足見現(xiàn)在科技巨頭們，為了讓用戶充分享受AI帶來的便利，真的是下了血本！
所以讓陶哲軒驚嘆的Github Copilot能在編碼之外還有如此強大的能力，也似乎不那么奇怪了。
顯然，現(xiàn)在所有人都已經(jīng)意識到：AI具有巨大潛力，它可以通過指導(dǎo)猜想生成、協(xié)助形式化數(shù)學(xué)等方式為數(shù)學(xué)發(fā)展做出貢獻(xiàn)。
在9月26日舉行的一場關(guān)于使用AI輔助數(shù)學(xué)推理的網(wǎng)絡(luò)研討會上，眾數(shù)學(xué)大咖云集，一起討論了人工智能技術(shù)如何用于推進(jìn)數(shù)學(xué)科學(xué)，跨學(xué)科合作如何開辟新的機會。
陶哲軒也參與了會議，并結(jié)合自己與AI合作的經(jīng)歷談了自己的觀點。
圖片
大會對于AI輔助數(shù)學(xué)研究，AI專家和數(shù)學(xué)家協(xié)作配合的新機會和新挑戰(zhàn)，都展開了充分地討論，可謂是干貨滿滿：
嘗試應(yīng)用機器學(xué)習(xí)方法來輔助或完成形式數(shù)學(xué)論證，現(xiàn)在已經(jīng)是人工智能應(yīng)用的一個獨特領(lǐng)域
AI在輔助數(shù)學(xué)研究中的獨特之處在于，數(shù)學(xué)具有一種自我驗證的方法，可以用來檢查AI產(chǎn)生的結(jié)果，而其他AI任務(wù)通常需要人類參與來評估反饋的質(zhì)量。
數(shù)學(xué)表達(dá)本身具有一種內(nèi)在的準(zhǔn)確性，因此機器學(xué)習(xí)在數(shù)學(xué)領(lǐng)域能夠在數(shù)據(jù)相對稀缺的情況下有效地推進(jìn)工作，這使得AI在數(shù)學(xué)領(lǐng)域具備明顯的優(yōu)勢。
在研討會上，多位數(shù)學(xué)領(lǐng)域?qū)＜疫M(jìn)行了知識分享和交流。
圖片
在使用機器學(xué)習(xí)協(xié)助數(shù)學(xué)發(fā)現(xiàn)方面,會議中數(shù)學(xué)家Heather提到了具體的幾個例子:
圖片
(1) DeepMind和數(shù)學(xué)家合作，利用機器學(xué)習(xí)從大量數(shù)據(jù)中尋找模式，形成了關(guān)于模形的新猜想。
(2) Sutherland等數(shù)學(xué)家也使用機器學(xué)習(xí)在模形式的工作中找到了新公式。
(3) Adam Wagner使用機器學(xué)習(xí)來尋找圖論問題的反例。
(4) Javier Pena利用機器學(xué)習(xí)找到偏微分方程近似的數(shù)值解,以方便后續(xù)的嚴(yán)格數(shù)值方法的推進(jìn)。
在使用AI輔助證明方面,會議提到形式化證明可以將一個大證明分解成小塊,不同人可以負(fù)責(zé)不同部分。
圖片
這可能會開啟新的科研協(xié)作模式——計算機可以自動化證明中的某些步驟，已經(jīng)有許多前沿的數(shù)學(xué)領(lǐng)域使用了這種模式。
這種形式化證明的過程有利于數(shù)學(xué)家以新方式與AI進(jìn)行創(chuàng)造性的互動。
這也體現(xiàn)了AI協(xié)助數(shù)學(xué)發(fā)現(xiàn)和傳統(tǒng)數(shù)學(xué)研究的不同：既有大公司提供計算資源的大規(guī)模合作，也有小規(guī)模的個人之間的合作探索。
學(xué)界需要對這些不同的合作模式保持開放。
圖片
會議中，還有多位學(xué)者討論了AI在數(shù)學(xué)翻譯中的應(yīng)用
數(shù)學(xué)翻譯是指將一個數(shù)學(xué)問題從一個領(lǐng)域翻譯到另一個領(lǐng)域的等價表達(dá),這是數(shù)學(xué)家解決問題的基本工具之一。
數(shù)學(xué)家以一個圖論問題為例。圖論問題可以翻譯成代數(shù)問題，兩者邏輯上是等價的，但表達(dá)上的術(shù)語和形式明顯不同。
AI轉(zhuǎn)換工具可以將一個看似毫無頭緒的問題，轉(zhuǎn)化成一個可以用已有技術(shù)來解決的問題。
還有學(xué)者進(jìn)一步指出，證明思路到形式證明的轉(zhuǎn)換，以及形式證明到實際算法的轉(zhuǎn)換，也是一種翻譯過程。
鑒于AI在不同語言之間的翻譯上取得了巨大進(jìn)展，未來可以研究如何應(yīng)用機器學(xué)習(xí)來實現(xiàn)數(shù)學(xué)領(lǐng)域內(nèi)的翻譯。
例如將不完整的證明草圖自動翻譯成可證明的形式表達(dá)。這是當(dāng)前一個非常有前景的研究方向。
會議中多位數(shù)學(xué)家也強調(diào)了。由于數(shù)學(xué)翻譯能顯著拓展問題解決的視角，應(yīng)用機器學(xué)習(xí)來實現(xiàn)數(shù)學(xué)翻譯將可能大大推進(jìn)數(shù)學(xué)研究。
圖片
AI專家和數(shù)學(xué)家進(jìn)行跨界合作，需要面對的差異和挑戰(zhàn)
AI界和數(shù)學(xué)界，存在著諸多差異。
比如，機器學(xué)習(xí)研究者習(xí)慣處理大規(guī)模數(shù)據(jù)集，而數(shù)學(xué)家習(xí)慣于處理相對較少的數(shù)據(jù)。機器學(xué)習(xí)研究者注重在一類任務(wù)上的平均表現(xiàn)，而數(shù)學(xué)家則更關(guān)注單個案例的解釋。
另外，兩者的出版文化不同，機器學(xué)習(xí)界會公開發(fā)表絕大部分研究內(nèi)容，數(shù)學(xué)界則不然。機器學(xué)習(xí)界普遍第一作者為主要貢獻(xiàn)者，數(shù)學(xué)界作者順序就比較隨機。
大規(guī)模合作項目的學(xué)術(shù)貢獻(xiàn)認(rèn)定上，二者也存在差異。形式化研究使得每個參與者只負(fù)責(zé)一小塊，如何評價貢獻(xiàn)是一個新問題。
還有一個差異，是資源獲取方式。
機器學(xué)習(xí)需要大數(shù)據(jù)集和計算資源，數(shù)學(xué)家對這方面的需求就相對較少。如何使各界研究者公平獲取資源也會是一個問題。開源文化不同。機器學(xué)習(xí)界更看重開源共享,而數(shù)學(xué)界不一定。如何處理二者關(guān)系需要考量。
由于這是一個全新的交叉領(lǐng)域,雙方在一些根本理念和工作方式上存在差異，需要在合作中加以認(rèn)識和調(diào)適，以實現(xiàn)更好的協(xié)同效果。
參考資料：
https://mathstodon.xyz/@tao/111206761117553482
本文鏈接：http://www.www897cc.com/showinfo-26-12685-0.html「陶哲軒×GPT-4」合寫數(shù)學(xué)論文！數(shù)學(xué)大佬齊驚呼，LLM推理神助證明不等式定理
聲明：本網(wǎng)頁內(nèi)容旨在傳播知識，若有侵權(quán)等問題請及時與本網(wǎng)聯(lián)系，我們將在第一時間刪除處理。郵件：2376512515@qq.com
Copyright ? 2016-2023 天津谷騏科技有限公司 版權(quán)所有 sitemap.xml
違法及侵權(quán)請聯(lián)系：2376512515@qq.com 津ICP備18001702號
津公網(wǎng)安備 12010102000574號