May, 2022
通过学习细化搜索策略来学习查找证明和定理 - 循环不变式合成的案例
Learning to Find Proofs and Theorems by Learning to Refine Search
Strategies
TL;DR我们提出了一种新的自动定理证明方法，其中使用AlphaZero风格智能体自我训练来改进表达为非确定性程序的通用高级专家策略，同时具有类似的教师代理机自我训练来生成适当相关性和难度的任务以供学习者解决，利用最小领域知识来解决合成训练数据不可用或难以合成的问题，具体举例来说，我们考虑了用于命令程序的循环不变量合成，并使用神经网络来改进教师和求解策略。