Venue: ICLR 2023 Conference

Reviews:

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: This paper defines equivalence-preserving program embedding, a constraint that requires the learned program embeddings to be equivalent if the corresponding programs have the same input-output behavior. It provides the conditions specifying when a programming language can be represented into embeddings that preserve the equivalence. It then provides empirical evidence showing that programming languages that satisfy the conditions can be more accurately embedded.
strength_and_weaknesses: Strength:
+ Describes an important property of program embeddings: they should remain invariant to semantic-preserving transformations.
+ First theoretical definition of equivalence-preserving program embedding problem. The paper provides formal conditions under which the programming languages can be tractably embedded.

Weaknesses: 

- The empirical study is not convincing by only evaluating BERT-Tiny. Numerous neural architectures have been used to model programs, e.g., large language models, graph neural networks, etc. Can the proposed theory help explain some of the successes of one architecture over others? Can the theory guide how to develop new models to learn program representations? 

- The practical implication of this paper is unclear. While the authors describe two applications (Section 2), these applications often deal with common programming languages that are intractable, e.g., code clones across binary code for vulnerability detection. Can the proposed theory help explain if the same code modeling task for some languages is strictly easier than the others? The theory can be more practically useful if it can be extended to quantify the intractability level so the resulting embeddings' error can be bounded or compared. 

- Figure 1: unclear why certain input sizes have their accuracy going down, even though they have reached 100% in the earlier epochs. 

- There is no discussion on why larger input space sizes need a smaller number of epochs to converge on the tractable language, which contradicts the observation that losses increase monotonically with input space sizes on the intractable language.
- Extensive results and discussions are put in the Appendix, costing great effort in going back and forth. 

- The paper uses code clone detection and semantic labeling to motivate their theory, but the theory focuses on characterizing language tractability. Can the theory extend to cross-language clone detection, e.g., one language is tractable, but the other language is not?
clarity,_quality,_novelty_and_reproducibility: Clarity: the paper describes the core idea clearly. 

Quality: the quality of the paper is good.

Novelty: the theory of equivalence-preserving embedding is novel.

Reproducibility: the evaluation is easy to reproduce.

summary_of_the_review: My main concern is the practical implication of the proposed theory. Ideally, equivalence-preserving program embedding makes sense if it remains invariant against program transformations. For example, code clone detection requires the model to understand that various classes of transformations on program syntax do not change their input-output behavior. Therefore, it makes more sense to characterize what transformations can be tractably embedded. However, the authors characterize it from the language perspective. Most of the programming languages that existing applications consider are intractable, i.e., assembly code or even undecidable, as pointed out by the authors.

Therefore, it is not unclear how the theory of equivalence-preserving embeddings could help solve existing semantic code modeling tasks.
review_title: null

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: The paper proposes a theoretical background on how to incorporate code semantics into code embedding.  They argue that when two programs behave identically on a given input, they are semantically equivalent, and their representation in the embedded space should capture such properties. They demonstrate their theoretical foundation across two tasks.  
strength_and_weaknesses: (+) Code semantics is an important program property, and proposing a theoretical framework to incorporate semantics to embedding is important. 

(+) The theoretical foundation is good.

(-) The demonstration is shown on small tiny problems. 

(-) I am not sure any general-purpose language can be tractably embedded. It is not clear how such a definition can be extended to such languages.

(-) If the intention is to use tractable embedding to domain-specific language, I would encourage the authors to show some convincing scenarios.
clarity,_quality,_novelty_and_reproducibility: The theoretical foundation presentation is clear. However, the potential of the idea is not thoroughly examined. The results should be reproducible.
summary_of_the_review: The paper presents some interesting and important ideas. However, there is a large gap between the idea and practicality and generalizability.  It is not clear to me how the proposed idea of tractable embedding can be applied to real-world problems.
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: The paper proposed a new notion of equivalence-preserving program embedding, proved a simple arithmetic language has an equivalence-preserving embedding, and experimentally demonstrated that having the embedding is crucial to learn an embedding of programs.

strength_and_weaknesses: Strengths:

+ The notion of equivalence-preserving program embedding is new, theoretically formulated, and proven to be satisfied by a simple arithmetic language and unsatisfied by a bit-vector language.

+ The usefulness of equivalence-preserving program embedding is experimentally demonstrated.

+ The documentation is well written and easy to follow.

Weaknesses:

- Little languages have equivalence-preserving program embedding functions. Theoretically, a tractably embeddable language (i.e., one with an equivalence-preserving embedding function) has a means to determine the equivalence of two programs. It means that no Turing-complete language is tractably embeddable. Furthermore, although recognizing the limitation of an approach is crucial in general, even the simple bit-vector language does not have such a function. Therefore, I am concerned about the practicality of the proposed approach in its current status. Considering the strictness of equivalence-preserving program embedding, I am not surprised that a machine learning model can learn an embedding for a tractably embeddable language even when the same model cannot learn an embedding for a language that is not tractably embeddable.

- As a minor point, the theory of the paper seems to assume the input space ($I$) is finite, but, in general, one can consider programs with an infinite input space (like list-processing programs).

clarity,_quality,_novelty_and_reproducibility: The paper is clear and easy to follow. It is also novel and original in that the paper proposed a new theoretical notion to indicate that a programming language is embeddable.

summary_of_the_review: The paper addresses a critical aim to apply machine learning techniques to programming language tasks. The proposed notion of equivalence-preserving program embedding is novel. However, as described above as a weakness, its practicality is a big concern because of its theoretical strictness. Research given in Section 5.1 would enhance the work much more.
review_title: null

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: This paper aims to provide a theory to analyze the semantic equivalence of programming languages. This is the classical equivalence problem and in general undecidable. This paper additionally imposes some assumptions and studies when the equivalence can be efficiently decided, defined as tractably embedded in this paper. The authors also conduct an empirical study, aiming to show that BERT-Tiny can learn languages with tractably embedded semantics but not intractably embedded semantics.
strength_and_weaknesses: **Strength**

Analyzing the hardness of equivalence decidability can be an interesting perspective to understand the learning capacity of neural network models, especially for programming language tasks.

**Weakness**
1. The theory is ad hoc:
The (semantic) equivalence problem is a classical problem and has been studied for decades for different formal systems, for example, automata, regular expressions, and pushdown systems. They are often at least PSPACE-hard. These are naturally encountered formal systems. In this paper, the authors impose assumptions like the (denotational) semantics is from a finite set, the input space is finite. Those assumptions in general do not hold.

2. The techniques are elementary:
The techniques used to develop the theory are elementary. With the finiteness and some efficient procedure assumptions, the proofs are usually direct manipulations of definitions and assumptions. It does not seem that there are useful theoretical or mathematical techniques.

3. The evaluation is rough:
The evaluations are on two toy languages defined in this paper, and the input space size is at most 11. It is conceivable that modular addition is easier than bitvector arithmetic to learn because the latter is a direct extension of the former. It is inconclusive to understand model's capacity to learn the semantics just based on this toy evaluation.
clarity,_quality,_novelty_and_reproducibility: **Clarity**

In the empirical study, the authors present two toy languages. The semantics of bitvector arithmetic is not defined for logical symbols. For example, what is 2 & 3 mod 7? It is fine to omit the semantic specification for modular addition because it has natural mathematical semantics, but bitvector arithmetic needs such specification. 

**Quality and Novelty**

 In essence, this paper studies the equivalence problem, which is a classical formal language problem. It appears that the authors are unaware of those results, and propose an ad-hoc theory. Therefore, the quality and novelty are insignificant at this time.

I think that understanding the hardness of semantic decidability can be an interesting angle in understanding semantic tasks arising from deep learning models. However, more works need to be done. For example, for existing programming semantic tasks, can the authors classify their hardness using the theory developed in this paper?
summary_of_the_review: This paper presents a theory to study the semantic equivalence of programming languages. However, the theory is ad hoc and the evaluation is inconclusive. This paper is not ready for acceptance yet.
review_title: null

Meta-review: metareview:_summary,_strengths_and_weaknesses: This paper presents an interesting characterization of equivalence-preserving program embeddings and studied under what conditions tractable embeddings exist for a programming language.  While the conceptual framework seems interesting, the assumptions required by the framework and the empirical studies show quite limited applicability to more general-purpose widely used programming languages, which all reviewers are concerned about.  As a theory paper this work also doesn’t discuss any insights for, e.g. learning program embeddings better.  I still think the problem of equivalence-preserving program embeddings is a good one to study, but the authors can try to think more along the above directions and improve the paper further for the machine learning community.
justification_for_why_not_higher_score: Theory makes assumptions that significantly reduce its applicability to more general purpose programming languages.

Empirical study shows results on toy programming languages and small representation learning models.

Limited insights for improving the current program embedding pipelines.
justification_for_why_not_lower_score: Can't be lower.
Decision: Reject