Assisting Mathematical Formalization with A Learning-based Premise Retriever

要約

前提選択は、特に経験が限られているユーザーにとって、数学的な形式化の重要でありながら挑戦的なステップです。
利用可能な形式化プロジェクトが不足しているため、言語モデルを活用する既存のアプローチは、しばしばデータ不足に苦しんでいます。
この作業では、数学の形式化をサポートするために、前提レトリバーをトレーニングするための革新的な方法を紹介します。
私たちのアプローチでは、BERTモデルを採用して、証明状態と施設を共有潜在スペースに埋め込みます。
検索モデルは、対照的な学習フレームワーク内でトレーニングされており、微調整された類似性計算方法とともにドメイン固有のトークナイザーが組み込まれています。
実験結果は、モデルが既存のベースラインと比較して非常に競争力があり、より少ない計算リソースを必要としながら強力なパフォーマンスを達成することを示しています。
再ランクモジュールの統合により、パフォーマンスがさらに強化されます。
形式化プロセスを合理化するために、ユーザーが証明状態を使用してMathlib定理を直接照会できるようにする検索エンジンをリリースし、アクセシビリティと効率を大幅に改善します。
コードはhttps://github.com/ruc-ai4math/premise-retrievalで入手できます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google