歐盟人工智能法案：四種AI系統(tǒng)風險類型的劃分及監(jiān)管措施
作者：趙志東 蔡佳雯來源：區(qū)塊鏈日報該法案采用風險分級的規(guī)制路徑，將人工智能系統(tǒng)的風險劃分成不可接受的風險、高風險、有限風險和輕微風險四種類型，并針對不同類型施加了不同
快來圍觀，陶哲軒當視頻博主了。
第一個產(chǎn)出就很炸裂：人類需要寫滿一頁紙的證明，結(jié)果借助 AI 33 分鐘就搞定了？！
整個過程看起來一氣呵成，還是全程“盲證”不用過腦子那種。
對于這一操作，網(wǎng)友們驚呆：這具有足夠的歷史意義。
在沒有明顯引導(dǎo)、宣傳之下，他的訂閱數(shù)一天時間已經(jīng)有 900+，觀看數(shù)超兩千，目前仍然在高速增長中。
大家趕在爆火之前留言：
今天我們相聚在這里，就是為了見證偉大數(shù)學頻道的誕生。
具體來看看是如何做到？
33 分鐘盲證定理陶哲軒這次選取了泛代數(shù)中的一個命題，即證明 Magma 方程 E1689 蘊含 E2。
方程具體是什么不重要，我們只需要了解，即使是方程理論項目的合作者 Bruno Le Floch，也足足人工花了一頁紙才完成證明。
而用上 AI 后，整個證明過程僅用時 33 分鐘：
具體而言，陶哲軒嘗試完全基于 Bruno Le Floch 的草稿，逐行進行形式化。
他將草稿拆分為微小邏輯單元，交由 GitHub 生成代碼骨架，再以 Lean 的 canonical 策略匹配填補細節(jié)，過程中也涉及部分手動補全。
最終，整個形式化證明能夠在 Lean 中通過驗證。
不僅時間大大縮短了，更重要的是滿足了“人類可讀性”。
要知道 Bruno Le Floch 最初挑戰(zhàn)該問題時，曾在論文中宣稱 E1689-E2 的所有已知證明都依賴計算機輔助。
直到后來他使用 prover9 ATP（自動定理證明器）給出了一個更具可讀性的人類版本，所以才對之前的想法產(chǎn)生動搖：
它是否仍然可以被認為是計算機輔助的，我不確定。
針對這一疑惑，陶哲軒提議今后可以在論文中明確說明，雖然最初的證明是由計算機生成的，但在項目進行過程中，研究者們成功地將其轉(zhuǎn)化為一個人類可讀的證明。
并且為了實際驗證 AI 能在多大程度上開啟自動化形式證明，陶哲軒就此開啟了本次 YouTube 首秀。
通過幾次親自嘗試，陶哲軒得出了如下結(jié)論：
這種半自動化的方法適用于那些技術(shù)性強、概念性弱的論證，即那些主要關(guān)注細節(jié)準確性而非整體概念理解的證明。
并且他再一次強調(diào)，AI 輔助證明能夠把數(shù)學家從一些相對不重要的繁瑣事務(wù)中解放出來，“讓 AI 去做一些它擅長的事”。
在他看來，盡管最終的結(jié)果“并不優(yōu)雅”，但它體現(xiàn)了 AI 輔助證明的巨大潛力。
最后需要說明一下，陶哲軒并非一次就成功了。
據(jù)他在視頻中透露，前兩次的證明過程都出現(xiàn)了一些“bug”——
第一次拿到的代碼才到第 5 行他就有點看不懂了，所以選擇了重開；第二次雖然完成了所有證明（用時 48 分鐘），但由于是新人博主不太熟悉錄屏設(shè)備，導(dǎo)致屏幕分享失敗，因此又只能重來。
數(shù)學證明助手迎來 2.0 版本此外，還有他開發(fā)的數(shù)學證明助手迎來 2.0 版本升級。
根據(jù)介紹，這是一個用 Python 開發(fā)的輕量級證明助手，其功能遠遜于 Lean、Isabelle 或 Rocq 等完整證明助手，但（希望）它能夠輕松用于證明一些簡短而繁瑣的任務(wù)。
一個具體的目標是，為漸近分析提供支持。
兩周前，在大模型的幫助之下，他花了四個小時編程得到了這么一個概念驗證工具。
結(jié)果不到兩周，這個工具就迎來了全面改進 ——
首先，將其改造成一個基本的證明助手，使其能夠處理一些命題邏輯；其次，根據(jù)反饋，這個證明助手變得更為靈活（在幾個關(guān)鍵方面刻意模仿精簡證明助手）。
目前這個助手有兩種模式：假設(shè)模式和策略模式。其中策略模式作為默認模式，有點類似于 Lean、Isabelle 或 Rocq 里面那樣式兒的策略模式。
目前策略列表主要分為四類：
命題策略（主要圍繞通過布爾運算操縱命題）
線性算術(shù)策略（依賴于線性規(guī)劃及其變體）
替代策略 —— 用一個假設(shè)或目標替代另一個假設(shè)或目標的各種技術(shù)
簡化策略 —— 利用其他可用假設(shè)來“簡化”假設(shè)或目標的方法
當然這些還不是全部，這個助手支持擴展，大家可以在里面進行添加。
舉個例子。
如果 x，y，z 是正實數(shù)，且 x<2y 和 y<3z+1，證明 x<7z+2。
將它形式化就會變成：
>>>frommainimport*>>>p=linarith_exercise()Startingproof.Currentproofstate:x:pos_realy:pos_realz:pos_realh1:x<2*yh2:y<3z+1|-x<7*z+2證明助手接收到指令后，指導(dǎo)助手使用各種“策略”來簡化問題，直到問題得到解決。
那么這個問題可以通過線性算術(shù) Linarith () 求解。
>p.use(Linarith())Goalsolvedbylineararithmetic!Proofcomplete如果想要有詳細解釋，也是 OK 的：
>>>frommainimport*>>>p=linarith_exercise()Startingproof.Currentproofstate:x:pos_realy:pos_realz:pos_realh1:x<2*yh2:y<3*z+1|-x<7*z+2>>>p.use(Linarith(verbose=true))Checkingfeasibilityofthefollowinginequalities:1*z>01*x+-7*z>=21*y+-3*z<11*y>01*x>01*x+-2*y<0Infeasiblebysummingthefollowing:1*z>0multipliedby1/41*x+-7*z>=2multipliedby1/41*y+-3*z<1multipliedby-1/21*x+-2*y<0multipliedby-1/4Goalsolvedbylineararithmetic!Proofcomplete!可以看到，首先，它通過反證法進行論證，即采用否定 x≥7z+2 目標 x<7z+2 并將其添加到假設(shè)中。
然后，它將假設(shè)中所有不等式轉(zhuǎn)化為“線性規(guī)劃”形式，變量在左邊，常數(shù)在右邊。
最后，它使用精確線性規(guī)劃來尋找這些不等式的線性組合，從而導(dǎo)致荒謬的不等式，在這種情況下 0<1。
解決完問題之后，還可以使用 proof（）進行檢查。
有時候，遇到證明過程會涉及案例拆分的情況，那么證明助手最終會呈現(xiàn)樹狀結(jié)構(gòu)。
對于這個證明助手，陶哲軒表示：非常滿意，并且愿意接受進一步的建議或貢獻新的功能。比如引入新的數(shù)據(jù)類型、公例和策略，或者貢獻一些有難度的例子。
此外還計劃開發(fā)用于估算符號函數(shù)的函數(shù)空間規(guī)范的工具。例如創(chuàng)建部署霍爾德不等式和索博列夫嵌入不等式等定理的策略。看起來 sympy 框架足夠靈活，可以為這類對象創(chuàng)建更多的對象類。
感興趣的朋友，可以前往去體驗下哦。
參考鏈接：
[1]https://mathstodon.xyz/@tao/114486537464033675
[2]https://www.youtube.com/watch?v=cyyR7j2ChCI
[3]https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean
本文來自微信公眾號：量子位（ID：QbitAI），作者：白交一水
本文鏈接：http://www.tebozhan.com/showinfo-45-12809-0.html陶哲軒油管首秀：33 分鐘，AI 速證「人類需要寫滿一頁紙」的證明
聲明：本網(wǎng)頁內(nèi)容旨在傳播知識，若有侵權(quán)等問題請及時與本網(wǎng)聯(lián)系，我們將在第一時間刪除處理。郵件：2376512515@qq.com
上一篇： ChatGPT 深度研究新增導(dǎo)出為 PDF 功能，可保留報告格式
下一篇： 畢馬威：中國職場 AI 應(yīng)用率高達 93%，半數(shù)使用者達到常態(tài)化應(yīng)用水平
Copyright ? 2016-2023 天津谷騏科技有限公司 版權(quán)所有 sitemap.xml
違法及侵權(quán)請聯(lián)系：2376512515@qq.com 津ICP備18001702號
津公網(wǎng)安備 12010102000574號