Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization

• URL: http://arxiv.org/abs/2501.13959v3
• Date: Wed, 16 Jul 2025 04:56:27 GMT
• Title: Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization
• Authors: Yicheng Tao, Haotian Liu, Shanwen Wang, Hongteng Xu,
• Abstract summary: 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.
• Score: 29.06255449960557
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formalized mathematics has recently garnered significant attention for its ability to assist mathematicians across various fields. Premise retrieval, as a common step in mathematical formalization, has been a challenge, particularly for inexperienced users. Existing retrieval methods that facilitate natural language queries require a certain level of mathematical expertise from users, while approaches based on formal languages (e.g., Lean) typically struggle with the scarcity of training data, hindering the training of effective and generalizable retrieval models. In this work, we introduce a novel method that leverages data extracted from Mathlib to train a lightweight and effective premise retrieval model. In particular, the proposed model embeds queries (i.e., proof state provided by Lean) and premises in a latent space, featuring a tokenizer specifically trained on formal corpora. The model is learned in a contrastive learning framework, in which a fine-grained similarity calculation method and a re-ranking module are applied to enhance the retrieval performance. Experimental results demonstrate that our model outperforms existing baselines, achieving higher accuracy while maintaining a lower computational load. We have released an open-source search engine based on our retrieval model at https://premise-search.com/. The source code and the trained model can be found at https://github.com/ruc-ai4math/Premise-Retrieval.

Related papers

• SPaRFT: Self-Paced Reinforcement Fine-Tuning for Large Language Models [51.74498855100541]
  Large language models (LLMs) have shown strong reasoning capabilities when fine-tuned with reinforcement learning (RL)<n>We propose textbfSPaRFT, a self-paced learning framework that enables efficient learning based on the capability of the model being trained.
  arXiv  Detail & Related papers  (2025-08-07T03:50:48Z)
• On the Usage of Gaussian Process for Efficient Data Valuation [3.688196752709501]
  In machine learning, knowing the impact of a given datum on model training is a fundamental task referred to as Data Valuation.<n>We have designed a novel canonical decomposition allowing practitioners to analyze any data valuation method as the combination of two parts.<n>The strength of our approach stems from both its theoretical grounding in Bayesian theory, and its practical reach, by enabling fast estimation of valuations thanks to efficient update formulae.
  arXiv  Detail & Related papers  (2025-06-04T14:53:51Z)
• Exploring Training and Inference Scaling Laws in Generative Retrieval [50.82554729023865]
  Generative retrieval reformulates retrieval as an autoregressive generation task, where large language models generate target documents directly from a query.<n>We systematically investigate training and inference scaling laws in generative retrieval, exploring how model size, training data scale, and inference-time compute jointly influence performance.
  arXiv  Detail & Related papers  (2025-03-24T17:59:03Z)
• Is a Good Foundation Necessary for Efficient Reinforcement Learning? The Computational Role of the Base Model in Exploration [32.77845864484552]
  We introduce a new computational framework for RL with language models, in which the learner interacts with the model through a sampling oracle.<n>We show that coverage, while not necessary for data efficiency, lower bounds the runtime of any algorithm in our framework.<n>We introduce a new algorithm, SpannerSampling, which obtains optimal data efficiency and is computationally efficient whenever the pre-trained model enjoys sufficient coverage.
  arXiv  Detail & Related papers  (2025-03-10T15:31:42Z)
• 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)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  We present LeanAgent, a novel lifelong learning framework for formal theorem proving. LeanAgent continuously generalizes to and improves on ever-expanding mathematical knowledge. It generates formal proofs for 155 theorems across 23 diverse Lean repositories.
  arXiv  Detail & Related papers  (2024-10-08T17:11:24Z)
• 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)
• CodeGen2: Lessons for Training LLMs on Programming and Natural Languages [116.74407069443895]
  We unify encoder and decoder-based models into a single prefix-LM. For learning methods, we explore the claim of a "free lunch" hypothesis. For data distributions, the effect of a mixture distribution and multi-epoch training of programming and natural languages on model performance is explored.
  arXiv  Detail & Related papers  (2023-05-03T17:55:25Z)
• 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)
• CorpusBrain: Pre-train a Generative Retrieval Model for Knowledge-Intensive Language Tasks [62.22920673080208]
  Single-step generative model can dramatically simplify the search process and be optimized in end-to-end manner. We name the pre-trained generative retrieval model as CorpusBrain as all information about the corpus is encoded in its parameters without the need of constructing additional index.
  arXiv  Detail & Related papers  (2022-08-16T10:22:49Z)
• 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)
• Deep Efficient Continuous Manifold Learning for Time Series Modeling [11.876985348588477]
  A symmetric positive definite matrix is being studied in computer vision, signal processing, and medical image analysis. In this paper, we propose a framework to exploit a diffeomorphism mapping between Riemannian manifold and a Cholesky space. For dynamic modeling of time-series data, we devise a continuous manifold learning method by systematically integrating a manifold ordinary differential equation and a gated recurrent neural network.
  arXiv  Detail & Related papers  (2021-12-03T01:38:38Z)
• 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)
• Monotonic Cardinality Estimation of Similarity Selection: A Deep Learning Approach [22.958342743597044]
  We investigate the possibilities of utilizing deep learning for cardinality estimation of similarity selection. We propose a novel and generic method that can be applied to any data type and distance function.
  arXiv  Detail & Related papers  (2020-02-15T20:22:51Z)

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.