# BERT is not The Count: Learning to Match Mathematical Statements with Proofs

arXiv: https://arxiv.org/abs/2302.09350 · HTML: https://mlsanity.com/paper/2302.09350/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 38 references that are in the map.
- First posted on arXiv 18 Feb 2023.

## Builds on (most cited first, 11 of 11)

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- ["Why Should I Trust You?": Explaining the Predictions of Any Classifier](https://mlsanity.com/paper/1602.04938/) (2016)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [MathBERT: A Pre-Trained Model for Mathematical Formula Understanding](https://mlsanity.com/paper/2105.00377/) (2021)
- [MathBERT: A Pre-trained Language Model for General NLP Tasks in Mathematics Education](https://mlsanity.com/paper/2106.07340/) (2021)
- [Mathematical Language Processing Project](https://mlsanity.com/paper/1407.0167/) (2014)
- [Erasure of Unaligned Attributes from Neural Representations](https://mlsanity.com/paper/2302.02997/) (2023)
- [POS Tagging and its Applications for Mathematics](https://mlsanity.com/paper/1406.2880/) (2014)
- [Learning to Match Mathematical Statements with Proofs](https://mlsanity.com/paper/2102.02110/) (2021)

## Built on by (most cited first, 10 of 10)

- [Reasoning or Reciting? Exploring the Capabilities and Limitations of Language Models Through Counterfactual Tasks](https://mlsanity.com/paper/2307.02477/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [The Larger They Are, the Harder They Fail: Language Models do not Recognize Identifier Swaps in Python](https://mlsanity.com/paper/2305.15507/) (2023)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [A Symbolic Framework for Evaluating Mathematical Reasoning and Generalisation with Transformers](https://mlsanity.com/paper/2305.12563/) (2023)
- [ARL2: Aligning Retrievers for Black-box Large Language Models via Self-guided Adaptive Relevance Labeling](https://mlsanity.com/paper/2402.13542/) (2024)
- [An Investigation of LLMs' Inefficacy in Understanding Converse Relations](https://mlsanity.com/paper/2310.05163/) (2023)
- [Spectral Attention Steering for Prompt Highlighting](https://mlsanity.com/paper/2603.01281/) (2026)
- [When Can Attention Heads Be Statically Defined?](https://mlsanity.com/paper/2609.34650/) (2026)
- [GameSmith: Scaling Zero-Sum Self-Play with Synthesised Games](https://mlsanity.com/paper/2610.13995/) (2026)

## Abstract (arXiv)

We introduce a task consisting in matching a proof to a given mathematical statement. The task fits well within current research on Mathematical Information Retrieval and, more generally, mathematical article analysis (Mathematical Sciences, 2014). We present a dataset for the task (the MATcH dataset) consisting of over 180k statement-proof pairs extracted from modern mathematical research articles. We find this dataset highly representative of our task, as it consists of relatively new findings useful to mathematicians. We propose a bilinear similarity model and two decoding methods to match statements to proofs effectively. While the first decoding method matches a proof to a statement without being aware of other statements or proofs, the second method treats the task as a global matching problem. Through a symbol replacement procedure, we analyze the "insights" that pre-trained language models have in such mathematical article analysis and show that while these models perform well on this task with the best performing mean reciprocal rank of 73.7, they follow a relatively shallow symbolic analysis and matching to achieve that performance.