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.

python

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

Samples:

sentence_0	sentence_1
`lemma ord_twopow_3_5:[object Object] assumes "k <ge> 3" "x mod 8 <in> {3, 5 :: nat}"[object Object] shows "ord (2 ^ k) x = 2 ^ (k - 2)"`	`One_nat_def: shows "1 = Suc 0"`
`lemma silent_moves_intra_path_no_obs:[object Object] assumes "obs_intra m <lfloor>HRB_slice S<rfloor><^bsub>CFG<^esub> = {}" and "method_exit m'"[object Object] and "get_proc m = get_proc m'" and "valid_node m" and "length s = length (m#msx')"[object Object] and "<forall>m <in> set msx'. return_node m"[object Object] 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[object Object] assumes "RedBlack prb"[object Object] assumes "subpath (red prb) rv1 res rv2 (subs prb)"[object Object] assumes "<not> marked prb rv2"[object Object] 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:
json
1{ 2 "scale": 20.0, 3 "similarity_fct": "cos_sim", 4 "gather_across_devices": false, 5 "directions": [ 6 "query_to_doc" 7 ], 8 "partition_mode": "joint", 9 "hardness_mode": null, 10 "hardness_strength": 0.0 11}

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

bibtex

@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

bibtex

@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},
}

	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