数学博弈
人工智能
2023-09-25 v1
摘要
蒙特卡洛树搜索可用于自动定理证明。Holophrasm是一种神经定理证明器，将MCTS与用于策略和评估的神经网络相结合。本文中，我们提出使用其他博弈树搜索算法来提升Holophrasm定理证明器的性能。
引用
@article{arxiv.2309.12711,
title = {The Mathematical Game},
author = {Marc Pierre and Quentin Cohen-Solal and Tristan Cazenave},
journal= {arXiv preprint arXiv:2309.12711},
year = {2023}
}