Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models

• URL: http://arxiv.org/abs/2606.23959v2
• Date: Fri, 26 Jun 2026 14:43:06 GMT
• Title: Does My Embedding Reflect That $A = B$? Evaluating Mathematical Equivalence in Embedding Models
• Abstract summary: A single statement can take very different forms depending on what subfield it is framed in.<n>Current embedding models tend to group statements by the terminology used to make them instead of the underlying math.<n>We propose a contrastive approach to learning embeddings of mathematical text that focuses on aligning informal statements with different formalizations.
• Score: 4.464113977291748
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• An Algebraic View of the Expressivity of Recurrent Language Models [50.88598486616582]
  The paper develops a unified algebraic account of the expressivity of recurrent neural networks.<n>The same architecture cannot implement an even-modulus counter once floating-point recurrences are enforced, yet realizes every even-modulus counter under unsigned-integer quantization.
  arXiv  Detail & Related papers  (2026-06-01T06:47:58Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• The Unreasonable Effectiveness of Model Merging for Cross-Lingual Transfer in LLMs [45.08958917457921]
  Large language models (LLMs) still struggle across tasks outside of high-resource languages.<n>In this work, we investigate cross-lingual transfer to lower-resource languages where task-specific post-training data is scarce.
  arXiv  Detail & Related papers  (2025-05-23T20:28:31Z)
• QUDsim: Quantifying Discourse Similarities in LLM-Generated Text [70.22275200293964]
  We introduce an abstraction based on linguistic theories in Questions Under Discussion (QUD) and question semantics to help quantify differences in discourse progression.<n>We then use this framework to build $textbfQUDsim$, a similarity metric that can detect discursive parallels between documents.<n>Using QUDsim, we find that LLMs often reuse discourse structures (more so than humans) across samples, even when content differs.
  arXiv  Detail & Related papers  (2025-04-12T23:46:09Z)
• LemmaHead: RAG Assisted Proof Generation Using Large Language Models [0.0]
  We develop LemmaHead, a knowledge base that supplements queries to the model with relevant mathematical context.<n>To measure our model's performance in mathematical reasoning, our testing paradigm focuses on the task of automated theorem proving.
  arXiv  Detail & Related papers  (2025-01-27T05:46:06Z)
• Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization [29.06255449960557]
  We introduce a novel method that leverages data extracted from Mathlib to train a lightweight and effective premise retrieval model.<n>The model is learned in a contrastive learning framework, in which a fine-grained similarity calculation method and a re-ranking module are applied.<n> Experimental results demonstrate that our model outperforms existing baselines, achieving higher accuracy while maintaining a lower computational load.
  arXiv  Detail & Related papers  (2025-01-21T06:32:25Z)
• Multilingual Mathematical Autoformalization [14.433478397963123]
  Autoformalization is the task of translating natural language materials into machine-verifiable formalisations. Existing methods tend to circumvent this challenge by manually curating small corpora. In this work, we create $textttMMA$, a large, flexible, multilingual, and multi-domain dataset of informal-formal pairs.
  arXiv  Detail & Related papers  (2023-11-07T06:42:15Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  We propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability.
  arXiv  Detail & Related papers  (2023-10-16T08:42:39Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  Autoformalization is the task of translating natural language mathematics into a formal language that can be verified by a program. Research paper mathematics requires large amounts of background and context. We propose an avenue towards tackling autoformalization for research-level mathematics, by breaking the task into easier and more approachable subtasks.
  arXiv  Detail & Related papers  (2023-10-12T00:50:24Z)
• Syntax and Semantics Meet in the "Middle": Probing the Syntax-Semantics Interface of LMs Through Agentivity [68.8204255655161]
  We present the semantic notion of agentivity as a case study for probing such interactions. This suggests LMs may potentially serve as more useful tools for linguistic annotation, theory testing, and discovery.
  arXiv  Detail & Related papers  (2023-05-29T16:24:01Z)
• Tree-Based Representation and Generation of Natural and Mathematical Language [77.34726150561087]
  Mathematical language in scientific communications and educational scenarios is important yet relatively understudied. Recent works on mathematical language focus either on representing stand-alone mathematical expressions, or mathematical reasoning in pre-trained natural language models. We propose a series of modifications to existing language models to jointly represent and generate text and math.
  arXiv  Detail & Related papers  (2023-02-15T22:38:34Z)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  We explore the abilities of a large language model (Codex) to help with formalisation in the Lean theorem prover. Codex is able to formalise short mathematical statements at undergrad level with nearly 75% accuracy for $120$ theorem statements. We show that with a new prompting strategy Codex can formalise these proofs in natural language with at least one out of twelve Codex completion being easy to repair into a complete proof.
  arXiv  Detail & Related papers  (2022-11-14T16:52:32Z)

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.