SJTULean/LeanStatement_RL

这是一个专门设计用于训练奖励模型的数据集，旨在评估自然语言数学问题到Lean4形式数学代码翻译的质量。数据集包含成对的自然语言数学语句及其对应的Lean4实现，以及质量状态注释。This is a specialized dataset designed for training reward models, aimed at evaluating the quality of translations from natural language mathematical problems to Lean4 formal mathematics code. The dataset contains pairs of natural language mathematical statements and their corresponding Lean4 implementations, along with quality status annotations.