基于Imandra的深度强化学习手把手教你给游戏“开挂”！
点击上方关注，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值表(长期奖励)，用于游戏环境中的每个<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
