Do Transformers Understand Polynomial Simplification? 
Authors: Vishesh Agarwal
Somak Aditya
Navin Goyal
Venue:  (2021)

Abstract: Recently researchers have demonstrated that Transformers can be trained to learn symbolic tasks such as solving integration and differential equations in an end-to-end fashion. In these setups, for an input symbolic expression, the Transformer predicts the final solution in a single step. Since such tasks may consist of a sequence of logical steps, question remains whether such networks have understood and learnt individual steps to reach the solution. To take a deeper look, we consider the task of polynomial simplification. Polynomials can be written in a simple normal form as a sum of monomials which are ordered in a lexicographic order. For a polynomial which is not necessarily in this normal form, a sequence of simplification steps is applied to reach the fully simplified (i.e., in the normal form) polynomial. For this task, we describe a synthetic Polynomial dataset generation algorithm which generates polynomials with unique proof steps. Then, we conduct an extensive analysis of the Transformer’s abilities to learn the polynomial simplification task along different dimensions.

Under review as a conference paper at ICLR 2021
Do TRANSFORMERS UNDERSTAND SIMPLIFICATION?
POLYNOMIAL
Anonymous authors Paper under double-blind review
ABSTRACT
Recently researchers have demonstrated that Transformers can be trained to learn symbolic tasks such as solving integration and differential equations in an end-to- end fashion. In these setups, for an input symbolic expression, the Transformer predicts the final solution in single step. Since such tasks may consist of se- quence of logical steps, question remains whether such networks have understood and learnt individual steps reach the solution. To take deeper look, we con- sider the task of polynomial simplification. Polynomials can be written in a simple normal form as a sum of monomials which are ordered in lexicographic order. For a polynomial which is not necessarily in this normal form, sequence of sim- plification steps applied to reach the fully simplified (i.e., in the normal form) polynomial. For this task, describe synthetic Polynomial dataset generation algorithm which generates polynomials with unique proof steps. Then, we con- duct an extensive analysis of the Transformer's 's abilities to learn the polynomial simplification task along different dimensions.
INTRODUCTION
With the state-of-the-art performance of Deep Neural Nets (DNNs) in perceptual tasks, researchers have started to explore their logical reasoning capabilities, in particular within the domain of Auto- mated Theorem Proving (ATP). In these domains (LEAN (de Moura et al. (015).. HOL Light and Mizar (miz) 2020)), many recent works (Paliwal et al. 2020 Aygün et al. 2020; Hahn et al. 2020) have shown that Graph Neural Networks (Gori et al. 2005| Veličković et al., 2018) and Transform- ers (Vaswani et al. 2017) can be trained to perform impressively on the pprovigg task as part of neuro-symbolic system.
In related but different development, recently Lample & Charton 2019) showed that for symbolic integration and differential equations, large amount of synthetic end-to-end examples can be gen- erated using symbolic systems. In these tasks, the authors show that Transformer networks can be trained to produce the final solution from an input integral (or differential equation) in a single step. This points to the exciting possibility of using deep neural nets learn end-to-end theorem provers, and can be beneficial for formal mathematics (Szegedy) (002)). However, the setup combines mul- tiple reasoning steps in single shot. Additionally, integration (or differential equation solving) is a complex task requiring understanding of the integral symbols, functions, variables, and the ba- sic concepts of arithmetic. As the system in Lample & Charton (2019) is simply trained to output the top solution(s) and a corresponding confidence score(s). it is unclear what internal mechanisms enable these models solve these problems. This lack of transparency has been noted in this con- text (Davis 2019). An earlier work by Piotrowski et al. (2019) showed similar results for certain symbolic manipulation tasks and their work shares the same limitation.
In this paper we ask if instead of only producing the end-result of symbolic manipulation or integral, can we have the model produce a human-readabe proof as well. While we do not know if these models reason in the way humans do, one way to produce proofs would be to "extract" a proof from the models of the above type by "probing" them in some mannner. The problem of unraveling the inner workings of Transformers by probing is active area of research; however, present understanding is still evolving (Rogers et al., 2020). Hence taking detour, we instead train the model produce the full proof.

---

Under review as a conference paper at ICLR 2021
Inspired by Piotrowski et al. 2019), explore a novel but simpler setting of polynomial simpli- fication. We illustrate the task with an example. We begin with a polynomial which sum of product of factors, where each factor is again sum of monomials (including constants), as shown below:
product
Po (2 x 33 +4) + (5 # of + of x2) (3 (3+x1) (2),
1 Initial */
To construct unique simplification steps, first each term in factor is simplified. Once all factors are simplified (facstep); then within product, all factors are multiplied (mulstep). Lastly simplified products are summed (sumstep).
Po = (2 2²) * (3 * 23 + 4
at
(2),
1 FACSTEP */
(2+ * (3 22 + +5
(2),
(Pi), FACSTEP */
(2*
(2),
(P2), MULSTEP */
-6+ 10+22+8*00 +8*
+5x
23+ (2),
(Pa), / MULSTEP #/
(6 2 + 8
(30
x +6 W2):
(P4), /* SUMSTEP $/
30 x + 6
+ 6
8 22.
(P:), / ENDPOINT */.
Piotrowski et al. (2019) explores the task of learning symbolic re-write of an entire expression. In contrast, in our setting, for step-wise prediction, each step the system needs find the candidate sub-expression and relevant simplification type to perform the simplification. This setup resembles the traditional ATP setup where a system needs to learn and execute symbolic steps reach final solution. But it is simpler as for each step only one type of simplification is applicable. By proof for an initial polynomial (Po) we mean the sequence of simplification steps (P) Ps). A model trained on step-wise prediction task, can be used to generate a full proof. Essentially, we start with an initial polynomial, and recursively feed the model output to itself, till it generates the final simplified polynomial (in normal form). A proof is correct when all steps are correct.
In the above setting (termed COARSE), all terms a factor are simplified at once in a facstep, and similarly all factors in product are simplified at once in a mulstep. Additionally, we define an- other setting FINER, where f facstep involves simplification of a single term, and a mu step in- volves multiplications of only two factors at once, illustrated below with an example (for fa csste)):
Po = (5 * of + at
xn)
* (2),
J FACSTEP #/
(5 2 + x2))
(2),
1 FACSTEP */
= (5 * o + 21 * x2)
21 (2).
As a state-of-the-art model, we explore Transformers. While both Graph Neural Networks and Transformers have been used for single-step representation learning of symbolic theorems and single step goal-theorem scoring, Transformer-bus based soquuncceto-sequenee networks have shown superior- ity in end-to-end tasks in integration, differential equations (Lample & Charton 2019) and temporal logic (Hahn et al. 2020) domains. Hence for the aforementioned tasks of step-wise polynomial simplification, explore the Transformer's ability along several dimensions. Our contributions the following: 1) we propose polynomial simplification tasks requiring multiple steps of symbolic manipulation, 2) we show how datasets of different configurations can be generated synthetically for the task, 3) we propose an array of metrics to dissect the performance of Transformers, and 4) lastly through extensive experiments we show the performance of the Transformer on this task, establishing strong baseline for future endeavors.
Results Summary By varying over coefficient size, proof granularity and input representation (in Tables 2
Appendix Table 6 we observe that 1) full proof accuracy is only slightly lower than single-shot endpoint prediction accuracy in many 1-variable configurations, 2) coarse granular proofs help leam somewhat more accurate proofs, 3) prefix representation helps in most cases but infix sometimes provides higher accuracy. More than 80% errors (Tab. 7 and g in Appendix) occur in multiplication steps, and observe (through independent experiments) Transformer's struggle
2

---

Under review as a conference paper at ICLR 2021
to learn how to multiply numeric coefficients. By letting the system annotate the candidate sub- expression, we observe that the system can understand candidate sub-expressions and which next step to perform explicitly (Tables 3 and Appendix Tables TO III. Also, through visualization
observe similar effects (Figures 1 2 Appendix). We see systems trained for 2-variable outperform corresponding 1-variable systems
1-variable test sets. For 1 variable, observe steady and significant higher gains (till 10% for full proof) using curriculum learning (Table 17 Appendix).
2
RELATED WORK AND DISCUSSION
Unlike the problems dealt with by the aforementioned automatic theorem provers and related neural- based systems, polynomial simplification does not involve any search. Our problem is simpler and tests specific ability, namely certain kinds of symbol manipulations. This simplicity affords certain advantages (shared by [Piotrowski et al. (2019) and Lample & Charton (2119))
(1) We can generate artificial data to train models without limitations on the size. (2) is easter to test the abilities of the
models more thoroughly along multiple axes. (3) Accuracy achieved is much higher than for harder tasks, suggesting that fully solving such tasks may be possible the near future.
To compare with symbolic manipulation systems we note that in more detail the ability tested by our task is the following: the model must be able to identify smallest parts of the polynomial that can be simplified: (1) simplification of factor, (2) multiplication of two factors, (3) addition of two sub- sub-polynomials. Having identified what simplification to apply the model must produce a new polynomial with just that simplification. This ability is not tested by previous neural- based symbolic manipulation systems such as Piotrowski et al. (2019) and Lample & Charton (2019) and related
works such as Saxton al. (2019) and Hahn al. (2020). Several recent works have produced synthetic datasets for theorem proving tasks (Aygün et al. [2020] Wu et al. 2020 2020). however, their focus remains more on search-based proofs.
Polu & Sutskever,
3 POLYNOMIAL SIMPLIFICATION DATASET
We proceed similarly to Lample& & Charton 2019) to generate the symbolic polynomials and sim- plified steps synthetically using the Sympy library of Python. To have fine-grained control over the generated polynomials and well-defined proof steps, we consider polynomials which are sums of product= We also note that symbolic generation using the Sympy library lets us ensure correctness of each generated expressions and validity of each steps.
3.1 NOTATIONS
We start with the set of variables xp {x1, .. (nwarr) We represent the starting point polynomial Po in Tp the sum of products of factors:
Po = P1 + P2 + ... + Paprod:
nfac;
P = II Sij.
1=1
where each factor (fiz) has the form f = ==E * II Et de1), where Tst E xp (dropping i, for clarity). Here coefficients as E N+ and powers of the variables du N. nprod is the number of products and nfac; denotes the number of factors in P,.
We denote the set of factors as fp = Bi, P. = Iy fayh. The simplified endpoint polynomial
of the form p = Em fm- where f.m = am II, In Amm, where In E TP. We use the symbol P; to denote the simplified form of P.. The functions terms(), vars(), coeffs() returns a list of terms, variables, coefficients in the input expression. Our sampling algorithm guarantees that the generated polynomial and its simplified endpoint abides by constraints on number of terms, products, factors and variables; limit on degree and coefficient sizes. An example is nprod E full list is provided in Appendix Table
maxPp) (The
'The generation algorithm in Lample & Charton 2019) may generate nested sums and products. For such polynomials, an unique proof sequence is hard to define which makes whole proffs harder to evaluate. Our restriction the form of the polynomial helps us generate unique proofs, which easier evaluate.
3

---

Under review as a conference paper at ICLR 2021
3.2 BUILDING A POLYNOMIAL PROOF
Here, we briefly describe the starting polynomial generation process; detailed algorithm is in the appendix. Any randomly sampled polynomial (represented as a sum of products) can be included as a starting point in the dataset as long as the polynomial respects certain configuration parameters (in Appendix Table 4). This is unlike Lample & Charton (2199) where many randomly generated integrals (or differential equations) might not have a solution. Hence, we randomly sample the con- straint parameters in a top-down manner; and then construct terms, factors and products in bottom- up manner using the parameters. We first sample the following 1) a set of participating variables ( Tp), 2) maximum degree for any monomial in the simplified polynomial (mdeg), and the num- ber of products in the starting polynomial (nprod), We then call the algorithm bui widdPPoddii roduct (Algorithm [ in appendix) to create nprod individual products.
In bui roductt (Algorithm 1 in Appendix), first we sample nfac; the maximum number of factors in the product (P:). We then build factors sequentially. For each new factor, we sample subset of variables in factor. We pass product-level constraints such as maximum degree in product, maximum terms in a product, and maximum coefficient for a product as rdegree, rterms and rcoeff respectively; and call the sub-routine buildFactor (Algorithm to create a factor. After a factor is sampled, the constraints rdegree, rterms and reoeff are updated. bui 1 actor used to create at most nfac; factors, that all abide by the above constraints and stops if the limit of maximum degree in the product is reached. The terms in factor are arranged in a lexicographical order. Since, this sequential generation of factors may induce a certain pattern of decreasing degrees and coefficients, shuffle the factors to create the final product.
Building a Product
Simplification Steps and Full Proof For both COARSE and FINER configurations, we build the proof steps in the following way: first we do sequence of facsteps where terms get collected within a factor (such as 2x + 3x to 5z, x² and 1x becomes z); 2) then sequence of mulsteps are performed where simplified factors are multiplied out; and 3) lastly, sumstep simplified products are added together. As mentioned before, the sequence of simplification steps till the endpoint constitute full proef.
4 EXPERIMENTS
4.1 DATASET
We vary dataset configurations along the following dimensions:
Number of Variables in polynomial, product and factor is varied between and 2.
Coefficients Size: Maximum coefficient in the polynomial, product and factor are gradually varied from {60, 20,5} (SMALL), to {120, 40, 8} (MEDIUM) and (300, 100, 10) (LARgE). DEFAULT is {120, 40,88, 8).
Maximum degree in polynomial and a factor has two configurations: [6,3) (DEFAULT), and [1,,5} (MEDIUM DEGREF).
Maximum number of terms in simplified product and a factor has two configurations: {8,3} (DEFAUlT), and {20, 4} (MEDIUM TERMS). For the latter, we also set maximum products in sum and maximum factors in product as 5 and 4 respectively.
No Backtrack: We also try a very large configuration (No BACKTRACK) where maximum coeffi- cients in polynomial, product and factor are (10125, 3375, 5], maximum degree in polynomial and factor are set to [9,3] 3). Maximum terms in product is set to 27. This is a configuration, where no sampled factor, or product is ever rejected for violating any higher-level constraint.
Infix and Prefix We focus exploring seq2seq networks for all our experiments. We consider the prefix and infix traversals of the abstract syntax tree of the polynomial input as sequences. Lample & Charton (2019) briefly touched upon the usefulness of the prefix notation over infix, but do not provide any empirical evidence supporting the statement. Hence, in our experiments, we consider both INFIX and PREFIX representations.
4

---

Under review as a conference paper at ICLR 2021
4.2 TASKS AND METRICS
We identify two central tasks: 1) Step-wise prediction: where an input polynomial is provided and the task to perform the next proof step, and 2) Endpoint Prediction: where given a polynomial, the task is to predict the fully simplified polynomial in a single step.
To compare with the Endpoint prediction task, we use the Step-wise prediction task to compute the full proof accuracy as the percentage of proofs where all individual proof steps accurate Apart from the accuracy, we also compare the examples seen by the systems trained in the above two types of tasks. For the Step-wise task, a training example corresponds to an individual simplification step; whereas for the Endpoint task an example is a pair denoting the initial and the endpoint polyno- mial. We also report the following: 1) error percentages grouped by each different types of steps facstep, mul mulstep, and sumstep, 2) calibration scores of the systems based on a threshold. To compute accuracy for an example (in both the tasks), we the simpl i fy method of Sympy library and check symbolically whether the difference between the predicted expression and the ground-truth expression is equal to zero.
Calibration: As end-to-end models grow more accurate and their usage increases, it's important that the users can trust such models. In addition to reporting each simplified step and a confidence score, we also report calibration score computed from the ratio of the top two outputs predicted for each step (using beam width 5). Using a Calibration constant threshold (usually 5), we report the sure rate which is percentage of times when the ratio (in log scale with base e) exceeds the threshold. We also report precision, recall and F-1 score for calibration.
4.3 MODEL
we train a seq2seq network to predict the next proof step provided a polynomial as sequence. For all the experiments, we train a Transformer network (Vaswani et al.) 2017) architecture with 4 attention heads, 4 encoder and decoder layers with hidden embedding size of 256. We use an Adam optimizer (Kingma & Ba, 2014) with a learning rate of 10-4, We limit the maximum token length to 512 and use a batch size of 32 polynomial pairs.
Adapting the experimental setup by Lample & Charton (2019 3
During training, we synthetically generate each batch of equations. To avoid collisions between train and test sets, we first use fixed seed to generate the test and the validation sets of polynomial simplification full proofs and collect the simplified end-points. We make sure that the simplified versions of the input polynomial in the training batches, do not collide with any endpoints in the the test and validation set. Authors in Piotrowski et al. 2) shows that probability of such collisions in the generated integration dataset by Lample & Charton (2019) to be quite high, and urges to report the test accuracy by accounting for such collisions explicilly.
During inference, we use beam-search with different beam widths (beam 1 and 5) to decode the expressions. For our results, beam width is used for proof accuracy. Calibration results are pro- duced using beam decoding. During decoding, if any malformed (prefix or infix) expressions are generated, we report the percentage such expression
4.4 EXPERIMENT ORGANIZATION
In the next sub-sections, we provide problem space-size estimate (4.55 to understand the accura- cies are an effect of memorization. Then we vary the proof granularity, coefficient configurations and input representation to test Transformers' accuracy and errors in both tasks (144.)). Next, to assess whether Transformers can specifically predict candidate next sub sub-expression to be simplified, we try an annotated proof setting (1).6.I). To estimate the learning ability of addition and multiplication on symbolic variables, we test setting where the coefficients also symbolic, thus bypassing the need for the Transformer to do integer multiplication. Next, we discuss out-of-distribution general-
2 We have also attempted recursive proof generation, where the output from the decoder is fed to the encoder in the next step. It does not vary from the tcacher-forcing since, if in any step the model is wrong, the model does not recover after that.
https: / /i thub. com wtt.:/om..aaaaaa cebookk researkkkeeerrrc Sasseeerch/SSooooo/oo cMat tomatheman themat is Similar to Lample & Charton (2019), we find that the percentage of malformed outputs was very low (< 0.5%). So did not explicitly correct for it.
5

---

Under review as a conference paper at ICLR 2021
ization ability of the systems (g4.7) We also explore several curriculum strategies to take advantage of the well-defined sub-tasks and their varying complexities (44.8). Lastly, we provide layer-wise
attention visualizations of trained system in the Appendix (Figs. T 2
4.5 PROBLEM SPACE SIZE ESTIMATION
For smaller configurations, it is probable that eventually all simplified polynomials would be in- cluded in the training data. To account for this, estimate the problem space size for each configu- ration and report the size of training data for comparison. We randomly generate two sets of starting polynomials say S and S2, and check for collisions among them. Assuming the actual size is X and uniform distribution over all starting polynomials, the expected number of collisions would be R = S,=S2_ Using the above method, we estimate the number of un-simplified polynomials and the number of unique endpoints, and report in Appendix Table 5 We observe that compared the number of training examples it took for the models to converge in both End-point and Step-wise prediction tasks, the space of possible equations is often 25 (or more) times higher.
Sampled polynomials are not uniformly distributed as we assign an equal probability while sampling polynomials of lower and higher degrees, say and 6; whereas there are more polynomials of degree 6 than degree 3. For non-unine non-uniform distributions, we expect more collisions as higher probability equations are more likely to occur in both S1 and S2. Moreover, since many equations may map to the same endpoint, such collisions for endpoints are even more likely. Thus, our empirical estimate of the population size provides lower bound on the true value.
4.6 INPUT REPRESENTATION
We report the results for one and two variables, for all configurations in Tables | and 2 ble []] we include results for both COARSE and FINER configurations. We observe that COARSE proof-steps with PREFIX representation provides the best full proof accuracy for four out of six con- figurations (especially for larger coefficient sizes). Across COARSE and FINER, in five out of six configurations PREFIX representation increases the full proof accuracy over INFIX, while the im- provement is not always substantial. In SMALL COFFF configuration, the FINER setting improves that the winning combi- nations often provide the highest calibration F-1 score (more prominent for 2 variables), indicating lesser ambiguity in the decision made. In Table 2 using PREFIX representation for two variables provides 3 to 4% boosts in full proof accuracy for 4 out of 6 configurations. Since, FINER steps do not improve full proof accuracy for two variables, we report the results in Table 6 in the appendix. However, for No BACKTRACK, the infix representation clocks 9.5% improvement over prefix. Comparing with Endpoint accuracy, as coefficient sizes grow from SMALL to No BACKTRACK, for I variable, the Endpoint accuracy is only slightly higher (1 to 2%) than the full proof accuracy. However, for MEDIUM TERMS and MEDIUM DEGREE, the Endpoint accuracy shows a 3.6% and 13% improvement respectively. For 2 variables, Endpoint task accuracy is larger in most cases.
In Ta-
over COARSE for full proof accuracy. From the calibration results,
In Tables 7 and (in Appendix) we show the model errors for each step type. We observe that more than 80% of the model errors occur in the multiplication step. In the MEDIUM TERMS setting, factor simplification causes 15-25% of the errors, possibly because of higher number of factors to simplify. For 2 variable case, addition step accounts for 10-15% of the errors. In all other cases, both factor simplification and addition cause close to 5% of the model errors each. As mentioned in $4.4] we experimented with symbolic coefficients mitigate the difficulties with integer multiplication. This however didn't 't give good results possibly due to output becoming too long.
4.6.1 ANNOTATED PROOFS
In each step, simplification is performed over sub-expression of the polynomial. To check explic- itly, if the system can locate the sub-expression and find the type of simplification step, we devise the annotated proof setting. For each simplification step, we add an intermediate step, in which the model annotates the part of polynomial to operate on. For example, the starting input sequence is
r1) x (2)"; and the corresponding expected output sequence is "MULS $ #(5 x 21 * 22) (3 x # (2)". Each sequence has two parts: 1) the step index to
"MARK $ (5 2 + I1 * Ø22)
perform (MARK, MUL, FAC, SUM), and 2) the polynomial expression. For MARK step, a marker
token (#) is used to annotate the candidate sub-expression to be simplified next.

---

Under review as a conference paper at ICLR 2021
Endpoints #Endpoint
Full Proof
Step-wise
Calibration
Fall Proof
Stepwise
Top-1
Beam-5
Sure
REE
#ltain
F1
Acc
Accuracy
Accuracy
Acc
Acc
Rate
Course/Ialix
SM
96
3.6M
95
98.83
88.13
89.67
83.2
100
94.4
0.97
Small
Fine/Intix
5M
56
4.8M
98.9
99.79
94,46
92.38
100
97.8
0.99
Coeff
Course/Prelix
5.2M
97.8
3.2M
95.3
98.97
87.83
89.37
83.03
100
94,54
0.97
Fine/Prellx
5.2M
97.8
4.4M
36.9
99.4
95.1
95.83
93:13
99.96
97.9
0.99
Coarse/Infix
4.1M
91.2
4.3M
92.8
98. 24
88.97
91.67
84.3
100
94.75
0.97
Medium
Fine/Ialix
4.1M
91.2
2.M
90.3
97.99
86.1
87.68
81.14
100
94,24
0.97
Coeff
Coarsel Coarse/Petlx
6.1
95.87
5.3M
93.6
98.58
86.6
88.47
82.83
99.83
95.54
0.98
Fine/PPrlix
6.1M
95.87
4.5M
91.7
98.37
95.1
96.43
91.27
100
95.97
0.98
Course/Iniix
4.8M
83.73
3.4M
82.1
95.97
92.34 14
94.22
87.2
99.98
99.41
0.97
Large
Fine/
4.8
83.73
3.4M
82.5
96.44
92.32
94.26
87.5
99.98
94.76
0.97
Coeff
Course/ Prelix
6.5M
85.87
3.5M
83,5
96.25
80.6
83.3
99.91
92.97
0.96
Fine/Preht
6.5
85.87
3.2M
82
96.32
79:13
80.63
75.57
99.96
95.45
0.98
Coarse/Inhs
5.9M
80.1
3.8
15.6
94.62
72.74
77.28
61.8
99.9
84,88
0.92
No
Fino/latix
5.9M
80.1
74.5
88.34
79.44
99.92
89.86
Backtrack
Coars:/rrefix
6.6M
78.87
5.6M
79.7
95.38
81.93
85.57
72.2
100
88.12
0.94
Fino/Prrlix
78.87
4.2M
74.7
82.03
72.23
91.43
Coarse/Intix
96.4
92.8
Medium
Iine/Inlix
9.2
96.4
3.3M
83.4
96.12
88.26
90.44
83.04
99.95
90,04
0.97
Degree
Course/Prefix
94.33
87.7
0.95
Fine/Prelix
7M
94.33
5.9M
90.6
97.92
82.2
83.7
77.27
99.96
93.96
0.97
CourseInnix
4.6M
81.9
2.3M
72.7
93.99
79.44
82.22
68.22
99.97
85.85
0.92
Medium
Fine/Talix
75.1
Terms
Course/Preth
7M
89.8
4.3M
76.3
95.78
87.8
91.17
81.3
100
92.6
0.96
Fine/Prelix
87.72
Table I: Results for 1 variable in the COARSE and FINE configuration for both Infix and Prefix representation.
Endpoints
Full Proof
Step-wise
Calibration
#Endpoint
Full Proof
Stepwise Accuracy
Top-1 Acc
Beam-5 Acc
Sure Rate
ABE
#Train
P
R
F1
Acc
Accuracy
Small
Infix
4.3M
94.7
3.7M
87.9
97.01
88.9
91
81.07
100
91.19
0.95
Coeff'
Pretx
4.5M
93.93
5.3M
91.2
98.08
83,83
86.7
77.37
100
92.32
0.96
Medium Coeff
Infix
7M
95.3
5.3M
88.5
97.35
90.98
93.7
84.64
99.98
93.01
0.96
Prefxx
5.2M
92.77
4.8M
96.03
89.57
92.93
81.27
90.7
0.95
Large
Coett'
Infix
9M
91.8
3.8M
80.4
95.18
90.44
93.14
82.74
99.93
91.42
0.95
Prefix
6.1M
86.6
5.4M
83.7
96.23
92.23
94.37
86.03
100
93.28
0.97
No
Infx
8.6M
83.8
72.7
93.13
75.48
78.74
64.4
100
85.32
0.92
Backtrack
Prefix
7.1M
79.2
4.3M
63.2
89.87
72.07
76.43
59.4
99.94
82.38
0.9
Medium Degree
Infix
4.9M
87.9
5.1M
80.5
95.13
90.3
92.53
80.63
100
89.29
0.94
Pretx
5.2M
83.73
6.1M
83.4
96.41
92.07
94.43
83.13
99.96
90026
0.95
Medium
Infix
8.5M
90
3.8M
64
92.03
80.5
83.66
66.62
100
82.76
0.91
Terms
Preñix
6.6M
87.07
6.3M
67.8
93.58
89.7
91.37
80.33
99.96
89.32
0.94
Table 2: Results for 2 variables for the COARSE configuration for both Infix and prefix representa- tions.
We experiment only with INFIX representation. The results for variable and 2 variables are in Table andd (in Appendix). The errors per step type are shown in Appendix Tables I0 and Compared to non-annotated setting, while the step-wise accuracy is similar, the proof accuracy sufters often by 7-10%. reason for such decrease in accuracy that length of the annotated proofs are twice as long non-annotated. However, we note that the errors in MARK step are the lowest compared to other types of steps. This indicates that the models are able to learn the candidate sub-expression for simplification, and predict the next operation correctly.
4.7 OUT-OF-DISS DISSRRIBIIIIIIIIONNN EVALUATION
We also test out-of-diittibuttion generalization by choosing different test configurations than train. The best 2 Variable models (COARsE/PREFIX) were tested on 1 Variable dataset with same coeffi- cient configuration. We interestingly observe (in Appendix Table 14p that in all settings except one

---

Under review as a conference paper at ICLR 2021
Proof Type
Endpoint
Full Proof
Stepwise
Calibration
Config
#Train
Full
Greedy
Endpoint Acc.
Top-1
Beam-5
Sure Rate
#EE
Proof
Stepwise
R
Acc.
Acc.
Acc.
Acc.
SMALL
Fine
2.4M
88.5
98.82
86.77
87.7
83.97
99.96
96.73
0.98
5M
96
COFFF
Coarse
3.7M
91.9
99.16
90.07
90.73
88.13
100
97.85
0.99
MEDIUM
4.1M
91.2
2.8M
97.66
92.67
93.63
88.23
95.22
0.98
COFFF
Coarse
3.5M
84.2
98.29
94.83
95.53
92.4
99.96
97.4
0.99
LARGE
Fine
8M
83.73
3.6M
75.5
97.37
96.8
97.8
92.4
99.93
95.39
0.98
COFFF
Coarse
4.6M
80.3
97.86
80.37
81.6
77.83
100
96.85
0.98
NO BACK
4.1M
96.78
90.43
92.33
84.5
93.4
0.97
5.9M
80.1
TRACK
Coarse
3.6M
59.7
95
92.5
94.33
86.47
99.81
93.3
0.96
MEDIUM
Fine
9.2M
96.4
3.7M
76
97.37
83.67
85.23
79.
100
94.34
0.97
DEG
Course
3.4M
78.7
97.38
93.2
94.37
88.2
100
94.64
0.97
MEDIUM
3.6M
70.4
97.48
91.5
92.2
86.87
100
94.94
0.97
TERMS
Course
4.6M
81.9
3.3M
66.2
96.34
88.9
90.27
83.17
99.84
93.4
0.97
Table
Results for FINE and COARSE configurations for Variable for annotated proofs
(MEDIUM COFFF), the 2 variable models outperform the corresponding 1 variable models. For the LARGE COFFF case, the improvement is close to 6% over the variable model. As expected, the 2 Variable models perform better on variable dataset than 2 variable. The results for OOD evaluation with respect to coefficient limits, polynomial degree and polynomial length (no. of terms in starting polynomial) are discussed in the Appendix (Tables 13 & 16..
4.8 CURRICULUM LEARNING
Simplification steps entail learning of addition and multiplication of numeric coefficients and sym- bolic variables. But, as some of the individual sub-tasks seem harder grasp, employ different types of curricula based on the Mastering-Rate by Willems al. (2020 For all our experiments, we the MR algorithm with gAmax Linreg A2D converter functions described in Willems et al. (2020). Model parameters and the training con- figurations remain the same. We show the results in Table 17 for variable COARSE configuration. As coefficient size grows from SMALL, MEDIUM, LARGE to No BACKTRACK, improvements in full proof accuracy steadily increase from 1% to 10.84% (COARsE/INFIIX) For No BACKTRACK, the improvement in top-1 accuracy is by 20% from a no curriculum setting. However, we observe for MEDIUM TERMS, there is a drop accuracy for all curricula and input representations. It is possible that, more carefully designed curricula may improve the results. There is no clear advan- tage observed between infix or prefix representations. However, compared to learning without a curriculum, the improvement observed for infix representation is often larger than prefix.
(MR) curriculum learning algorithm proposed
CONCLUSION
We explored the polynomial simplification task to investigate the capabilities and shortcomings of Transformer networks across various dimensions. We proposed a synthetic polynomial generation algorithm which generates constrained polynomials with unique proof steps. While Transformers perform impressively in many settings, reaching above 90% proof accuracies, there were also clear limitations and there are many avenues for future work. Among notable results, in many cases full proof accuracy is lower than endpoint accuracy, but with low margin. This is perhaps not surprising because the model is trained to optimize for stepwise accuracy and generating a valid proof requires getting all of the multiple proof steps correct. Thus a more proof-centrie training approach might further improve proof-wise accuracies. Prefix representation has a slight advantage over infix and coarse proofs have slight advantage over fine proofs. Transformers quickly learn addition, but consistently struggle with multiplication. Carefully designed curriculums can boost full proof accuracy up to 10% for large coefficient sizes. Models trained on two variable datasets often did very well single variable datasets-eved better than the models trained on single variable datasets. Exploring multivariate polynomial manipulations and more general algebraic systems are some immediate future directions, though even for the polynomial simplification task significant gaps remain in our understanding.
FFor full details, please see Appendix Section I.
8

---

Under review as a conference paper at ICLR 2021
REFERENCES
Mizar Mathematical Library, 2020. URL
Eser Aygin, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot, Laurent Orseau, Doina Precup, and Shibl Mourad. Learning prove from synthetic theorems. arXiv preprint arXiv:2006. httv:2006.1259,, 11259, 2020.
Ernest Davis. The use of deep learning for symbolic integration: A review of (lample and charton, 2019). arXiv preprint 192.0559/ 2019.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp Automated Deduction CADE-25, pp. 378-388, Cham, 2015. Springer International Publishing. ISBN 978- 3-319-21401-6.
Marco Gori, Gabriele Monfardini, and Franco Scarselli. new model for learning in graph domains. In Proceedings. 2005 IEEE International Joint Conference on Neural Networks, 2005., volume 2, pp. 729-739-747 IEEE, 2005.
Alex Graves, Mare Bellemare, Jacob Menick, Rémi Munos, and Koray Kavukcuoglu. Automated curriculum learning for neural networks. In International Conference Machine Learning, pp. 1311-1320, 2017.
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner. Trans- formers generalize to the semantics of logics, 2020.
Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv: /4ti::44/..00 pttp////2....... 6980, 2014.
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In International Conference on Learning Representations, 2019.
Tambet Matüsen, Avital Oliver, Taco Cohen, and John Schulman. Teacher-student curriculum learn- ing. IEEE transactions on neural networks and learning systems, 2019.
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In The Thirty-Fourde AAAI Confer- ence on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Ar- tificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Ad- vances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pp. 2967-2974 AAAI Press, 2020. URL /aap:: www.oog///ooooooooooo hwtps//inexxxeee httpo///snnnne.pp//....eeee php/AAAI// article/view/ 5689
Bartosz Piotrowski. Josef Urban, Chad E. Brown, and Cezary Kaliszyk. Can neural networks learn symbolic rewriting?, 2019.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, his/2009.03399) 2020. htRtssts::///at http:::///xxvvvveeae wwtp://///wpab.....o///// htl.:tpp.//axx...rrr//////2....3 03393
Anna Rogers, Olga Kovaleva, and Anna Rumshisky. A primer in bertology: What know about how bert works, 2020.
David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In 7th International Conference Learning Represen- tations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL https::/openrevieer net net forum wonoruumii--H.. H1gR1s5FK
Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce Miller (eds.), Intelligent Computer Mathematics, pp. 3-20, Cham, 2020. Springer International Publishing. ISBN 978-3-030-53518-6
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in neural information processing systems, pp. 1998-6008. 2017.

---

Under review as a conference paper at ICLR 2021
Petar Veličković, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Liô, and Yoshua Bengio. Graph attention networks. In International Conference on Learning Representations, 2018.
Jesse Vig. A multiscale visualization of attention in the transformer model. In Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics: System Demonstrations, pp. 37-42, 2019.
Lucas Willems, Salem Lahlou, and Yoshua Bengio. Mastering rate based curriculum learning, 2020.
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger B. Grosse. INT: an inequality benchmark for evaluating generalization in theorem proving. CoRR, abs/2007.02924, 2020. URL https:
//arxiv.org/abb/200.00oo
A VISUALIZATION OF TRANSFORMER LAYERS
Following Piotrowski al. (2019), we also attempt to understand what the Transformer networks are learning through layer-wise Visualization of attention (Vig 2019). We take model trained on COARSE granularity proofs using INFIX representation for varialle using the SMALL COFFF con- figuration. We take the following example:
Po * xf) (5 un 41 (12 xı),
/ MULSTEP #/
= -20 2 + 16 * 21 +3) + (12 * x1)
In Figure I we observe that in layer encoder-decoder attention indicates that while generating the number 16, the Transformer network is clearly able attend the two digits 4 and 4 required for the multiplication. In Figure _ we observe that the Transformer networks, in the same time also learns copy the expression T2 #1 in Layer 1. Even though such clear logical patterns emerge quite frequently, in some cases patterns become hard to interpret.
Algorithm 1: BuildProduct (Sampling Products)
Input: Tp, mdeg
Constraints: nvars-prod, max.coeff.prod, max.fac.prod, max.terms.prod
Output: A list of factors Feeq
Sample near E (num_vars
nvar min( near)
Sample near variables from Tp as rp.
// Variable set for this product
Sample nfac E (2...., fax.fac.prom
// #Facorrs for this product /* Get maximum degree, terms and coefficient available */ rdegree = mdeg, rterms max.terms.prod, reoeff max.coeff.proo
eprod= =
// Keeping track of product built till now
F Fseg
for
j nfac do f, bui idFactor(pp, rdegree, rterms, rcoeff)
+ Update degree, terms and coefficient for next factor x/ eprod = cprod fj
10
rdegree rdegree degree(f,)
11
rterms = max terms proo/ (erms((prod))
12
13
reoef f = max coeff proš/mar (coe scprrod))
14
Append S; in Fxeg
15
rdegree == then
break
end 17
I8 end
Shuffle Fseg
10

---

Under review as a conference paper at ICLR 2021
Layer:
Attention:
Sentence A >>
Sentence B v
Layer.
Attention:
Sentence Sentence B
<S>
<S>
<S>
<S>
(
INT+
INT+
INT
INT
2
4
0
mul
mul
mul
x1
mul
x1
x1
pow
x1
pow
pow
INT+
pow
INT+
INT+
2
INT+
2
5
add
mul
add
mul
INT+
INT
(
INT+
INT
6
5
mul
mul
mul
x1
x1
x1
pow
pow
pow
pow
INT
INT
INT
INT
3
3
add
add
INT+
add
INT+
4
INT+
mul
INT
mul
x1
2
mul
add
mul
x1
(
x1
)
INT
INT+
<g>
<>>
1
2
mul
mul
x1
)
<g>
<5>
Figure I: The layer 2 encoder-decoder attention for the output digits 16 in the first simplified product
for the output (20 * .rf + 16 * 21 +3) + (12 x1). As expected, the digits 1 and 6 attends to the coefficients of the first and third monomial in the input expression (4 zf) x (5 * oी + x1) +
(12 .1). Config: COARSE, SMALL COEFF, INFIX, variable.
11

---

Under review as a conference paper at ICLR 2021
ayer
Attention
Sentence A Sentence Layer:
Attention.
Sentence A >> Sentence
<S>>
<S>
<S>
(
INT
INT
INT
INT
4
2
mul
0
mul
mul
x1
mul
x1
x1
pow
pow
pow
INT+
INT+
INT+
2
INT+
5
)
add
mul
add
mul
INT+
(
INT+
INT+
INT
5
6
5
mul
mul
mul
mul
x1
x1
x1
x1
pow
pow
pow
pow
INT+
INT+
INT
INT
3
3
add
add
add
INT
add
INT+
4
INT+
mul
INT+
mul
x1
2
2
mul
add
mul
add
x1
(
INT
INT+
1
2
mul
mul
x1
<S>
Figure 2: The layer 1 encoder-decoder attention for the coefficient 12 in the last product (20 2 + 16 Ii +3) + (12 x 21). It is expected, that in this step, this product remains unchanged and simply copied the output. Therefore, we see that the layers learn to copy the coefficients directly by attending to the corresponding digits (i.e. attends to in the last product). Config: COARSE, SMALL COFFF, INFIX, variable.
12

---

Under review as a conference paper at ICLR 2021
B ALGORITHMS
The polynomial sampling algorithms www.dproiuuiii and buildFactor are provided in Algo- rithms I and respectively.
Algorithm 2: BuildFactor (Sampling Factor)
Input: Ip,, rdegree, rterms, rcoef
Constraints: num vars fac, max coeff fac, max terms fac, degree fac Output: A factor fj. Number of terms nderms;
Sample near {l,..., num.vars.fase
cvars = Sample nvar variables from IP, www.mmmmtmmaemmmeeeee.mmm rtermss))
// Variable set for this factor
Sample nterms
// # Terms for this factor Sample {de k=l I s.t. dy E m00_.,,mmmaxx.eegreee http::ddgreee.fa.dddee.. rdegree)
// Term degrees: degree allows for constant terms Sample [c
Vaterms, s.t. ch E .I,..., www.mmmiimmmc...ffeee... rcoeff)
// Term coefficients
for is to nterms! 1 do selects d[k] variables from evers with replacement
// E.g. d[k = 4, evars = [2), May sample xı, x1
Convert the selected d[k] variables to term // t = ck xf 22
end
10 fg
nnterme t A=1 Jzi
return
C TABLE OF CONSTRAINTS AND NOTATIONS
We provide the full list of constraints and notations in Table
#Products
uprod E {2, .... maxPp)
Term Constraints
#Factors in P.
nfac; E {2, 12..... maxfp), vi (1,.... ........ uprod}
#Terms in faj
terms((fu E {1...., maxT, Vfj E fp termss( (P:) maxTpVP E Po
#Terms in P:
Degree
#Degree in P5
dmn S Dp, Vm f' E tterms P), Vn x, E vars(f Σ dei DD, Vk terms(((s)))) Vfg Sp
Constraints
#Degree in fij
#Variables Po
xPl Vp
Variable
#Vaiiables in P:
vars Pi) S VV. VP: Po vars(fi;) S Vr, E
Constraints
#Variables in fa
Coeff in P
á Cp.Vd coeffs(P)
Coefficient Constraints
Coeff in P.
dej Cp, Va coeffs (P.). VP, e Po as < C₁ Va coeffi coeffs(ffy) Vfg E fp
Coeff in
Table 4: List of notations, and corresponding constraints that generated polynomial satisfies.
D PROBLEM SPACE SIZE ESTIMATION
We present the problem space size estimates here in Table
13

---

Under review as a conference paper at ICLR 2021
NVAR
NVAR
Config
Equation
Endpoint Size Estimate
Equation Size Estimate
Endpoint
Size Estimate
Size Estimate
SMALL COFFF
104M
8.24M
184M
27. .MM
MEDIUM COFFF
179M
16.3M
325M
42. 4M
LARGE COFFF
289M
32M
507M
68.8M 8M
NO BACKTRACK
324M
54.9M
538M
104M
MEDIUM DEG
459M
67.4M
902M
144M
MEDIUM TERMS
866M
31.5M
1.73B
801M
Table 5: Size Estimates for the problem space, after generating sets of size 5M.
E INPUT REPRESENTATION (ADDITIONAL RESULTS)
We present the results for FINE configuration for 2 variable setting here in Table 6 The errors made by the models for Variable and 2 Variable settings are presented in Tables and
respectively.
Config
Proof Type
Endipint
#Train
Full Prool
Stepwise
Calibration
Endpoint
Greedy
Top-1 Acc.
Beam-5 Acc.
Sure Rate
#EE
Proof
Stepwise
P
R
F1
Acc.
Acc.
SMALL
Innx//ine
4.3M
94.7
4.6M
88.1
97.19
90.7
92.2
83.47
100
92.02
0.96
COEFF
Pretx/PFiee
43M
93.33
54M
90.3
97.83
94.63
96.2
87.9
99.96
92.85
0.96
MEDIUM
Infi//Fnee
95.3
4.4M
82.2
96.25
94.28
95.76
86.24
100
91.47
0.96
COEFF
Prefix/Fine
5.2M
92.77
2.9
72.4
93.6
91.53
94.33
81.97
100
89.55
0.94
LARGE
3.2M
77.93
0.89
COFFF
Pretx/Pine
6.1M
86.6
4.7
78.6
95.6
91.93
93.47
83.87
100
91.23
0.95
NO
Infx//ine
8.6M
5.8M
72.5
94.64
81.54
84.82
72.34
100
88.72
0.94
BACKTRACK
Prefx/Fime
7.M
79.2
4.131
60.7
90.48
81.73
83.67
70.2
9931
85.81
0.92
MEDIUM
Innx/Fine
4.9M
87.9
3.6M
73.5
94.21
89.78
92.46
77.22
100
86.01
0.2
DEG
Prefix/Fine
5.2M
83.73
73.6
76.93
100
MEDIUM
Fine/Fine
8.3M
90
4.8M
64
92.98
79.04
81.86
66.92
99.88
84.56
0.92
TERMS
Table 6: Results for FINE configuration for 2 Variables for Infix and Prefix representation (No cur- riculum, No annotation).
Full Proof
Error Percentage
Config
Proof Type
Greedy Stepwise Accuracy
Full Proof
First FacStep
Total FacStep
First MulStep
Total MulStep
First SumStep
Total SunStep
Accuracy
Coarse/Inix
93
98.83
8
9.43
88
84.91
5.66
SMALL COFFF
98.9
99.79
Coarse/Preñx
933
98.97
4.26
4.08
72.34
7143
23.4
24.49
Fine/Prelix
96
99.4
9.68
9.68
77.42
71.42
12.9
12.9
Course/Inix
92.8
98.24
1.39
1.25
93.85
92.5
2.78
6.25
MEDIUM
Fine/lafix
97.99
11.34
11.32
85.57
84.91
3.77
COFFF
Coarse/Pretix
93.6
98.58
3.12
2.94
95.31
95.59
1,56
1.47
Fine/Prefix
98.37
2.41
2.33
96.39
96.51
Coarse/Infe
82.1
95.97
3.35
3.02
93.85
91.46
2.79
5.53
LARGE
96.44
2.86
2.56
93.71
COFFF
Coarse/Preix
83.3
96.25
4.24
3.78
93.94
92.97
1.82
3.24
Fine/Prelix
96.32
3.33
2.97
90.56
86.63
Course/Inix
75.6
94.62
2.87
3.13
93.44
86.83
3.69
10.03
NO
Fine/lafix
74.5
94.76
3.14
3.56
93.33
78.63
3.53
17.81
BACKTRACK
Coarse/Pretix
79.7
95.38
7.39
6.57
89.16
83.94
3.45
9.49
Fine/Prefix
95.23
2.37
2.41
96.44
89.16
1.19
8.43
Coarse/Infix
92.8
98.26
5.56
6.02
86.11
79.52
8.33
14.46
MEDIUM DEG
3.56
89.76
Coarse/Preii
87.
96.82
4.07
3.57
93.5
90.71
2.44
5.71
Fine/Prelix
90.6
97.92
8.51
7.55
89.36
87.74
2.13
4.72
Course/Inix
72.7
93.99
25.64
24.18
73.26
69.77
1.1
6.1
MEDIUM TERMS
Fine/lafix
75.1
95.42
21.29
20.51
75.1
69.94
3.61
9.55
Coarse/Pretix
76.3
95.78
7.59
8.71
88.61
84.67
3.8
6.62
Finc/Prefix
95.55
14.68
16.76
79.76
74.28
Table 7: Errors for 1 variable in the COARSE and FINE configuration for both Infix and Prefix input representation. (No curriculum, No annotation).
14

---

Under review as a conference paper at ICLR 2021
Full Proof
Error Percentage
Config
Proof Type
Greedy Stepwise Accuracy
Full Proof
First FacStep
Total FaeStep
First MulStep
Total MulStep
First SumStep
Total SumStep
Accuracy
Course/Inbx
87.9
97.01
5.79
4,9
88.43
79.72
5.79
15.38
SMALL COFFF
Fine/Iafi
97.19
8.4
7.98
75.63
68.1
15.97
23.93
Coarse/Prehx
91.2
98.08
1.14
1.03
88 64.64
84,54
10.23
14.43
Finc/Prefix
90.3
97.83
8.25
6.35
80.41
73.02
11.34
20.63
Coarse/Inlix
88.5
97.35
4.35
3.73
83.48
76.87
12.17
19.4
MEDIUM
Fine/Intix
82.2
96.25
2.25
1.83
76.4
68.81
21.35
29.36
COFFF
Coarse/Pretix
84.5
96.03
3.87
3.68
88.39
81.58
7.74
14.74
Fine/Pretix
72.4
93.6
12.68
9.95
76.09
67.74
11.23
22.31
Coarse/Inhx
80.4
95.18
6.12
4.84
82.65
75.81
11.22
19.35
LARGE COFFF
Fine/Infix
93.85
11.85
8.74
70.74
62.3
17.41
28.96
Coarse/Preeix
83.7
96,23
4.29
3.61
87.12
82.99
8.59
13.4
Fine/Prefix
78.6
95.6
5.14
4.2
81.31
74.43
13.55
21.37
Coarse/Inlix
72.7
93.13
4.4
3.15
87.55
75.79
8.06
21.07
Fine/latix
72.5
94.64
3.27
2.54
85.09
73.79
11.64
23.66
BACKTRACK
Coarse/Pretix
63.2
89.87
3.26
2.24
91.3
78.73
5.43
19.03
Finc/Pretix
60.7
90.48
2.29
1.38
89.31
72.64
25.79
Coarse/Inhx
80.5
95.13
6.67
5.44
81.54
71.97
11.79
22.59
MEDIUM
Fine/Intix
73.5
94.21
7.17
6.55
68.3
57.83
24.53
35.61
DEG
Coarse/Preñix
83.4
96.41
4.82
4.19
81.33
75.39
13.86
20.42
Fine/Pretix
73.6
94.37
7.58
6.38
75.38
67.48
17:05
26. 14
Cuarse/Inlix
64
92.03
25
19.05
72.5
66.5
2.5
14.45
13.61
8.62
TERMS
Coarse/Pretxx
67.8
93.58
10.25
7.69
87.89
80.98
1,86
11.32
Fing/Pretix
62.9
92.74
9.16
3.97
85.71
74.37
5.12
19:65
Table 8: Errors for 2 variables in the COARSE and FINE configuration for both Infix and Prefix input representation. (No curriculum, No annotation).
F ANNOTATED PROOF (ADDITIONAL RESULTS)
We present the results for COARSE and FINE configuration for 2 variable setting for annotated proofs here in Table The errors made by the models for I Variable and 2 Variable settings are presented in Tables 10 and respectively.
Config
Proof Type
Endpoint Examples
Endpoint
Endpoint Accuracy
# Train Esamples
Full Proof
Full Frunl
Greedy Stepuise Accuracy
Top-I Accuracy
Slepuise
Bram-5
Sure Rate
Calibrabio
SMALL COFFF
Courac
Fine
4.3
94.7
3.1M
3.6
$2.3
35
93.11
97.93
36.47
93.3
$4.03
$7.5
$1.85
30.27
100
100
06.54
94.61
0.96
MEDIUM CUEFF
95.3
3,35
3M
30.1
97.69
97.78
80.57
93.
51.5
96.77
90.2
99.93
LARGE COFFF
Coarse
Fine
9M
91.5
4.1M
4M
73.2
70.1
96.66
90.39
92.77
34.3
30.03
93.8
63.33
7727
99.85
100
04.04
91.33
0390
0.97
NO BACKTRACK
8.M
83.8
MEDIUM DEG
Course
Line
49M
87.9
3.9
4.1M
39.6
651
9501
95.28
91.13
85.43
67.43
93.7
36.4
18.2
99/90
100
91.47
91.78
0.96
0.96
R593
Table 9: Results for FINE and COARSE configurations for 2 Variables for annotated proofs (No curriculum).
G FULLY SYMBOLIC PROOFS
As > 80% of the eтrоrs occurred in multiplication step, we separately tested the Transformer's abil- ity to arithmetic, by creating datasets involving multiplication and addition of 4-digit and 9-digit numbers. While the models quickly achieved an accuracy of close to 99% for addition; for multipli- cation, they could not go beyond even 1% after seeing 2M examples. Hence, we envision a setting where polynomial simplification steps only involve symbolic addition and multiplication, without any arithmetic manipulation. For example, instead of multiplying and 4 as 12, the model will output C1 C2 given coefficients C₁ and cg. The results for Variable setting are presented in Table I2 Here, MEDIUM COEFF and MEDIUM DEGREE denote the same configuration as the case with integer coefficients. The only difference being that the limits of coefficients longer apply. The
15

---

Under review as a conference paper at ICLR 2021
Config
Proof Type
Full Proof
Full Proof
Greedy Stepwise Accuracy
First FacStop
Total FacStup
First MuilSte
Total MulStop
Error Percentage
First SumSSop
Total SumStup
First MarkStep
Todal MarkStep
Accuracy
SMALL COFFF
Cusrse
Fine
88.5
91.9
99.16
98.82
3,68
1.23
2.99
1.19
98.17
89.57
83.58
96.43
6.09
0
11.19
1.19
0.87
0
2.24
1.19
V8.29
84.88
5.81
LARGE CORFF
Hine
9:21
87.30
66.35
19.08
4.76
2.25
NO BACKTRACK
Lourse
Fine
29.7
68
96.78
93
1.19
6.2
5:25
5:16
56.56
33.19
78.54
7688
3.72
5.62
1520
12.0
0.82
1330
2229
243
MEDIUM DEG
Cousse
Fine
78.7
07.88
11.57
6.1
10.35
534
56.38
32.5
31.32
80.31
3.35
4.09
9.23
6.78
232
2003
5:11
MEDIUM TERMS
838
Table 10: Errors for FINE and COARSE configurations for Variable for annotated proofs (No cur- riculum).
Config
Proof Type
Full Proof
Erear Percenlage
Full Proof Accuracy
Stupwise
FacStep
Total FacStup
First
Total MulStep
SumSlep
Total SumSSte
MarkStep
Total MarkSlep
Accuracy
SMALL COEFF
Fine
87.5
07.33
98.31
4.52
307
36.44
68.97
78.21
7.34
24.14
18.25
1.99
3.81
1.55
MEDIUM COFFF
Fine
79.8
97.75
8.96
6.79
80.19
68.21
9:45
22.5
1,42
2.5
Cousse
80.1
97.69
9.05
7.29
$2.94
30.33
3.02
10.66
1.23
Course
73.2
96.66
10:45
7.84
79.85
70.87
7.84
18:49
1.87
2.8
NO BACKTRACK
Fine
92.93
9.16
5:35
74.31
57.9
14.58
33.69
2,06
3.25
MEDIUM DEG
Corsse
Fine
59.6
65.1
95.25
9546
6.88
7.43
3.26
5.48
78.31
72.03
67.79
57.1
11.40
15.35
24.03
32.9
3.15
5.2
233
4.52
21.55
67.9
23.95
300
MEDIUM TERMS
Consse 32R
04.37
23.34
150
6022
62.77
3.5
16.07
4.24
436
Table 11: Errors for FINE and COARSE configurations for 2 Variable for annotated proofs (No cur- riculum).
errors made by the model for each kind of step summarized in Table We observe that the proof accuracy is about 20% less than the non-symbolic models. This could be because the intermediate polynomials in the simplification sequence become very long with sym- bolic coefficients.
Proof
Endpoint
Full Proof
Config
#Train
Type
Full Proof
Greedy Stepwise
Endpoint Acc.
#EE
Acc.
Acc.
Coarsc/Infix Fine/Infix
4.3M
78.5
94.19 19
5M
93.5
MEDIUM COFFF
2.8M
63.5
90.64
Coarsc/Prefix
3.7M
70.9
91.53
Fine/Pretix 4.9M
89.77
4.3M
70.9
93.2
Coarse/Infix
3.7M
65.2
89.55
5.6M
88
MEDIUM DEGREE
Fine/Inñix
6.3M
75.5
94.59
Coarse/Prelix
3.4M
57.6
85.98
6.3M
83.93
Fine/Prefix
6.7M
67.7
92.76
Table 12: Results for Variable Symbolic Coeff setting. (No curriculum, No annotation).
H OUT-OFF-DITTRBUTION EVALUATION
We present the results for Out-of-Distribution evaluation here. Table 14 contains results for best variable models (Prefix/Coarse) tested on Variable setting. Table 15 contains results for best variable models (Prefix/Coarse) tested on SMALL, MEDIUM and LARGE coefficient setting. As expected, the SMALL and MEDIUM models perform much worse when tested on higher coefficients.
We also evaluated the best variable models (Prefix/Coarse) MEDIUM DEGREF and TERMS set-
16

---

Under review as a conference paper at ICLR 2021
Full Proof
Error Percentage
Config
Type
Greedy Stepwise Accuracy
Full Proof
First FacStep
Total FacStep
First MulStep
Total MulStep
First SumStep
Total SumStep
Accuracy
Course/Intix
78.5
94.19
3.72
2.82
77.67
67.25
18.6
29.93
MEDIUM COFFF
Fine/Infix
63.5
90.64
3.29
2.29
79.73
67.43
16.99
30.28
Coarse/Prefix
91.53
2.06
1.45
76.29
64.01
21.65
34.54
Finc/Prefix
70.9
93,2
1.37
0.97
73.88
66.1
24.74
32,93
Coarse/Intix
65.2
89.55
2.01
1.41
85.06
71.49
12.93
27.11
MEDIUM DEGREE
Fine/Innx
94.59
0.31
86.12
77.02
13447
22.67
Coarsc/Prelix
85.98
4.34
83.25
63.42
10.14
30.24
Fine/Prelix
67.7
92.76
1,86
1.39
88.54
79.35
9.6
19.26
Table 13: Errors made by models in 1 Variable Symbolic Coeff setting. (No curriculum, No annota- tion).
tings, to check generalization with respect to # terms and degree of polynomial. Table 16 contains results for the same. The MEDICM COFFF model is not able to generalize more terms or polyno- mials of higher degree.
Train/ Test= 2 Varí1 Var
Train/Test= 1 Var/1 Var
Train/ Var22 Var
Config
Greedy Stepwise Acc.
Full Proof Acc.
Greedy Stepwise Acc.
Greedy
Proof Acc.
Proof Acc.
Stepwise Aec.
SMALL
95.34
99.12
95.3
98.97
91.2
98.08
COEFF
MEDIUM
87.4
97.11
93.6
98.58
84.5
96.03
COEFF
LARGE
97.13
96.25
COFFF
NO BACK
TRACK
84,2
98.29
79.7
95.38
63.2
89.87
MEDIUM
DEG
87.7
97.83
87.7
96.82
83.4
96.41
MEDIUM
TERMS
78.5
96.16
76.3
95.78
67.8
93.58
Table 14: Results for OOD Testing. NVAR = 2 COARSE/PREFIX models tested on corresponding NVAR setting (No curriculum, No annotation).
Test Config
Train Config
SMALL
MEDIUM
LARGE COEFF
COFFF
COFFF
Full Proof Acc.
Greedy
Full
Greedy
Full
Greedy
Stepwisc
Proof
Stepwise
Proof
Stepwise
Acc.
Acc.
Acc.
Acc.
Acc.
SMALL COEFF
95.3
98.97
33.4
69.05
31
68.02
MEDIUM
96.6
99.29
93.6
98.58
33.6
68.96
COFFF
LARGE COFFF
95.8
99.1
94.4
98.64
83.5
96.25
Table 15: OOD Testing: Prefix/Coarse Variable Models tested on various coefficient limit config- urations (SMALL, MEDIUM and COARSE). (No curriculum, No annotation).
I CURRICULUM LEARNING
Learning the simplification steps should entail learning the sub-tasks, such as addition and mul- tiplication (of numeric coefficients and symbolic variables); where multiplying variables precludes learning to add exponents of similar variables. As these sub-tasks well-defined and dependencies among them are clear, we explore different types of curriculums based on the Mastering- Rate-based (MR) curriculum learning algorithm proposed in Willems et al. (2020). Authors in Willems et al.
17

---

Under review as a conference paper at ICLR 2021
Test Config
Train Config
MEDIUM COFFF
MEDIUM
MEDIUM TERMS
DEG
Full
Greedy
Full
Greedy
Full Proof Acc.
Greedy
Proof Acc.
Stepwise
Proof Acc.
Stepwise
Stepwise
Acc.
Acc.
Acc.
MEDIUM
93.6
98.58
20.8
47.77
26.1
54.65
COFFF
MEDIUM
94.8
98.93
87.7
96.82
25.5
54.39
DEG
MEDIUM TERMS
92.7
96.87
18.6
46.97
76.3
95.78
Table 16: Prelix/Coarse 1 Variable Models tested on various #term and degree configurations (MEDIUM DEGREE and MEDIUM TERMS). (No curriculum, No annotation).
2020) define curriculum learning by 1) curriculum i.c. set of tasks C = {cI...., Cn }. where a task is set of examples of similar type with a sampling distribution, and 2) a program which for each training step defines the tasks train the learner given its learning state and the curriculum. Formally, the program d N + DC, is a sequence of distributions over C. The authors estimate the program function through an attention function which defines attention over the tasks a time-step, and an attention-tor irrention-to-distribnn to-distribution converter which converts the attention to a distribution over C. Au- thors observe that other algorithms (Matiisen et al. 2019 Graves al. 2017) are special cases of the above setting with different choices for program.
To learn on tasks that are learnable but not learnt yet, authors define an ordered curriculum O which is a directed graph over tasks in C. An edge from A to B indicates that learning task A before is preferable. For supervised learners, the learnability for each task depends on mastering rate (Ma(t)) computed from the normalized mean accuracy for that task at time-step t. At each time- step, the MR algorithm computes attention over a task (t)( from mastering rates of its ancestors and successors. During training to sample batches, hyperparameter N₂ for the curriculum deter- mines the number batches to be considered at a step, before ce-momuuing the attention over tasks. Using the program d, first sample N₂ b examples from tasks in C. The model is then trained on randomly sampled N2 minibatches are sampled updating the mastering rates.
For polynomial simplification for variable, SCOEFF and MIXED. For ADD, only one factor per product allowed, so there is no multiplication. For MUL2 and MUL3 only product is allowed with maximum two factors and three factors spectively, SCOEFF points to the SMALL COEFF configuration and MIXED is the final variable size configuration of the target variable configuration. We define the following curriculums:
define the following tasks ADD, MUL.2, 2, MUL.3,
C: {(ADD, MUL3), (MUL3, MIXED), (ADD, MIXED)]
C2: {(ADD, MCL2), (MUL2, MUL3), (MUL3, MIXED), (ADD, MIXED)).
C4: (ADD,, MUT.2), (MUL.2, MUT.3), (MUL33, SCOFFF), (ADD, SCOFFF) (SCOFFF, MIXED)). For all our experiments, we use the MR algorithm with gAmax Linreg A2D converter functions de- scribed in Willems et al. (2020). Model parameters and the training configurations remains the same as beford 5 We show the results in Table 17 for COARSE configuration. As coefficient size grows from SMALL, MEDIUM, LARGE to No BACKTRACK the improvements in full proof accuracy steadily increase from 1% to 10.84%. For No BACKTRACK, the improvement in top-1 accuracy is by 20% from no curriculum setting. However, observe for MEDIUM TERMS, there is drop in accuracy for all curriculums and input representations. It is possible that, more carefully designed curriculums may improve the results. There is conceivable pattern observed for infix prefix representations. However, compared to learning without curriculum, the improvement observed for infix representation is larger than prefix.
We use N₂ 10. For other default parameters in CI., please check g wtthub.ccommee. e automati c- curric culum Tum)
18

---

Under review as a conference paper at ICLR 2021
Proof
Step-wise
Calibration
Cumi
Full Proof
Stepwise
Top-1
Beam-5
Sure
#Train
R
F1
culum
Accuracy
Accuracy
Ace
Acc
Rate
2.8M
94.38
98.76
94.84
96.68
89.36
100
94.22
0.97
Infix
Small
2M
95.98
99.0
91.64
93.24
99.9
93.98
Coeff
2.02M
94.26
98.65
77.76
80.46
70.62
99.94
90.77
Prefix
C2
2.29M
94.6
98.56
93.44
95.28
88.02
99.89
94.09
0.97
Infix
3.9M
95.44
99.02
94.86
96.44
96.12
Medium
C4
2M
93.86
98.59
88.22
90.24
84.68
99.91
95.90
Coeff
C2
3.7M
94.78
98.82
91.98
93.66
88.08
99.93
95.69
0.98
Prefix
C4
4.4M
94.8
98.87
85.3
87.82
80.62
99.98
94.49
0.97
C2
6.9M
91.26
97.92
96.4
98.06
90.24
99.89
93.51
0.97
Infix
Large
C4
7.6M
91.62
98.16
91.54
93.3
87.38
99.84 84
95.3
0.98
Coeff
C2
6.5M
92.2
98.31
85.38
87.78
81.42
99.95
95.32
0.98
Prefix
C4
6.97M
92.46
98.42
91.3
93.34
87.54
100.0
95.88
0.98
C2
4.8M
86.44
97.27
93.68
95.46
88.72
99.98
94.68
0.97
No
C4
5.1M
85.96
97.21
94.64
96.1
89.5
100)
94.57
0.97
Backtrack
C2
7M
86.16
97.30
82,24
84.44
77.46
99.95
94.12
0.97
Prefix
C4
5.3M
86.48
97.45
92.6
94.3
87.78
99.95
94.75
0.97
C2
3.5M
87.12
97.01
84.16
87, 47.44
78.46
99.95
93.18
0.96
Infix
Medium
C4
3.4M
94.12
98.65
90.62
81.984
86.66
99.93
95.56
0.98
Degree
C2
5,35M
94.28
98.71
80.8
82.84
75.76
100
93.5
0.97
Prefix
C4
3.3M
92.38
98.30
83.7
85.48
78.94
99.92
94.24
0.97
C2
4.4M
59.54
75.76
65.6
69.56
60.84
95.36
88.45
0.92
Infix
Medium
C4
3.8M
36.94
76.72
69.84
73.44
60.77
97.3
84.82
0.91
Terms
C2
2.8M
41.84
51.24
40.62
45.36
36.9
92.57
84.10
0.88
Prefix
C4
3.37M
49.02
65.41
58.56
64.64
45.44
96.83
75.14
0.85
Table 17: Currieulum Learning results for variable for the COARSE configuration for both Infix and prefix representations.
19


Reviews:
[{"review_id": "dWBgvQvwmr8", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper \"Do Transformers Understand Polynomial Simplification?\" introduces a new reasoning task (convert polynomials into a normal form) and studies the performance and errors of Transformers on this task. The task itself is quite simple: given a randomly generated term involving small constants, variables, additions, and multiplications, bring the term into a well-defined normal form. Each task has to be solved in a unique sequence of steps. The authors study the performance of Transformers to either simplify the expressions step by step or to predict the simplified version directly.\n\nContributions I highly appreciate:\n- Contrasting step-wise generation of proofs vs end-point prediction.\n- Contrasting different representations of formulas: prefix notation appears to be better than infix notation.\n- Observation that transformers struggle with multiplication.\n\nQuestions to the authors:\n- The task is pretty simple compared to other (mathematical) reasoning tasks studied in the literature. The task is also not very useful as a prediction target, because it can be solved with a simple algorithm, as far as I can see. The paper essentially claims that this allows us to study Transformers better. What insights were produced here that couldn't have been produced on more challenging benchmark from the literature?\n- Why is it important for your paper that proofs are unique? Do we simply train Transformers to execute a simple algorithm? If so, how does that relate to the existing theorem proving and reasoning approaches where we usually have many possible proofs for a task.\n- What is the point of \"establishing baselines\" if the task is essentially solved already with moderately-sized Transformers?\n- What can be learned from the curriculum learning experiments? The way the curriculum is defined here appears to essentially require a synthetic benchmark for which we can generate examples of different hardness levels. So how could this help for real problems?\n- Introduction and Conclusion: The paper claims that training on the two variable case leads to better performance on the one variable case than training on it directly. This sounds very much like an artifact that could stem from the lack of training data or so. How is this possible?\n\n\nMinor comments:\n\np.1, pargraph 1: I believe Hahn et al also propose an \"end-to-end\" task using Transformers instead of embedding their approach in an existing neuro-symbolic system.\n\np.1, paragraph 2: The reference to Lample & Charton is slightly off: It was published in ICLR 2020.\n\np.2, paragraph 1: \"we observe that the system can understand candidate sub-expressions ...\" I am always wary of the use of \"understand\" in the context of neural networks, as it is not very clear what it means.\n\np2. related work: I do not understand how you contrast your work to the existing theorem proving works: There are a number of neural theorem provers (HOList, GamePad, GPT-f, and probably some more) that also generate proofs step by step. They might employ more advanced search ideas, but I think it would be good to state why your paper does not want to go in this direction.\n\np.2, Section 3: How does Sympy \"ensure correctness\"? There could be bugs in the code even if you didn't write the code yourself?\n\np.2, footnote: \"an unique\" -> \"a unique\"\n\np.3, last paragraph: remove \"Hence\".\n\nAdditional details about the training setup would be appreciated. For example, how many training steps/epochs did you train for?", "extra_scores": {}, "extra_text": {}}, {"review_id": "Zx8WRLxWsX", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper studies the capability of the transformer architecture to\nperform rewriting to normal form in a simplified polynomial setting.\n\nIt is a continuation of the research by Piotrowski et al (PUBK) in the\narea of using neural nets to do symbolic rewriting, followed later by\nLample&Charton (LC).\n\nSeveral datasets are generated, using various\nconstraints on the sizes of coefficients, etc. Using infix vs prefix\nnotation is also analyzed. The number of variables is either 1 or 2,\nwhich seems insufficient. Already PUBK shows that going from 2 to 3\n(poly 5 vs poly6) variables reduces the performance considerably.\n\nThe main difference to PUBK is that the unnormalized polynomials are\ngenerated in a simpler format (sum of products of factors) that makes\n(or should make) the normalization procedure very simple. And that the\nevaluation is done step-wise, similar e.g. to work of Gauthier [3].\n\nThe setting is a bit problematic when compared to the full setting\nalso by forcing the normalization to be done in a particular \"obvious\"\nway. A richer set of rewriting steps consisting e.g. of finding common\nfactors (as e.g. in 2*(2x+1)*(y+1)*(z+2) + 2*(2x+1)*(y+1)*(z+3)) could\nlead to shorter rewriting sequences. These two issues - very\nsimple polynomials and very constrained rewriting rules - imply that\nthe setting is insufficient to answer the question posed by the title.\n\nMy overall feeling is that the paper shows a lot of experimental data,\nbut it does not bring sufficiently interesting new insights.\n\nSome more comments:\n\nThe poor generalization (e.g. Table 16) of the transformer to symbolic\ndata generated differently is not very surprising. Still, I am missing\ninformation about testing transformers trained on fewer variables on\ndata with more variables.\n\nOn page 5 the authors say \"We make sure that the simplified versions\nof the input polynomial in the training batches, do not collide with\nany endpoints in the  test and validation set.\"  \n==> \nHow was this done? PUBK shows that one simple kind of replacement in data (CONST\ninstead of all digits) leads to very large train/test overlaps in\nLC. But PUBK says that this is initial and much more needs to be\ndone. A simple improvement suggested there is measuring the\nLevenshtein distance as in Wang et al., 2018. [1]. I would expect much\nmore on this topic given the previous work and their issues.\n\nCompared with Zombori et al. [2], none of the settings is ever\nshown to learn perfectly a usable (even if simple) algorithm.\n\np2: \"As a state-of-the-art model, we explore Transformers. While both Graph Neural Networks and\nTransformers have been used for single-step representation learning of symbolic theorems and single\nstep goal-theorem scoring, Transformer-based sequence-to-sequence networks have shown superior-\nity in end-to-end tasks in integration, differential equations\"\n==>\nVarious versions of tree neural nets have been used quite successfully by Gauthier for related symbolic tasks [3].  Similarly for guiding theorem provers, in particular in ENIGMA [4] .\n\nPrefix vs infix: see [5] for previous related work on this and more.\n\np2: symbolic re-write==> symbolic rewriting\n\np2: the facstep in the example is unclear/confusing - X^1 is replaced just by X.\n==> What is the underlying representation? Can you give a more illustrative example of facstep?\n\n\nReferences:\n\n[1] Qingxiang Wang, Cezary Kaliszyk, Josef Urban:\nFirst Experiments with Neural Translation of Informal to Formal Mathematics. CICM 2018: 255-270\n\n[2] Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban:\nTowards Finding Longer Proofs. CoRR abs/1905.13100 (2019)\n\n[3] Thibault Gauthier:\nDeep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic. LPAR 2020: 230-248\n\n[4] Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban:\nENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CADE 2019: 197-215\n\n[5] Bartosz Piotrowski, Josef Urban:\nStateful Premise Selection by Recurrent Neural Networks. LPAR 2020: 409-422\n\n========================\n\nUPDATE\n\nThe response says:\n\n\"With the straightforward use of Transformers, where the model has only seen a single variable in training, there’s no information for the model about what to do with the second variable and thus it will not generalize to the two variable case. Training on two variable-polynomials and testing on two variable-polynomials has relatively low accuracies in our experiment. This suggests that training on single variable-polynomials and testing on two variable-polynomials will result in even lower accuracies. With more work, one may be able to design a model with appropriate inductive bias that understands the concept of multiple variables. This is beyond our scope.\"\n\nI am afraid that this makes the study rather insufficient for me. The problem of representing variables, eigenvariables/skolems, and capturing structural similarity between different theories and signatures is ubiquitous in the ML-for-TP area. Practically all useful systems developed so far - both features-based and DL-based - have to address this. The authors' answer is \"our representation is unsuitable\". The observation that if you have no shared representation of variables, you will get little/no generalization is a no-brainer and there is hardly any need to publish negative papers about it. In particular, in a conference about *representations* and some 15 years after first useful systems dealing with such issues have been developed. There are many fixes to this - see e.g. Gauthier's representation of variables in his Tree NNs, etc.\n\nMy score will stand, but I would like to encourage the authors to dig deeper and follow the suggestions given in this and other reviews. The general topic of learnability of symbolic rewriting by various neural architectures is certainly interesting, potentially very useful, and far from well understood.\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "MMUFF9E2xmm", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper studies the efficacy of transformers on a polynomial simplification tasks. \n\nThere are two main motivations for this work: Piotrowski et al and, Lample and Sarton (references in the paper). The paper is set out to explore the capability of transformer networks of creating muti-step proofs. \n\nOne of the contributions of the paper is the creation of dataset of polynomial simplifications. They use the method in Lample and Charleston to generate a large random dataset of polynomials represented as a sum of products. Each term in that product is a product of a small set of factors. So the basic question is: how do we represent this polynomial by a formula of minimum length, in which each operation is one of the +, - or *.  \n\nThis is a hard question for sure.\n\nBut is this question as hard as in Lample and Sarton?\n\nIs it hard as computing integrals of expressions?\n\nEverybofy knows that computing integrals is hard. In fact, it is much harder than computing partial derivatives.\n\nHow hard is it to give a representation of a sum of products? It might be hard. But is it as hard as the above?\n\nI can't tell, but this paper does not even specify what is a baseline. When do we believe that something is important.\n\nThis paper fails to specify what is an interesting message and fails to specify that message.\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "ANkct9HsvT", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The authors analyze the performance of Transformer models on simplifying polynomials and - importantly - generating proofs at the same time. This is a very nice idea that allows to study the performance of Transformers in depth and at the same time in an important setting where verification is performed as part of running the model. And the authors show a strong baseline, with models performing very well in a number of settings. A few areas seem to have been neglected though. For one, the authors only train a 4-layer 4-head model, which is quite small as far as Transformers go. Maybe it's irrelevant for this problem - but having at least one bigger model as a point of comparison would be good. Next, the out-of-distribution question warrants more experiments. Can the Transformers simplify polynomials with way more factors than trained on? With a higher number of variables? Higher degrees? The authors also show that one main problem for Transformers is learning to multiply the coefficients. But - assuming this reviewer understood correctly - the authors do not apply the proof requirement to multiplication. E.g., for \"12*3\" the model has to immediately output \"36\" rather than \"10*3 + 2*3 = 30 + 6 = 36\". Maybe this could help the Transformer learn and be more resilient to coefficient size? So while the current version of the paper is ok, there are a few areas for improvement which prevent it from being a clear accept.", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: While the reviewers find the experiments in the paper somewhat interesting, they find that the paper does not sufficiently address whether the limitations shown for models in this paper translate to larger models and other, more realistic, tasks, or an artifact of the setup considered in the paper.  Overall the takeaways seem unclear from the paper and I believe it is not ready for acceptance.  Addressing the issues raised by reviewers and having a more clear discussion on connections to existing results will help the paper.
Decision: Reject