Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models

• URL: http://arxiv.org/abs/2106.02452v2
• Date: Wed, 9 Jun 2021 02:42:43 GMT
• Title: Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models
• Authors: Steve Kommrusch, Th\'eo Barollet and Louis-No\"el Pouchet
• Abstract summary: We develop a graph-to-sequence neural network system for program equivalence. We extensively evaluate our system on a rich multi-type linear algebra expression language. Our machine learning system guarantees correctness for all true negatives, and ensures 0 false positive by design.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We target the problem of provably computing the equivalence between two complex expression trees. To this end, we formalize the problem of equivalence between two such programs as finding a set of semantics-preserving rewrite rules from one into the other, such that after the rewrite the two programs are structurally identical, and therefore trivially equivalent.We then develop a graph-to-sequence neural network system for program equivalence, trained to produce such rewrite sequences from a carefully crafted automatic example generation algorithm. We extensively evaluate our system on a rich multi-type linear algebra expression language, using arbitrary combinations of 100+ graph-rewriting axioms of equivalence. Our machine learning system guarantees correctness for all true negatives, and ensures 0 false positive by design. It outputs via inference a valid proof of equivalence for 93% of the 10,000 equivalent expression pairs isolated for testing, using up to 50-term expressions. In all cases, the validity of the sequence produced and therefore the provable assertion of program equivalence is always computable, in negligible time.

Related papers

• An Expressive Trace Logic for Recursive Programs [0.36832029288386137]
  We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points. Both, programs and trace formulas, are equipped with a direct-style, fully compositional, denotational semantics. Our results shed light on the correspondence between programming constructs and logical connectives.
  arXiv  Detail & Related papers  (2024-11-20T08:35:29Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  We propose a hybrid system capable of solving arithmetic problems that require compositional and systematic reasoning over sequences of symbols. We show that the proposed system can accurately solve nested arithmetical expressions even when trained only on a subset including the simplest cases.
  arXiv  Detail & Related papers  (2023-06-29T18:35:41Z)
• P(Expression|Grammar): Probability of deriving an algebraic expression with a probabilistic context-free grammar [0.0]
  We show that the problem of calculating the probability of deriving a given expression with a given grammar is undecidable in general. We then present specific grammars for generating linear, rational, and hyperbolic expressions. For those grammars, we design algorithms for calculating the exact probability and efficient approximation with arbitrary precision.
  arXiv  Detail & Related papers  (2022-12-01T18:36:54Z)
• Hierarchical Phrase-based Sequence-to-Sequence Learning [94.10257313923478]
  We describe a neural transducer that maintains the flexibility of standard sequence-to-sequence (seq2seq) models while incorporating hierarchical phrases as a source of inductive bias during training and as explicit constraints during inference. Our approach trains two models: a discriminative derivation based on a bracketing grammar whose tree hierarchically aligns source and target phrases, and a neural seq2seq model that learns to translate the aligned phrases one-by-one.
  arXiv  Detail & Related papers  (2022-11-15T05:22:40Z)
• Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules [9.1570563482476]
  Two programs are equivalent if there exists a sequence of application of 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. Our system, S4Eq, achieves 97% proof success on a curated dataset of 10,000 pairs of equivalent programs.
  arXiv  Detail & Related papers  (2021-09-22T01:37:08Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  This thesis serves as a means of transforming the semantics of a modal and/or constructive logic into an 'economical' proof system. The refinement method connects two proof-theoretic paradigms: labelled and nested sequent calculi. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics.
  arXiv  Detail & Related papers  (2021-07-30T08:27:15Z)
• Contrastive Learning with Adversarial Perturbations for Conditional Text Generation [49.055659008469284]
  We propose a principled method to generate positive and negative samples for contrastive learning of seq2seq models. Specifically, we generate negative examples by adding small perturbations to the input sequence to minimize its conditional likelihood. We empirically show that our proposed method significantly improves the generalization of the seq2seq on three text generation tasks.
  arXiv  Detail & Related papers  (2020-12-14T06:20:27Z)
• Pseudo-Convolutional Policy Gradient for Sequence-to-Sequence Lip-Reading [96.48553941812366]
  Lip-reading aims to infer the speech content from the lip movement sequence. Traditional learning process of seq2seq models suffers from two problems. We propose a novel pseudo-convolutional policy gradient (PCPG) based method to address these two problems.
  arXiv  Detail & Related papers  (2020-03-09T09:12:26Z)
• Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model [0.0]
  We formalize the problem of equivalence between two programs as finding a set of semantics-preserving rewrite rules from one into the other. We then develop the first graph-to-sequence neural network system for program equivalence.
  arXiv  Detail & Related papers  (2020-02-17T06:43:00Z)
• Consistency of a Recurrent Language Model With Respect to Incomplete Decoding [67.54760086239514]
  We study the issue of receiving infinite-length sequences from a recurrent language model. We propose two remedies which address inconsistency: consistent variants of top-k and nucleus sampling, and a self-terminating recurrent language model.
  arXiv  Detail & Related papers  (2020-02-06T19:56:15Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.