BriefGPT.xyz
Mar, 2025
高效的神经子句选择强化学习
Efficient Neural Clause-Selection Reinforcement
HTML
PDF
Martin Suda
TL;DR
本文研究了子句选择在饱和定理证明中的重要性，提出了一种将子句选择框架化为强化学习任务的方法，挑战了现有的人工设计启发式方法。通过将神经网络集成至Vampire定理证明器并使用成功的证明尝试进行训练，实验结果显示该神经引导的证明器在处理新问题时的解题能力在短时间内提高了20%。
Abstract
Clause Selection
is arguably the most important choice point in saturation-based
Theorem Proving
. Framing it as a
Reinforcement Learning
(
→