SentenceTransformer based on sentence-transformers/all-MiniLM-L6-v2

Model Details

Model Description

• Model Type: Sentence Transformer
• Base model: sentence-transformers/all-MiniLM-L6-v2
• Maximum Sequence Length: 256 tokens
• Output Dimensionality: 384 dimensions
• Similarity Function: Cosine Similarity
• Training Dataset:
  • train

Model Sources

• Documentation: Sentence Transformers Documentation
• Repository: Sentence Transformers on GitHub
• Hugging Face: Sentence Transformers on Hugging Face

Full Model Architecture

SentenceTransformer(
  (0): Transformer({'max_seq_length': 256, 'do_lower_case': False}) with Transformer model: BertModel 
  (1): Pooling({'word_embedding_dimension': 384, 'pooling_mode_cls_token': False, 'pooling_mode_mean_tokens': True, 'pooling_mode_max_tokens': False, 'pooling_mode_mean_sqrt_len_tokens': False, 'pooling_mode_weightedmean_tokens': False, 'pooling_mode_lasttoken': False, 'include_prompt': True})
  (2): Normalize()
)

Usage

Direct Usage (Sentence Transformers)

Training Details

Training Dataset

train

• Dataset: train
• Size: 20,935 training samples
• Columns: theorems_content, refs_content, and score
• Approximate statistics based on the first 1000 samples:

  	theorems_content	refs_content	score
  type	string	string	float
  details	min: 16 tokens mean: 129.25 tokens max: 256 tokens	min: 12 tokens mean: 141.91 tokens max: 256 tokens	min: 0.0 mean: 0.49 max: 1.0

• Samples:

  theorems_content	refs_content	score
  Let $C_n$ be the [[Definition:Cyclic Group	cyclic group]] of [[Definition:Order of Structure	order]] $n$.Let $C_n = \gen a$, that is, that $C_n$ is [[Definition:Generator of Cyclic Group
  Let $T = \struct {S, \tau}$ be a [[Definition:Topological Space	topological space]] where $\tau$ is the [[Definition:Discrete Topology	discrete topology]] on $S$.Then $T$ is a [[Definition:Scattered Space
  Let $A \subseteq \R$ be the [[Definition:Set	set]] of all points on $\R$ defined as::$A := \set 0 \cup \set {\dfrac 1 n : n \in \Z_{>0} }$Let $\struct {A, \tau_d}$ be the [[Definition:Integer Reciprocal Space	integer reciprocal space]] with [[Definition:Zero (Number)

• Loss: CosineSimilarityLoss with these parameters:
  json

  1{ 2 "loss_fct": "torch.nn.modules.loss.MSELoss" 3}

Evaluation Dataset

train

• Dataset: train
• Size: 5,193 evaluation samples
• Columns: theorems_content, refs_content, and score
• Approximate statistics based on the first 1000 samples:

  	theorems_content	refs_content	score
  type	string	string	float
  details	min: 22 tokens mean: 134.45 tokens max: 256 tokens	min: 11 tokens mean: 139.82 tokens max: 256 tokens	min: 0.0 mean: 0.5 max: 1.0

• Samples:

  theorems_content	refs_content	score
  Let $F$ be a [[Definition:Field (Abstract Algebra)	field]].Then $F$ is a [[Definition:Principal Ideal Domain	principal ideal domain]].
  :$G$ is a [[Definition:Left Ideal	left ideal]] of $\struct {\map {\MM_S} 2, +, \times}$.	$J$ is a '''left ideal of $R$''' {{iff}}::$\forall j \in J: \forall r \in R: r \circ j \in J$that is, {{iff}}::$\forall r \in R: r \circ J \subseteq J$
  Let $S$ be a [[Definition:Set	set]].Let $T \subseteq S$ be a given [[Definition:Subset	subset]] of $S$.Let $\powerset S$ denote the [[Definition:Power Set

• Loss: CosineSimilarityLoss with these parameters:
  json

  1{ 2 "loss_fct": "torch.nn.modules.loss.MSELoss" 3}

Training Hyperparameters

Non-Default Hyperparameters

• eval_strategy: epoch
• push_to_hub: True
• hub_model_id: TONKKrongyuth/finetune-all-minilm-L6-v2-proofwiki_wo-theorem

All Hyperparameters

Training Logs

Framework Versions

• Python: 3.11.11
• Sentence Transformers: 3.4.1
• Transformers: 4.48.3
• PyTorch: 2.6.0+cu124
• Accelerate: 1.3.0
• Datasets: 3.3.2
• Tokenizers: 0.21.0

Citation

BibTeX

Sentence Transformers