Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules
We target the problem of automatically synthesizing proofs of semantic equivalence between two programs made of sequences of statements. We represent programs using abstract syntax trees (AST), where a given set of semantics-preserving rewrite rules can be applied on a specific AST pattern to generate a transformed and semantically equivalent program. In our system, two programs are equivalent if there exists a sequence of application of these rewrite rules that leads to rewriting one program into the other. We propose a neural network architecture based on a transformer model to generate proofs of equivalence between program pairs. The system outputs a sequence of rewrites, and the validity of the sequence is simply checked by verifying it can be applied. If no valid sequence is produced by the neural network, the system reports the programs as non-equivalent, ensuring by design no programs may be incorrectly reported as equivalent. Our system is fully implemented for one single grammar which can represent straight-line programs with function calls and multiple types. To efficiently train the system to generate such sequences, we develop an original incremental training technique, named self-supervised sample selection. We extensively study the effectiveness of this novel training approach on proofs of increasing complexity and length. Our system, S4Eq, achieves 97% proof success on a curated dataset of 10,000 pairs of equivalent programs.
Code (1)
Tasks
Self-Supervised LearningvalidSimilar Papers 제목 키워드 기반
Self-Taught Metric Learning without Labels
We present a novel self-taught framework for unsupervised metric learning, which alternates between predicting class-equivalence relations between data through a moving average of an embedding model and learning the mode…
Metric LearningContrastive Learning Can Find An Optimal Basis For Approximately View-Invariant Functions
Contrastive learning is a powerful framework for learning self-supervised representations that generalize well to downstream supervised tasks. We show that multiple existing contrastive learning methods can be reinterpre…
Contrastive LearningGeneralization BoundsOn Some Equivalence Relations between Incidence Calculus and Dempster-Shafer Theory of Evidence
Incidence Calculus and Dempster-Shafer Theory of Evidence are both theories to describe agents' degrees of belief in propositions, thus being appropriate to represent uncertainty in reasoning systems. This paper presents…
Musical Training, but not Mere Exposure to Music, Drives the Emergence of Chroma Equivalence in Artificial Neural Networks
Pitch is a fundamental aspect of auditory perception. Pitch perception is commonly described across two perceptual dimensions: pitch height is the sense that tones with varying frequencies seem to be higher or lower, and…
Self-Supervised LearningMusic TranscriptionAlleviating neighbor bias: augmenting graph self-supervise learning with structural equivalent positive samples
In recent years, using a self-supervised learning framework to learn the general characteristics of graphs has been considered a promising paradigm for graph representation learning. The core of self-supervised learning …
Graph Representation LearningNode ClassificationRepresentation LearningSelf-Supervised Learning