Add new SentenceTransformer model

18c550b verified 2 months ago

17.5 kB

tags:
  - sentence-transformers
  - sentence-similarity
  - feature-extraction
  - generated_from_trainer
  - dataset_size:500
  - loss:MultipleNegativesRankingLoss
base_model: sentence-transformers/all-MiniLM-L6-v2
widget:
  - source_sentence: |-
      theorem ptyping_match:
        "\<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> [] \<turnstile> t : T \<Longrightarrow> t \<in> value \<Longrightarrow>
          \<exists>ts. \<turnstile> p \<rhd> t \<Rightarrow> ts"
        "\<turnstile> fps [:] fTs \<Rightarrow> \<Delta> \<Longrightarrow> [] \<turnstile> fs [:] fTs \<Longrightarrow>
          \<forall>(l, t) \<in> set fs. t \<in> value \<Longrightarrow> \<exists>us. \<turnstile> fps [\<rhd>] fs \<Rightarrow> us"
    sentences:
      - ' cases: fixes a1 :: "pat"   and a2 :: "trm"   and a3 :: "trm list" assumes "\<turnstile> a1 \<rhd> a2 \<Rightarrow> a3" obtains T :: "POPLmarkRecord.type" and t :: "trm" where "a1 = PVar T" and "a2 = t" and "a3 = [t]"   | fps :: "(char list \<times> pat) list" and fs :: "(char list \<times> trm) list" and ts :: "trm list" where "a1 = PRcd fps" and "a2 = Rcd fs" and "a3 = ts" and "\<turnstile> fps [\<rhd>] fs \<Rightarrow> ts"'
      - ' less_le_not_le: fixes less_eq :: "''a \<Rightarrow> ''a \<Rightarrow> bool"   and less :: "''a \<Rightarrow> ''a \<Rightarrow> bool"   and x :: "''a"   and y :: "''a" assumes "class.preorder less_eq less" shows "less x y = (less_eq x y \<and> \<not> less_eq y x)"'
      - ' UnE: fixes c :: "''b"   and A :: "''b set"   and B :: "''b set" assumes "c \<in> A \<union> B" obtains "c \<in> A"   | "c \<in> B"'
  - source_sentence: >-
      lemma (in infinite_coin_toss_space)
      nat_filtration_borel_measurable_singleton:
        fixes f::"bool stream \<Rightarrow> 'b::{t2_space}"
        assumes "f\<in> borel_measurable (nat_filtration n)"
        shows "f -`{f x} \<in> sets (nat_filtration n)"
    sentences:
      - ' size_3: shows "length [] = 0"'
      - ' Un_subset_iff: fixes A :: "''a set"   and B :: "''a set"   and C :: "''a set" shows "(A \<union> B \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"'
      - ' vimage_eq: fixes a :: "''b"   and f :: "''b \<Rightarrow> ''c"   and B :: "''c set" shows "(a \<in> f -` B) = (f a \<in> B)"'
  - source_sentence: >-
      lemma subst_psubst: "\<lbrakk> closed_env \<rho>; FV v = {} \<rbrakk>
      \<Longrightarrow> 
          subst x v (psubst ((x, EVar x) # \<rho>) e) = psubst ((x, v) # \<rho>) e"
    sentences:
      - ' at_within_def: fixes "open" :: "''e set \<Rightarrow> bool"   and a :: "''e"   and s :: "''e set" assumes "class.topological_space open" shows "topological_space.at_within open a s = inf (topological_space.nhds open a) (principal (s - {a}))"'
      - ' psubst_change: fixes \<rho> :: "(nat \<times> exp) list"   and \<rho>'' :: "(nat \<times> exp) list"   and e :: "exp" assumes "equiv_env \<rho> \<rho>''" shows "psubst \<rho> e = psubst \<rho>'' e"'
      - ' edges_of_walk_in_E: fixes xs :: "''a list" assumes "walk xs" shows "edges_of_walk xs \<subseteq> E"'
  - source_sentence: 'interpretation real_euclid: tarski_first5 real_euclid_C real_euclid_B'
    sentences:
      - ' weakly_fair_def2: fixes enabled :: "(nat \<Rightarrow> ''b) \<Rightarrow> bool"   and taken :: "(nat \<Rightarrow> ''b) \<Rightarrow> bool" shows "weakly_fair enabled taken = \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. enabled s \<and> \<not> taken s)) s)"'
      - ' add_diff_eq: fixes minus :: "''b \<Rightarrow> ''b \<Rightarrow> ''b"   and plus :: "''b \<Rightarrow> ''b \<Rightarrow> ''b"   and zero :: "''b"   and uminus :: "''b \<Rightarrow> ''b"   and a :: "''b"   and b :: "''b"   and c :: "''b" assumes "class.group_add minus plus zero uminus" shows "plus a (minus b c) = minus (plus a b) c"'
      - ' bottom_exists: shows "\<exists>x. least L x (carrier L)"'
  - source_sentence: |-
      lemma normal_mult: 
        fixes f g::"real poly"
        assumes hf: "normal_poly f" and hg: "normal_poly g"
        defines "df \<equiv> degree f" and "dg \<equiv> degree g"
        shows "normal_poly (f*g)"
    sentences:
      - ' pCons_0_as_mult: fixes p :: "''a poly" shows "pCons (0::''a) p = [:0::''a, 1::''a:] * p"'
      - ' less_Nil_2: fixes xs :: "''a list" shows "[] < xs"'
      - ' subprob_space_measure_pmf: fixes x :: "''a pmf" shows "subprob_space (measure_pmf x)"'
pipeline_tag: sentence-similarity
library_name: sentence-transformers

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

This is a sentence-transformers model finetuned from sentence-transformers/all-MiniLM-L6-v2. It maps sentences & paragraphs to a 384-dimensional dense vector space and can be used for retrieval.

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
Supported Modality: Text

Model Sources

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

Full Model Architecture

SentenceTransformer(
  (0): Transformer({'transformer_task': 'feature-extraction', 'modality_config': {'text': {'method': 'forward', 'method_output_name': 'last_hidden_state'}}, 'module_output_name': 'token_embeddings', 'architecture': 'BertModel'})
  (1): Pooling({'embedding_dimension': 384, 'pooling_mode': 'mean', 'include_prompt': True})
  (2): Normalize({})
)

Usage

Direct Usage (Sentence Transformers)

First install the Sentence Transformers library:

pip install -U sentence-transformers

Then you can load this model and run inference.

from sentence_transformers import SentenceTransformer

# Download from the 🤗 Hub
model = SentenceTransformer("Manborough/isabelle-premise-encoder")
# Run inference
sentences = [
    'lemma normal_mult: \n  fixes f g::"real poly"\n  assumes hf: "normal_poly f" and hg: "normal_poly g"\n  defines "df \\<equiv> degree f" and "dg \\<equiv> degree g"\n  shows "normal_poly (f*g)"',
    ' pCons_0_as_mult: fixes p :: "\'a poly" shows "pCons (0::\'a) p = [:0::\'a, 1::\'a:] * p"',
    ' less_Nil_2: fixes xs :: "\'a list" shows "[] < xs"',
]
embeddings = model.encode(sentences)
print(embeddings.shape)
# [3, 384]

# Get the similarity scores for the embeddings
similarities = model.similarity(embeddings, embeddings)
print(similarities)
# tensor([[1.0000, 0.3714, 0.0459],
#         [0.3714, 1.0000, 0.3391],
#         [0.0459, 0.3391, 1.0000]])

Training Details

Training Dataset

Unnamed Dataset

Size: 500 training samples
Columns: sentence_0 and sentence_1
Approximate statistics based on the first 100 samples:
sentence_0 sentence_1
type string string

modality text text
details
min: 3 tokens
mean: 97.25 tokens
max: 256 tokens

min: 12 tokens
mean: 67.63 tokens
max: 256 tokens

	sentence_0	sentence_1
type	string	string
modality	text	text
details	min: 3 tokens mean: 97.25 tokens max: 256 tokens	min: 12 tokens mean: 67.63 tokens max: 256 tokens

Samples:

sentence_0	sentence_1
`lemma ord_twopow_3_5: assumes "k <ge> 3" "x mod 8 <in> {3, 5 :: nat}" shows "ord (2 ^ k) x = 2 ^ (k - 2)"`	`One_nat_def: shows "1 = Suc 0"`
`lemma silent_moves_intra_path_no_obs: assumes "obs_intra m <lfloor>HRB_slice S<rfloor><^bsub>CFG<^esub> = {}" and "method_exit m'" and "get_proc m = get_proc m'" and "valid_node m" and "length s = length (m#msx')" and "<forall>m <in> set msx'. return_node m" obtains as where "S,slice_kind S <turnstile> (m#msx',s) =as<Rightarrow><^sub><tau> (m'#msx',s)"`	`distinct_1: fixes x21 :: "'a" and x22 :: "'a list" shows "[] <noteq> x21 # x22"`
`lemma assumes "RedBlack prb" assumes "subpath (red prb) rv1 res rv2 (subs prb)" assumes "<not> marked prb rv2" shows "<not> marked prb rv1"`	`subsumee_not_marked: fixes prb :: "('d, 'e, 'f) pre_RedBlack" and sub :: "('d <times> nat) <times> 'd <times> nat" assumes "RedBlack prb" and "sub <in> subs prb" shows "<not> marked prb (subsumee sub)"`

Loss: MultipleNegativesRankingLoss with these parameters:

{
    "scale": 20.0,
    "similarity_fct": "cos_sim",
    "gather_across_devices": false,
    "directions": [
        "query_to_doc"
    ],
    "partition_mode": "joint",
    "hardness_mode": null,
    "hardness_strength": 0.0
}

Training Hyperparameters

Non-Default Hyperparameters

per_device_train_batch_size: 32
num_train_epochs: 1
per_device_eval_batch_size: 32
multi_dataset_batch_sampler: round_robin

All Hyperparameters

Click to expand

per_device_train_batch_size: 32
num_train_epochs: 1
max_steps: -1
learning_rate: 5e-05
lr_scheduler_type: linear
lr_scheduler_kwargs: None
warmup_steps: 0
optim: adamw_torch_fused
optim_args: None
weight_decay: 0.0
adam_beta1: 0.9
adam_beta2: 0.999
adam_epsilon: 1e-08
optim_target_modules: None
gradient_accumulation_steps: 1
average_tokens_across_devices: True
max_grad_norm: 1
label_smoothing_factor: 0.0
bf16: False
fp16: False
bf16_full_eval: False
fp16_full_eval: False
tf32: None
gradient_checkpointing: False
gradient_checkpointing_kwargs: None
torch_compile: False
torch_compile_backend: None
torch_compile_mode: None
use_liger_kernel: False
liger_kernel_config: None
use_cache: False
neftune_noise_alpha: None
torch_empty_cache_steps: None
auto_find_batch_size: False
log_on_each_node: True
logging_nan_inf_filter: True
include_num_input_tokens_seen: no
log_level: passive
log_level_replica: warning
disable_tqdm: False
project: huggingface
trackio_space_id: None
trackio_bucket_id: None
trackio_static_space_id: None
per_device_eval_batch_size: 32
prediction_loss_only: True
eval_on_start: False
eval_do_concat_batches: True
eval_use_gather_object: False
eval_accumulation_steps: None
include_for_metrics: []
batch_eval_metrics: False
save_only_model: False
save_on_each_node: False
enable_jit_checkpoint: False
push_to_hub: False
hub_private_repo: None
hub_model_id: None
hub_strategy: every_save
hub_always_push: False
hub_revision: None
load_best_model_at_end: False
ignore_data_skip: False
restore_callback_states_from_checkpoint: False
full_determinism: False
seed: 42
data_seed: None
use_cpu: False
accelerator_config: {'split_batches': False, 'dispatch_batches': None, 'even_batches': True, 'use_seedable_sampler': True, 'non_blocking': False, 'gradient_accumulation_kwargs': None}
parallelism_config: None
dataloader_drop_last: False
dataloader_num_workers: 0
dataloader_pin_memory: True
dataloader_persistent_workers: False
dataloader_prefetch_factor: None
remove_unused_columns: True
label_names: None
train_sampling_strategy: random
length_column_name: length
ddp_find_unused_parameters: None
ddp_bucket_cap_mb: None
ddp_broadcast_buffers: False
ddp_static_graph: None
ddp_backend: None
ddp_timeout: 1800
fsdp: []
fsdp_config: {'min_num_params': 0, 'xla': False, 'xla_fsdp_v2': False, 'xla_fsdp_grad_ckpt': False}
deepspeed: None
debug: []
skip_memory_metrics: True
do_predict: False
resume_from_checkpoint: None
warmup_ratio: None
local_rank: -1
prompts: None
batch_sampler: batch_sampler
multi_dataset_batch_sampler: round_robin
router_mapping: {}
learning_rate_mapping: {}

Training Time

Training: 26.4 seconds

Framework Versions

Python: 3.13.12
Sentence Transformers: 5.5.1
Transformers: 5.9.0
PyTorch: 2.12.0
Accelerate: 1.13.0
Datasets: 4.8.5
Tokenizers: 0.22.2

Citation

BibTeX

Sentence Transformers

@inproceedings{reimers-2019-sentence-bert,
    title = "Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks",
    author = "Reimers, Nils and Gurevych, Iryna",
    booktitle = "Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing",
    month = "11",
    year = "2019",
    publisher = "Association for Computational Linguistics",
    url = "https://arxiv.org/abs/1908.10084",
}

MultipleNegativesRankingLoss

@misc{oord2019representationlearningcontrastivepredictive,
      title={Representation Learning with Contrastive Predictive Coding},
      author={Aaron van den Oord and Yazhe Li and Oriol Vinyals},
      year={2019},
      eprint={1807.03748},
      archivePrefix={arXiv},
      primaryClass={cs.LG},
      url={https://arxiv.org/abs/1807.03748},
}