炼金术：通过符号变异提升定理证明能力
原文中文，约300字，阅读约需1分钟。发表于：。本研究解决了神经定理证明（NTP）中可用正式数据匮乏的问题，提出了一种名为“炼金术”的数据合成框架。该方法通过符号变异生成新的定理，将Mathlib中的定理数量提升至600万，从而有效增强了大型语言模型在定理证明任务中的表现。
该研究通过结合学习和定理证明的方法，大幅提升了E自动定理证明器在Isabelle Sledgehammer问题上的性能。利用ENIGMA指导、神经前提选择和E的策略开发，系统在15秒内性能提升25.3%，超越所有之前的ATP和SMT系统。该方法可用于大规模问题的迭代训练。
