Automated theorem proving (ATP) has become an appealing domain for exploring the reasoning ability of the recent successful generative language models. However, current ATP benchmarks mainly focus on symbolic inference, but rarely involve the understanding of complex number combination reasoning. In this work, we propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas and its capability to manipulate, group, and factor number terms. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We then automatically generate additional examples from the annotated samples to expand the dataset. Furthermore, we develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability. Our extensive experiments show our proposed TRIGO poses a new challenge for advanced generative LM's including GPT-4 which is pre-trained on a considerable amount of open-source formal theorem-proving language data, and provide a new tool to study the generative LM's ability on both formal and mathematical reasoning.

翻译：自动定理证明已成为探索近期成功生成式语言模型推理能力的一个引人注目的领域。然而，当前的自动定理证明基准主要关注符号推理，很少涉及复杂数字组合推理的理解。本研究提出TRIGO基准测试，它不仅要求模型通过逐步证明对三角函数表达式进行约简，还评估生成式语言模型在公式上的推理能力，以及其操作、分组和分解数字项的能力。我们从网络收集三角函数表达式及其约简形式，手工标注简化过程，并将其转化为Lean形式化语言系统。随后，我们基于标注样本自动生成额外实例以扩展数据集。此外，我们开发了基于Lean-Gym的自动生成器，创建不同难度和分布的数据集切分，从而深入分析模型的泛化能力。大量实验表明，我们提出的TRIGO为包括GPT-4（该模型在大规模开源形式化定理证明语言数据上预训练）在内的先进生成式语言模型带来了新挑战，并为研究生成式语言模型在形式化推理与数学推理方面的能力提供了新工具。