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

• URL: http://arxiv.org/abs/2302.09350v1
• Date: Sat, 18 Feb 2023 14:48:20 GMT
• Title: BERT is not The Count: Learning to Match Mathematical Statements with Proofs
• Authors: Weixian Waylon Li, Yftah Ziser, Maximin Coavoux and Shay B. Cohen
• Abstract summary: The task fits well within current research on Mathematical Information Retrieval and, more generally, mathematical article analysis. We present a dataset consisting of over 180k statement-proof pairs extracted from modern mathematical research articles. We propose a bilinear similarity model and two decoding methods to match statements to proofs effectively.
• Score: 34.61792250254876
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Logic Contrastive Reasoning with Lightweight Large Language Model for Math Word Problems [0.0]
  This study focuses on improving the performance of lightweight Large Language Models (LLMs) in mathematical reasoning tasks. We introduce a novel method for measuring mathematical logic similarity and design an automatic screening mechanism. By employing carefully crafted positive and negative example prompts, we guide the model towards adopting sound reasoning logic.
  arXiv  Detail & Related papers  (2024-08-29T08:26:42Z)
• Towards a Knowledge Graph for Models and Algorithms in Applied Mathematics [0.0]
  We aim to represent models and algorithms as well as their relationship semantically to make this research data FAIR. The link between the two algorithmic tasks is established, as they occur in modeling corresponding to corresponding tasks. Subject-specific metadata is relevant here, such as the symmetry of a matrix or the linearity of a mathematical model.
  arXiv  Detail & Related papers  (2024-08-19T13:57:49Z)
• Discovering symbolic expressions with parallelized tree search [59.92040079807524]
  Symbolic regression plays a crucial role in scientific research thanks to its capability of discovering concise and interpretable mathematical expressions from data. Existing algorithms have faced a critical bottleneck of accuracy and efficiency over a decade when handling problems of complexity. We introduce a parallelized tree search (PTS) model to efficiently distill generic mathematical expressions from limited data.
  arXiv  Detail & Related papers  (2024-07-05T10:41:15Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  We propose Math-Minos, a natural language feedback-enhanced verifier. Our experiments reveal that a small set of natural language feedback can significantly boost the performance of the verifier.
  arXiv  Detail & Related papers  (2024-06-20T06:42:27Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• Semantic Representations of Mathematical Expressions in a Continuous Vector Space [0.0]
  This work describes an approach for representing mathematical expressions in a continuous vector space. We use the encoder of a sequence-to-sequence architecture, trained on visually different but mathematically equivalent expressions, to generate vector representations.
  arXiv  Detail & Related papers  (2022-10-08T22:33:39Z)
• JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem Understanding [74.12405417718054]
  This paper aims to advance the mathematical intelligence of machines by presenting the first Chinese mathematical pre-trained language model(PLM) Unlike other standard NLP tasks, mathematical texts are difficult to understand, since they involve mathematical terminology, symbols and formulas in the problem statement. We design a novel curriculum pre-training approach for improving the learning of mathematical PLMs, consisting of both basic and advanced courses.
  arXiv  Detail & Related papers  (2022-06-13T17:03:52Z)
• Syntax-Aware Network for Handwritten Mathematical Expression Recognition [53.130826547287626]
  Handwritten mathematical expression recognition (HMER) is a challenging task that has many potential applications. Recent methods for HMER have achieved outstanding performance with an encoder-decoder architecture. We propose a simple and efficient method for HMER, which is the first to incorporate syntax information into an encoder-decoder network.
  arXiv  Detail & Related papers  (2022-03-03T09:57:19Z)
• Learning to Match Mathematical Statements with Proofs [37.38969121408295]
  The task is designed to improve the processing of research-level mathematical texts. We release a dataset for the task, consisting of over 180k statement-proof pairs. We show that considering the assignment problem globally and using weighted bipartite matching algorithms helps a lot in tackling the task.
  arXiv  Detail & Related papers  (2021-02-03T15:38:54Z)
• A Mathematical Exploration of Why Language Models Help Solve Downstream Tasks [35.046596668631615]
  Autoregressive language models, pretrained using large text corpora to do well on next word prediction, have been successful at solving many downstream tasks. This paper initiates a mathematical study of this phenomenon for the downstream task of text classification.
  arXiv  Detail & Related papers  (2020-10-07T20:56:40Z)

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.