Learning Axioms to Compute Verifiable Symbolic Expression Equivalence Proofs Using Graph-to-Sequence Networks
Authors: Steven James Kommrusch
Louis-Noel Pouchet
Theo Barolett
Venue:  (2021)
Keywords: Graph Neural Network
Symbolic Proofs
Graph-to-Sequence

Abstract: We target the problem of proving the semantic equivalence between two complex expressions represented as typed trees, and demonstrate our system on expressions from a rich multi-type symbolic language for linear algebra. We propose the first graph-to-sequence deep learning system to generate axiomatic proofs of equivalence between program pairs. We generate expressions which include scalars, vectors and matrices and 16 distinct operators combining them, with 147 distinct axioms of equivalence. We study the robustness of the system to generate proofs of increasing length, demonstrating how incremental graph-to-sequence networks can learn to represent complex and verifiable symbolic reasoning. It achieves 93% average true positive coverage on 10,000 test cases while ensuring zero false positives by design.

Under review as a conference paper at ICLR 2021
LEARNING AXIOMS TO COMPUTE VERIFIABLE SYM- BOLIC EXPRESSION EQUIVALENCE PROOFS USING GRAPH-TO-SEQUENCE NETWORKS
Anonymous authors Paper under doublc-blind review
ABSTRACT
We target the problem of proving semantic equivalence between two complex expressions represented as typed trees, and demonstrate our system on expressions from rich multi-type symbolic language for linear algebra. We propose the first graph-to-sequence deep learning system to generate axiomatic proofs of equivalence between program pairs. We generate expressions which include scalars, vectors and matrices and 16 distinct operators combining them, with 147 distinct axioms of equivalence. We study the robustness of the system to generate proofs of increasing length, demonstrating how incremental seaph-to-sqqeene networks can learn to represent complex and verifiable symbolic reasoning. It achieves 93% average true positive coverage on 10,000 test cases while ensuring zero false positives by design.
INTRODUCTION
Deep neural networks have excelled at a variety of classification and reinforcement learning tasks (Goodrellow al. 2016). However, their stochastic nature tends hinder their ability to learn repre- sentations useful for manipulating symbolic information. For applications requiring a guarantee of correctness, such as occur relation to determining the semantic equivalence between two programs (or symbolic expressions), a system that produces provably correct output must be developed.
In this work we target the problem of automatically computing whether two input programs are semantically equivalent (Kaplan 1969). under well-defined axiomatic system for equivalence using semantics- prretticespeeeevinggggg. rewrite rules (Dershowitz) 1985). Program equivalence summarized as determining whether two programs would always produce the same outputs for all possible inputs, and is central problem in computing (Kaplan 1969) [969] Godlin Strichman 2008 Verdoolaege et al.
2009). The problem ranges from undecidable, e.g. Goldblatt & Jackson (2012), trivial in cases of testing the equivalence of a program with itself. Our work directly studies the subset of programs represented by symbolic linear algebra expressions which include scalar, vector, and matrix types for both constants and variables, and 16 different operators with 147 distinct axioms of equivalence, creating foundation for future work with broader program semanties. For example, the expression using matrices, scalars, and vector: (A + [[a + (b - aajū AT can be proven equivalent to Bū by applying 10 axioms in sequence; our work generates the proof steps between these expressions.
While prior work has shown promise for deep networks to compute some forms of program equiv- alence (Xu et al. 2017 Alon et al.) 2019 Rabin et al.) 2020), the system typically outputs only probability of equivalence, without any reasoning or insight that can be verified casily: false positives can be produced. Programs can be represented as tree (or graph) of symbols, and deep networks for symbolic reasoning have been studied, e.g. to compute the derivative of a symbolic expression (Lample & Charton 2020), but such systems can produce output which is not directly explained by the system itself. In this work, we take fundamentally different approach to the problem of symbolic program reasoning with deep networks: we make the system produce the sequence of steps that lead to rewriting one program into another, that is the reasoning for (or proof of) equivalence between the two programs, instead of producing directly the result of this reasoning (c.g.. the transformed expression (Lample & Charton 2020

---

Under review as a conference paper at ICLR 2021
We propose method for generating training samples using probabilistic applications of production rules within a formal grammar, and then develop a graph-to-sequent eLi et al.) 2016)] Beck et al. 2018) neural network system for program equivalence, trained to learn and combine rewrite rules to rewrite one program into another. It can deterministically prove equivalence, entirely avoids false positives, and quickly invalidates incorrect answers produced by the network (no deterministic answer is provided in this case, only a probability of non-equivalence). In nutshell, we develop neural network system to accelerate the search in the space of possible
the first graph-to-sequee combinations of transformation rules (i.e., axioms of equivalence in the input language) to make two graphs representing programs structurally identical without violating their original semantics. We make the following contributions:
(i) We propose machine learning system for program equivalence which ensures correctness for all non-equivalent programs input, and a deterministically checkable output for equivalent programs (no false positives, specificity = 100%).
(ii) We introduce pe graph2axiom the first incremental graph-to-sequee tem targeting program equivalence to the best of our knowledge. We provide the first implementation of such traph-to-sequence systems in the popular OpenNMT-py framework (Klein et al., (017). (iii) We present a complete implementation type linear algebra expressions. Our system provides correct rewrite rule sequence between two equivalent programs for 93% of the 10,000 test cases. The correctness of the rewrite rule is deterministically checkable in all cases in negligible time.
neural network sys-
our system operating on a rich language for multi-
2 PROGRAM EQUIVALENCE USING DEEP LEARNING
We outline below the key intuitions and concepts for our program equivalence system. Extensive details, including full formal framework for program equivalence reasoning, are presented in supplementary material, Secs. A B, We illustrate below four very simple computations, represented as graphs, that are all equivalent under various axioms of natural arithmetic.
pl:(1+a)
(b
P2:0+ eb+
P3:
Pe:a+c+art
Rewrite rules as axioms of equivalence In this work we represent programs with symbolic expres- sions made of variables (c.g., a, b, c), operators (e.g., +, +) and neutral/absorbing elements (c.g., 1). We consider rich linear algebra expression language, supporting three variable types (scalars as shown in P1-P4, vectors, and matrices) and 5 different variables per type; 16 operators including operators mixing different variable types such as vector-mate matrix product. We represent these programs as dataflow graphs Buck & Lee (1993) with root node that is to compute single value.
P1 is equivalent to P2 we consider the axiom A1 : IN x T, Vr E This axiom also a clear rewrite rule: the I. LHS expression I x (with x E N) can be matched and replaced by the RHS expression I anywhere in the program without altering its semantics. An axiom, or cquivalently here graph rewrite rule, may be applied repeatedly to different subtrees. When applying Al specific location, the node a of Pl, we obtain an equivalent and yet syntactically different program, we note P1 = (a, P1). To assess the validity of transformation sequence S where P2 = S(P1), one simply needs to check for S. in sequence, that each axiom is applicable at that program point, apply it obtain a new temporary program, and repeat the process for each axiom in the complete sequence. If the sequence is verified to be valid, and S(P1) I) is structurally equivalent to P2, then we have proved P1 P2, and S forms the complete proof of equivalence between the two programs. These equivalences can be composed, incrementally, to form a complex transformation. Using A2 x (y + 2) = x y + I. 2, Vx, y, z E N and A3 x + = y + x, Vr, E N, we have P1 P4 A3( A2(*, (l, P1))), verifiable proof of equivalence under our axioms between the programs la(b + c) and ac + ab, which involved structural changes including node deletion, creation and edge modification. Note the non-unicity of sequence: by possibly many ways program can be rewritten into another one, for example the sequence P4 = A2(,, A3(+, Al(a, P1))) also correctly rewrites P1 into P4. Conversely, sequence may not exist: for example sequence of the 3 above axioms allows rewriting a + b into a b. We call these non-equivalent in our system, that is precisely if there is sequence of axioms that can be applied to rewrite program into the other.
2

---

Under review as a conference paper at ICLR 2021
Our approach aims to compute some S for pair of programs P1, P2, that S is verified correct when P1 = P2. Consequently, if P1 & P2, no sequence S produced can be verified correct: true negatives are trivially detected.
Pathfinding program equivalence proofs Intuitively, we can view the solution space as a graph, where every possible syntactically different program in the language is represented by its own vertex vg. And 3 e(Az..) vs Ui iff 3Ag an axiom and E such that vi A& (zr, 0z). Any two programs connected by a path in this graph are therefore semantically equivalent. Building S for P1 = ((2)) amounts to exposing one path between P1 and P2 in this graph when it exists, the path forming the proof of equivalence. We build a deep learning
system to learn stochastic approximation of iterative algorithm to construct such feasible path when possible, trained only by randomly sampling pairs of programs and one carefully labeled path between them. This avoids the need craft smart exploration heuristics make this path-finding problem practical.
Verifiable proof
Lexical equivalence
Axioms
(prag2 prog irogint)= proof found
N
Output components
Global Attention
Token generator
sprog
Intermediate
Sample Generation las 30 akkn desi)
program
Decoder
generation
components
Graph neural
LSTM2
network
layers
Encoder
Grammar
Axiom
components
Slentt :2 WWatnoo dlectors ddaltan
sprog 1>
Node
Token
Initialization
Embedding
start
Figure I: pe gra.haaaiiaaiiooom om System Overview
Graph-to-sequence network for pathfinding The system in Fig. | takes as input two programs represented as symbolic trees, and produces a sequence of axioms along with their position of application (or node) that can be used to rewrite sequentially one input program into the other input program. Node initialization initializes the graph neural network, converting the input programs text (e.g.. + (b + c)) into nodes and edges in the Graph Neural Network Scarselli et al. (2009); ; Xu et al. (217)) The details of the network are covered in Sec. [5] In nutshell, the key principle is to combine a memory-bate based neural network approach, e.g., using Long- Shoor Term Memory (LSTM) Hochreiter & Schmidhuber (1997) neurons and a graph neural network design (which uses Gated Recurrent Units (GRUs) internally) Beck et al. 2018) that matches our program graph representation. Token embedding is neural network layer in which tokens are assigned learnable multidimensional embedding vector Mikolov et al. (2013). Each layer in /.TM layers has 256 neurons, which support sequence generation. Token generator is the final output portion of the network. It learns to output the tokens based on the current LSTM hidden states and the Global Attention from the graph neural network. As each token is output, it feeds back into the LSTM layer through the embedding layer to affect its next state. We use a sequence generation principle, using a global attention mechanism Luong et al. (2015) to allow observation of program graph node information while generating the axiom and location on which it is applied. We specifically study the robustness of our approach to generate proofs of increasingly complex length. contrasting models to output the entire path once with wwlpppe-apaeeee -wwggrappphaaa axion which incrementally builds the sequence one step at a time in Sec. 6
RELATED WORK
Program analysis with machine learning Numerous prior works have employed (deep) machine
learning for program analysis (Allamanis et al. 2018a Alon et al. 2019 Tufano al. 2019
Lacomis et al. 2019. Raychev et al. 2013 Bavishi et al. 2017). PHOG (Billik et al. 20166) presents a probabilistic grammar to predict node types in an AST. Program repair approaches, (Tufano 2019 Chen et al.) 2019) are deployed to automatically repair bugs in a program. Wang et al. ct al. (018 learn to extract the rules for Tomita grammars (Tomita) 1982) with recurrent neural networks. The learned network weights are processed to create a verifiable deterministic finite automata representation of the learned grammar. This work demonstrates that deterministic grammars can be learned with RNNs, which we rely on. Recent work by Rabin et al. (2020) shows that GGNNs learn more general representations of semantically equivalent programs than code2vec (Alon et al.) 2019, which creates code representations using AST paths. Bui (222)) shows that using semantics
3

---

Under review as a conference paper at ICLR 2021
preserving transformation can improve machine learning on code; we target learning to identify the transformations that prove equivalence.
Symbolic mathematics using machine learning has received recent interest. Fawzi et al. (2019) develop a system which learns to apply a set of incquality axioms and derived lemmas using a reinforcement learning model with ford-forward neural network. A challenge of using reinforcement learning is the determination of a feasible reward function from the environment and the resulting training time. [aansal al. (2019) present system that can interact with large rule set score tactics in the search for a proof but discuss the compute time limitations of training a reinforcement learning network for theorem proving. Unlike their model, we output both the tactic (axiom) as well as the location to apply it (eliminating the need to score various premises individually). Paliwal ct al. (2019) explores using graph neural networks as applied to theorem proving in the HOList environment. Our work aims at laying the foundation for program equivalence proofs by studying language subset that includes variable types and maintains a high accuracy. Our approach to data modeling is similar to Lample & Charton 2020). who randomly create representative symbolic transformer model which can perform symbolic integration. They note that their system requires an external framework to guarantee validity, however our system outputs a verifiable reasoning that is straightforward to check for correctness, guaranteeing false positive and the correct handling of all true negatives.
equations to develop a deep learning sequence-to-seuee
Graph neural networks Graph neural networks (Scarelli et al. 2009 Wu et al. 2019), such as a graph-to-sequence network with attention, have been investigated for natural language processing (Beck et al. 2018). Structure2vec (Xu et al. 2017) uses graph neural network to detect binary code similarity where probability of equivalence is sufficient. Allamanis et al.) (2017) explore methods in which semantically exquivalence expressions have similar embedding representations. Allamanis al.] (2018b) use graph neural networks to analyze code sequences and add dedicated edge types to improve the system's 's ability to reason about the code. Their work achieves 84% accuracy on correcting variable misuse cases and provides insights to useful edge types. The G2SKGE model (Li et al. 2019) uses a node embedding (information fusion mechanism) to capture node relationships similar to ours. Given the inherent graph structure of expressions we manipulate, and potential
advantages of using graph neural networks for symbolic computing (Lamb et al. 2020 Rabin et al. 2020), our model makes use of a graph-to-sequence model for producing axiomatic proofs.
Static program equivalence Algorithms restricted to specific classes of programs have been de- veloped (Verdoolaege et al. [2022] Alias & Barthou (004; Barthou et al. [0022] looss et al., (014)). These approaches typically restrict to proving the equivalence of different schedules of the operations,
possibly via abstract interpretation (Schordan et al. 2014) Churchill et al. 2019) or even dynamically (Bao et al. 2016). The problem of program equivalence we target may be solved by other (smart) brute-force approaches, where a problem is solved by pathfinding. This includes theorem provers (Bertot & Castéran 2013 Paulson), which handle inference of axiomatic proofs. Program rewrite
systems have been heavily investigated, (Dershowizz 1985; Steffen 1991, Clarke et al. 2003 Visser ltt al. 2003 Namjoshi & Kurshan 20000 Kalvala et al., (2099 Mansky Gunter 2010). Our contribu-
rewrite systems have been studied (Visser [2004] Lucanu & Rusu 2015) Reddy (989). But recognizing this
tion is not in the formal definition of program equivalence we presented, pemmantics-prservviii
compositional formalism is well suited to deep learning graph-to-sequence systems was essential. The merits of stochastic search to accelerate such systems has been demonstrated (Murawski & Ouaknine 2005| Hérault et al.] 2004 Gogate & Domingos 2012). The novelty of our work is to develop carefully crafted graph-to-sequent neural networks to automatically learn an efficient pathfinding heuristic for this problem.
4 SAMPLES GENERATION
The careful creation of our training dataset is key: as we let the DNN learn by example only what the axioms are and when they are applicable in the structure of a program, we must carefully sample the space of equivalences to ensure appropriate distributions of the examples. We produce final dataset of tuples (P1, P2, S), a pair of input programs and a possible rewrite rule sequence that proves the pair equivalent. Duplicates are removed such that all samples have unique P1. From this dataset, we create 1, 1,000,000 training samples, 10,000 validation samples, and 10,000 test samples. We outline below its generation principles; extensive details and the algorithms used are presented in section C.1
4

---

Under review as a conference paper at ICLR 2021
Random sample generation Deep learning typically requires large training sets to be effectively deployed, hence we developed a process to automate sample generation. We specifically use random- ized program generation algorithms that are inspired by given language grammar. By randomly choosing between production rulse, one can build random parse trees by simply iterating the grammar. The leaves obtained will form sentence accepted by the language, i.e., program (Bielik et al. (2016). We limit to programs of 50 nodes in the program tree (or AST), with maximal tree depth of 7. We assert that our random production rule procedure has a non-zero probability of producing any program allowed by the grammar for our datasets.
We produce equivalent program samples by pseudo-randomin applying axioms on one randomly generated program to produce rewrite sequence and the associated equivalent program. Given randomly selected node in the program graph, our process checks which axiom(s) can be applied. F.g., the +m operator may have the Commute axiom category applied, or it may have the Transpose axiom category applied, which affects the operator's 's children.
Final experimental dataset: AxiomStep10 To train our network to produce one axiom step at time, as described in Sec. 2 AxiomStep10 10 has a single axiom in each output sequence S. For a complete proof S (122 (...) in a (P1, P2, S) we generated made of N axioms, we then create N training examples for the network: (P1, P2, AN) the first intermediate step by applying the first axiom, then (An (PI) P2, AN- etc. We limit proof length to 10 axioms in our experiments (hence AxiomStep10), Test samples only have the original and target program and the network proposes axioms which create intermediate programs towards the proof, fed back to the system.
Table 1: Distribution for the 14 axiom categories in AxiomStep 10 test set. Considering scalars (a, b, ...), vectors (7,w,, ...) and matrices (A, ...) types combinations, 147 distinct axioms are represented.
Axiom Category Example axiom(s)
Samples with
Axiom Category Example axiom(s)
Samples with
Cancel
(b,
13.8%
NeutralOp
(8- ō) + (A*O)-0, (b*0)~0
40.0%
DoubleOp
At' + A, 1/1/x +x
7.3%
AbsorbOp
30.3%
Commute
(a b) + (b a)
48.6%
DistributeLefft
(a b)c + ac + be
36.3%
DistributeRight
a(b + c) + ab + ac
27.8%
FactorLeft
ab + ac - a(b+c)
6.1%
FactorRight
ac be (a+b)e
9.0%
AssociativeLefi
a(bc) - (ab)e
46.3%
AssociativeRight
(ab)c + a(be)
43.1%
FlipLeft
-(0- + ui
8.4%
FlipRight
a/(b/c) + a(c/b)
26.1%
Transpose
(AB)" - B'A
11.1%
Datasets to study generalizability and robustness In order to study our model's ability to gener- alize, we have created alternate datasets on which to train and test models which are summarized in table[] WholeProefI0 will help us contrast learning approaches. This dataset has the complete proof sequence S made of N axioms reference output for program pair, while for Axiom- Step10, N = 1. Models trained on WholeProofX must maintain internal state representing the graph transformations that the axioms create. They not "iterative": single inference is expected to produce the complete proof; in contrast to AxiomStep 10 for which a single axiom of the sequence is produced each inference step. Training long output sequences can benefit from complex training approaches such as Professor forcing Lamb et al. (2016), but we will show that our AxiomStep10 model generalizes well with our sequence model training approach.
Table 2: Datasets used for studies in experiments.
Datasct
AST depth
AST #nodes
Proof length
Iterative
Comments
AxiomStep10
2-7
2-50
1-10
Yes
Main dataset- most general
AxiomStep5
2-6
2-25
1-5
Yes
Less general version of AxiomStep10
WholeProof10
2-7
2-50
1-10
Constrains AST traversal No
WholeProof5
2-6
2-25
1-5
No
Less general version of WholeProof10
Complexity of equivalence space Figure provides a view of the complexity of the equivalence problem we tackle. The distribution of the dataset per proof length is displayed in the right chart; the left chart shows by size bubble the number of test samples with a given number of semantics- preserving axioms that may be implemented as the first step of the proof and the proof length needed. There is a large number of proofs possible in our system, as detailed in Appendix C For example, for proofs of length 5, about 340,000 proofs made only of legal applications of axioms can be performed on the average sample in our dataset. Since many programs have multiple possible proofs, about 10,000 different programs can be produced, only one of which is the target prove, i.e.,
5

---

Under review as a conference paper at ICLR 2021
Aulomms raq quureeddd to proved pains equirolstt
AalomStop10
AvlomSteps WholeProofs
Whrde
Asiomm requieed equisient
1500
2500
Initial possibbl axiomss
#alomSteep10
*AvlomstepS
Number of samples in test set given axiom proof length
Figure 2: Distribution of axiom possibilities and proof complexity for test datasets.
randomly drawing valid axiom proof on a program known to be 5 axiom steps from the target has roughly a 1 in 10,000 chance of being a correct proof of equivalence between the two programs.
PE-GRAPH2AXIOM DNN FOR PROGRAM EQUIVALENCE
Fig. [ overviews the entire system architecture including sample generation, the pe-grapphaxiooo network, and the rewrite checker. Key design decisions are presented below.
Graph neural network The sample generation discussed in section 4 provides input to the Node Initialization module in Fig. [ to create the initial state of our graph neural network (Beck et al.) 2018)) For each node in the program graph, a node will be initialized in our graph neural network with value that encodes the AST level and language token of the program node. To interconnect the edges we support 9 edge types and their reverse edges which allows information to move in any direction necessary: 1) left child of binary op. 2) right child of binary op, 3) child of unary op, 4) root node to program 1, 5) root node to program 2, 6-9) there are edge types for the node grandchildren (LL, LR, RL, RR). The node states and edge adjacency matrix represent the initial graph neural network state.
After initialization, the graph neural network iterates 10 times in order to convert the initial node state into the embeddings needed for rewrite rule generation. Given an initial hidden state for node of In (0), Fr + 1) is computed with a learnable function ff which combines the current hidden state Tn (0), the edge types (n) of edges entering node n, the edge types loudjs] of edges exiting node n, and the hidden states Zne|u] (n] of the neighbors of node nı zn (t-(t1) = fIx, (t), lin(r)) Tne (t), (out(n))
Each edge type has a different weight matrix for learning, allowing aggregation of information into given node related to its function in the full graph of the program. The root node's 's initial state along with the edge types connecting it to the program graph trees allow it to aggregate and transfer specific information regarding rewrite rules demonstrated by our experimental results. This is novel feature of our network not used in prior work with GNNs on program analysis (Allamanis et al. 2018h
Xu et 2017).
Graph neural network output to decoder After stepping the GGNN, the final node values are used by the decoder in two ways create rewrite rules. First, the final root node value Froot (10) is fed through a learnable bridge function to initialize the LSTMs of the decoder. In this way, the aggregated information of the programs seeds the generation of rewrite rules. The LSTMs update as each output token yy is generated with a learnable function based on the current decoder hidden state hy at decoder step j and the previous output token V;- (Chen al. 2019). Second, all nodes the graph can be used by an attention layer (Bahdanau et al.) 2015). The attention layer creates a context vector e, which can be used by learnable function when computing the probability for generating the jth output token P(y;): P(y; 1 Y0 2/j-2:- ..., Vo, ey) = g(hg M/- 11j-,,03 Cz). Because pe -r-ggraphaaa axpphaxxieeee om has robust output verification, we make use of beam search to track up to 10 likely candidates for proofs of equivalence.
By using the root node only for seeding the initial hidden state hg of the decoder, the weights associated with its connections to the program graphs for P1 and P2 learn to represent the information necessary for the rewrite rule sequence. In parallel, after the graph neural network iterations complete, the final embedding for all the nodes the graphs for P1 and P2 are only used by the attention network, so their final embedding represents information useful during rewrite rule generation.
Intermediate program generation pe- arraphaaxii applies the axiom and program node cho- by the neural network token generator to the input program create intermediate program

---

Under review as a conference paper at ICLR 2021
P' the path from P1 to P2. If this program is equal to P2, then our axiom path is complete, otherwise the new pair P', P2 inferred to determine the next axiom step.
Incremental versus non-ineremental sequence production The models train on the Axiom- Step5, WholeProof10, and WholeProof5 datasets have the same neural network hyperparemeters as the AxiomStep10 10 data model. However, the models for WholeProof10 and WholeProof5 are trained to output the entire sequence of axioms needed to prove the 2 programs identical, hence these models do make use of the intermediate program generation and instead have a component which checks whether the full sequence of axioms legally transforms P1 into P2. We encode the path to the AST node an which to apply an axiom using 'left' and 'right' tokens which specify the path from the current program root node. This encoding is sufficient for the iterative model and necessary to allow the non-iterative model to identify nodes which may not have been in the initial AST for P1. The non-iterative models must learn a representation in the LSTM network to allow them to track AST transformations as they are generated.
6 EXPERIMENTAL RESULTS
We focus our experiments below on 4 key questions: 1) performance related to input program size? 2) Is performance related to proof length? 3) Is the incremental, per-axiom approach more generalizable than producing the full sequence in a single inference step? And 4) Is performance consistent across range of datasets, including human- writttn examples?
Implementation setup We developed the neural network system presented in the OpenNMT-py new encoder based on a prior implementation of gated graph
system (Klein et al.,, 2017), adding neural networks (Li et al. 2016). For our training and evaluation experiments, we use systems with Intel Xeon 3.6GHz CPUs and 6GB GeForce GTX 1060 GPUs. During training, save model snapshot every 50,000 iterations and score the accuracy the model achieved on the validation dataset. Graphs showing that validation accuracy plateaus 200,000 to 300,000 iterations are provided in section F We run each model twice and evaluate the test set using the saved model which achieved the highest validation score.
Evaluation procedure and neural network alternatives The benefits of key components of our neural network model studied in table The bidirectional RNN model is similar to state-of-the art sequence-tor torecee-tt--euunnee models used for program repair (Chen et al. 2019). The results for the graph-to-sequer to-suunnee model without attention show the benefit of providing the node information during the axiom generation process.
Table 3: pe-graphZaxion mini ablation study.
Beam width
Model description
2
5
10
Bidirectional RNN seq-to-seq with attention
48
62
71
75
Graph-to- so-s--ecee w/o attention
73
87
90
pe- ti-graph2axxiie model
76
84
90
93
Our final design was influenced by explorations we performed on varied models, datasets, and hyperparameters such as LSTM layers and graph neural network parameters. In relation to the model's 's ability learn representation of the proof sequence, we note that our GGNN initialization using the root node connection to the decoder outperforms the embedding learned by bidirectional RNN model. Also, we found that averaging the embedding of all graph nodes had about 10% lower accuracy than using the more specific root node information. Numerous additional results are reported in Suppl. material
Generalizing across different datasets We specifically look at the generalization potential for our models by studying their success rate as a function of the input program complexity, represented as the AST depth, in Table and as function of the output complexity, represented by the proof length in Table 5 all using a beam size of 10. We designed our datasets in Sec. 4 to study how well pe-graph2axx x generalizes and to assess in-depth additional experimental results are presented in Suppl. Material F. we summarize key results only below.
not overfitting training data. Extensive
7

---

Under review as a conference paper at ICLR 2021
Table 4: Performance vs. AST size: counts and percentage pass rates.
Testset
Model trained on AxiomStep5
Model trained
Sample Count
on AxiomStep10
AST depth
AS5
AS10
AS5
AS10
AS5
AS10
2-6
10000
6865
99
93
99
7
0
3135
n/a
86
n/a
92
All
10000
10000
99
90
99
93
Table illlstrattes the ability of model trained AxiomStep5 (i.e., limited proof's of length 5) to perform well when evaluated on the more complex AxiomStep10, which includes proofs of unseen length of up to 10. The robustness the input program complexity is illustrated with the 86% pass rate on AST depth 7, for the model trained on AxiomStep5 which never saw programs of depth 7 during training.
Table 5: Performance vs. proof length: percentage pass rates.
Axiom
Model trained
Model trained
Model trained AxiomStep5 (AS5)
Model trained AxiomStep10 (AS10)
Count
WholeProofS (WP5)
WholeProof10 (WP10)
Proof
WP5
AS5
WP5
AS5
WP5 WP10 AS5
ASI0
WP5 WPIn AS5
ASID
1-5
95
89
44
44
94
93
44
44
99
97
99
98
99
98
99
98
6
14
72
5
81
88
93
7
63
2
67
81
87
8
54
1
54
75
73
82
9
0
47
0
35
64
63
74
10
34
0
24
57
46
66
All
95
66
44
94
84
27
99
99
93
Table 5 compares the results of our 4 models, each trained on one of our 4 datasets, and evaluated with the test set of all datasets. The models all have identical hypermeter settings. We observe the inability of models trained to output the whole proof to generalize to proofs of higher length (WP5 model on AS10/WP10), with near zero success rate. However, per-axion models (AS5 and AS10) show potential for generalization to proof length: AS5 model performs well when evaluated on AS10, showing the ability to produce proofs of length/complexity unseen training. Overall, the success rate degrades gracefully with proof length, bottoming at 66% for AS10 for proofs of length 10.
Human written test expressions from Khan academy exercises Unfortunately there is dearth of existing large reference datasets for equivalence of linear algebra expressions, which justified our careful dataset creation approach in Sec. and their upcoming public release. However numerous math exercises involve exactly this problem, and can provide small but human-written datasets. We solve all of the matrix expression equivalence programs from relevant Khan academy modules designed to test student's knowledge of matrix algebra (Khan) 2020). Our AxiomStep10 model is able to correctly prove all 15 equivalent pairs from the modules with beam width and wider. With beam width of 10, the WholeProof10 model proved 12. An example problem solvable by AxiomStep 10 but not WholeProof10 is: c(1A + B) cB + c.A which can be proven by applying the rewrite rules NeutralOp. DistributeRight, and Commute the proper nodes. The WholeProof10 model mostly fails because it was not trained on how to apply repeated transformations at the same point in the AST. This suggests AxiomStep10 generalized well these -iritenttten problems.
CONCLUSION
In this work, we presented pe-graph2axion the first graph-to-sequenc neural network system to generate verifiable axiomatic proofs (via rewrite rules) for equivalence for class of symbolic programs. Evaluated on a rich language for linear algebra expressions, this system guarantees no false positives are ever produced, all true negatives are preserved, and produces correct proofs of up to 10 axioms in length in 93% of the truly equivalent cases. We believe the performance of our approach comes in part from using graph neural networks for what they aim to excel at: learning efficient heuristics to quickly find paths in a graph; and the observation that program equivalence can be cast path-based solution that efficiently found by such networks.
8

---

Under review as a conference paper at ICLR 2021
REFERENCES
Umair Z Ahmed, Pawan Kumar, Amey Karkare, Purushottam Kar, and Sumit Gulwani. Compilation error repair: for the student programs, from the student programs. Proceedings of the 40th International Conference on Software Engineering: Software Engineering Education and Training. pp. 78-87. ACM, 2018.
Christophe Alias and Denis Barthou. On the recognition of algorithm templates. Electronic Notes in Theoretical Computer Science, 82(2):395 409, 2004.
Miltiadis Allamanis, Pankajan Chanthirasegaran, Pushmeet Kohli, and Charles A. Sutton. Learning continuous semantic representations of symbolic expressions. In Doina Precup and Yee Whye Tch (eds.), Proceedings of the 34th International Conference on Machine Learning. ICML 2017, Sydney, NSW. Australia, 6-11 August 2017, volume 70 of Proceedings of Machine Learning Research, pp.
80-88. PMLR, 2017. URL http: / http:::///ccceecnng.... m. press.pesss...... wtt...pres//////aaaaaaaaaa html
Miltiadis Allamanis, Earl T. Barr, Premkumar Devanbu, and Charles Sutton. A survey of machine learning for big code and naturalness. ACM Compur. Surv., (1(4):811-81::33) July 2018a. ISSN 0360-0300. doi: 10.1 145/3212695. http:t//p////
acc. org/
Miltiadis Allamanis, Mare Brockschmidt, and Mahmoud Khademi. Learning represent programs with graphs. In 6th International Conference on Learning Representations, ICLR 2018, Vancouver. BC, Canada, April 30 May 3. 2018, Conference Track Proceedings, 2018b. URL https
7/ //openrevien net htt//formm/// -.JOFFTXX-
Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav. Code2vec: Learning distributed represen- tations of code. Proc. ACM Program. Lang., 3:P0PL):40:140:22: January 2019. ISSN 1421.
doi: 10.1145/3290353. URL http::: http//axivvv/// www.a.tww........a.a.ooo.oo.ot.t abs 1803. 09473
Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, OpenAl Pieter Abbeel, and Wojeiech Zaremba. Hindsight perience replay. In I. Guyon, U. V. Luxburg. S. Bengio, H. Wallach, R. Fergus, S. Vish- wanathan, and R. Garnett (eds.), Advances in Neural Information Processing Systems 30, pp. htth--iiidigggtteeeeeeeeeee
Curran Associates. Inc., 2017. URL hww.tttp:/// htttp://papers www.ersn.iis...m www.. httpssccc/pppp..
Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. Neural machine translation by jointly learning align and translate. 2015. URL htL:ht:::/// arxiv...vvvv..////// www.o/////a.....eeo aa/aa/ba/44000 0t////14..000 0473
Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, volume 97 of P Proceedings of Machine Learning Research, pp. 454-463, Long Beach, California, USA, 09-15 Jun 2019. PMLR. /RL.atto://prrceeeeeo bansal19a.1v html
ml r www..m.........eeeeeeeee prwss/v97/
Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, and Ponnuswamy Sa- dayappan. Polycheck: Dynamic verification of iteration space transformations on affine programs. In ACM SIGPLAN Notices, volume 51, pp. 539-554. ACM, 2016.
Denis Barthou, Paul Feautrier, and Xavier Redon. On the equivalence of two systems of affine recurrence equations. In Euro-Par 2002 Parallel Processing. 2002.
Rohan Bavishi, Michael Pradel, and Koushik Sen. Context2name: A deep based approach to infer natural variable names from usage contexts, November 2017. URL http::/ttbbbliioo
ulb. tu- rmastadt..... deeeddtteee1100 /ww.d////109999
Daniel Beck, Gholamreza Haffari, and Trevor Cohn. Graph-to-sequence learning using gated graph neural networks. In Proceedings of the 56th Anmual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 273-283, Association for Computational Linguistics,
2018. URL http::/t//// web. .ocbb.orgg/ee ort./tthog/attoooooooooooooooooa www.anttoooooyyyyyoo

---

Under review as a conference paper at ICLR 2021
Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq Art: the calculus of inductive constructions. Springer Science & Business Media, 2013.
Pavol Bielik, Veselin Raychev, and Martin Vechev. Phog: Probabilistic model for code. In Maria Flo- rina Balcan and Kilian Q. Weinberger (eds.), Proceedings of The 33rd International Conference Machine Learning, volume 48 of Proceedings of Machine Learning Research, pp. 2933-2944 New York, New York, USA, June 2016. PMLR. htRlhhtt::/// hhttt:://proceeeeeeeee ngs. ml press/ v48/bie 1tl.bielkkk........
Joseph Tobin Buck and Edward A Lee. Scheduling dynamic dataflow graphs with bounded memory using the token flow model. In 1993 IEEE international conference acoustics, speech, and signal processing, volume 1, pp. 429-432. IEEE, 1993.
Nghi D. Q. Bui. Efficient Framework for Learning Code Representations through Semantic-Preservingg Program Transformations, arXiv e-prints, art. MiXiv:2009902731,, September 2020.
Zimin Chen, Steve Kommrusch, Michele Tufano, Louis-Noël Pouchet, Denys Poshyvanyk, and Martin Monperrus. Sequencer: Sequence-to-sqquence learning for end-to-end program repair.
IEEE Transactions on Software Engineering. 2019. doi: (100//TSE.201.29441777 URL
http://arxiv.. org. wwt.ootgg//ooooooooooooooooo.. http://p//19..1. 1101 11990101110 01808
Berkeley Churchill, Oded Padon, Rahul Sharma, and Alex Aiken. Semantic program alignment for equivalence checking. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1027-1040, 2019.
Edmund Clarke, Daniel Kroening, and Karen Yorav. Behavioral consistency of c and verilog programs using bounded model checking. In Proceedings 2003. Design Automation Conference (IEEE Cat. No. 03CH37451), pp. 368-371. IEEE, 2003.
Nachum Dershowitz. Computing with rewrite systems. Information and Control, 62(2-3)::22-157, 1985.
Alhussein Fawzi, Mateusz Malinowski, Hamza Fawzi, and Omar Fawzi. Learning dy- namic polynomial proofs. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d' d'Alché Buc, E. Fox, and R. Garnett (eds.), Advances Neural Information Processing Systems 32, pp. 4179 4188. Curran Associates. Inc., 2019. URL htttp://papes httppppprsniss.....peppppp.ppptp 8671
Benny Godlin and Ofer Strichman. Inference rules for proving the equivalence of recursive procedures. Acta Informatica, 45(6):403-455 2008.
2008.
Vibhav Gogate and Pedro Domingos. Probabilistic theorem proving, arXiv preprint arXiv:1202.33 1202.3724, 2012.
Robert Goldblatt and Marcel Jackson. Well-structured program equivalence is highly undecidable. ACM Transactions on Computational Logic (TOCL), 13(3):26, 2012.
Ian J. Goodfellow, Yoshua Bengio, and Aaron Courville. Deep Learning. MIT Press, Cambridge, MA, USA, 2016. httt:://ww. http://wwww.eeeeleeaiiioooooooo org
Kazushige Goto and Robert Van De Geijn. High- peehorerfoomacc implementation of the level-3 blas. ACM Trans. Math. Softw., 35(1):4-1, 2008
Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvain Peyronnet. Approximate probabilistic model checking. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 73-84. Springer, 2004.
Sepp Hochreiter and Jürgen Schmidhuber. Long short-term memory. Neural computation, 9(8): 1735-1780, 1997.
Guillaume looss, Christophe Alias, and Sanjay Rajopadhye. On program equivalence with reductions. In International Static Analysis Symposium, pp. 168-183.. Springer, 2014.
10

---

Under review as a conference paper at ICLR 2021
Sara Kalvala, Richard Warburton, and David Lacey. Program transformations using temporal logic side conditions. ACM Trans. on Programming Languages and Systems (TOPLAS), 31(4):14, 2009.
Donald M Kaplan. Regular expressions and the equivalence of programs. Journal of Computer and System Sciences, 3(4):361-386 1969.
Sal Khan.
Properties of matrix multiplication.
Khan
Academy (ac-
cessed May 20,
2020), May 2020.
URL https: www www.kacaaaaddmy
Guillaume Klein, Yoon Kim, Yuntian Deng. Jean Senellart, and Alexander M. Rush. OpenNMT: Open-source toolkit for neural machine translation. In Proc. ACL, 2017. doi: 10.18653/v1/
http://o...rrgg///// 1ttp://11..1163/////11111 P17-4012. /ttp:t/ss//ooo..rrro.../////////
Jeremy Lacomis, Pengcheng Yin, Edward Schwartz, Miltiadis Allamanis, Claire Le Goues, Graham Neubig, and Bogdan Vasilescu. DIRE: A neural approach decompiled identifier naming. In International Conference on Automated Software Engineering, ASE '19 2019.
Alex M Lamb, Anirudh Goyal ALIAS PARTH GOYAL, Ying Zhang, Saizheng Zhang, Aaron Courville, and Yoshua Bengio. Professor foreing: A new algorithm for train- ing recurrent networks. In D. D. Lee, M. Sugiyama, U. V. Luxburg, I. Guyon, and R. Garnett (eds.), Advances in Neural Information Processing Systems 29, pp. 4601- 4609. Curran Associates, Inc., 2016. URL
nips. wwt.:iiipss........./...pp works.
6099
pdf
Luis C. Lamb, Artur Garcez, Marco Gori, Marcelo Prates, Pedro Avelar, and Moshe Vardi. Graph Neural Networks Meet Neural-Symbolic Computing: Survey and Perspective. arXiv e-prints, art. arX1vv2003.00330, February 2020.
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In International Conference on Learning Representations, 2020.
Dd-See2YeHFDS)
W. Li, X. Zhang, Wang, Z. Yan, and Peng. Graph2seq: Fusion embedding learning for knowledge graph completion. IEEE Access, 7:157960-157971, 2019. doi: 10.1109/ACCESS. 2019.2950230.
Yujia Li, Richard Zemel, Mare Brockschmidt, and Daniel Tarlow. graph sequence neural networks. In Proceedings of ICIR'16, April 2016. URL
Gated
gated graph- -
neural networks/
Dorel Lucanu and Vlad Rusu. Program equivalence by circular reasoning. Formal Aspects of Computing, 27(4):701-726, 2015.
Thang Luong, Hieu Pham, and Christopher D. Manning. Effective approaches to attention- based neural machine translation. In Proceedings of the 2015 Conference Empirical Methods in Natural Language Processing, pp. 1412-1421, Lisbon, Portugal, September 2015. Association for
Computational Linguistics. doi: 10.18653/11/D155 1166. URL www aclweb. org/
Sachhooogy/D11-111
William Mansky and Elsa Gunter. A framework for formal verification of compiler optimizations. In Interactive Theorem Proving. Springer, 2010.
Tomas Mikolov, Ilya Sutskever, Kai Chen, Greg S Corrado, and Jeff Dean. Distributed representations of words and phrases and their compositionality. In C. J. C. Burges, L. Bottou, M. Welling,
Advances Z. Ghahramani, and K. Q. Weinberger Advances in Neural Information Processing Systems
26, pp. 3111-3119. Curran Associates, Inc., 2013. URL http://aapppr..e nips ec cc/paper/ 502l-distributed http:a/sssiitttooopppppeeeaaaaaa wordss-ww-----oooooo- wawhlsa-aaddppphaassaee -nd stneeesrmmomosiiionlltttt
pdf

---

Under review as a conference paper at ICLR 2021
Andrzej S Murawski and Joël Ouaknine. On probabilistic program equivalence and refinement. In International Conference on Concurrency Theory, pp. 156-170. Springer, 2005.
Kedar Namjoshi and Robert P Kurshan. Syntactie program transformations for automatic abstraction. In International Conference on Computer Aided Verification,, 435 449. Springer, 2000.
Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph Representa- tions for Higher-Order Logic and Theorem Proving, arXiv e-prints, art. arXiv: 10006, May 2019.
Lawrence C. Paulson. Isabelle
Isabelle Page.
cl cam ac www..a....keeeerrcc/aaaaaaa httpp///www.....ccccccccccaaaaaa
Md Rafiqul Islam Rabin, Nghi D. Q. Bui, Yijun Yu, Lingxiao Jiang, and Mohammad Amin Alipour. On the Generalizability of Neural Program Analyzers with respect Semantic- Preeeeriiin Program Transformations. arXiv e-prints, art. arXiv:2008.011 015066 July 2020.
Veselin Raychev, Martin Vechev, and Andreas Krause. Predicting program properties from "big code". In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 15, pp. 111-124, New York, NY, USA, 2015. ACM. ISBN 978- 1-4503-3300- doi: 10.1 10.114522666726266779999
URL http:://diiii acm. oct..///00...111195531319
2676726 2677009
Uday S Reddy. Rewriting techniques for program synthesis. In International Conference on Rewriting Techniques and Applications, pp. 388-403. Springer, 1989.
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. IEEE Transactions on Neural Networks, 20:61-80, 2009.
Markus Schordan, Pei-Hung Lin, Dan Quinlan, and Louis-Noël Pouchet. Verification of polyhedral optimizations with constant loop bounds in finite state space computations. In Proc. of the 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Springer, 2014.
Bernhard Steffen. Data flow analysis model checking. In International Symposium Theoretical Aspects of Computer Software, pp. 346-364. Springer, 1991.
M. Tomita. Dynamic construction of finite automata from examples using hill-climbing. In Proceed- ings of the Fourth Annual Conference of the Cognitive Science Society, pp. 105-108, Ann Arbor, Michigan, 1982.
Michele Tufano, Cody Watson, Gabriele Bavota, Massimiliano Di Penta, Martin White, and Denys Poshyvanyk. An empirical study learning bug- fixing patches in the wild via neural machine translation. ACM Trans. Softw. Eng. Methodol, 28(4): September 2019. ISSN 1049- 331X. doi: 10. 145/3340544. URLptttp //t::///doo..o acm www......or....1.0 01530//39011111133344444444
Sven Verdoolacge, Gerda Janssens, and Maurice Bruynooghe. Equivalence checking of static affine programs using widening to handle recurrences. In Computer aided verification, pp. 599-613. Springer, 2009.
Sven Verdoolacge, Gerda Janssens, and Maurice Bruynooghe. Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. on Programming Languages and Systems (TOPLAS), 34(3):11, 2012.
Felco Visser. Program transformation with stratego/xt. Domain-specific program generation, pp- 216-238. Springer, 2004.
Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park, and Flavio Lerda. Model checking programs. Automated software engineering. 10(2):203-22) -202, 2003.
Qinglong Wang, Kaixuan Zhang, Alexander G. Ororbia, II, Xinyu Xing, Xue Liu, and C. Lee Giles. An empirical evaluation of rule extraction from recurrent neural networks. Neural Compur., 30 (9):2568 2591, September 2018. ISSN 0899-7667. doi: 16. a 01111, URL https aaboi.org//1o 10. 6162/ a_01111
12

---

Under review as a conference paper at ICLR 2021
Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S. Yu. A comprehensive survey on graph neural networks. CoRR, abs/1901.00596, 2019. URL http:
//axxxv.ogg/ab/////. 1901.. 00596
Xiaojun Xu, Chang Liu, Qian Feng, Heng Yin, Le Song, and Dawn Song. Neural network-based
graph embedding for cross-platform binary code similarity detection. In Proceedings of the 2017
ACM SIGSAC Conference on Computer and Communicaation Security, CCS '7, pp. 376-376. New York, NY, USA, 2017. ACM. ISBN 978-1-4503--946-88 doi: 00.14445/13399631144018
URL mttp:://dot a acm wttg:/1....11111133555533333333
13

---

input program Under review as a conference paper at ICLR 2021
Supplementary Materials:
Learning Axioms to Compute Verifiable Symbolic Expression Equivalence Proofs using
Networks
DOCUMENT OVERVIEW
This document supplements the submission Learning Axioms to Compute Verifiable Symbolic Expres- sion Equivalence Proofs using Srepeeto-Seeuence Networks. We have provided below numerous additional information for completeness. We also provide access to anonymized software artifacts to replicate our results. Our supplementary materials are organized as follows:
Appendix A of this document revisits the motivation and overview of our system in more depth. Appendix B this document formalizes the complete framework for axiomatic program equiva-
Ience we leverage in our work.
Appendix Cf this document presents the dataset generation approach we developed.
Submitted with this supplementary document is the pe-graph2 io directory which contains our code for generating datasets and training models, the testsets for our key datasets, and key results files from testset evaluations. The test dataset for AS10, most complex dataset, http///at//AxiomSSept///e Lel___tss_fflliooonrr
for convenience. The results file showing 9,310 successful proofs found our 10,000 sample testset for AS10 is pe- AxiommStepl0/saardde
is provided in
graph2axiom/run/AAe diiomStep10/mbbbtt
Appendix D of this document presents exhaustively the language for complex linear algebra expressions we evalaute on, including the list of all 147 axioms of equivalence we learned. Appendix of of developed.
this document presents additional details about the neural network architectures we
contains all trained models evaluated in this paper, including scripts train them directly from datasets, using OpenNMT. The AS10 model, our best/golden model, also provided in file hig.aa/iwooiiiguuuu///oooonspllo model step 300000.pt of this archive for convenience.
The anonymized
Appendix [ of this document presents complementary experimental results and additional in-depth details results presented in the main paper body.
A MOTIVATION, INTUITIONS AND SYSTEM OVERVIEW
A.1 INTUITIONS ON AXIOMATIC PROGRAM EQUIVALENCE
=
Pl:as (1b++1+c)
P2:a (b+c)
P3:0 asc
P4:a 10:a*c-i p4:a+c+a+b
Figure 3: Examples of Computations
Input program representation We illustrate in Fig. four very simple computations, represented as graphs, that are all equivalent under various axioms of natural arithmetic. For example, P1 models the expression a(1b + lc), one can imagine it to be the result of a(db + de) after e.g. constant- by a compiler. They are defined by single root, have nodes which can be
propagation of operations consuming the value of their immediate predecessor terminal/input values, and node produces a value that can be used by its immediate successors. In essence this is classical dataflow representation of the computation Buck & Lee (193),, and what our system representation.
In this work represent programs with symbolic expressions made of variables (e.g., a, b, c). operators (e.g., +, +) and neutral/absorbing elements (c.g., 1). We consider rich linear algebra expression language, supporting three variable types (scalars shown in P1-P4, vectors, and
14

---

Under review as a conference paper at ICLR 2021
matrices) and 5 different variables per type; 16 operators including operators mixing different variable types such as vector- pector-matrix product. Details are provided in Sec. B and Sec. D
Rewrite rules as axioms of equivalence Consider the programs P 1 versus P2. The multiplication of an integer value by does not change the value, we rely on an axiom of equivalence A1 : 1N*2 = n, Va E N. This axiom specifies strict criterion of application: the node must be of type N, the expression pattern must be Iy z; and a strict rewrite rule: replace a sub-graph IN * z for any rewrite,
E N by the graph x. In other words, replacing 1 * 6 by b in P1 is cemaantics-prseevvee from the axiom of equivalence A1. In this work we view the problem of program equivalence as finding sequence of semantics- presservii rewrites, each from a precisely defined axiom of equivalence, that rewrites one program into the other. If one program can be rewritten by a sequence of individually-corres correct semanties- prreeeiispp transformations into another one, then not only are they equivalent under the set of axioms used, but the sequence forms the constructive and verifiable proof of equivalence.
An example In this work we illustrate and experimentally evaluate our system using a rich linear algebra expression language because it exposes clearly (and intuitively) the various key concepts that must be handled: (1) operating on dataflow graphs as input, supporting transformations that can (2) delete or (3) create new nodes in the graph, and transformations that (4) manipulate entire subtrees. We also wanted a language with (5) multiple variable types, c.g. scalars, vectors and matrices and (6) a large number of different operators with (7) distinct axioms applicable for each. All of these are captured in the language we experiment with, see Sec. B for its formal definition.
When applying the axiom A1 1 I z, Vo E N on the program P1 for its node b. we obtain an equivalent and yet syntactically different program, we have PI = Abbb, PI). Applying the same axiom A1 on e the resulting program leads to program P2, and P2 = P1 A1 (1 (1,, P1)).
Consider now the axiom A2 : (y + 2) = I + Z 2, Vr, y. E N. This is the standard distributivity axiom on natural arithmetic. In terms of graph transformations, this complex rewrite: new node is created (+), one node is moved (+ to the root), and edges are significantly modified, When this complex, but semantics-preservingg rewrite is applied to P2, we obtain P3, that is P3- A2(,, (c, Ab, P1))).
Finally consider the axiom A3 x - y Vz, y E N, the standard commutativity axiom for +. The graph transformation does not change the number of nodes nor edges, instead only alters two specific edges. Note that as the previous axioms, it also illustrates operations on sub-graphs: indeed and do not need to be input/terminal nodes, they proper type. This is illustrated by applying it on P3 to obtain P4, that is the computation ac + ab. We have P4 = A3(+, A2( s, Al(c, (b, P1)))). verifiable proof of equivalence under our axioms between the programs a( b + Ic) and ac + ab, which involved structural changes including node deletion, creation and edge modification. Note the bidirectional nature of the process: one can rewrite from a(1b + 1c) to ac + ab, or the converse using the same (but reverted) sequence. Note also the non-unicity of a sequence: by possibly many ways a program can be rewritten into another one, for example the sequence P4 = A3(+, (1 (b, A2( PI)) also correctly rewrites P1 into P4. Conversely, a sequence may not exist: for example no sequence of the above axioms allow to rewrite + b into a b. We call these non-equivalent in our system, that is precisely if there is no sequence of axioms that can be applied to rewrite one program into the other.
be any subgraph producing value of the
The need for a verifiable procedure A key motivation of our work is to enable in safe and provably correct way the use of machine learning for program equivalence by ensuring no false negative can be produced. For full automation of the process, we focus on ensuring correctness in case an equivalence result computed by the system. That is, our system by design answers only with probability of confidence that the two programs are not equivalent, but it produces verifiable procedure to assess equivalence otherwise. We believe such an approach is key for a practical, automated deployment of neural networks for program equivalence: verifiably proving equivalence to ensure no false positive, while tolerating a moderate amount of false negative (i.e., missing that two programs were in fact equivalent).
Applications of such system include for example the automatic generation and correction of exercises for students, where they typically need to prove equivalence between two formulas by successive
15

---

Under review as a conference paper at ICLR 2021
application of other formulas/axioms. Languages like e.g. Matlab could use interactive checking of the equivalence between the expression being typed and the pre-existing library implementations (e.g., BLAS--bseel Gooo & Van De Geijn (2008) to instead accelerated implementations when possible in real-time. But we have designed and evaluated our system in a robust enough way to be applicable wide variety of languages and problems, long they can be cast in the framework in Sec. B
The space of equivalences Intuitively, our approach to program equivalence is as follows. We can intellectually reason graph for equivalent programs where each node represents distinct program in the language, and two nodes (i.e., two different programs) are connected by a directed edge iff the source node can be rewritten as the target node by the application of single one of the pre-defined axioms for equivalence. The edge is labeled by the axiom used and the specific position in the source node's program where it needs be applied to obtain the program in the target node. Then there will be one or more paths in this graph from the two nodes modeling the two input programs if they are equivalent (one can be rewritten into the other while preserving semantics); and no path if no such rewrite is possible, that is the programs would be not equivalent in our framework. Exposing a path between two nodes is sufficient to prove the equivalence of their associated programs.
This path is exactly a sequence of rewrite rules from one program to another. To test the correctness of an arbitrary sequence, i.e., verify if this path exists in the graph and assess equivalence if it does, one then needs to simply apply the proposed sequence to one of the input programs: verify at each step that the rewrite in the sequence is indeed applicable (by a simple check of the applicability of the axiom at this particular program point), and eventually ensure the rewritten program is identical to the other input one. This test can be computed in time mostly linear with the program size in our framework, and when successful it implements constructive proof of equivalence between the two programs.
Pathfinding equivalence proofs When formulating the program equivalence problem this way, we can then view its solution as learning how to build at least one feasible path between any two pairs of nodes in the above graph, when it can exist. We can see that by design, there is lot of redundancy in this space: the same labeled path will occur between many different pairs of programs (e.g.. those where only the variable symbols differ), and there are typically many paths between the same two (equivalent) programs. This creates opportunities for the system to learn program representation and path construction techniques more easily.
Our key contribution is the development of deep learning framework that learns this procedure automatically. The neural network system we build is trained by randomly sampling this graph, with samples made of two nodes and path between them when training equivalent programs, and an empty path otherwise. We specifically learn a generalization of the problem of finding paths in this graph as follows. We represent input programs in a carefully-crafted normalized dataflow graph encoded as gated graph neural network Scarselli et al. (209)); Beck et al. (2018). to enable structural, size-tolerant reasoning by the network on the imputs. It combined with a global attention- based mechanism and a memory- based LSTM Hochreiter & Schmidhuber ( (9977) decoder which can memorize graph changes for producing the rewrite sequence and enable path-size tolerant reasoning, while following the properties of the axioms for equivalence.
In a nutshell, we make the network learn stochastic approximation of an iterative algorithm that would be able to construct a feasible path (when possible) between any two pairs of nodes in this cquivalence graph, but trained simply by randomly sampling pairs of nodes and one carefully labeled path between them. This avoids entirely the need to craft smart exploration heuristics to make this path-finding problem feasible in practice. This is instead what we let the neural network learn automatically; and specifically why we implemented graph neural networks to solve this problem Scarselli et al.] (209);; Xu et al. (2017). We rely on the network to suggest a transformation path by inference, and then verify its validity in linear time.
A.2 SYSTEM OVERVIEW
To implement our approach, we enumerate randomly valid sentences in language, and set of axioms of equivalence expressible as semantics semantics-peeserving rewrite rules from one to the other. The system in Fig. 4 takes as input two programs represented symbolic trees representing a dataflow
16

---

Under review as a conference paper at ICLR 2021
Verifiable proof
Lexical equivalence [prog2 == prog int) =>
Axioms
proof found
Output components
sprog_ints
Global Attention
Token generator
Intermediate
Sample
program
Decoder
Generation
generation
components
Graph neural
LSTM2
network
lavers
Encoder
Grammar
Axiom
components
<temmo <Mantto
<vlcttrs <Saaler>
corog
Node initialization
Token
cprog 2+
Embedding
Start
Figure 4: pe- ve-graph2axion System Overview
graph of an expression computation, and eventually produces sequence of axioms along with their position of application (or node) that can be used to rewrite sequentially one input program into the other input program. As each axiom is produced, it checked to insure it legal application within the grammar and if the transformed program matches the target then correct proof of equivalence has been found. To train the system, we generate pairs of equivalent programs by iterating the axioms with random probability one program, thereby generating both path to equivalence and the target program. Random programs are generated so as to respect the grammar defined. The training set
then appropriately selected from these random samples, detailed in Sec. EL Node initialization
initializes the graph neural network, converting the input programs text (e.g., (a (b+ c)) into nodes
and edges in the Graph Neural Network Scarselli al. 2009); Xu et al. (2017). The details of the
network are covered in Sec. [ In nutshell, the key principle is to combine a memory-base. neural network approach, e.g.. using Long-Shop -Sog-Short Term Memory (LSTM) Hochreiter Schmidhuber (197)) neurons and a graph neural network design (which uses Gated Recurrent Units (GRUs) internally) Beck et al. (2018) that matches our program graph representation. Token embedding neural network layer in which tokens are assigned a learnable multidimensional embedding vector Mikolov cct al.] (013).. Each layer in LSTM 2 layers has 256 neurons, which support sequence generation. Token generator is the final output portion of the network. It learns to output the tokens based on the current LSTM hidden states and the Global Attention from the graph neural network. As each token is output, it feeds back into the LSTM layer through the embedding layer affect its next state. We use a sequence generation principle, using a global attention mechanism Luong et al.] (2013) to allow observation of program graph node information while generating the axiom and location on which it is applied. As developed below, we specifically study the robustness of our approach to generate proofs of increasingly complex length, contrasting models to output the entire path once with pe pe-graph2aa axtappphaxiiooo om which incrementally builds the sequence one step at a time, as shown in Sec.
B FORMAL FRAMEWORK FOR PROGRAM EQUIVALENCE
We now present the formalism we use in this work to represent programs and their equivalences. We carefully co-designed the chosen problem representation and the (graph) neural network approach to make the best use of machine learning via deep networks, as discussed in Sec. B
B. PROGRAM REPRESENTATION
key design aspect to match the capability of the neural network to model the input as walkable graph with the actual input program representation to be handled. We therefore model programs in dataflow-like representation (i.e., a directed graph), using a single root/output node, that is programs produce single final value, their root.
Note we restrict programs evaluated in our work to be directed acyclic graphs, and ensure every node has single successor: if a value is used multiple times, nodes representing this value are replicated in the imput program accordingly, as shown in Fig. where several nodes modeling the same variable are used in the same program.
17

---

Under review as a conference paper at ICLR 2021
A program is represented by its program graph, defined as follows.
Definition (Program graph node). A node n E N in the program graph models n-ary operations and input operands. A node produces value which can be consumed by any of its immediate successors in the graph. When a node has no predecessor, it models an input value. The ouipu value for the computation is produced by the unique root node Troot of the graph, the only node without successor.
Definition 2 (Program graph directed edge). directed edge mas : ny - n2 with ny, 02 E N in the program graph connects the producer of value (11) to node consuming this value in the computation.
Definition 3 (Program graph). A program graph G is directed dataflow graph modeling the computation, made of nodes n, E N and edges en.,, E E as defined in Def. 7 Land Def. 2 That is, G (nroot: N, E). There is no dangling edge nor unconnected node in G.
Language of linear algebra expressions We developed a complex-enough language to evaluate carefully our work, that captures rich linear algebra expressions. Specifically, we support types of data/variables in the program: scalars, vectors and matrices. We use the standard notation a, ã, A for scalars, vectors and matrices. We evaluate using different variable names for each of the 3 types above, along with their identity and absorbing elements.
We also model rich set of operators, mixing different unary and binary operations for each type. Specifically, we support *,, +x; s./s /s between scalar operands, t.: -. *y between vectors and tm, m:: *m for matrices. For -, / we also support their unary version for all types, e.g. -1, for unary scalar inversion and -m for unary matrix negation. For example a al,, computes to 1 1/a. We support two specific unary matrix operations, transpose 4m and matrix inversion as -1m, The operators designate the type of their result, and hence the * supports scalar, vector, and matrix operands, and *m supports scalar and matrix operands. Operator types facilitate the learning of the program embedding, avoiding the need to learn type propagation.
Examples Programs of the form DBB" 02, b) + (c(d/e)), (aA + +B)C etc. can be parsed trivially our representation, one simply needs be able to provide a unique name for each operand and operator type (possibly via some analysis, or simple language design principles), that is avoiding to overload the semantics of operators and operands. Note the semantics is never explicitly provided to our DNN approach, it is learned by examples. There will be no example of the form e.g. a + A, an invalid program in our language.
We believe a sensible approach is to develop a clean, regular grammar for the language to be handled, as implicitly these are concepts the DNN will need to learn. We did so, using a classical LL(() grammar description of our linear algebra language. This is not requirement of our approach, as one can arrive to the desired input program graph by any means necessary, but we believe making the reasoning on the language structure simple enough is an important design aspect.
B.2 AXIOMS OF EQUIVALENCE
central aspect of our approach is to view the problem of program equivalence as finding a sequence of locally-correet rewrite rules that each preserve the semantics, thereby making incremental reasoning possible. We explicitly do not consider non-semantics preeeenniis--eservinng "axioms". A rich structure of alternate but equivalent ways to rewrite one program to another makes the problem easier to sample and more amenable to machine learning. Semantics-preserr preserving axioms enable incremental per-axiom reasoning, and enforce semantics preservation without overly complicated semantics analysis; while still manipulating a very rich space of transformations. To illustrate this we specifically design axioms that perform complex graph modifications, such as node deletion or creation, subtree manipulation, multi-node graph changes, etc.
graph pattern can be viewed as a pattern-matching rule on graphs and its precise applicability criteria. It can also be viewed as sentential form of the language grammar, e.g. ScalarVal PlusOp Scall 1. LarVal 1 is a pattern, if the grammar is well formed.
Definition 4 (Graph pattern). A graph pattern P is an unambiguous structural description of a (sub- (grb- Gp. which can be deterministically matched in any program graph G. We have P= (Gr, Mn. Me) where for each node n, NGr, {Amatchh] = (n4) returns the set of node
18

---

Under review as a conference paper at ICLR 2021
values Nmatch accepted to match n, on graph G. For n,, ny E ENGr, C, Me(n,, n.) returns the
set of edges between (na) and (nz) to be matched in A pattern Gp is matched in G if (a) vn, E Gp: 3 nm = M (m.) E NN; (b) Ve, E , (eM.(m)).M.(n)) = Me(n,, n2) E EC; and (c)
(m) E EG + My)
Note when graph pattern models rewrite, Mn and Me are adjusted accordingly to output the rewrite of a node n E NG into its desired value, instead of the set of acceptable nodes from n E NGr.
Definition 5 (Axiom of equivalence). An axiom A is semantics prreserrii-- rewrite rule G' A(n, G) that can arbitrarily modify a program graph G, and produces another program graph G' respecting Def.
3 with identical semantics to G. We note A (Pmateh, P Preplace) an axiom, where P matchh, P reploce are graph patterns as per Def. 4 The application of axiom A to node n in G is written A(n, G).
We can compose axioms to form a complex rewrite sequence.
Definition 6 (Semanties-preserving
axiom composition). Given sequence S : Ai (mi, A2,,,,..., Am (Nm, G))) of m axioms applications. It is a semantic--peseervngg composition for each G2- = (n, G.) E S. p match succeeds on the subgraph with root n, in G and G2 is obtained by applying Prepiace 74.-
Theorem (Equivalence between program graphs). Given a program G. If S(G) such that S is a semantics prreserriss sequence as per Def. 6 then G = G", they are equivalent under the axiom system used in S.
This is direct consequence of using only semantics- preserving axioms, each rewrite cannot individ- ually alter the semantics, so such incremental composition does not. It leads to the formal problem we are addressing:
Corollary (Sufficient condition for program equivalence). Given two programs G, G. If there exist a sementics-preserving sequence S such that G' = S(G), then G = G".
Note here means complete structural equivalence between the two graphs: they are identical in structure and label/node values. Determining G = G' amounts to visiting both graphs simultaneously e.g. in depth-first search from the root to ensure structural equivalence, and also verifying the same node labels appear in both at the same time. This is trivally implemented in linear time in the graph size.
Language of linear algebra expressions We have implemented a total of 143 different axioms for our language, which are grouped for learning by our network into 14 multi-typed rewrite rules described later Table They all follow established linear algebra properties. Note different data types have different axioms following typical linear algebra rules, e.g., matrix-multipliatton does not commute, but scalar and vector multiplications do. Examples axioms include a(y)) + (æy)a,
X - X + O, (x - 7) T F. or X + X, an exhaustive list is displayed in Sec. D
In our experiments, we presume matrix and vector dimensions are appropriate for the given operation. Such dimension compatibility checks are simple to implement by e.g. introducing additional nodes in the program representation, but are not considered in our test language.
Examples We illustrate axiom-based rewrites using axioms presented in main Table [ Note axiom names follow the structural changes applied. For example, we have + b = b + c + a {a+ b c
a: {a + b} = Commutee( (++), (b + a)). a + + Commute((+i)) ( Commmtte (+2).11) (b + c + a}). Note we refer to different nodes with the same symbol (e.g., +2) subscripting them by their order in a DFS traversal of the program graph, starting from the unique root. We have 0 =
Cancel(l-)) - These can be combined in complex paths, e.g., b+c = c b + (a a) a) {b+ c} Commute((+)) . Noop(( {+), Cancel(f-), (c+ b (a a))))) Such axioms developed for scalars, matrices and vectors, and include complex rewrites such as distributivity rules and transposi- tions. A total of 143 axioms used in our system.
{0)
19

---

Under review as a conference paper at ICLR 2021
B.3 SPACE OF EQUIVALENCES
We now define the search space being explored in this work, i.e., the exact space of solutions on which the DNN system formally operates, and that we sample for training.
Definition 7 (Graph of Program Equivalences). Given a language L. The directed graph of equiv- alences belween programs is GPF (Nequiv Fequus) such that VI E L. ny E Nequse, and eA.. Cni :, >> nj E Eequiv iff n = A1 VA, in the axiom system and x: a position in ng where Ag is applicable.
In other words, the graph has one node per possible program in the language L, and single axiom application leads to connecting two nodes. We immediately note that GPE is a (possibly infinite) multigraph, and contains circuits.
Theorem (Program equivalence with pathfinding). Given two progrums nay ny E Nequin If there is any path from to nj in GPF, then n, nzj-
The proof is direct consequence of Def. 7 In this work, we randomly sample this exact graph GPE to learn how to build paths between arbitrary programs, themselves represented as nodes in the GPE. As it is multigraph, there will be possibly many different sequences modeled to prove the equivalence between two programs. is sufficient to expose one to prove equivalence.
Corollary (Semantics-preservin rewrite sequence). Any directed path in GPE a semantics- preserving rewrite sequence between the programs, described by the sequence of axioms and program position labeling the edges in this path. This sequence forms the proof of equivalence.
We believe that ensuring there are possibly (usually) many ways to compute a proof of equivalence in specific framework is key enable the DNN approach to learn automatically the pathfinding algorithm for building such proofs. Other more compact representations of this space of equivalences clearly possible, including by folding nodes in the equivalence graph for structurally-simile programs and folding equivalent paths between nodes. When building e.g. a deterministic algorithm for pathfinding. such space size reduction would bring complexity benefits Kaplaan (1669;; |Brtthou let al. (2002). We believe that for the efficient deployment of graph-to-sequence systems, exposing significant redundancy in the space facilitates the learning process. We also alleviate the need to reason on the properties of this space to find an efficient traversal heuristic.
C DATASET GENERATION
C.I GENERATION OF EXAMPLES
Machine learning benefits from large training sets, so in order produce this data, we created algorithms that would generate programs meeting a given language grammar along with target programs which could be reached by applying a given axiom set. By creating this process, we could create as large and varied dataset as our machine learning approach required.
Algorithm I provides an overview of the full program generation algorithm. For this generation process, we define a set of operations and operands on scalars, matrices, and vectors. For our process, we presume matrix and vector dimensions are appropriate for the given operation as such dimension checks are simple to implement and are not considered in our procedure. Note the token syntax here exactly the one used by our system, and is strictly semantically equivalent the mathematical notations used to describe these operations, e.g. IN is 1.
Scalar operations: +s -S +S /s is ns, where is the unary reciprical and ns is the unary negation.
Matrix operations: +m -m *m im nm tm, where im is matrix inversion, nm negates the matrix, and tm is matrix transpose.
Vector operations: tv -V nv, where nv is the unary negation.
Scalars: a b c e 0
Matrices: A B C
O I, where O is the empty matrix and I is the identity matrix.
Vectors: v W x y 2 o, where o is the empty vector.
Summary: 16 operations, 20 terminal symbols
20

---

Under review as a conference paper at ICLR 2021
Initially, GenPl is called with GenP1 (*+s -8 / +5 - / ns +m -m *m +m -m *m +m -m *m im nm tm +V -V *V +V -V nv", 0. 94) In this initial call binary operations repeated so that they more likely to be created than unary operations, and the initial probability that a child of the created graph node will itself be operation (as opposed to terminal symbol) set to 94%. Since the algorithm subtracts 19% probability for children at each level of the graph, trees are limited to 7 levels.
+8 - /s is
*V +V -V *V
Algorithm| starts execution by randomly selecting an operation from the set provided input. When GenP1 is called recursively, the operation set is limited such that the operation produces the correct type as output (scalar, matrix, or vector). Lines 3 through 15 of the algorithm show an example case where the operation is processed. This operation requires scalar operands. If the probability of children at this level is met, then GenP1 is called recursively with only scalar operands available, otherwise random scalar operand is chosen.
The text for algorithm [ does not show the process for operations. Certain operations, such as have variety of operand types that can be chosen. The +v operand is multiplication which produces a vector. As such, Av (matrix times vector), be (scalar times vector), or ve (vector times scalar) are all valid options and will be chosen randomly.
Algorithm 1: GenPI
Result:
Prefix notation of computation with parenthesis
Input :Ops, P
Output (op R) or (op I.)
op = select randomly from Ops // Create subtree for chosen op
op = "#y" then
if' random < P then
= GenP1("+s -s /s +s # ns P-0..9))
else
= select random scalar operand
end
random < P then
R GenP1 -s *s Is *s /s is ns" ns" P-0.19)
11
else
12
select random scalar operand
13
end
14
return (op L R)
1s end
16 // Other ops may have more complex options for children types.
17 (For example, "#m" may have matrix multiplied by scalar or matrix)
18
After generating a program which follows the grammar rules of our language, algorithm 2 will produce new program along with a of rewrite rules which transform the source program the target program.
Algorithm 2 receives as input the source program (or subprogram) along with the path to the current root node of the source program. If the source program is terminal symbol, the algorithm returns with no action taken. Otherwise, the program starts with an operation and the algorithm proceeds to process options for transforming the given operation. For our wholeproof1 and wholeproof5 datasets, algorithm is only called once, simplifying the possible node order and proof complexity. for the axiomstep 10 and axiomstep5 datasets, algorithm iss called multiple times, allowing for the possibility that after path is chosen for one axiom any node can be accessed for the next axiom (including the same node).
As shown on line 10 the algorithm, when the operation and children meet the conditions necessary for rewrite rule (in this case NeutralOp), the rule is applied with some probability (in this case 50%). Note that before processing a node, the left and right operands are further analyzed to determine their operators and operands well (or if the child is terminal). Processing the left and
21

---

Under review as a conference paper at ICLR 2021
right operands allows for complex axioms be applied, such distribution factorization. When a rule is applied, the rewrite rule is added to the rewrite rule sequence and a new target program is generated for any remaining subtrees. When creating the rewrite rules for subtrees, the path variable is updated as rewrites are done. In the case Neutra ra 1 0p, the current node is being updated, so the path is not changed. But in the case of the Commute rule, the return would be generated with (op GenP2 2 (3, path. "left ") GenP 2 (L, path. "right ")) which creates rewrite rules for the prior right and left operands of the op and updates the path used to the new node positions. In order to analyze nearly equal programs, illegal rewrites can be optionally enabled; for example, commuting a subtraction operation mutating one operation into another. In that case, the GenP2 process continues to create target program, tornsforrn_seeee forn_sqquencee is set to Not_equal.
Algorithm 2: GenP2
Result: Second program and transforr_sequencce Input :PI, path
Output:
terminal symbol then
return P1
end
op find operator of P1
I. = find left operand of P1
find right operand of P1
Lop,LL,LR operator and operands of left child
Rop.RL.RR operator and operands of right child // Randomly apply transform if allowed
10
random < 0.5 and ((op == "+y" and (L == or or")) == ".v" and == "o"")
then
11 append path. "NeutraltO to transform transform_sequence sequence // Eliminate unnecessary operator and 0 vector
13
if = "o" then
14
return GenP2(R.path) else
15
16
return GenP2(L.path)
17
end
18 end
After these generation algorithms run, final data preparation process is done which prunes the data set for the learning algorithm. The pruning used on our final data set insures that the (P1, P2) program pair total to 100 tokens fewer (where token is operation terminal), that the graph such that every node is reachable from the root with path of length 6 or less, and that there are 10 or fewer rewrite rules applied. But within these restrictions, rule procedure has a non-zero probability of producing any program allowed by the grammar. Also, the pruning insures that there are no lexically equivalent programs in the process and removes some of the cases with fewer than 10 rewrite rules generated to bias the dataset to longer rewrite sequences. Table details the distribution of rewrite rules created by the full process. Section D details all axioms when variable types and operators are considered.
assert that our random production
We produce equivalent program samples by pseudo-randomly applying axioms on one randomly generated program to produce rewrite sequence and the associated equivalent program. Given randomly selected node in the program graph, our process checks which axiom(s) can be applied. E.g., the +mm operator can have the Commute axiom applied, or depending allowed to have the Factorleft axiom applied, as discussed in Sec. 6 Generally we choose to apply or not operator with 50% probability, so that pe-graph2an om forced to rely analysis of the two programs to determine whether an operator applied instead of learning a bias due to the local node features.
subtrees it may be
22

---

Under review as a conference paper at ICLR 2021
C.2 INTERMEDIATE PROGRAM GENERATION
The intermediate program generation algorithm is very similar to algorithm 2 of the target program, algorithm 2 will check that a node can legally apply a given rule, apply the rule with some probability, record the action, and process the remaining program. For intermediate program generation, we begin with a P1 and a rewrite rule. We follow the path provided to identify the node, check that node can legally accept rule, apply the rule, and return the adjusted program. a rule cannot legally be applied, P1 is not successfully transformed. If a rule can be legally applied to P1, the program is compared lexically to P2 and if they match then equivalence has been proven.
For program generation
C.3 COMPLEXITY OF PROVING EQUIVALENCE
Table 6Jshows the complexity of the solution space for our problem for proofs from our AxiomStep10 test dataset up to length 7 (deterministically computing all possible programs requires too many resources for longer proof lengths). The All possible nodes and axioms' row includes the total number of proofs of given length available to our problem space. The entry 5933 for a single axiom represents that for an AST depth of 7 we have 43 axioms which can be applied to all 63 possible operator nodes and 104 axioms which can be applied to the 31 nodes which possibly have child operator nodes themselves: 63*43+31* 104=5933. Subsequent columns can select repeatedly from the same set growing as 5933² to 59337 The 'sample node + axiom group' row is based on our 10,000 sample test dataset and represents the possible selection of any of the 14 axiom groups being applied to any node in the program. The 'sample node + legal axiom' row represents only legal node plus legal axiom group being applied and effectively represents the total number of programs derivable from the start program in the test dataset. The final row 'Sample derivable unique programs' represents the total number of programs derived from legal node and axiom sequences which are lexically unique.
Table 6: Counts for equivalence proof possibilities
Proof length in axioms
Proof description
2
3
6
7
All Possible nodes and axioms
5933
3.5E+07
2.1E+11
1.2E+15
7.4E+18
4.4E+22
2.6E+26
Sample Node Any Axiom
226
46900
1.5E+07
8.8E+09
5.0E+12
3.
2.7E+18
Sample Node Legal Axiom
11.2
77.8
931
15812
3.4E+05
8.2E+06
1.8E+08
Unique Programs from Sample
9.2
47.4
264
1574
10052
65176
4.6B+05
D LANGUAGE AND AXIOMS FOR COMPLEX LINEAR ALGEBRA EXPRESSIONS
We now provide the complete description of the input language for multi-type tupti--tpee/aee linear algebra pressions we use to evaluate our work, and the complete list of all axioms that are used to compute equivalence between programs.
We model programs made of scalars, vectors and matrices. We limit programs to contain no more than 5 distinct variable names of each type in a program:
Variable types
Scalar variables are noted a, b, .... C.
Vector variables are noted ū. W. .... Z. Matrix variables are noted A, B, ..., E.
Note we also explicitly distinguish the neutral and absorbing elements for scalars and matrices, e.g.
= 1y. This enables the creation of simplification of expressions as a program equivalence problem, e.g. if A B [B A) Og
Unary operators priate type:
We model 6 distinct unary operators, all applicable to any variable of the appro-
is (a) -1 the unary reciprocal for sealars, im (A) A matrix inverse.
ns (a) = a is unary negation for scalars, nv (v) --7 17 for vectors, nm (M) = -M for matrices.
tm (M) = M is matrix transposition.
23

---

Under review as a conference paper at ICLR 2021
Binary operators We model 10 distinct binary operators that operate require the same type for both operands, while enable multi-type operands (e.g., scaling matrix by scalar). Note do not consider potential vector/matrix size compatibility criterion for these operators, in fact we do not represent vector or matrix sizes at all in our language, for simplicity.
values. operators
the addition scalars, along with (a, b) and /s (a, b) = a/b.
b, (a,b) w) v- w. x V, w) +m. (A, B) A + B. the addition on matrices, along with -m (A, B)
(a, b)
b
+v V, w) - wi, the addition vectors, along with -v
J.W the dot product between two vectors, producing scalar.
and *m (A,
B = AB the product of matrices.
*II (a, A) = a.A and xm (A, a) = Aá are used to represent scaling matrix by a scalar.
*m (v, A) E. represents a vector-matrix product.
* (a, = aT and +V (v, a) da represent scaling a vector by scalar.
List of axioms of equivalence Tables 7
show the full 147 axioms supported by our rewrite rules.
Many rewrite rules can be applied to all variable types as well as multiple operator types.
Rewrite Rule
ID
Example(s)
Rewrite Rule
ID)
Example(s)
Cancel
1
(a- a) +
AbsorbOp
28
(a 0) +
2
(b/b) +
29
(0 a) +0
3
(A- A) -
30
(A * 00) +
4
(A+ +1
A) +0
5
(A-1 A) +1
32
(A O) +0
6
(V-V)-0
33
(0 * A) +0
NeutralOp
7
(a+0) -a
34
(A o) ~
8
(0+a) +
35
0) +
9
(a-0)
a0 40
10
(a*1)
37
(0 -0
a1) +
38
(v*0) +
13
(a/1) +
(0+v)
14
(A O) 7 A
Commute
(a+b) > (b a)
15
(0 + A) A
41
(a*b) + (b a)
16
(A-O) +
42
(A+ B) (B A)
17
(A I) +
43
(A (a A)
18
(I + A
* {) - A)
19
(v+ +V
(A (A* + (0 A)
20
(D+V) +v
46
(0 A) -) (A OO)
(V-0)-v
47
(A - (I+
DoubleOp
22
-(aa)++
48
(I (A
23
(a (a-1)-1-2
(V W
24
-(-A)-A
50
(v* +aa)) vv)
25
(A (A-1---
51
26
(A''
DistributeLeft
52
(a+
((v)) +v
(a-b)c ac
DistributeRight
64
a(b a(b+c) ab acc
54
(a (a+ + a/c b/c
65
a(b ab
55
(a- a/c b/c
56
(v ++)
66
a(v
w) - wa
a(v - w) - aV
68
A(B + +C+
AC
(A + BJC + AC + BC
69
A(B - C) +B -AC
59
(A BBJC - AC
70
a(B C) aB aC
60
(A B)y - Av + By
61
(A Bly Av
a(B
B)a + + Ba
(A B)a + Aa Ba
Table 7: Full axiom count when all type options and other supported permutations are included (part
1 of 2)
24

---

Under review as a conference paper at ICLR 2021
Rewrite Rule
ID
Example(s)
Rewrite Rule
ID
Example(s)
FactorLeft
72
ab + ac + a(b+c)
AssociativeRight
113
(a+b)+c + a+(b+))
73
ab - ac - a(b-c)
114
(a+b)-c + ++((bc)
74
AB AC A(B+C)
115
(ab)c + a(bc)
75
AB- AC A(B-C)
116
(A+B)+C A+(++C)
76
+ + Aw + A(v+w)
117
(A+B)-C - A+(B-C)
77
Av Aw + A(v-w)
118
(AB)C + A(BC)
78
Aa + Ab + A(a+b)
119
(AB)a + A(Ba)
79
Aa Ab A(a-b)
120
(Aa)B A(aB)
80
va + vb > v(a+b)
121
(aA)B + a(AB)
81
va vb + v(a-b)
122
(Av)a + A(va)
FactorRight
82
ac + be - (a+ble
123
(Aajv 7 A(av)
83
bc (a-b)e
124
(aAJv + a(Av)
84
a/c + b/c + (a+b)/c
125
(va)b v(ab)
85
a/c b/c + (a-b/c
126
(av)h a(vb)
86
AC BC + (A+ByC
127
(ab)y + a(bv)
87
AC BC (A-B)C
128
(v+W)+x v+(W+x)
88
Av Bv (A+Bjv
129
(v+W)-x v+(Wx)
89
Av Bv - (A-Bjv
Flipleft
130
-(a-b)
90
Aa + Ba - (A+B)a
131
(a/b) b/a
91
Aa Ba - (A-B)a
132
(A- B) + (B A)
92
(V+w)a
133
-(v (v- - w) (W V)
93
va wa + (V-w)a
FlipRight
134 + - a(c/b)
AssociativeLeft
94
a+(b+c) - (a+b)+c
135
o/(b
ab
95
a+(b-c) + (a+b)-c
136
a-(b-c) at(c-b)
96
a(bc) (ab)e
137
a-(-b) + atb +
97
a(b/c) + (ab)/c
138
A-(B-C) - A+(C-B)
98
A+(++C) - (A+B)+C
139
A-(-B) - A+B
99
A+B C) (A+B)-C
140
v-(W-x) - v+(x-W)
100
A(BC) -> (AB)C
141
v-(-W) V44
V4W
101
A(Ba) (AB)a
Transpose
142
(AB) - +BBAT
102
A(aB) + (Aa)B
143
(A+ +++ (A' B
103
a(AB) + (aA)B
144
(A A- -)
B+)'
104
A(Bv) (AB)v
145
(AB)' B'A
105
A(va) (Av)a
146
(A+ B)¹ + A + B'
106
A(av) 7 (Aa)v
147
(A B) + + B
107
a(Av) 7 (aA)v
108
v+(W+*) + (V+w)+x
109
V+(W-x) + (v+w)-x
110
v(ab) (va)b
111
a(vb) > (av)b
112
a(bv) + (ab)v
Table 8: Full axiom count when all type options and other supported permutations are included (part
2 of 2)
E DETAILS ON NEURAL NETWORK MODEL
Figure 4 overviews the entire pe grrgpaaaaaiiioo architecture including sample generation, the graph-to-sequence network, the intermediate program generation, and lexical equivalence checker. In this section will discuss the implementation details of these components.
Graph neural network internal representation The sample generation discussed in section provides input the Node Initialization module in Fig. to create the initial state our graph neural network. For each node in the program graph, node will be initialized in our graph neural network. Each node has a hidden state represented by a vector of 256 floating point values which are used to create an embedding for the full meaning of the given node. Initially all 256 dimensions of the hidden states of the nodes are set to zero except for Given tokens in our input program language, one of the dimensions from through N of node will be set based the token at the program position that the node represents. For example, if the scalar variable a is assigned to be token 3 in our language, then the nodes of Fig. 3 would have their 3rd dimension initialized 1.0. This is
25

---

Under review as a conference paper at ICLR 2021
one-hot encoding similar to that used in neural machine translation models which leverage Word2vec MMkkolov et al. (2013). The second non-zeru zero dimension in our node initialization indicates the tree depth, with the root for the program being depth 1. We set the dimension N+depth to 1.0; hence, the a nodes in Fig which vary from level 2 or 3 in the graph, would set dimension N + 2 or N + 3 to 1. In addition nodes correlating to all tokens in both input programs, we initialize root node for program comparison which has edges connecting to the root nodes of both programs. The root node does not represent a token from the language, but it is initialized with 1.0 in a hidden state dimension reserved for its identification.
For graph neural network, the edge connections between nodes are crucial part of the setup. In particular, to match the formulation of our problem, we must case the ability of the network to walk the input program graphs. We therefore designed a unified graph input, where both program graphs are unified in single graph using a single connecting root node; and where additional edges are inserted to make the graph fully walkable.
In our full model, we support 9 edge types and their reverse edges. The edge types are: 1) left child of binary op, 2) right child of binary op, 3) child of unary op, 4) root node to program 1, 5) root node to program 2, 6-9) there are 4 edge types for the four node grandchilden (LL. LR, RL, RR). After the node hidden states and edge adjacency matrix are initialized, the network is ready to begin processing. This initial state is indicated in figure 5 by the solid circles in the lower left of the diagram.
left
FactorLeft
Graph Neural Network Nettra encoder
Node attention
Token
Taken
generator
generator
R
Bridge
LSTM
L.7MM
LSTM
LSTM
R
b
Token embeddding
Token
embedoling
R
Stort
P1
Root
P2
RNN decoder
Figure 5: Graph-to-sequencc neural network data flow details.
systems is to enable beam search, the process of asking for multiple answers to the same question to the network. It is particularly relevant when creating outputs which can be automatically checked Chen et al. (2019); [ et al.) (2018). Beam search can be viewed as proposing multiple possible axioms to apply. Given the stochastic nature of generation model, a beam width of n can be thought of as creating the most likely sequences given the training data the model as learned on. Each proposal can be checked for validity, the first valid one is outputted by the system, demonstrating equivalence. Our system builds on the neural network beam search provided by OpenNMT to create a 'system beam search' of variable width. In particular, we set the OpenNMT network beam search to 3, which constrains the token generator to produce 3 possible axiom/node proposals for given pair of input programs. Using these 3 proposals, when our system beam width is 10, we build up to 10 intermediate programs that are being processed in the search for proof. To illustrate with system beam width of 5, after P1 and P2 are provided to the neural network, 3 possible intermediate programs may be created (so long as all axioms are legal and don't produce duplicates). After those 3 intermediates are processed, 9 possible new intermediates are created, all of which are checked for lexical equivalence with P2, but only 5 of which are fed back into the neural network for further axiom generation. This process is continued for up to 12 axioms at which point the system concludes an equivalence proof cannot be found and the programs 10, showing higher success with larger beams.
Beam search A typical approach when using sequence-to-sequenne
likely not equivalent. We evaluate in Sec. 6eeam sizes ranging from to
F DETAILS ON EXPERIMENTAL RESULTS
F. COMPLEMENTARY RESULTS AND OBSERVATIONS
Table describes part of our neural network hyperparameter tuning showing that our golden model has as high a result as other variations explored. Note that the validation token accuracy is not too high (it's not above 90%) despite the ability to predict full correct proofs with over 93% accuracy. This is
26

---

Under review as a conference paper at ICLR 2021
because the training dataset have multiple examples of axioms given similar input programs. For example, proving "(a+b)(c+d) = (b+a)(d+c)" requires commuting the left and right subexpressions. The training dataset could have similar programs which sometimes transformed first with right Commute and then a left or vice-versa. Given this data, the network would learn to apply one or the other (it would not get trained to associativity for these program pairs for example), hence the actual output given may or may not match the validation target axiom. We will discuss this further in section
Table 9: Hyperaarameter experiments. Summary of best validation token accuracy result after runs for up to 100,000 training iterations. The golden model has 256 graph nodes and decoder dimensions, 2 decoder LSTM layers, starts training with learning rate 0.8, and uses 10 steps to stabilize the GGNN encoder.
Parameter
Value
Validation token accuracy
Golden model
83.89
Graph node and decoder LSTT dimension
192
83.89
320
83,58
Decoder LSTM layers Initial learning rate
83.53
0.75
83.76
0.85
83.57
GGNN stability steps
12
83.19
83.61
Training convergence Since our model trains on axiomatic proofs which may vary in order (allowing or options to be correct and occur in the training set), see our training and token accuracies plateau below 90% during training for AxiomStepl0 as shown in Figure Full testset proof accuracies for beam width 10 exceed 90%, but also plateau along with the training and validation results. This result differs from our WholeProof10 training, which achieves training and validation accuracies above 96% because the expected axiom sequence is more predictable, but have less generalized.
As another observation generalization and overfitting, note that figure 6 shows slight separation between the training and validation accuracies starting at around iteration 180,000. While the training accuracy rises slowly, validation accuracy plateaus, indicating slight overfitting training data. Yet our model continues to slowly increase in quality, with the model snapshot that best on both validation and test accuracies occurring at iteration 300,000. This our golden model, with 93.1 % of P1 to P2 proofs accurately found using beam width 10.
the
100
95
Training
90
Validation
85
Test Beam
80
Test
75
Test beam 10
70
65
60
50000
100000
150000
200000
250000
300000
Figure 6: Model training percentage accuracy up 300,000 iterations AxiomStepl0. Training and Validation accuracies are per-token on the target axioms in the samples. Test accuracies are for full correct proofs of P2.
Testing simpler models In addition the sequence-to-sequeeee to-sequence and graph-to-sen tou-uue--eueeeeeee models, we explored a feed-forward equal/not equal classifier on a simple version our language. That model uses autoencoder the program to find embedding of the program and then classifier
27

---

Under review as a conference paper at ICLR 2021
based on the program embeddings found. It achieves 73% accuracy on identifying equivalent pairs in the test data, which, as expected, is much lower than the full proof rate of 93% achieved with supphto--squencee proof generator our full language. This simple experiment highlights the importance of a system which prevents the false positives which a classifier might have by creating a verifiable proof.
We explore initial language generation using a simple language in order to assess feasibility of different approaches. For fine tuning network parameters and architectural features, we add more complexity to the language as shown in table TO Language IDs through are all based on simple grammar which only allows the "+" or "." operators on scalar variables labeled a through j. The only axiom is Commut e, which can be applied on up to 3 nodes in language IDs 2 and 3. Language ID adds the scalar constants and 1, scalar operations and /, and more axioms. We perform fair amount of network development on this model in an effort to maintain high accuracy rates. Language ID also 4 expands the operands to types and hence the number of operators also increases. To speed up model evaluation,
reduced the program length for IDs 5, 6, and 7, allowing data sets for more epochs. ID is a forward looking-mont model which makes a minor increment to the language to support the analysis of loop rolling and unrolling, discussed further in section is the WholeProof5 model in relation to these early experiments.
to train larger
ID 8
with beam width 10
Percent matching
Percent matching
Training set size
with beam width
Program length
# Axioms in
Rewrite rule
Operators
Operands
language
axioms
ID
Description
*
*
Rewrite sequence is Commutes
2
10
5-24
2
80K
98.9
99.8
2
Rewrite sequence is Commutes
2
10
7-45
3
80K
91.4
99.0
3
Rewrite sequence 1-3 Commutes Commute, NeutralOp, Cancel, DistributeLeft, DistributeRight Scalars, Vectors, and Matrices
2
10
3-45
1-3
180K
97.1
99.2
4
4
12
3-45
1-3
180K
93.1
97.4
5
16
20
3-30
1-5
250K
88.3
95.6
6
13 Axioms
16
13
20
3-30
1-5
400K
85.5
95.5
7
Add loop axioms
18
15
20
3-30
1-5
400K
83.8
94.7
14 Axioms
16
20
3-50
1-5
1M
81.8
94.4
Table 10: Description and results for various language complexities studied with WholeProof models.
We designed our datasets in section with the goal of using the varied models to understand the generalizability of pe nee-gapphaxii om and show that model is not overfitting on training data. For these next experiments, all results of for beam width 10, which provides for a neural-network directed search of up to 10 axiomatic proofs of equivalence for each program pair. Recall that our most complex dataset is AxiomStep10 which includes (P1, P2, S) samples requiring up to 10 rewrite rules, P1 and P2 can have up to 50 AST nodes each, and an AST depth of up to 7. AxiomStepS has samples requiring AST depth of up to Tables 11 and 12 (repeated from main paper below) demonstrate the ability of a model trained on AxiomStep5 to perform well on the larger distribution of programs from 1xiomStep10, implying that the model has generalized well to our program equivalence problem and that pe-pee--aee grwph2apph22aa ax om does not overfit its response to merely the training set distribution.
to 5 rewrite rules, P1 and P2 can have up to 25 AST nodes each, and an
Table 12 illustrates the ability of model trained on AxiomStep5 (i.e., limited to proofs of length 5) to perform well when evaluated on the more complex AxiomStep 10, which includes proofs of unseen length of up to 10. The robustness to the input program complexity is illustrated with the 86% pass rate AST depth 7, for the model trained on AxiomStep5 which never programs of depth 7 during training.
As indication of the breadth of equivalent programs represented by AxiomStep10 relative to WholeProof10, table 13] the full detail of models trained on all 4 datasets when tested on test data from all 4 datasets. AxiomStep10, while training our broadest dataset in which axioms can
28

---

Under review as a conference paper at ICLR 2021
Table 11: Generalizing to longer PI inputs. Percentage pass rates for equivalence proofs with PI having increasing program graph nodes. The model trained with the AxiomStep5 dataset had no training examples more than 25 program graph nodes yet performs relatively well on these more complex problems. The furthest right column shows the pe graph2axion model results on the most complex dataset.
Testset Sample Count
Model trained on AxiomStep5
Model trained
on AxiomStep10
P1 nodes
AS5
AS10
AS5
AS10
AS5
AS10
1-5
231
109
100
100
100
100
6-10
2147
1050
100
99
99
11-15
3980
2175
96
16-20
2583
2327
98
92
98
93
21-25
1059
1989
97
89
98
92
26-30
0
1229
N/A
83
N/A
90
31-35
698
N/A
N/A
88
36-40
0
304
N/A
N/A
87
41-45
0
101
N/A
68
N/A
84
46-50
0
27
N/A
67
N/A
85
All
10000
10000
99
90
99
93
Table 12: Performance vs. AST size: counts and percentage pass rates.
Testset Sample Count
Model trained on AxiomStep5
Model trained
on AxiomStepl0
AST depth
ASS
AS10
AS5
AS10
AS5
AS10
5
100
100
100
3
306
133
100
100
100
100
4
1489
577
100
99
99
99
5
4744
1844
98
95
3456
4308
93
7
0
3135
n/a
86
n/a
92
All
10000
10000
99
90
99
93
be applied to nodes repeatedly and in variable order, achieves a 93% average success rate. 72% of the proofs of length 6 from the WholeProof10 testset were solved by the model trained on WholeProof10, but only 5% of such proofs from AxiomStep10 were, suggesting the method of generating AxiomStep pairs covers the problem space more thoroughly.
The complete result for the WholeProof10 model on the WholeProof10 dataset was 8,388 out of 10,000 program pairs had a correct proof found; of those, 8,350 were the exact proof created during P1, P2 generation, implying that WholeProof10. while performing well on its own testset distribution, not learning to generalize to alternative proof paths.
Manual verifications We conducted series of manual verifications of the system used to produce all the above results. First, we are happy to confirm that most likely AB + BA given no verifiable equivalence sequence was produced, but that provably ab = ba indeed. We also verified that A (B + C C* AB, and that ABT ABи AB w) which would be much faster implementation. The system correctly suggests that ABT BAu + AB w³). We ensured that A' A'(AA')- & A'(AA-I)AA A, from typo once made when typing the computation of an orthonormal sub-space. We also verified that indeed AB + AC + aD aD = A(B + C).
Generalizing variable types We explored the ability of the model to understand variable typing by training a model with the AxiomStep10 distribution but with no samples that included the sealar variable 'e" and scalar multiplication **. This removed about 50% of the training set, longer programs were often included both tokens. When tested with the unaltered AxiomStep10 test set and beam width 10, test samples that included scalar variable not "e' and *, were proven equal
29

---

Under review as a conference paper at ICLR 2021
Table 13: Generalizing to longer proofs. Percentage pass rates for equivalence proof's of increasing axiom counts when testing each of 4 datasets on models trained using each of 4 datasets.
Axiom Count in
Model trained on
Model trained on WholcProof10 (WP10)
Model trained on
Model trained on
WholcProof5 (WP5)
AxiomStep5 (AS5)
AxiomStep10 (AS10)
Proof]
WP5
WP10
AS5
AS10
WP5 WP10
AS5
AS10
WP5
WP10
AS5
AS10
WP5 WP10 AS5
AS10
100
100
99
100
100
100
100
100
100
100
100
100
99
98
66
64
99
99
65
63
100
99
100
99
100
100
100
100
98
94
34
33
97
95
33
33
100
98
99
98
100
99
99
99
93
84
16
15
90
88
16
15
98
95
98
97
99
98
98
98
84
70
82
96
97
95
96
14
4
72
5
81
88
90
93
63
83
87
0
54
54
75
73
82
0
0
47
0
35
64
6.3
74
10
0
0
34
0
24
57
46
66
95 66
44
27
94
84
44
99
87
99
90
99
93
99
93
90% of the time; test samples that included 'e' and *2 were also proven equal 90% of the time. For beam width 1 the proof success rates were 72% and 70% for without and with 'e', implying that the heavily biased training set did have small effect on the system generalization, pe-graph2as was still able generalize the relation 'e' to the *, operator given that 'e" was used in contexts similar to other scalar variables in the training samples that were provided, implying it was forming internal representation of 'scalar' type by learning from examples.
om
F.2 LEARNING THAT MULTIPLE AXIOM CHOICES ARE POSSIBLE
Our AxiomStep10 model trained on axioms which may be applied varying order the training set. For example, ((a + b) (c+ ((b (66-a) * (d + c)) may have the training data to Commute the left node a a+b b first and then c d second; in the same dataset, ((a + e) xb+ (b+c)) = ((e + a) * (c+ b)) might occur and the training data has the right node Commuted first. In this way, expect the model to learn that either commuting the left or right node is proper first axiom choice. Table expllores the ability of the model produce such axiom proposals. Given 5 scalar variables, there 120 possible expressions where two 2-variable additions are multiplied together such as ((a+b) * (c+d)) We consider here all 120 program pairs in which the left and right additions are commuted. The table shows which axioms and positions are recommended by the graph-to-sequent model within the pe-graph22 axi om system as most probably moving the 2 programs closer to equivalence by the beam width 3 on this problem. Note that the 2 correct axioms are always within the top 3 choices and the other axioms (Commute and DistributeLeffi on the root), while not necessary for this problem, are at least legal choices for axioms within our expression language.
neural network
The results in table 1ellte to the value our approach in relation to reinforcement learning models for proof generation Fawzi et al. (2019) Bansal et al. (201)). To make an analogy with reinforcement learning, in our training, the world 'state' presented as a Pl, P2 pair and the system must learn to produce axiom location which performs an 'action' on the 'state' of P1 in predictable way. Unlike reinforcement learning, we do not produce a reward function and our system canmot learn from a poor reward produced by incorrect axiom. However, our system, as is presented with a wide distribution of (P1,P2, S) tuples to train on, learns a probability distribution of possibly correct axioms produce for given program pair. There may be value in combining our graph-neural- neural- hindsight mechanism Andrychowicz al. (2017) learn from every attempted axiom, but is immediately obvious that our approach of learning only from examples of successful equivalence proofs would be improved.
have demonstrated that
within a reinforcement learning framework that used
Exploration of alternate designs In order to design the system, explored parts of the design space quickly and performed several single training run comparisons between 2 options, as shown in Table 15
30

---

Under review as a conference paper at ICLR 2021
Table 14: Learning multiple output options. When considering scalar expressions that can be proven equivalent by commuting the left and right subexpressions, such as (a b)(c d) (b a) + c). pe-graph2axl
learns that either the left or right commute can oceur first. The columns show counts for axioms and locations proposed by the token generator with beam width of 3 when given 120 different scalar expression pairs.
Axiom
Beam
Commute left child
Commute right child
Commute root
Distributel.eft
position
root
First
49
35
Second
58
59
3
Third
13
26
45
36
Any of top
120
120
84
36
In cases where 2 options were similar, we chose the model which ran faster, or run the models a experience based prior experiments to
second time get more precise evaluation, select an option.
Table 15:
Example explorations as single feature or parameter is changed. Each comparison is distinct experiment, as the entire network and language used was being varied.
Match beam
Match beam 10
Options compared
layer LSTM vs
1380
2 layer LSTM vs
5020
9457
3 layer LSTM
4358
8728
No edges grandchild nodes vs
9244
9728
Edges to grandchild nodes
9284
9774
Emcooder=DDecoder only root node vs
8616
9472
Encoder==Decoder avg all nodes
7828
9292
Experiments such as these informed our final network architecture. For example, in pe pe-graph2axicom om, we include 4 edges with Iearnable weight matrices from a node to its grand- children because such edges were found to improve results multiple runs. Li et al. Li et al. (2019) discusses the importance of selecting the optimal process for aggregating the graph information hence explore that issue for network. Our approach uses the root comparison node create aggregate the graph information for the decoder as it performs better than a node averaging.
Including Vot_equall option Table analyzes the challenge related a model which only predicts Equal or Not_equal for program pairs along with various options which produce rewrite rules which can be checked for correctness. all 4 output cases shown, 2 programs are provided as input. These programs use earlier version of our language model with 16 operators, core axioms, and 20 operands generated with distribution similar to WholeProof5.
Table 16: Table showing alternate options for handling not equal programs
Network
Predicted Rules Eq
Correct Rewrite Rules
output
Predicted NotEq
Description
Actual
Eq NotEq.
Eq
5.4%
94.6%
N/A
Beam width
NotEq
90.4%
9.6%
N/A
Rules or NotEq.
Eq
6.6%
93.4%
70.7%
Beam width
NotBq
90.9%
9.1%
N/A
Rules only,
Eq
N/A
100%
87.8%
Beam width
NotEg
N/A
N/A
N/A
Rules only.
B4
N/A
100%
96.2%
Beam width 10
NotEq
N/A
N/A
N/A
31

---

Under review as a conference paper at ICLR 2021
For the first output case, the output sequence produce is either Equal or Not Not_equal. Given false positive rate of 9.6%, these results demonstrate the importance of producing a verifiable proof of equivalence when using machine learning for automated equivalence checking. For the second output case, the model can produce either Not_equal or a rewrite rule sequence which can be checked for correctness. The source programs for the first and second case identical: 250,000 equivalent program pairs and 250,000 non-equivalent program pairs. In the second case, the false positive rate from the network is 9.1% % (rules predicted for Not_equal programs), but the model only produces correct rewrite rules between actual equivalent programs in 70.7 0.7%% of the cases.
One challenge with model that produce rules or Not _ot_equal that beam widths beyond are less usable. Consider that with beam width of 1, if the network predicts Not not_equal then the checker would conclude the programs are not equal (which is correct for 90.9% of the actually not equal programs). With a beam width of 10, there would be more proposed rewrite rules for equal programs to test with, but if of the 10 proposals is Not Not_equa should the checker conclude they are not equal? Or should the the checker only consider the most likely prediction (beam width 1) when checking for non-equivalence? The third and fourth network output cases provide an answer. For these cases, the training set is 400,000 equivalent program pairs none non-equivalent. 250,000 of these pairs are identical to the equivalent programs the first 2 cases, and 150,000 are new but produced using the same random generation process. Note that by requiring the network to focus only on creating rewrite rules, beam width is able to create correct rewrite rules for 87.8% of the equivalent programs. And now, since we' ve remove the confusion of the Not _ot__qqal prediction option, beam width 10 can be used to produce 10 possible rewrite rule sequences and in 96.2% of the cases these rules are correct. Hence, we propose the preferred use model for pe-graph2axiom is to always use the model which is trained for rule generation with beam width 10 and rely on our rule checker prevent false positives. From the 10 rewrite rule proposals, non-equivalent programs will never have correct rewrite rule sequence produced, hence we guarantee there are no false positives.
F.3 AN EXAMPLE OF BACK-EDGE IN THE PROGRAM GRAPII
Figure 7 shows an example of DoX and DoHalf. The new operators result in 2 new edges in our graph representation (along with 2 new back-edges): there is 'loopbody' edge type from the loop operator node to the start of the subgraph, and there is a 'loopfeedback' edge type from the variable which is written to each loop iteration. These 2 edge types are shown in the figure. The new Dohal f axiom intuitively states that DoX (g(x)) = DoHal fo (()((())) (where is the variable reused each iteration), and Dox states the reverse.
DoH
DoX
Dox (b (a + b)/c)
DoHalf = (a + (a + b)/c)/e)
Figure 7: Adding loop constructs creates cycles in the program graph.
32


Reviews:
[{"review_id": "x0sJ1038FNY", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 3, "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 introduce a new synthetic dataset of equational proofs over the basic axioms of linear algebra.  The dataset consists of triples `(t1, t2, rewrites)` where `rewrites` is a sequence of rewrite instructions that can transform `t1` into `t2`, though some of their models emit one rewrite at a time and observe the result of applying the rewrite instruction to `t1`.  They develop a GNN for the task called pe-graph2axiom and show that it beats two baselines.  Finally, they show that their trained system can solve 15 problems from two Khan Academy modules that can be expressed in their fragment.  The appendix refers to supplementary material including code and data, but no supplementary material was submitted.\n\nIt is a fine paper, but ultimately I do not think the work is sufficiently interesting to merit publication at ICLR.  As far as I can tell, the entire synthetic dataset is easily decidable by traditional approaches, e.g. by simplifying and distributing modulo AC then checking for syntactic equality.  Their pe-graph2axiom model also seems relatively standard for theorem proving domains, and their Khan Academy validation set of 15 problems seems rather meager.\n\nOther miscellaneous comments:\n- The novelty claim in the abstract seems overstated. It is common to use GNNs for axiomatic theorem proving.\n- The second sentence of the intro is unclear: \"However, their stochastic nature tends to hinder their ability to learn representations useful for manipulating symbolic information.\" I don't think the word \"stochastic\" is being used correctly here.\n- Later in the intro: \"[the authors' new method] can deterministically prove equivalence\". I find the intended meaning of the word \"deterministically\" unclear in this context.\n- The \"no false positives\" point is made several times in the introduction, even though most ML-for-theorem-proving papers have operated in formal environments where this property holds.\n- Page 2: I think `P1 ≡ A1(a, P1)` should be `P2 ≡ A1(a, P1)`\n- Page 4: Why is it necessary for datapoints not to share `P1`s?\n- I do not see discussion of the \"Graph-to-sequence w/o attention\" baseline presented in Table 3. What are the exact differences between this architecture and the pe-graph2axiom model? The question is particularly relevant since it performs almost as well.\n- It seems odd that they do not compare against transformers.\n- Page 8: \"hypermeter\" -> \"hyperparameter\"\n- I personally did not find the \"WholeProof\" approach to add much to the paper\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "UE0pb2qWgpT", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 5, "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": "Summary: This paper proposes a synthetic dataset of algebraic expressions with various kinds of symbols (e.g. scalars, vectors, matrices), and applies graph-to-sequence networks (with attentions) for predicting a sequence of rewrite rules (i.e. axioms) as an equivalent proof between two expressions. The prediction can be validated by a simple checker so that any false positives can be eliminated.\n\nI like this work in general but hesitate to recommend acceptance before a few concerns can be addressed.\n\nDetailed comments:\n- Quality: The authors present a comprehensive discussion of related work. The dataset generation is carefully designed and very systematic. However, comparison with baseline approaches seems arbitrary. It is not clear what data is used for the mini ablation study shown in Table 3. The claim of \"generate axiomatic proofs of equivalence between program pairs\" is a bit over-claimed and misleading, as programs are way complicated than algebraic expressions. Similarly, \"scalars, vectors and matrices\" are mere symbols (associated with different kinds).\n\n- Clarity: The overall writing is clear. The last part of section 5, i.e. the discussion about \"Incremental versus non-incremental  sequence production\" is quite confusing. Why path encoding is needed? How is it related to the \"incremental/non-incremental\" thing? \n\n- Originality: Graph-to-sequence networks were proposed by Beck et al. 2018; leveraging type information with graph neural networks is not new as well (see [1]). \n\n- Significance: This paper investigates a very important research topic, i.e. deep learning for symbolic reasoning, and proposes an interesting dataset, which could motivate many future works in this direction.\n\nQuestions:\n\nQ0: How is the model trained? Particularly, how to provide (intermediate) supervision? Introducing intermediate programs makes AxiomStep5 and AxiomStep10 essentially \"AxiomStep1\" in training, i.e. \"single-step prediction\", is that right?  That means multiple-step prediction (with beam search) only happens in testing. \n\nQ1: the authors argue \"ensures correctness for all non-equivalent programs input\", \"no sequence S produced can be verified correct: true negatives are trivially detected.\", which I find very hard to understand.  Correct me if I am wrong here. It is obvious that false positive (i.e. a sequence of rewrites is invalid) can be easily checked. But, if the model fails to find a sequence of rewrites, we are not sure if the input pair of _expressions_ are equivalent or not, how can we draw the conclusion that there is no such sequence?  \n\nQ2: given an input pair, do you limit the maximum number of generation steps? Say the ground truth takes 3 steps, the model may find a sequence of rewrites in 7 steps?  Do you count that as a success or failure? \n\nQ3: regarding embeddings, do different symbols have different initial embedding? In NLP tasks, assigning the same token with the same embedding is less problematic.  Does the same symbol in different algebraic expressions have the same initial embedding?  \n\nQ4: After intermediate program generation, P1 is rewritten to P'. Will embeddings of P1 be reused in P' in the next step prediction? Or they may be simply reset and another single-step prediction is invoked?\n\nQ5: How quantifiers are supported in axioms? Will \"(a+b+c) - (a+b+c)\" be reduced (or canceled) to 0 in one step? how many steps it might take?\n\nQ6: Can the system prove equivalence between \"1 + 1\" and \"2\", or a slightly more complicated example, \"a + a\" and \"2a\"?\n\nMinor typo:\nPage 5, \"production rulse\" => \"production rules\"\n\n[1] LambdaNet: Probabilistic Type Inference using Graph Neural Networks, ICLR 2020", "extra_scores": {}, "extra_text": {}}, {"review_id": "7wkB9AwuZNG", "reviewer": "AnonReviewer4", "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": "Summary: \nThis paper proposes a model for verifying semantic equivalence  between symbolic linear algebra expressions. Expressions are represented by trees and equivalence is proven by a sequence of axioms applied to the first expression. The proposed model encodes the expression/program trees as nodes on a graph connected by edges representing one of a set of axioms being applied to one of the elements in the first expression to yield a node in the second expression. The output of the model is a path, a sequence of edges, on this constructed graph that correspond to a sequence of axioms applied to the first expression to arrive at the second.\n\nStrengths:\n* The paper investigates an interesting problem of provably-correct equivalence proof generation for symbolic expressions.\n* Results on incremental versus comprehensive supervision over the entire proof sequence motivate the training method proposed by the work.\n\nWeaknesses:\n* It’s not clear how this work fits into the context of the field and experiments are only conducted as ablation studies on the architecture choices and training regimes, with no other existing methods for expression rewriting or proof generation considered.\n* The system is trained and tested on expressions that are very few rewrite steps away. While datasets were generated for up to 5 and 10 rewrite steps, even the 10-step dataset contains mostly pairs that have fewer (1-5) rewrite steps. In any case, 5 and 10 steps are very few and claims of robustness and generalization are weak with such few steps in the required proofs and such a large overlap in the steps required for pains in both datasets.\n* The system relies strongly on training one step at a time by requiring samples generated for every intermediate step in the proof of equivalence between two expressions.\n* There is no motivation for using a deep model over another path-finding method on the constructed graph that connects the input programs.\n\nRecommendation:\nI recommend against acceptance of the paper in its current form. The idea of GNN based path-finding for expression/program equivalence proving is promising, but the methods are not clearly and rigorously explained and the experimental settings are too weak to support the claims of generalizability and applicability to realistic scenarios. \n \nUpdate: Thank you to the authors for clarifying the points brought up in reviews. I acknowledge that I have reviewed their responses.\n\nQuestions:\n1. The development of the equivalence proofs on page 3 is very unclear. What does it mean to say “$x \\in v_i$”? This notation is not well explained. What is $x$ and what does it mean for $x$ to be _in_ $v_i$?\n2. The text says that models were “run” twice, does this mean trained twice with different initializations? If so, it would be more informative to report average performance rather than the one from the best random seed. If this is not the case, could you please clarify the training set-up?\n3. What are the evaluation metrics used and reported? What measure was used for the validation score that determined the best-performing model?\n\nMinor comments:\n* It is best practice to define acronyms the first time they are used. This will avoid confusion, especially for readers from a wider machine learning audience. In particular, GNN, GGNN and AST are not defined\n* There are many cases where citations should be within parentheses, please check for these. If the work is not referenced as part of the text of the sentence, it should be in parentheses for clarity.\n\nTypos:\nPg 5, “production rulse\" should read “production rules”\nPg 5, there is a sentence that begins with “E.g.” which should be replaced with the grammatical “For example,”. Similarly, on page 5, the sentence that begins “Fig. 1” should read “Figure 1”.", "extra_scores": {}, "extra_text": {}}, {"review_id": "64Jjddd9B0l", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "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 present an algorithm for proving equivalence between algebraic expressions. Their solution relies on a graph-to-sequence neural network that generates the rewrite strategy for translating one program to the other. I think it is very positive that the authors implemented it in OpenNMP-py. \n\nComments\n* On page (2) the claim (ii) is not novel in the sense that it produces a sequence of the proof, but because it uses the OpenNMT-py framework. Framing the theorem proving problem in a translation framework is very practical and useful.\n\n* In page2 “...It can deterministically prove equivalence, entirely avoids false positives, and quickly invalidates incorrect answers produced by the network (no deterministic answer is provided in this case, only a probability of non-equivalence). “ Most of the systems provide this guarantee. It is always easy to verify the proof deterministically and check if it is valid. I don’t understand the emphasis on that fact\n\n* I think it would have been useful if the authors had characterized their method as self-supervised. This is actually the way they generated data. Adopting this formalism it would make it much easier to communicate their writing easier to other research areas\n\n* It would make a lot of sense to use the proposed technique for compiler rewrites in compiler optimization. I think there are other competing methods that are much more successful in theorem proving. This one seems to be more appropriate for compiler optimization.\n\n\n* One of the details that is hidden in the appendix is that the algorithm is not invariant to the name of the variables. The algorithm recognizes only 4 variable names. For that reason would be curious to see how the algorithm behaves in the case of trying to reprove the same theorem it was trained on but with different variable names. Also, the authors should give a direction of how they can solve this limitation. \n\n\n* One complaint that I have is that the appendix is unreasonably big (20 pages). I noticed that there is a lot of redundancy, as a lot of the same information is unnecessarily repeated in the appendix\n\n\n* Figure 1 is very confusing. I struggle to understand how it maps to the description of the algorithm. I think the paper needs more graphics, given the complexity of the algorithm\n\n\n* I don’t understand the use of the Graph Neural Network. Is it used to model the AST of the program and generate an embedding for the LSTM?\n\n\n* The related work section is sufficient\n\n\n* On the positive side of the paper, I liked the comparative study between incremental and non-incremental proof.\n\n\n* The ability to generalize on longer proofs is definitely on the plus side of the paper\n\nIn general, I have a positive opinion about the paper, although it could have written in a more clear way. \n", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: I think this is a very promising paper, but the work is not ready for publication. 

The most significant concern shared by several reviewers is the insufficient evaluation. For example, the work is not compared with more traditional approaches to equivalence checking or any other baselines beyond ablations of the proposed method. Given that this is not the first paper to propose the use of deep learning to search for proofs, it seems important to compare to alternative methods. There is also a misalignment between the claims of novelty and the evaluation. For example, section 4 cites the novel approach to generating data as key to this approach, but the evaluation does not really address this claim. On the positive side, I was impressed with the ability to search for proofs of length 10 given the large branching factor, and I thought the results were promising. 

The authors should also consider some of the concerns with presentation raised by the reviewers.

Decision: Reject