Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models
For researchers and practitioners using embeddings for mathematical text, this work highlights a critical failure of current models and offers a method to better capture mathematical equivalence.
The paper introduces the MELD dataset of mathematically equivalent but lexically different statements and shows that current embedding models group statements by terminology rather than mathematical content. They propose a contrastive learning approach that aligns informal statements with different formalizations, improving retrieval on both informal-formal tasks and the MELD dataset.
Because mathematics is highly abstract, a single statement can take very different forms depending on what subfield it is framed in. There are many examples where breakthroughs occurred after researchers discovered that a question had already been answered in a different field. At the same time, the growth of new resources related to formalization has increased the need for tools that enable efficient and reliable navigation between mathematical 'languages' (e.g., from Lean to natural language). In this paper, we investigate whether current embedding models capture mathematical equivalence. To do this, we introduce the Mathematically Equivalent but Lexically Different Pairs (MELD) Dataset, a collection of mathematically equivalent statements that are expressed in very different language. We show that current state-of-the-art embedding models tend to group statements by the terminology used to make them instead of the underlying math. Motivated by this, we propose a contrastive approach to learning embeddings of mathematical text that focuses on aligning informal statements with different formalizations. Our experiments demonstrate that this leads to improvements not only on informal-formal retrieval tasks but also on MELD, which only contains natural language statements.