miniCTX

miniCTX数据集是一个用于神经定理证明的数据集，特别关注处理长上下文的情况。该数据集包含从Mathlib中提取的Lean 4战术预测示例，这些示例尚未为指令调优格式化。数据集通过ntptoolkit的ntp-training-data工具生成，使用了特定的配置来提取数据。数据格式包括证明状态、战术调用前的源代码、下一个战术、战术调用前的声明、声明的唯一ID、声明本身以及文件ID。