We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LG

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Machine Learning

Title: Self-Supervised Learning to Prove Equivalence Between Programs via Semantics-Preserving Rewrite Rules

Abstract: We target the problem of synthesizing proofs of semantic equivalence between two programs made of sequences of statements with complex symbolic expressions. We propose a neural network architecture based on the transformer to generate axiomatic proofs of equivalence between program pairs. We generate expressions which include scalars and vectors and support multi-typed rewrite rules to prove equivalence. For training the system, we develop an original training technique, which we call self-supervised sample selection. This incremental training improves the quality, generalizability and extensibility of the learned model. We study the effectiveness of the system to generate proofs of increasing length, and we demonstrate how transformer models learn to represent complex and verifiable symbolic reasoning. Our system, S4Eq, achieves 97% proof success on 10,000 pairs of programs while ensuring zero false positives by design.
Comments: 18 pages
Subjects: Machine Learning (cs.LG); Programming Languages (cs.PL)
Cite as: arXiv:2109.10476 [cs.LG]
  (or arXiv:2109.10476v1 [cs.LG] for this version)

Submission history

From: Steven Kommrusch [view email]
[v1] Wed, 22 Sep 2021 01:37:08 GMT (1514kb,D)

Link back to: arXiv, form interface, contact.