MUSTARDSAUCE 数学定理问题数据集

来自香港城市大学、中山大学、华为诺亚方舟实验室等机构的研究人员提出了一个统一的数学推理数据合成框架 MUSTARD，能够生成大量的、正确的且人类可读可理解的高质量数学推理数据。该数据集为研究开源的 MUSTARDSAUCE 数据集。其中每一个数据都包含了自然语言的问题描述和多步求解，以及对偶的形式化语言 Lean 3 的问题描述和多步求解。 MUSTARDSAUCE 的数据包括了数学应用题和定理证明题，涵盖了从小学到高等教育阶段的难度分级。题目的推理步数随着题目难度的增长而增长。最难的题目需要 30 步左右的求解步骤，约 20 个 Lean 3 tactics 。