點擊上方關注，All in AI中國
將統計量(例如神經網絡)和經典的"符號主義"人工智能結合起來，長期以來一直吸引著人工智能研究人員的青睞，並取得了一些非常有趣的結果。
倫敦金融科技公司（Aesthetic Integration）開發了imandra（https://imandra.ai/），這是一個自動雲原生符號推理引擎，建立在形式驗證方面的突破之上。Imandra將算法的無限狀態空間分解為有限的符號區域集合的能力為傳統符號搜索技術提供了可擴展的基礎。這種可擴展性有可能在強化學習領域釋放出巨大的能量。在這篇文章中，我們將介紹一些初步的成果。
在最近的其他文章中，我們已經看到了如何使用Imandra來設計和驗證車輛自動控制器（https://docs.imandra.ai/imandra-docs/notebooks/simple-vehicle-controller/）和RobotOS節點（https://medium.com/@kostya_81339/9f3888c5c3a1）。這篇文章展示了Imandra的另一個方面——不涉及驗證本身，而是應用了Imandra對算法可能行為的推理能力，以從根本上增強現代人工智能的統計能力。
介紹
在tabula rasa（一款射擊遊戲）中，遊戲AI取得的重大突破吸引了人們對強化學習法的關注[7]。即不使用先驗知識或啟發式的方法，而是通過自我遊戲和遊戲規則基礎知識的大量迭代來實現學習的方法。
此外，將數據驅動的學習技術與"古典"的符號化人工智能結合的想法也出現了激增[4][6]:人們正在研究輸入經典符號系統的神經網絡層，它是利用基於（純粹的）神經網絡/強化學習的方法將已知問題最小化的一種方法，即人工智能決策過程的不透明性和收斂所需的龐大訓練數據集。
這種體系結構由無模型學習器（者）和基於模型的求解器組成，這看起來非常棒。因為它呼應了認知神經科學的雙重過程理論，即學習和推理是通過：（1）快速的、感性的、直觀的和（2）緩慢的、邏輯的、分析性的 相互作用而產生的。(雖然沒有得到證實，但有證據支持這種雙重過程理論。具體內容詳見文末參考[2]，[3]。)
最新的突破(參見DeepMind AlphaZero[5])包括嵌入一個有預見性的蒙特卡羅搜索算法(MCS)訓練內循環,以快速提高學習速度和精度。
Imandra
在Aesthetic Integration中，我們開發了imandra，一個強大的自動推理引擎(屬於"經典"符號化人工智能空間)，它的許多特性包括對一種非常強大和高效的狀態空間探索的極高支持，稱為主區域分解（https://docs.imandra.ai/imandra-docs/notebooks/decomposition-flags/）。該特性允許計算給定查詢約束程序的可能唯一行為的符號表示，並對屬於每個特定區域的可能輸入值進行採樣。
當涉及到RL(強化學習)時——正如我們在下面演示的那樣，我們將環境狀態與所有可能(有效)狀態轉換一起建模為(潛在的無限)狀態機。Imandra的分解機制允許我們計算N多個符號狀態的轉變。最後一句中的"符號化"一詞是關鍵——大多數相關模型都有無限多個(或多個不可行的)可能的狀態，所以對"所有可能的"轉換進行有效的推理是非常重要的。蒙特卡羅搜索(MCS)方法也多用於計算N多個步驟，然而，他們這樣做的方式過於"天真"，很難應用到比棋盤遊戲更復雜的領域中，簡而言之，我們必須要換一種策略。這也是我們認為Imandra為可擴展的通用RL"鋪平道路"的一個關鍵原因。
相比更廣泛符號推理系統,如邏輯編程語言(如Prolog)或規則系統,Imandra可以用更高的精確度表達更加強大的概念,通過高度自動化對遞歸函數和數據類型的符號分析來換取更強大的邏輯，這是一種先進的推理技術和反例生成的搜索策略，可以完成關鍵的基本推理任務。
因此，我們認為Imandra有潛力在以下幾個領域大大擴展、補充和改進目前最先進的人工智能方案：
開發更安全的人工智能系統：航空電子、自主駕駛系統或基於統計的生物信息學等關鍵領域。人工智能或不完全搜索方法註定會以意想不到的方式運行。比如在採用詳盡的搜索方法和定量分析的情況下，時間的拖延有可能導致生命損失（https://www.reuters.com/article/us-uber-selfdriving/uber-sets-safety-review-media-report-says-software-cited-in-fatal-crash-idUSKBN1I81Z4）。而通過Imandra，我們可以使用系統狀態空間的分解來自動創建測試場景，並獲得對定量覆蓋率的度量，以幫助確定我們探索到了哪裡。這種嚴格的空間探索方法有可能帶來更加完整和安全的訓練程序。
對當前"黑匣子"方法的改進，非符號方法的推動導致了眾所周知的不透明決策過程的出現：我們可以看到一臺訓練有素的機器執行手頭的任務，但我們不知道它是如何或基於什麼完成我們訓練它做的事情。深層符號強化學習通過將高維低層原始輸入映射到低維、高度抽象的狀態空間(例如通過Imandra"合理的表示")，有可能對這種情況做出改善。
基於強化學習方法的更快收斂：雖然目前的tabula-rasa強化學習方法是完全通用的，但它需要大量的計算能力和龐大的訓練集。最近的研究表明，利用符號搜索方法可以顯著提高RL方法的收斂性，特別是在初始階段。
在這篇文章的其餘部分，我們將通過查閱最近一篇論文的結果來探索最後一種假設：在強化學習中嵌入蒙特卡羅搜索算法是如何使收斂速度加快的，並通過用Imandra替換MCS來擴展這一思想，從而加快收斂速度。
概念證明
對於我們的PoC實現，我們決定使用一個簡單的TicTacToe遊戲和一個table-based Q-learning算法來複制QM學習論文中的簡單實驗設置；我們知道這種方法不會擴展到過去的簡單遊戲中，但是我們現在的重點是先證明這個方法的可行性，然後再擴展它，因此我們不會在這篇文章中研究更復雜的基於神經網絡的方法。
我們還意識到，對於這次的研究目的而言，TicTacToe不是一個非常令人興奮的遊戲，蠻力比使用強化學習技術可以更有效地解決它，但它是一個足夠簡單的遊戲，它完美的契合這次分析的目的。此外，我們的PoC是以一種通用的遊戲方式編寫的，並且在任何2人的零和博弈遊戲中都不會有任何改變(它還可以擴展到其他有微小變化的遊戲中)。
我們對TicTacToe實現是用邏輯模式IML（https://docs.imandra.ai/imandra-docs/notebooks/logic-and-program-modes/）編寫的(Imandra具有形式語義的OCaml的純子集)，因此可以直接進行形式化分析（和"合理化推測"）。這意味著我們可以使用遊戲模型來詢問Imandra問題，或者在任意約束下枚舉可能的未來遊戲狀態。這對我們基於分解的代理來說是至關重要的。
Q(M|D)-
學習在沒有太多細節的情況下(有大量可用的[7])，Q學習背後的想法是讓代理學習在特定遊戲狀態下采取的最佳行動的策略。
以最簡單的形式(也是我們將要使用的一種形式)，Q學習對每一個人而言只是一個Q值表(長期獎勵)，用於遊戲環境中的每個
對於α∈[0，1]=學習率，γ∈[0，1]=未來獎勵的折扣因子，a範圍為"未來可用行動"和R=獎勵。
在偽碼中，整個學習算法如下所示：
如果ε-greedy是一個代理定義的函數，根據代理使用兩種不同的策略：
靜態ε-greedy定義為rand1.0<=
ε動態遞減ε-greedy定義為：
從Q到QM學習的轉變在於將第10行改為：
其中，mcs大致定義為：
通過嵌入這種蒙特卡羅搜索，我們有效地將MCTS的播出和備份階段的版本添加到Q-學習循環中。
最後，為了獲得QD學習(使用Imandra分解的Q-學習)，我們將第10行替換為：
其中idf_s大致定義為:
該算法的核心位於idf.decompose函數中。這個函數是由我們的idf_s(我們在imandra_tools筆記本中用可執行的例子編寫的)通過靜態分析我們的TicTacToe的邏輯模式實現而產生的（https://docs.imandra.ai/imandra-docs/notebooks/imandra-tools-intro/），當調用時，通過靜態分析、符號推理和代碼合成的複雜舞蹈，並返回在一個邊界條件可以到達的狀態空間的所有可能區域(在這種情況下，我們的邊界條件將是ticTactoe.is_valid_move)，利用區域對稱性，有效地"摺疊"不同的運動序列，從而產生相同的最終狀態，這樣一來就有可能減少更復雜的遊戲的探索空間。
與MCS相比，這種方法具有顯著的優勢，因為它形式簡單(正如我們前面所描述的)，確保了探索所有長度為max_lookkahead的不同路徑，以達到更好的遊戲狀態。
在更復雜的遊戲中，產生這種寬的前瞻性樹通常是不可行的，因此需要對區域進行隨機抽樣(使用MCTS中的UCT策略)，而不是對它們進行徹底的搜索，但是IDF方針仍然能夠探索比傳統MCS方法更獨特的行為區域，從而使Q代理更快地收斂。此外，即使被迫使用簡單搜索，我們的方法仍然允許我們跟蹤未探索的區域並標記它們以供將來的探索，並使用剪枝算法以獲得更好的結果。
換句話說，我們使用IDF框架作為一種完全通用的方法來生成類似MC的搜索機器，而不需要手工編碼複雜的遊戲啟發式算法或特定於遊戲的搜索算法，而是通過對遊戲規則的正式推理自動推斷它們。
基準
我們進行了6種不同的比較
Q靜態：經典ε-greedy 靜態Q代理ε
Q動態：經典ε-greedy 遞減動態Q代理ε
QM靜態：ε-greedy 靜態Q代理ε
+ 時間限制MCS
QM動態：ε-greedy 遞減動態Q代理ε
+ 時間限制MCS
QD靜態：ε-greedy 靜態Q代理ε + 移動限制分解前瞻
QD動態：ε-greedy 遞減動態Q代理ε + 移動限制分解前瞻
超參數是我們比較的QM論文中使用的參數，即：
α=0.1
γ=0.9
ε=0.3(在動態版本中為0.5)
每個代理的初始獲勝率為50%，並進行30 000次"學習"匹配，其中ε-greedy被打開，插入隨機的探索性片段(即讓代理探索新的行動路徑)，而隨後有20，000場ε-greedy的"比賽"被關閉。（也就是說，讓代理開發行為的學習路徑，而不去探索新的路徑，從而鞏固所學的知識）
上述基準證實了以下發現：在Q-學習循環中嵌入有限的搜索將導致比"純"Q-學習代理具有更快和更高的收斂速度。
它也證實了我們的假設，即將這種有限的搜索從MCS替換為基於分解的方法會導致更快和更高的收斂速度。
有趣的是，對於經典的Q和QM代理，動態ε-greedy策略雖然較慢，但容易收斂到更高的獲勝率，而QD代理則收斂到大致相同的值。這只是因為tictactoe的狀態空間很小，這導致QD玩家在狀態空間明顯增大的遊戲中並不特別受益於ε-greedy ，我們將看到QD動態代理最終收斂到比QD靜態更高的勝率。
接下來是什麼？
正如我們從這個小而獨立的PoC中看到的，我們相信，用Imandra提供的符號處理能力來增強當前最先進的RL技術可以顯著提高學習率，特別是我們認為Imandra的狀態空間分解設施是強化學習空間中的一個主要的新參與者。
一些可能的研究領域包括使用分解直接從博弈模型+當前博弈狀態中抽取Q值，以及在符號推理階段更多地利用Imandra的定理證明能力。
我們打算通過將該方法擴展到基於神經網絡的方法來進一步推進這項研究，從而超越table-based Q-learning 方法在上述PoC中的侷限性，並試圖將這種方法擴展到簡單的棋盤遊戲之外。
我們還致力於構建我們所稱的"Imandra推理器"，這是一種基於雲的、自動可伸縮的推理基礎設施， 或許是亞馬遜的lambdas解決方案，但它是為符號推理量身定製的。
參考文獻：
1. https://arxiv.org/pdf/1802.05944v2.pdf
2.https://www.sciencedirect.com/science/article/pii/001002779490018
3.https://scottbarrykaufman.com/wp-content/uploads/2014/04/dual-process-theory-Evans_Stanovich_PoPS13.pdf
4. https://www.ijcai.org/proceedings/2018/0002.pdf
5. https://arxiv.org/pdf/1712.01815.pdf
6. https://arxiv.org/pdf/1609.05518.pdf
7.http://incompleteideas.net/book/bookdraft2017nov5.pdf
閱讀更多 AI中國 的文章
