Assisting Mathematical Formalization with A Learning-based Premise Retriever

• URL: http://arxiv.org/abs/2501.13959v1
• Date: Tue, 21 Jan 2025 06:32:25 GMT
• Title: Assisting Mathematical Formalization with A Learning-based Premise Retriever
• Authors: Yicheng Tao, Haotian Liu, Shanwen Wang, Hongteng Xu,
• Abstract summary: We introduce an innovative method for training a premise retriever to support the formalization of mathematics. Our approach employs a BERT model to embed proof states and premises into a shared latent space. To streamline the formalization process, we will release a search engine that enables users to query Mathlib theorems directly using proof states.
• Score: 29.06255449960557
• License:
• Abstract: Premise selection is a crucial yet challenging step in mathematical formalization, especially for users with limited experience. Due to the lack of available formalization projects, existing approaches that leverage language models often suffer from data scarcity. In this work, we introduce an innovative method for training a premise retriever to support the formalization of mathematics. Our approach employs a BERT model to embed proof states and premises into a shared latent space. The retrieval model is trained within a contrastive learning framework and incorporates a domain-specific tokenizer along with a fine-grained similarity computation method. Experimental results show that our model is highly competitive compared to existing baselines, achieving strong performance while requiring fewer computational resources. Performance is further enhanced through the integration of a re-ranking module. To streamline the formalization process, we will release a search engine that enables users to query Mathlib theorems directly using proof states, significantly improving accessibility and efficiency. Codes are available at https://github.com/ruc-ai4math/Premise-Retrieval.

Related papers

• LoRE-Merging: Exploring Low-Rank Estimation For Large Language Model Merging [10.33844295243509]
  We propose a unified framework for model merging based on low-rank estimation of task vectors without the need for access to the base model, named textscLoRE-Merging. Our approach is motivated by the observation that task vectors from fine-tuned models frequently exhibit a limited number of dominant singular values, making low-rank estimations less prone to interference.
  arXiv  Detail & Related papers  (2025-02-15T10:18:46Z)
• BRiTE: Bootstrapping Reinforced Thinking Process to Enhance Language Model Reasoning [78.63421517563056]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in complex reasoning tasks. We present a unified probabilistic framework that formalizes LLM reasoning through a novel graphical model. We introduce the Bootstrapping Reinforced Thinking Process (BRiTE) algorithm, which works in two steps.
  arXiv  Detail & Related papers  (2025-01-31T02:39:07Z)
• Retrieval-Oriented Knowledge for Click-Through Rate Prediction [29.55757862617378]
  Click-through rate (CTR) prediction is crucial for personalized online services. underlineretrieval-underlineoriented underlineknowledge (bfname) framework bypasses the real retrieval process. name features a knowledge base that preserves and imitates the retrieved & aggregated representations.
  arXiv  Detail & Related papers  (2024-04-28T20:21:03Z)
• DIMAT: Decentralized Iterative Merging-And-Training for Deep Learning Models [21.85879890198875]
  Decentralized Iterative Merging-And-Training (DIMAT) is a novel decentralized deep learning algorithm. We show that DIMAT attains faster and higher initial gain in accuracy with independent and identically distributed (IID) and non-IID data, incurring lower communication overhead. This DIMAT paradigm presents a new opportunity for the future decentralized learning, enhancing its adaptability to real-world with sparse lightweight communication computation.
  arXiv  Detail & Related papers  (2024-04-11T18:34:29Z)
• Back to Basics: A Simple Recipe for Improving Out-of-Domain Retrieval in Dense Encoders [63.28408887247742]
  We study whether training procedures can be improved to yield better generalization capabilities in the resulting models. We recommend a simple recipe for training dense encoders: Train on MSMARCO with parameter-efficient methods, such as LoRA, and opt for using in-batch negatives unless given well-constructed hard negatives.
  arXiv  Detail & Related papers  (2023-11-16T10:42:58Z)
• Exploring validation metrics for offline model-based optimisation with diffusion models [50.404829846182764]
  In model-based optimisation (MBO) we are interested in using machine learning to design candidates that maximise some measure of reward with respect to a black box function called the (ground truth) oracle. While an approximation to the ground oracle can be trained and used in place of it during model validation to measure the mean reward over generated candidates, the evaluation is approximate and vulnerable to adversarial examples. This is encapsulated under our proposed evaluation framework which is also designed to measure extrapolation.
  arXiv  Detail & Related papers  (2022-11-19T16:57:37Z)
• Generalization Properties of Retrieval-based Models [50.35325326050263]
  Retrieval-based machine learning methods have enjoyed success on a wide range of problems. Despite growing literature showcasing the promise of these models, the theoretical underpinning for such models remains underexplored. We present a formal treatment of retrieval-based models to characterize their generalization ability.
  arXiv  Detail & Related papers  (2022-10-06T00:33:01Z)
• Benchopt: Reproducible, efficient and collaborative optimization benchmarks [67.29240500171532]
  Benchopt is a framework to automate, reproduce and publish optimization benchmarks in machine learning. Benchopt simplifies benchmarking for the community by providing an off-the-shelf tool for running, sharing and extending experiments.
  arXiv  Detail & Related papers  (2022-06-27T16:19:24Z)
• HyperImpute: Generalized Iterative Imputation with Automatic Model Selection [77.86861638371926]
  We propose a generalized iterative imputation framework for adaptively and automatically configuring column-wise models. We provide a concrete implementation with out-of-the-box learners, simulators, and interfaces.
  arXiv  Detail & Related papers  (2022-06-15T19:10:35Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT (bf Proof bf Artifact bf Co-bf Training) is a general methodology for extracting self-supervised data from kernel-level proof terms for co-training. We instrument Lean with a neural theorem prover driven by a Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32% to 48%.
  arXiv  Detail & Related papers  (2021-02-11T18:59:24Z)

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.