Search: id:"swepub:oai:DiVA.org:kth-334711" >
Self-Supervised Lea...
-
Kommrusch, SteveColorado State Univ, Ft Collins, CO 80523 USA.
(author)
Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules
- Article/chapterEnglish2023
Publisher, publication year, extent ...
-
Institute of Electrical and Electronics Engineers (IEEE),2023
-
printrdacarrier
Numbers
-
LIBRIS-ID:oai:DiVA.org:kth-334711
-
https://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-334711URI
-
https://doi.org/10.1109/TSE.2023.3271065DOI
Supplementary language notes
-
Language:English
-
Summary in:English
Part of subdatabase
Classification
-
Subject category:ref swepub-contenttype
-
Subject category:art swepub-publicationtype
Notes
-
QC 20231127
-
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.
Subject headings and genre
Added entries (persons, corporate bodies, meetings, titles ...)
-
Monperrus, MartinKTH,Teoretisk datalogi, TCS(Swepub:kth)u13jhcyf
(author)
-
Pouchet, Louis-NoelColorado State Univ, Ft Collins, CO 80523 USA.
(author)
-
Colorado State Univ, Ft Collins, CO 80523 USA.Teoretisk datalogi, TCS
(creator_code:org_t)
Related titles
-
In:IEEE Transactions on Software Engineering: Institute of Electrical and Electronics Engineers (IEEE)49:7, s. 3771-37920098-55891939-3520
Internet link
Find in a library
To the university's database