autoformalization

MathAtlas 是一个针对研究生级别数学的自动形式化的大规模基准测试，包含从103本教科书中提取的约5.2万个定理和定义，并附带一个包含约17.8万条关系的数学依赖图。实验表明，最先进的模型正确率最高仅为9.8%，凸显了其难度。