勁爆！有人不用深度學習作強AI?道翰天瓊認知智能機器人平臺API接口大腦爲您揭祕-6

認知智能是計算機科學的一個分支科學，是智能科學發展的高級階段，它以人類認知體系爲基礎，以模仿人類核心能力爲目標，以信息的理解、存儲、應用爲研究方向，以感知信息的深度理解和天然語言信息的深度理解爲突破口，以跨學科理論體系爲指導，從而造成的新一代理論、技術及應用系統的技術科學。 認知智能的核心研究範疇包括：1.宇宙、信息、大腦三者關係；2.人類大腦結構、功能、機制；3.哲學體系、文科體系、理科體系；4.認知融通、智慧融通、雙腦(人腦和電腦)融通等核心體系。 認知智能四步走：1.認知宇宙世界。支撐理論體系有三體（宇宙、信息、大腦）論、易道論、存在論、本體論、認知論、融智學、HNC 等理論體系；2.清楚人腦結構、功能、機制。支撐學科有腦科學、心理學、邏輯學、情感學、生物學、化學等學科。3.清楚信息內涵規律規則。支撐學科有符號學、語言學、認知語言學、形式語言學等學科。4.系統落地能力。支撐學科有計算機科學、數學等學科。
認知智能CI機器人是杭州道翰天瓊智能科技有限公司旗下產品。認知智能機器人是依託道翰天瓊10年研發的認知智能CI體系爲核心而打造的認知智能機器人大腦，是全球第一個認知智能機器人大腦。具備突破性，創新性，領航性。是新一代智能認知智能的最好的產品支撐。 認知智能機器人技術體系更加先進，更加智能，是新一代智能，認知智能領域世界範圍內惟一的認知智能機器人。 認知智能機器人是新時代的產物，是新一代智能認知智能的產物。表明了新一代智能認知智能最核心的優點。和人工智能機器人大腦相比，優點很是明顯。智能度高，客戶粘性大，客戶滿意度高，易於推廣和傳播等核心特色。 依託認知智能機器人平臺提供的機器人大腦服務，能夠賦能各個行業，各個領域的智能設備，各種須要人機互動的領域等。認知智能機器人平臺網址：www.weilaitec.com，www.citec.top。歡迎註冊使用，走進更智能機器人世界。
認知智能和人工智能的優劣勢對比主要能夠分爲四大方面： 第一：時代發展不一樣。人工智能是智能時代發展的第二個階段，認知智能是智能時代發展的第三個階段。時代發展上決定了認知智能更顯具備時代領先性。 第二：基礎理論體系不一樣。人工智能的基礎理論體系以數學爲基礎，以統計機率體系爲基礎。認知智能基礎理論體系以交叉許可理論體系爲基礎。包含古今中外哲學體系，心理學體系，邏輯學體系，語言學體系，符號學體系，數學體系等學科。其基礎理論體系更加具備創新性，突破性和領先性。且交叉學科理論體系的研究也是將來智能發展的大方向。其具體理論體系，還包含三體論（宇宙，信息，大腦三者關係），融智學，和HNC等。 第三：技術體系不一樣。人工智能的核心技術體系主要是算法，機器學習，深度學習，知識圖譜等。其主要功用在感知智能。感知智能其核心主要是在模仿人類的感知能力。認知智能的核心技術體系是以交叉學科理論體系而衍生出來的。具體包含三大核心技術體系，認知維度，類腦模型和萬維圖譜。認知智能的技術體系核心以類腦的認知體系爲基礎。以全方位模仿類腦能力爲目標。人工智能以感知智能爲基礎的體系，只能做爲認知智能中的類腦模型技術體系中的感知層技術體系。類腦模型大體包含，感知層，記憶層，學習層，理解層，認知層，邏輯層，情感層，溝通層，意識層等9大核心技術層。所以人工智能的核心只是做爲認知智能類腦模型中的感知層。所以在技術體系上，人工智能和認知智能基本上沒有太多的可比性。 第四：智能度成本等方面的不一樣：人工智能產品的綜合智能程度，廣泛在2-3歲左右的智力水平。認知智能產品其智能程度大體在5-8歲左右。認知智能體系構建的機器人更加智能。且更省時間，更省人力和資金。優點很是多。具體請看下列的逐項對比。
AI 這個詞被偷走了。
圖靈獎得主Alan Kay在智源大會上曾經這樣說：由於在深度學習帶來人工智能的一波熱潮下，不少人被誤導，認爲人工智能就等於機器學習。而事實上，機器學習只是整個智能研究中的子領域。
所以，咱們始終要意識到，儘管機器學習在近十年取得了使人矚目的成就，但在此以外，仍有大量值得深度探究的其餘人工智能研究。
例如：布爾可知足性問題（Boolean satisfiability problem，SAT）。
SAT ，即肯定是否存在知足給定布爾公式的解的問題。舉例來講，針對公式「a AND NOT b」，詢問是否存在一個 a 和 b 的解，可以使公式爲真，若是存在，則說這個公式可知足；反之，則稱不知足。例如「a AND NOT a」即是不知足的，由於不存在一個 a 的解使公式爲真。
SAT 研究的重要性，不言而喻。首先，SAT是人工智能領域自動推理中的一個經典問題，也是歷史上第一個被證實爲 NP 徹底的問題。其次，在工業領域（尤爲是軟硬件驗證中），SAT求解器具備普遍的應用，例如Intel芯片和Windows操做系統驗證中都用到了SAT求解器。
在深度學習所遇挑戰愈發艱難之際，事實上，咱們須要回過頭來，去看看人工智能的其餘領域的研究，特別是包含着人類知識的研究方向，將這些研究與以深度學習爲表明的機器學習方法進行結合，從而創造出下一代具備知識的人工智能算法。同時也只有從一個全面的角度，才能認清人工智能的全貌，而不被深度學習這「一葉」而障了目。
智源針對SAT的研究及發展，與中科院軟件所研究員蔡少偉進行了一次深度對話，從中或可一窺 SAT 研究的進展及社羣現狀。
蔡少偉，是國內少有的幾位對 SAT 有較深刻研究的學者之一。他在近日與其博士生張昕荻共同開發的SAT 求解器在SAT Competition 2020比賽中得到了Main Track SAT冠軍。此外，蔡少偉團隊也曾得到SAT Competition 201四、2016亞軍和20十二、2018冠軍的獎項，以及2018年聯合邏輯奧林匹克金牌。他所提出的約束求解技術和研製的SAT求解器被分別應用於微軟Azure雲平臺的虛擬機預配置和異常檢測、騰訊地圖優化以及美聯邦通訊委員會的頻譜分配等項目中。
Q1：恭喜你再次得到SAT國際比賽冠軍。就布爾可知足性問題（SAT）而言，目前你們彷佛還比較陌生。你能不能先介紹一下？
蔡少偉：SAT也稱爲命題邏輯公式可知足性問題，就是要判斷一個命題邏輯公式是否可知足，也便是否存在對該公式變量的一組賦值，使得公式爲真。由於命題邏輯公式的變量都是布爾變量，因此經常稱爲布爾可知足性問題。
Q2：斷定一個命題是否可知足頗有意思，但從問題研究自己以及工業應用來講，它有什麼意義呢？
蔡少偉：要談SAT的意義，得先認識到 SAT不只僅是一個具體問題，它是個元問題，表明一種解決問題的思路。
SAT是用布爾邏輯表達的，是很是底層的表達，這使得它在理論和實踐上都有很普遍的意義。當時SAT被證實爲NP徹底問題，就是從圖靈機的角度去證實的。這是第一個被證實爲NP徹底的問題，是NP徹底性理論的種子問題。不少漂亮的複雜性理論結果都和SAT有關係，隨機SAT和統計物理也有密切關係。

另外一方面，SAT是有普遍應用的，好比軟硬件驗證，數學定理的自動證實，密碼學，資源配置，生物計算，等等。SAT是軟硬件驗證的基礎引擎，像NASA，Intel，微軟這些巨頭都用到了SAT求解器去作相關的事情。
Q3：能不能從歷史角度，介紹一下SAT研究經歷過哪些階段？每一個階段表明性方法及特色是什麼？
蔡少偉：SAT研究涵蓋面比較大，我就從SAT算法相關的研究歷史講吧，比較粗糙的分能夠分爲三個階段。
早期階段（1960-1990）: 通常認爲SAT算法能夠追溯到1960年Davis和Putnam提出的DP過程以及後來的DPLL。這也是機器定理證實歷史上的一個重要工做。1971年，SAT被證實爲NP徹底問題，這是另外一個重要的事情，在這以後有不少複雜性方面的工做。這個時期的研究比較集中在歸結原理和複雜度研究，也包括易解子類好比2SAT和Horn SAT的研究。
快速發展階段（1990-2010）：這個階段SAT求解的研究有了巨大的進展，目前經常使用的SAT方法包括衝突分析子句學習（簡稱CDCL）方法和局部搜索方法都是在90年代提出的。
1992年，Seman和Gu幾乎同時開啓了SAT的局部搜索算法研究，GSAT算法在幾個典型的問題包括N皇后和圖着色等問題上比DPLL算法取得了更好的效果，也引發了AI領域啓發式搜索社羣的興趣，以後出現了各類SAT局部搜索算法，華裔法國教授Chumin Li老師在這方面作了一些有影響的工做。
CDCL方法是在90年代中期提出的，主要特色是非時序回溯和子句學習，以後從算法和數據結構都有一些改進的工做。在這方面有一個典型的求解器MiniSAT，2003年研發的，後來有持續改進，基本實現了CDCL的主要技術。
另外一個典型求解器就是Glucose，提出了文字區塊距離，從學習子句的管理方面對CDCL作了進一步改進。這期間，SAT求解器的應用也獲得普遍推廣。
此外，研究人員對一類特殊的SAT問題有較高的興趣，就是隨機k-SAT問題，尤爲是對相變現象的研究以及對相變區隨機k-SAT的算法研究，從理論上和求解算法上都有很多工做，有一個基於統計物理的Survey Propagation方法在求解相變區的隨機3-SAT問題有很好的效果。
現代階段（2010至今）：2010年先後，曾經一度SAT求解的進展近乎停滯，很多人也以爲這個方向發展了那麼多年了，應該很難突破了。確實，通過快速發展的20年以後，SAT求解要進一步改進的難度更大了。
或許是停滯的期間激發了新的探索，2012年至2015年這幾年期間，出現了一批新的局部搜索SAT算法，由於採用的技術和以前的有較大不一樣且性能上有大幅度提高，在文獻中經常被稱爲現代局部搜索求解器，主要包括格局檢測方法和機率分佈方法，對應的表明性算法分別是CCASat（這也是我拿到SAT比賽第一個冠軍的算法）和ProbSAT。
在CDCL方面，對於學習子句的管理更加精緻了，而且開始有研究利用機器學習方法來改進算法的啓發式，表明工做是Maple算法用MAB多臂賭博機方法來改進分支啓發式。
另外，局部搜索和CDCL的結合引發了愈來愈多的興趣，尤爲是最近3年，這方面的研究愈來愈深刻，今年的SAT比賽中Main track的前三名都結合了這兩種方法。這個方向還不是很成熟，但已經顯出其潛力，我相信在接下來幾年是SAT求解的一個主要方向。
除了這兩個主要方法的發展，SAT並行處理也有了較大進展，主要是Cube-and-Conquer方法。算法選擇器和自動算法配置也被引入來提升SAT求解，它們是對已有的SAT算法經過機器學習方法進行算法或策略的自動選擇，更多的是從工程的角度去研究，SAT社羣通常把它們和核心算法區分開。此外，SAT社羣對SAT應用的重視達到了新的高度，這也能夠從最近幾年發表的論文看出來，從數學定理，經濟學定理的自動證實，到頻譜分配等和軟件驗證等實際項目，能夠愈來愈多地看到SAT求解的應用，論文中的實驗也更加側重於現實數據。
Q4：你剛纔提到「SAT社羣」。如今以深度學習爲表明的機器學習社羣已經達到幾百萬的規模。那麼，研究 SAT 問題的社羣目前有多大呢？
蔡少偉：這個沒有去認真統計過，也很難統計，只能從相關會議的人數和文獻的數量去估計，但有很多作這方面研究的人可能好久發一篇論文。目前SAT會議每一年大概100多人，另外SAT研究的論文也主要出如今CP（約束求解領域的會議，今年錄用55篇論文）和IJCAI，AAAI等會議的相應session。總的來講，和目前比較熱的機器學習方向相比，SAT社羣要小不少。 
從分佈上看，最主要是歐洲，包括德國，法國，奧地利，英國，芬蘭，西班牙等，歐洲向來有邏輯和形式化的傳統，在這方面一直保持的挺好，緊接着是北美（美國和加拿大），而後，亞太地區包括中國，日本，澳大利亞，新加坡等也作，可是規模小一些。
中國在這方面的社羣應該說沒有造成，作的人太少了，比較零散，學生們大都不肯意作這種偏邏輯和傳統算法的方向，多是受到發論文和找工做的壓力的影響，不過最近幾年仍是慢慢有一些人加入進來作，我以爲有個好的趨勢。

Q5：SAT比賽應該是研究SAT問題的研究者一個主要集散地了，從2002年至今，國際 SAT 學會已經舉辦了13屆SAT比賽。這個比賽對SAT社區產生了哪些有價值的影響？
蔡少偉：舉辦SAT比賽，一個是爲了促進SAT求解的進展，一個也是促進SAT應用，每屆比賽都會鼓勵你們提交從現實應用編碼過來的SAT問題提交做爲比賽的測試集。
我以爲SAT比賽帶來的價值是多方面的。首先是促進SAT算法的研究，不只是促進你們去改進算法，並且參加比賽的代碼大部分時候是要求開源的，這也促進你們互相學習（互相競爭），每每前一屆比賽的冠軍到了下一屆都難以保持前三名。這對學生是個很好的事情，有充分的資源能夠學習。
固然，也提升了SAT社羣的凝聚力和知名度，而且向工業界隨時反饋最新進展，SAT會議上也有很多來自工業界的人員去參與，去聽取最新進展，也促進了SAT求解器在工業界的應用。
Q6：這頗有意思。SAT 比賽的評比過程怎樣？
蔡少偉：每屆比賽通常是在4，5月份截至求解器的提交，沒有限定你的研發時間，只要在截至時間以前提交到比賽指定的平臺便可，同時也會徵集比賽的測試集，舉辦方也會本身生成測試集並從提交的測試集裏面挑選一些做爲比賽測試集。
比賽測試集只有在賽後纔會公佈，每屆比賽的測試集是不同的。測試集來自數學問題和工業問題編碼過來的SAT問題。
當比賽提交的截至日期到了以後，組織方就會進行實驗，對提交的求解器進行評估，評估的標準主要是以給定的時間限制（好比5000秒）求解的問題個數爲主，也參考求解時間。比賽結果會在當年的SAT會議上公佈。
Q7：咱們注意到，從2012年起，你幾乎每屆都得到過冠/亞軍。在每一年比賽中，所使用的方法有哪些變化？並且咱們也比較好奇，你每屆都能獲獎的祕訣是什麼？
蔡少偉：其實也沒有每屆都得到過冠/亞軍，好比我在2013年SAT比賽就沒得獎。SAT Competition有時候是一年辦一次，有時候是兩年辦一次，中間一年多是一個稱爲SAT Race的活動。不過比較好的一件事是，從2012年起每一屆SAT比賽都有獲獎求解器是用到個人方法開發的。
在比較早的幾屆，也就是從2012到2016那幾年，個人SAT求解器主要是局部搜索求解器；從2018年開始，我主要研究對CDCL求解器的改進，這幾年主要的方法是我在2018年提出來的鬆弛CDCL方法，2018和2020我得到冠軍的求解器都是基於該方法研發的。
說實話，我沒發現什麼獲獎的祕訣。每一屆比賽的結果公佈以前，我都不知道本身會不會得獎，因此每次到了公佈結果的時候仍然會激動。我惟一確定的就是，我在這個方向付出了持續不斷的努力。從我本科二年級2006年第一次接觸SAT問題，我就開始喜歡這個問題，一直作到如今。如今我帶着一個博士生作這個方向，我也提醒他，這個方向的前期須要積累比較長的時間，會比較辛苦，不要羨慕其餘同窗發論文，咱們作的事比發論文更有意義。
Q8：你在 SAT 上的研究有哪些實際應用？以及你比較關心的實際應用是哪些？
蔡少偉：咱們的SAT求解器被實際項目直接調用的，我知道的有美聯邦通信委員會的頻譜分配項目，意大利銀行ARC系統優化，以及MIT的新型材料研究項目，若是說到相關方法的應用，還包括騰訊地圖優化和微軟Azure雲平臺裏虛擬機預配置用到的約束求解算法等。
目前我更加關心SAT求解在芯片驗證上的應用，實際上最近咱們正在跟國內這方面的主要企業討論這方面的事情，也作了一些初步的實驗，但願有機會能爲我國的芯片事業貢獻微薄的力量。
Q9：我看到你以前提到，你在人工智能和算法設計有着比較普遍的興趣。那麼在這些方面，你研究思路是什麼呢？
蔡少偉：人工智能是很大的領域，不一樣方法擅長求解不一樣類型的問題。不過如今可能不少人以爲人工智能和機器學習是同義詞，他們可能不知道人工智能還有約束求解和自動推理這些方向。我本身會堅持作約束求解和自動推理這些偏向於符號主義的方向。我感受機器學習更適合於感知任務，而基於邏輯和約束的方法在認知層次會更合適一些。固然，不一樣的方法其實能夠互相借鑑，相互融合，我相信機器學習方法能夠用來提升約束求解方法。但我傾向於相信在這方面比較好的途徑是，將人類經驗知識（好比成功的算法框架/方法）和機器學習進行結合。

此外，作求解器就是作工具，老是要找到實際問題去發揮它的價值，不少智能應用的底層都涉及到複雜的約束問題，咱們作的研究處於人工智能比較底層的研究。
在算法設計方面，我一直比較關心的一個事情就是，如何縮小理論算法/複雜度理論和實驗算法之間的距離。從現狀上，這個距離能夠稱得上是鴻溝了。理論算法有漂亮的理論結果，可是實際應用的時候卻不多有效解決問題，而實驗算法好比SAT求解器能夠很好解決實際問題，可是缺少理論上的理解。這須要兩個方向的人互相交流合做，然而這正是目前比較缺少的。我和幾個朋友組織了一個研討會，是關於難解問題的理論、算法和應用，也是想促進這個事情。我和北航的許可老師就這個問題討論過不少次，談到目前對算法的分析方法也許須要作出調整，好比理論上認爲比較難的最大團問題，在實際中一些幾千萬點的大圖上卻能夠在幾秒鐘精確求解，由於具體問題的難度不只和規模有關，也和問題的結構有關，直觀上是很容易理解的事情，可是如何作就不知道了。理論算法和實驗算法在思路上有時候也是能夠互相啓發的，好比我在SAT方面有一個關於「關鍵子句」方面的想法，就是受到一個SAT理論算法PPSZ的啓發。上次陸品燕老師跟我討論時也提到他在考慮如何將近似算法的方法用於啓發式算法，我以爲很高興，越多人重視這個問題，那麼就越早有進展。
Q10：很棒，最後問一個比較寬泛的問題。你以爲作學術研究，最重要的品質是什麼？
蔡少偉：我以爲本身仍是學術界的學生，如今還不適合來回答這個問題。我只知道，作學術研究，內心得有學術，「要保守你的心，賽過保守一切。」