TRIGO : Benchmarking Formal Mathematical Proof Reduction for Generative Language Models (2023)

Abstract: 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 are 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 proof but also evaluates a generative LM’s reasoning ability on formulas and capability to manipulate, group, and factor number terms. We gather trigonometric expressions and their reduced forms from 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 also create three automatically generated training and testing datasets of varying difficulty and distributions. 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.

## introduction automated theorem proving (atp) requires formal reasoning and deduction from conclusion to axioms or known theorems. this task requires general and flexible reasoning and is easy to validate, making it an appealing domain for exploring the reasoning ability of the recent successful pre-trained generative language models. these models show strong proof generation capabilities @xcite , but its ability to perform formal mathematical proof reduction, which involves complex numerical reasoning, has not been thoroughly explored. current atp benchmarks @xcite @xcite ) mainly focus on symbolic inference but rarely involve the understanding of complex number combination reasoning, such as term grouping, term factorization and equivalent substitution. for advanced mathematical proving such as trigonometric expressions, atp can be beneficial for evaluating the crucial complex number combination. for example, as shown in figure 1 , to correctly reduce the left-hand-side expression, one must recognize the specific angles or terms such as cos( π 12 ), capable of applying the half-angle formula and know the result is cos( 1 2 * π 6 ). 11594 figure 2 : an example of gpt-4 struggling to solve trigo. gpt-4 corrects its response after the second prompt (box in right), but continues generating error tactics (highlighted in red with a cross mark). such proof steps can be automatically denoted by the formal language deduction as shown in the right-hand-side, and then verified via the interactive theorem-proving environment in atp. to develop such profound atp evaluation for current generative lms, we propose the task of trigonometric expression reduction (trigo). given a trigonometric expression, a model is required to accept formal input with lean formal language and then perform step-by-step proof reduction. the proposed trigo poses a new challenge for current state-of-the-art generative lms. figure 2 presents an illustrative example of a proof generated by @xcite . inspired by self-refine @xcite , we first provide the prompt "please help me prove this problem using lean: lemma trigo_0 : sin(107 * pi) = 0 :" to gpt-4 and the gpt-4 generates non-exist tactics and gives the incorrect equations. we further prompt it with "we require to use lemma from lean's standard library for the proof and to ensure the correctness of the equation" to correct the gpt-4. however, in the second attempt, the gpt-4 still applies the tactic "sin_periodic_pi" that does not exist in the lean standard library and comments it "--available in lean standard library". surprisingly, gpt-4 produced the correct equation "have h: sin(107*pi) = sin(1*pi)" in the second proof attempt, even though the proof for this subgoal is incorrect. this example demonstrates the potential of gpt-4 in accurately manipulating numbers and formulas, as well as the challenge of strict formal reasoning posed by the trigo task. to construct the trigo dataset, we collect trigonometric expression reduction problems and corresponding answers from high school exercises and exams. we then develop an interactive annota-tion software to manually label the reduction steps and formalize the processes into "lean" formal language. finally, based on this manually formalized data, we develop an automatic proof generation program to expand the dataset with real-world data and create datasets of artificially generated samples. specifically, we generate 3 types of samples by controlling their proof length and generating trigonometric functions with larger numerical values to assess the models' ability to generalize to out-of-distribution data. our contributions are three-fold: ## related work automatic theorem proving (atp) has numerous formal environments such as holist @xcite , metamath @xcite , and coqgym @xcite . there are several formal benchmark tasks for theorem proving that exist. @xcite extracts (state, tactic) pairs from mathlib (mathlib, 2020), a comprehensive library of theorem proofs in lean. the isarstep dataset @xcite mines intermediate proof steps from the archive of formal proofs (afp). minif2f @xcite is a cross-system benchmark of olympiad-level mathematics problems, containing 488 problems formalized in metamath, lean, isabelle, and hol light, but only a small portion has formalized solutions. fimo @xcite targets formal international mathematical olympiad (imo) problems. the geometry3k dataset @xcite includes 3,002 geometry problems with annotated formal language descriptions but lacks interaction with formal environments. many other works also focus on informal math problem solving @xcite @xcite . our work is most similar to @xcite . they use formal mathematical reasoning to reduce equations and inequalities and employ programs to automatically generate proofs to explore combinational generalization. however, they lack real-world problems to assess the model's generalization to real distributions and do not involve complex numerical operations combination. compared with previous work @xcite which has 18 axioms and 9 transformations, our generation process has a total of 85 transformation rules and diverse sampled parameters. our proposed trigo generates complex samples with controlled difficulties and distribution, and includes manually annotated samples and proof steps from real-world problems. ## background on lean environment formal language systems are effective tools for strictly verifying the correctness of each proof step generated by the model. in this work, we use @xcite as formal environment. the correctness of a given proof can be verified by a lean verifier program. a lean proof example is shown in figure 1 . it starts from a goal state "⊢ sin(π/3) + 2 * cos(π/12) * * 2cos(π/2) = sqrt(3) + 1", representing the current proof goal. in the row next to the "begin", a tactic "rw cos_pi_div_two" is applied to the current goal state, meaning rewrites the term cos(π/2) to 0. in the following rows, the proof applies "have" tactic generates a new sub-goal such as proving cos(π/12) 2 = cos(π/6)/2 + 1/2, and applies the "ring_exp" to solving exponents equations in comlean-gym @xcite ) is an interactive environment that allows language models to interact with formal systems. as depicted in figure 3 , we begin by acquiring the initial goal state g 1 as "⊢ sin(π/3) + 2 * cos(π/12) * * 2cos(π/2) = sqrt(3) + 1". this goal state is inputted into language model with the prompt "goal g 1 proof-step". subsequently, gpt-2 generates the corresponding tactic t 1 as "rw cos_pi_div_two,". given the goal state and tactic, lean-gym outputs a new goal state "⊢ sin(π/3) + 2 * cos(π/12) * * 2 -0 = sqrt(3) + 1" for language model to obtain the next tactic. we iteratively perform this process until the lean-gym returns "no goals" which indicates the proof is complete. ## trigo dataset in this section, we first introduce how we collect trigonometric expression reduction problems from "tiku" foot_0 , annotate the step-by-step reduction processes, and transform them into lean formal language to create the trigo-real and trigo-web datasets. then we introduce how to automatically generate data to construct the trigo-gen. ## baseline models recent works utilize gpt-based language models for automated theorem proving and have made significant improvement @xcite @xcite @xcite . in this work, we use gpt-2 @xcite with a proof search algorithm as a baseline method for our dataset. ## experiment in this section, we evaluate the performance of gpt-2 base (gpt-2 b ), gpt-2 large (gpt-2 l ), and gpt-2 l -pact, a gpt-2 large pre-trained on the formal proof dataset pact @xcite . furthermore, we evaluate the model's out-ofdistribution generalization ability by examining its performance across various levels of difficulty and different ranges of numbers, while also evaluating model manual labeling trigo-gen trigo-real trigo-web tg-1 tg-2 tg-3 the impact of generating data distributions beyond those observed in real-world data. additionally, we conduct a comprehensive analysis of the models, including an evaluation of gpt-4's performance. ## conclusion in this paper, we introduce trigo, a dataset focusing on trigonometric expression reduction for formal mathematical reasoning with both real-world and generated samples. to the best of our knowledge, trigo is the first lean-based dataset with manually annotated and automatically generated reduction proofs for exploring the formal mathematical ability of current language models. our comprehensive experiments reveal that, in comparison to generated data, pre-training on pact significantly enhances performance on realworld problems. furthermore, expanding the data scale by utilizing real-world data as the starting point for the theorem generation program can effectively boost the model's performance on the realworld test set. additionally, we reveal the model's incapability on generalizing numeric operations to larger unseen numbers and find that both the di-versity of tactics and search paths have significant impacts on the final proof pass rate.