Generating Equivalent Expression Datasets using Formal Verification and Term Rewriting Algorithms

Zheng, Hongbo

Permalink

https://hdl.handle.net/2142/124785 Copy

Description

Title

Generating Equivalent Expression Datasets using Formal Verification and Term Rewriting Algorithms

Author(s)

Zheng, Hongbo

Issue Date

2023-05-01

Keyword(s)

Term-rewriting, E-graph, Context-free grammar/Context-sensitive grammar, Optimization, Formal Verification, Theorem Proving

Abstract

The manipulation and analysis of mathematical expressions are essential tasks in various scientific and engineering fields, particularly in machine learning, control system design, and electrical circuit analysis. Mathematical expression embedding models have been proposed to capture mathematical semantics and encode the representations of complex equations in a continuous vector space. However, obtaining large training datasets of equivalent mathematical expressions for these embedding models remains a significant challenge. To address this problem, we propose a novel term-rewriting algorithm that leverages e-graph, a graph data structure that represents collections of terms along with a congruence relation over those terms, in combination with context-free/context-sensitive grammars. This approach enables the generation of large datasets of equivalent mathematical expressions. In addition, our algorithm operates using multi-threading, allowing it to save significant computation time compared to single-threading approaches. By taking mathematical expressions, simple or relatively complicated, and a large number of mathematical rewrite rules, our algorithm can effectively generate several mathematical expressions that are mathematically equivalent to the original equation. Our approach bridges the gap in current mathematical expression language processing techniques, enhancing the robustness of embedding models.

Type of Resource

text

Language

eng

Owning Collections