連 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，現在已經是 10 月了，不知道團隊的摸夠了沒有哇？doge
