北大團隊搞定ChatGPT都頭痛的算法優化，普通筆電就能跑

衡宇 蕭簫 發自 凹非寺

量子位 | 公眾號 QbitAI

連ChatGPT看了都直搖頭的算法優化，被北大團隊給搞定了。

測試表明，新研究能解驗證集中90%的題目，包括NOIP、Codeforce、Leetcode等比賽中的分治和動態規劃題目——這些題目，很多大模型也難以解決。

而且自家的普通筆電就能跑！

畢竟算法優化這塊，是大模型乃至整個AI的能力盲區。

哪怕是Nature刊發過的DeepMind AlphaTensor，給程序合成領域帶來一些震撼不假，但實際作用對業內專業人士來說，“還是不夠”。

所以，AI無法橫掃到的這個領域，算法優化該咋提速提效？

北大一支團隊，采取程序演算和程序枚舉相結合的辦法，做出了兩套算法優化軟件。

一套可以搞定分治、并行化、增量計算、線段樹等算法的優化，另一套則支持動態規劃算法的優化。

介紹動態規劃算法的綜合方法一篇（《Synthesizing Efficient Memoization Algorithms 》），已經被程序設計語言領域三大頂會之一的OOPSLA’23接收；另一篇關于分治類算法的論文也已經在arXiv（2202.12193）公開。

而且這兩套軟件需要的硬件門檻并不高，Intel Core i7-8700 3.2GHz 6核處理器就能跑，平均用時6.53s。

據悉，這兩套軟件未來都會開源，還會做成更易用的服務，放到網上。

有些神奇的事是，兩篇論文共同的作者之一，北大副教授熊英飛，之前一度專研在AI領域，首次用CNN實現爐石傳說的代碼，就出自他之手。

帶著好奇，我們和熊英飛本人聊了聊。

為什么AI設計算法還不行？

算法設計，需要給出滿足規約的程序，并且在時間和空間復雜度上盡量優化。

大模型的進展有目共睹，因此，在“轉向”之前，熊英飛和團隊確實也想過用ChatGPT來搞算法設計。

（包括Copilot等代碼補全和其他AI技術在內，他們將所有會寫程序的AI都試了一遍，感覺ChatGPT最好用）

但即使是ChatGPT，在搞算法設計時也還是會出bug。

例如，將一些經典任務交給ChatGPT，它能很好地完成，如求解一個背包問題；但一旦對經典問題進行小改動，比如讓物品重量和價值從其他屬性組合得到，它輸出的代碼就會“一團亂”，完全沒法用。

其關鍵原因，在于算法設計需要在程序語法語義、算法設計模式、算法復雜度分析等一系列專業知識的基礎上，進行嚴密的邏輯推理。

現在，大模型主要在大量程序上做訓練，很難僅靠訓練就重新發現這些人類頂尖科學家研究了數十年的知識。

同時，雖然大模型具有少量分析能力，但要進行復雜和嚴謹的邏輯推理，在現在的神經網絡架構下還存在困難。

這樣寫出來的代碼，“即使跑得通，公司也不敢用”，因為修bug的成本可能比寫bug還高（手動狗頭）。

所以，有沒有什么方法可以解決這個問題？

熊英飛表示，團隊其實兩種思路都在嘗試，包括“用AI”和“不用AI”的。

一方面，他們訓練了一個幾億參數的小模型，也在嘗試使用AI來生成代碼，同時也在思考AI和常規方法結合的來保證代碼正確性的途徑；

另一方面，團隊也嘗試將之前業界已有的兩種方法結合起來，結果發現效果不僅比現在的AI方法更好，而且速度上也要更快。

所以，這種神奇的新思路究竟是什么？

先“找規律”，再“暴力窮舉”

具體來說，熊英飛團隊采用的新思路，結合了程序演算和程序枚舉兩種方法。

程序演算方法，簡單來說就是“找規律”。

目前針對算法，已經有人總結出了許多不同的設計模式，有點像是一套代碼設計經驗的總結。

設計模式包含了許多算法優化相關的程序變換規則，類比到解方程中，就是左右加減移項、以及兩邊同乘同除等技巧。

算法優化也和解方程一樣，雖然我們能學會不同的變換規則，但真正到了解決復雜問題的時候，還是得自己運用這套規則來對程序求解。

這種方法就和做數學題一樣，需要用到一些“程序員的智慧”。但如果程序員想不到更好的解決方法怎么辦呢？

因此，除了程序演算，此前還有一種思路是程序枚舉，顧名思義就是“暴力窮舉”。

這種方法就是讓電腦去試所有可能的程序，經過驗證后，總有一個程序是對的。例如給變量x和y，計算機就會嘗試x+y，x-y……

但這種方法同樣存在一個問題，就是雖然計算機很快，但世界上所有的程序太多了，而且基本上隨著程序長度增加呈指數型增長。

因此，直接暴力窮舉，對于計算機來說同樣是不可能的。

為此，熊英飛團隊結合這兩種思路，設計了一種新的算法優化方法。

簡單來說，就是先基于程序演算的思路，將問題縮小到只需要用程序去填寫幾個關鍵程序的情況，就像給“完形填空”挖空一樣。

然后，用窮舉法列舉需要“填空”的程序，最終驗證得到結果。

當然，這里面也用到了一些近似的技術，因為理論上，形式化規約無法完全和需要“填空”的部分對應起來，要填空的地方肯定也和其他地方有條件關系。

因此針對這種問題，團隊也設計了一些技巧，確保在一定概率下這種方式不會出錯。

相比AI而言，這種思路設計出來的算法優化軟件，不僅正確率更高，解題過程也要更快。

目前，團隊設計出了兩套算法優化軟件AutoLifter和SynMem。

其中AutoLifter支持分治、并行化、增量計算、單通道、流算法、線段樹等算法的優化，SynMem則支持動態規劃算法的優化。

所以，這兩套算法優化軟件的效果究竟如何？

團隊從Codeforces、NOIP全國青少年信息學奧林匹克聯賽、Leetcode上收集了所支持算法對應的題目，對兩套方法進行了測試

其中，在分治類的96個算法問題中，AutoLifter解出來了82題，相比之下另兩種此前最好的程序合成方法，只解出來不到一半。

硬件要求也不高，只需要Intel Core i7-8700 3.2GHz 6核處理器就能跑，平均用時在6.53秒左右。

在40道動態規劃題目上，團隊解出來了37道，而且平均用時僅僅1.87秒?（相比之下另外兩種方法幾乎沒有解出來多少）：

這兩套軟件，團隊在未來都會開源，也會做成更方便使用的服務放到網上。

熊英飛表示，最終的目標是希望做出一套軟件，能自動檢測到代碼中需要優化的算法，然后軟件自動將它們優化起來。

以App為例，即使啥都不做，用上這套算法后，對應的APP運行速度也能大幅增加。

當然，達成這一目標，可能還需要一段時間。

“發Nature耽誤拿獎學金了”

AutoLifter這項工作背后的論文，是熊英飛團隊3年前就開始的算法合成項目，完成的第一篇論文。

熊英飛給出的原因是之前的方法堪稱“理論大合集”，不僅有程序合成，還加上了程序演算、范疇論、概率論、隨機算法……總之，整篇論文充滿了數學符號。

“這樣一來，要找到合適的審稿人比較難。”熊英飛表示，2年間刪刪改改，現在論文已經是一個“不依賴于特定領域的符號，基本大家都能讀懂的樣子了”。

交流期間，量子位問了句題外話，AlphaTensor能發Nature，咱們的論文2年沒被頂會接收，沒考慮過投投Nature？

熊老師開玩笑地回應道：

我也勸我的博士生，不要跟程序設計頂會較勁，發篇Nature影響多大啊！試著投一下也不會掉塊肉。

你知道他們怎么說？“不行，我要趕緊（在專業領域）發出來，不然明年獎學金沒了！”

玩笑歸玩笑，言歸正傳，介紹一下AutoLifter和SynMem兩項工作的論文一作，兩位都是算法競賽圈的知名選手。

吉如一，AutoLifter工作論文一作。

北京大學編程語言實驗室（PLL）博四在讀，研究方向是程序合成，導師為胡振江和熊英飛。

2016年，吉如一以全國青少年信息學奧林匹克競賽金牌獲得者保送北大信息科學與技術學院，后成為北大第一屆圖靈班的一員。

曾擔任ACM大賽北大隊隊長，第二次參賽時帶隊獲得金牌和全球第三、亞洲第一的成績。同時也是北京大學學生算法協會的創始人和第一任主席，人送外號“吉老師”。

孫奕燦，SynMem一作。

北京大學編程語言實驗室（PLL）博三在讀，指導教師為熊英飛。

他同樣是全國青少年信息學奧林匹克競賽金牌保送北京大學。

他的研究方向為程序合成、決策過程和概率程序驗證，也做過一些關于參數化復雜度制度下的不可近似性的工作。

本科時，他就讀于北京大學EECS學院圖靈班。他曾以共同一作的身份在編程語言的頂級會議PLDI上發表論文，并且有其它工作發表在編程語言頂級會議OOPSLA和人工智能頂級會議AAAI上。

兩篇論文的共同作者熊英飛，是上述二人的博士指導老師。

他的身份是北大信息科學技術學院軟件工程研究所長聘副教授、研究員，分別在電子科技大學、北京大學、日本東京大學獲得本碩博學位。

除了本文提到的程序合成，熊英飛的主要研究方向之一就還有缺陷修復領域，這也是他和所在組長期以來做的一項工作。

缺陷修復，俗稱修bug，他做的工作還是自動修bug。

具體而言就是先讀程序，分析出程序有哪些地方需要改，然后想出一個新的程序的寫法。

熊英飛和團隊提出的理論、方法和技術中，基于差別的修復模型已經成為演化缺陷領域廣泛使用的模型之一，而基于統計的缺陷修復技術將程序缺陷修復的準確率提升約40%。

采用他們工作的公司，包括華為、Linux內核配置項目等。

之所以能達到這樣的效果，熊英飛介紹道，是因為團隊是最早把概率引導傳統程序合成中的研究隊伍之一。

這項發表在2017年的工作，通過統計引導程序合成，把缺陷修復正確率最高水平從40%拉到了70%。

有意思的是，此后許多研究機構都開始從概率統計和傳統機器學習下手研究程序合成，但那時的熊英飛團隊，卻轉而琢磨如何利用深度學習做程序合成。

2018年，他們發表一篇論文，提出基于語法的結構化CNN代碼生成器，用《爐石傳說》基準數據集進行實驗。

結果表明，準確性明顯優于以往最先進的方法5個百分點。

這篇論文最后被AAAI 2019收錄，論文中表示，他們是第一個成功將CNN解碼器用于代碼生成的團隊。

2019年，團隊又用Transformer替換了CNN解碼器，準確性再次提升約5個百分點。熊英飛笑道，一不小心做了最早應用Transformer生成代碼的工作，“見證了歷史”。

等到了2021年，團隊再把上面的工作結合了基于差別的修復模型，做了一個缺陷修復工作。“那次就是深度學習修bug能力首次超過了傳統技術。”熊英飛說。

不過略戲劇的是，等學界多數團隊開始用深度學習來做程序合成、缺陷修復時，熊英飛團隊又開始專研傳統方法去了——結果就是，本文提到的兩套算法優化軟件誕生了。

聽起來，他們團隊在研究程序合成這條路上，頗有種“不管黑貓白貓”的精神。

還有一種大家一起摸魚的傳統美德：

其實算法優化軟件暑期8月就該上線的，不過大伙兒都在摸魚哈哈。

Fine，現在已經是11月了，不知道團隊的摸夠了沒有哇？doge