ATLAS：通过数据提升、增强和合成实现定理的自动形式化

本文研究了自然语言数学与机器可验证的形式语言配对数据稀缺的问题，提出了ATLAS框架，通过迭代数据生成来生产高质量的平行定理陈述。在经过10次迭代后，ATLAS构建了一个包含30万条定理的本科生级别数据集，并在定理翻译中取得了显著提高的准确率，推动了自动形式化的前沿研究。