MathZero、分类问题与会集依赖类型论
计算机科学中的逻辑
2020-05-19 v2 人工智能
摘要
AlphaZero 仅给定游戏规则，便通过自我对弈以超人水平学会下围棋、国际象棋和将棋。这引发了一个问题：类似的事情能否在数学领域实现——即一个 MathZero。MathZero 将需要一个形式化基础和一个目标。我们提出以会集依赖类型论(set-theoretic dependent type theory)为基础，并以分类问题——即按同构对概念实例进行分类的问题——来定义目标。自然数作为有限集会集分类问题的解而出现。在此我们将经典的 Bourbaki 会集论同构推广到会集依赖类型论。据我们所知，我们给出了首个带有命题性会集相等的会集依赖类型论的同构推理规则。本文的表述旨在使此前未接触过类型论的数学家也能读懂。
引用
@article{arxiv.2005.05512,
title = {MathZero, The Classification Problem, and Set-Theoretic Type Theory},
author = {David McAllester},
journal= {arXiv preprint arXiv:2005.05512},
year = {2020}
}