用强化学习训练神经网络，提升自动定理证明中选句效率。
Efficient Neural Clause-Selection Reinforcement
- 设计高效神经网络评分模型，基于强化学习优化选句策略。
- 在TPTP基准上，解决未见问题数提升20%，限时条件下表现更优。
- 适合自动化推理、形式化验证领域研究者参考。
clause selection 是饱和式定理证明中最关键的选择点。将该问题建模为强化学习任务，可挑战现有证明器中人工设计的启发式规则，并仅通过证明过程的经验自动演化出潜在最优的替代方案。本文提出一种强大且高效的神经网络架构，用于对候选子句进行打分。遵循强化学习原则进行设计决策，将该网络集成至 Vampire 定理证明器中，并从成功的证明尝试中进行训练。在多样化的 TPTP 基准测试中，经过训练的神经引导证明器相比初始基线策略，在有限的短时间 CPU 指令限制下，解决了 20% 更多的未见问题，显示出显著性能提升。
原文摘要 · Abstract (English)
Clause selection is arguably the most important choice point in saturation-based theorem proving. Framing it as a reinforcement learning (RL) task is a way to challenge the human-designed heuristics of state-of-the-art provers and to instead automatically evolve -- just from prover experiences -- their potentially optimal replacement. In this work, we present a neural network architecture for scoring clauses for clause selection that is powerful yet efficient to evaluate. Following RL principles to make design decisions, we integrate the network into the Vampire theorem prover and train it from successful proof attempts. An experiment on the diverse TPTP benchmark finds the neurally guided prover improve over a baseline strategy, from which it initially learns -- in terms of the number of in-training-unseen problems solved under a practically relevant, short CPU instruction limit -- by 20%.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。