让AI从零自学归纳推理，自动发现数学归纳法关键条件。
Learning Conjecturing from Scratch
- 用神经翻译器学习问题与归纳谓词的对应关系，通过反馈循环迭代优化。
- 自动生成新归纳谓词，成功解决5565个难题，远超传统工具的2265个。
- 适合对自动化定理证明、形式化推理感兴趣的研究人员。
我们提出一种自学习方法，用于在来自OEIS的16197个问题数据集上推断归纳谓词。这些问题对当前的SMT和ATP系统而言极具挑战性，因其需结合归纳与算术推理。该方法从零开始，通过反馈循环实现：(i) 训练神经翻译器以学习已解问题与其有用归纳谓词之间的映射；(ii) 利用训练好的神经模型为问题生成大量新的归纳谓词；(iii) 快速调用z3求解器尝试用生成的谓词证明问题；(iv) 基于谓词大小和求解速度等启发式策略，从成功证明的问题中选择最优谓词进入下一轮训练。该算法自主发现了大量有趣的归纳谓词，最终解决了5565个问题，显著超过CVC5、Vampire或Z3在60秒内各自解决的2265个问题。
原文摘要 · Abstract (English)
We develop a self-learning approach for conjecturing of induction predicates on a dataset of 16197 problems derived from the OEIS. These problems are hard for today's SMT and ATP systems because they require a combination of inductive and arithmetical reasoning. Starting from scratch, our approach consists of a feedback loop that iterates between (i) training a neural translator to learn the correspondence between the problems solved so far and the induction predicates useful for them, (ii) using the trained neural system to generate many new induction predicates for the problems, (iii) fast runs of the z3 prover attempting to prove the problems using the generated predicates, (iv) using heuristics such as predicate size and solution speed on the proved problems to choose the best predicates for the next iteration of training. The algorithm discovers on its own many interesting induction predicates, ultimately solving 5565 problems, compared to 2265 problems solved by CVC5, Vampire or Z3 in 60 seconds.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。