TRIGO

TRIGO数据集是首个专注于三角函数表达式简化的自动定理证明基准，由中山大学深圳校区的研究团队创建。该数据集不仅要求模型逐步证明三角表达式的简化，还评估生成语言模型在公式推理和数值操作方面的能力。数据集通过从网络收集三角表达式及其简化形式，手动注释简化过程，并将其转换为Lean形式语言系统。此外，数据集还包括自动生成的示例，以扩展数据集并分析模型的泛化能力。TRIGO数据集为研究生成语言模型在形式和数学推理方面的能力提供了新的工具，特别是在解决复杂的数值组合推理问题方面。

The TRIGO dataset is the first automated theorem proving benchmark focused on trigonometric expression simplification, created by a research team from the Shenzhen Campus of Sun Yat-sen University. This dataset not only requires models to incrementally prove the simplification of trigonometric expressions, but also evaluates the capabilities of large language models (LLMs) in formula reasoning and numerical manipulation. The dataset is constructed by collecting trigonometric expressions and their simplified forms from the web, manually annotating their simplification procedures, and converting them into the Lean formal language system. In addition, the dataset also includes automatically generated examples to expand its scale and analyze the generalization ability of models. The TRIGO dataset provides a novel tool for researching the capabilities of large language models in formal and mathematical reasoning, particularly in solving complex numerical combinatorial reasoning problems.