---
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:\n  \"\\<turnstile> p : T \\<Rightarrow>\
    \ \\<Delta> \\<Longrightarrow> [] \\<turnstile> t : T \\<Longrightarrow> t \\\
    <in> value \\<Longrightarrow>\n    \\<exists>ts. \\<turnstile> p \\<rhd> t \\\
    <Rightarrow> ts\"\n  \"\\<turnstile> fps [:] fTs \\<Rightarrow> \\<Delta> \\<Longrightarrow>\
    \ [] \\<turnstile> fs [:] fTs \\<Longrightarrow>\n    \\<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:\n\
    \  fixes f::\"bool stream \\<Rightarrow> 'b::{t2_space}\"\n  assumes \"f\\<in>\
    \ borel_measurable (nat_filtration n)\"\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> \n    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: \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)\""
  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](https://www.SBERT.net) model finetuned from [sentence-transformers/all-MiniLM-L6-v2](https://huggingface.co/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](https://huggingface.co/sentence-transformers/all-MiniLM-L6-v2) <!-- at revision c9745ed1d9f207416be6d2e6f8de32d1f16199bf -->
- **Maximum Sequence Length:** 256 tokens
- **Output Dimensionality:** 384 dimensions
- **Similarity Function:** Cosine Similarity
- **Supported Modality:** Text
<!-- - **Training Dataset:** Unknown -->
<!-- - **Language:** Unknown -->
<!-- - **License:** Unknown -->

### Model Sources

- **Documentation:** [Sentence Transformers Documentation](https://sbert.net)
- **Repository:** [Sentence Transformers on GitHub](https://github.com/huggingface/sentence-transformers)
- **Hugging Face:** [Sentence Transformers on Hugging Face](https://huggingface.co/models?library=sentence-transformers)

### 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:

```bash
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]])
```
<!--
### Direct Usage (Transformers)

<details><summary>Click to see the direct usage in Transformers</summary>

</details>
-->

<!--
### Downstream Usage (Sentence Transformers)

You can finetune this model on your own dataset.

<details><summary>Click to expand</summary>

</details>
-->

<!--
### Out-of-Scope Use

*List how the model may foreseeably be misused and address what users ought not to do with the model.*
-->

<!--
## Bias, Risks and Limitations

*What are the known or foreseeable issues stemming from this model? You could also flag here known failure cases or weaknesses of the model.*
-->

<!--
### Recommendations

*What are recommendations with respect to the foreseeable issues? For example, filtering explicit content.*
-->

## Training Details

### Training Dataset

#### Unnamed Dataset

* Size: 500 training samples
* Columns: <code>sentence_0</code> and <code>sentence_1</code>
* Approximate statistics based on the first 100 samples:
  |          | sentence_0                                                                         | sentence_1                                                                          |
  |:---------|:-----------------------------------------------------------------------------------|:------------------------------------------------------------------------------------|
  | type     | string                                                                             | string                                                                              |
  | modality | text                                                                               | text                                                                                |
  | details  | <ul><li>min: 3 tokens</li><li>mean: 97.25 tokens</li><li>max: 256 tokens</li></ul> | <ul><li>min: 12 tokens</li><li>mean: 67.63 tokens</li><li>max: 256 tokens</li></ul> |
* Samples:
  | sentence_0                                                                                                                                                                                                                                                                                                                                                                                                    | sentence_1                                                                                                                                                                                                                       |
  |:--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
  | <code>lemma ord_twopow_3_5:<br>  assumes "k \<ge> 3" "x mod 8 \<in> {3, 5 :: nat}"<br>  shows   "ord (2 ^ k) x = 2 ^ (k - 2)"</code>                                                                                                                                                                                                                                                                          | <code> One_nat_def: shows "1 = Suc 0"</code>                                                                                                                                                                                     |
  | <code>lemma silent_moves_intra_path_no_obs:<br>  assumes "obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {}" and "method_exit m'"<br>  and "get_proc m = get_proc m'" and "valid_node m" and "length s = length (m#msx')"<br>  and "\<forall>m \<in> set msx'. return_node m"<br>  obtains as where "S,slice_kind S \<turnstile> (m#msx',s) =as\<Rightarrow>\<^sub>\<tau> (m'#msx',s)"</code> | <code> distinct_1: fixes x21 :: "'a"   and x22 :: "'a list" shows "[] \<noteq> x21 # x22"</code>                                                                                                                                 |
  | <code>lemma<br>  assumes "RedBlack prb"<br>  assumes "subpath (red prb) rv1 res rv2 (subs prb)"<br>  assumes "\<not> marked prb rv2"<br>  shows   "\<not> marked prb rv1"</code>                                                                                                                                                                                                                              | <code> 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)"</code> |
* Loss: [<code>MultipleNegativesRankingLoss</code>](https://sbert.net/docs/package_reference/sentence_transformer/losses.html#multiplenegativesrankingloss) with these parameters:
  ```json
  {
      "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
<details><summary>Click to expand</summary>

- `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`: {}

</details>

### 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},
}
```

<!--
## Glossary

*Clearly define terms in order to be accessible across audiences.*
-->

<!--
## Model Card Authors

*Lists the people who create the model card, providing recognition and accountability for the detailed work that goes into its construction.*
-->

<!--
## Model Card Contact

*Provides a way for people who have updates to the Model Card, suggestions, or questions, to contact the Model Card authors.*
-->