从零开始学习猜测
人工智能
2025-03-04 v1 机器学习
计算机科学中的逻辑
神经与进化计算
符号计算
摘要
我们发展了一种自学习方法，用于从源自 OEIS 的 16197 个问题中进行归纮谓词的猜测。这些问题对当今的 SMT 和 ATP 系统而言都很难解决，因为它们需要归纮推理与算术推理的结合。从零开始，我们的方法包括一个反馈回路，不断迭代：(i) 训练神经翻译器学习已解决的问题与用于它们的归纮谓词之间的对应关系，(ii) 使用训练好的神经系统为问题生成大量新的归纮谓词，(iii) 运行 z3 prover 尝试使用生成的谓词来证明这些问题，(iv) 使用诸如谓词大小和解题速度等启发式方法从已证明的问题中选择最佳谓词用于下一轮训练。该算法自行发现许多有趣的归纮谓词，最终解决了 5565 个问题，而 CVC5、Vampire 或 Z3 在 60 秒内只能解决 2265 个问题。
引用
@article{arxiv.2503.01389,
title = {Learning Conjecturing from Scratch},
author = {Thibault Gauthier and Josef Urban},
journal= {arXiv preprint arXiv:2503.01389},
year = {2025}
}