将统计量(例如神经网络)和经典的\"大众符号主义\"大众人工智能结合起来，长期以来一贯吸引着人工智能研究职员的青睐，并取得了一些非常有趣的结果。
伦敦金融科技公司（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值表(长期褒奖)，用于游戏环境中的每个<state，action>，这个表可以利用下列Bellman方程更新：
对付α∈[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