Learning Axioms to Compute Verifiable Symbolic Expression Equivalence Proofs Using Graph-to-Sequence Networks
We target the problem of proving the semantic equivalence between two complex expressions represented as typed trees, and demonstrate our system on expressions from a rich multi-type symbolic language for linear algebra. We propose the first graph-to-sequence deep learning system to generate axiomatic proofs of equivalence between program pairs. We generate expressions which include scalars, vectors and matrices and 16 distinct operators combining them, with 147 distinct axioms of equivalence. We study the robustness of the system to generate proofs of increasing length, demonstrating how incremental graph-to-sequence networks can learn to represent complex and verifiable symbolic reasoning. It achieves 93% average true positive coverage on 10,000 test cases while ensuring zero false positives by design.
Code (0)
등록된 구현이 없습니다.
Tasks
Graph-to-SequenceSimilar Papers 제목 키워드 기반
Learning Continuous Semantic Representations of Symbolic Expressions
Combining abstract, symbolic reasoning with continuous neural reasoning is a grand challenge of representation learning. As a step in this direction, we propose a new architecture, called neural equivalence networks, for…
Representation LearningProving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models
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 re…
Graph-to-SequencevalidEGG-SR: Embedding Symbolic Equivalence into Symbolic Regression via Equality Graph
Symbolic regression seeks to uncover physical laws from experimental data by searching for closed-form expressions, which is an important task in AI-driven scientific discovery. Yet the exponential growth of the search s…
Reinforcement LearningDeep Symbolic Superoptimization Without Human Knowledge
Deep symbolic superoptimization refers to the task of applying deep learning methods to simplify symbolic expressions. Existing approaches either perform supervised training on human-constructed datasets that defines …
Decoderreinforcement-learningReinforcement LearningReinforcement Learning (RL)Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model
In this work we target the problem of provably computing the equivalence between two programs represented as dataflow graphs. To this end, we formalize the problem of equivalence between two programs as finding a set of …
Graph-to-Sequence