Peano：学习形式数学推理
摘要：数学推理是无法计算的，但人类常常解决新问题。此外，几个世纪以来发展的发现很快传授给后代。是什么结构使这成为可能，这如何指导自动化数学推理？我们认为，解决这两个难题的核心是数学的程序化抽象结构。我们在Khan Academy平台上对5个初等代数部分进行了案例研究。为了定义计算基础，我们引入了Peano，一个定理证明环境，其中任何时刻的有效操作集是有限的。我们使用Peano来形式化引导代数问题和公理，从而得到明确定义的搜索问题。我们观察到，现有的符号推理的强化学习方法不能解决更难的问题。通过添加从自身解决方案中诱导可复用抽象（“策略”）的能力，一个智能体能够稳定进展，解决所有问题。此外，这些抽象在训练过程中以随机方式引导问题的顺序。所恢复的顺序与专家设计的Khan Academy课程具有显著一致性，并且在恢复的课程上训练的第二代智能体学习速度明显更快。这些结果说明了抽象和课程在数学文化传播中的协同作用。
作者：Gabriel Poesia and Noah D. Goodman
论文ID：2211.15864
分类：Artificial Intelligence
分类简称：cs.AI
提交时间：2023-06-21