| --- |
| 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.* |
| --> |
