Modelpublic

TONKKrongyuth/finetune-all-minilm-I6-v2-proofwiki_w-theorem

sourceHugging Faceupdated 2y agoView on Hugging Face

0likes16downloads

Model Card

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

This is a sentence-transformers model finetuned from sentence-transformers/all-MiniLM-L6-v2 on the train dataset. It maps sentences & paragraphs to a 384-dimensional dense vector space and can be used for semantic textual similarity, semantic search, paraphrase mining, text classification, clustering, and more.

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)

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("TONKKrongyuth/finetune-all-minilm-I6-v2-proofwiki_w-theorem")
# Run inference
sentences = [
    'Let $m$ be a [[Definition:Number|numbers]] which is presented to $d$ [[Definition:Significant Figures|significant figures]].Then the most [[Definition:Significant Figures|significant figures]] that $\\sqrt m$ can have is also $d$.',
    ':$\\displaystyle \\int x \\csc a x \\rd x = \\frac 1 {a^2} \\paren {a x + \\frac {\\paren {a x}^3} {18} + \\frac {7 \\paren {a x}^5} {1800} + \\cdots + \\frac {\\paren {-1}^{n - 1} 2 \\paren {2^{2 n - 1} - 1} B_n \\paren {a x}^{2 n + 1} } {\\paren {2 n + 1}!} + \\cdots} + C$where $B_{2 n}$ is the $2 n$th [[Definition:Bernoulli Numbers|Bernoulli number]].',
    "Let $G$ be a [[Definition:Group|group]].Let $N$ be a [[Definition:Subgroup|subgroup]] of $G$.$N$ is a '''normal subgroup of $G$''' {{iff}}:=== [[Definition:Normal Subgroup/Definition 1|Definition 1]] ==={{:Definition:Normal Subgroup/Definition 1}}=== [[Definition:Normal Subgroup/Definition 2|Definition 2]] ==={{:Definition:Normal Subgroup/Definition 2}}=== [[Definition:Normal Subgroup/Definition 3|Definition 3]] ==={{:Definition:Normal Subgroup/Definition 3}}=== [[Definition:Normal Subgroup/Definition 4|Definition 4]] ==={{:Definition:Normal Subgroup/Definition 4}}=== [[Definition:Normal Subgroup/Definition 5|Definition 5]] ==={{:Definition:Normal Subgroup/Definition 5}}=== [[Definition:Normal Subgroup/Definition 6|Definition 6]] ==={{:Definition:Normal Subgroup/Definition 6}}=== [[Definition:Normal Subgroup/Definition 7|Definition 7]] ==={{:Definition:Normal Subgroup/Definition 7}}",
]
embeddings = model.encode(sentences)
print(embeddings.shape)
# [3, 384]

# Get the similarity scores for the embeddings
similarities = model.similarity(embeddings, embeddings)
print(similarities.shape)
# [3, 3]

<!--

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

train

—Dataset: train
—Size: 21,701 training samples
—Columns: <code>theoremscontent</code>, <code>refscontent</code>, and <code>score</code>
—Approximate statistics based on the first 1000 samples: | | theoremscontent | refscontent | score | |:--------|:-------------------------------------------------------------------------------------|:-------------------------------------------------------------------------------------|:---------------------------------------------------------------| | type | string | string | float | | details | <ul><li>min: 18 tokens</li><li>mean: 131.53 tokens</li><li>max: 256 tokens</li></ul> | <ul><li>min: 11 tokens</li><li>mean: 132.64 tokens</li><li>max: 256 tokens</li></ul> | <ul><li>min: 0.0</li><li>mean: 0.48</li><li>max: 1.0</li></ul> |
—Samples: | theoremscontent | refscontent | score | |:------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:-----------------| | <code>Let $\left({S, \preceq}\right)$ be an [[Definition:Ordered Set|ordered set]].Let $a, b \in S$.The following are [[Definition:Dual Statement (Order Theory)|dual statements]]::$b \in a^\prec$, the [[Definition:Strict Lower Closure of Element|strict lower closure]] of $a$:$b \in a^\succ$, the [[Definition:Strict Upper Closure of Element|strict upper closure]] of $a$</code> | <code>Let $\left({S, \preccurlyeq}\right)$ be an [[Definition:Ordered Set|ordered set]].Let $a \in S$.The '''strict upper closure of $a$ (in $S$)''' is defined as::$a^\succ := \left\{{b \in S: a \preccurlyeq b \land a \ne b}\right\}$or::$a^\succ := \left\{{b \in S: a \prec b}\right\}$That is, $a^\succ$ is the [[Definition:Set|set]] of all [[Definition:Element|elements]] of $S$ that [[Definition:Strictly Succeed|strictly succeed]] $a$.</code> | <code>1.0</code> | | <code>There exists only one [[Definition:Strictly Positive Integer|(strictly) positive integer]] that is exactly twice the [[Definition:Integer Addition|sum]] of its [[Definition:Digit|digits]].</code> | <code>Let $n$ be a [[Definition:Number|number]] expressed in a particular [[Definition:Number Base|number base]], $b$ for example.Then $n$ can be expressed as::$\sqbrk {rm r{m - 1} \ldots r2 r1 r0 . r{-1} r{-2} \ldots}b$where::$m$ is such that $b^m \le n < b^{m+1}$;:all the $ri$ are such that $0 \le ri < b$.Each of the $ri$ are known as the '''digits of $n$ (base $b$)'''.</code> | <code>1.0</code> | | <code>Let $p, q \in \R{\ne 0}$ be non-zero [[Definition:Real Number|real numbers]] with $p < q$.Let $x1, x2, \ldots, xn \ge 0$ be [[Definition:Real Number|real numbers]].If $p < 0$, then we require that $x1, x2, \ldots, xn > 0$.Then the [[Definition:Hölder Mean|Hölder mean]] satisfies the inequality:: $Mp \left({x1, x2, \ldots, xn}\right) \le Mq \left({x1, x2, \ldots, xn}\right)$Equality holds if and only if $x1 = x2 = \cdots = x_n$.</code> | <code>:$\map {\dfrac \d {\d x} } {\map {\tanh^{-1} } {\dfrac x a} } = \dfrac a {a^2 - x^2}$where $-a < x < a$.</code> | <code>0.0</code> |
—Loss: <code>CosineSimilarityLoss</code> with these parameters:

json

  {
      "loss_fct": "torch.nn.modules.loss.MSELoss"
  }

Evaluation Dataset

train

—Dataset: train
—Size: 5,387 evaluation samples
—Columns: <code>theoremscontent</code>, <code>refscontent</code>, and <code>score</code>
—Approximate statistics based on the first 1000 samples: | | theoremscontent | refscontent | score | |:--------|:-------------------------------------------------------------------------------------|:-------------------------------------------------------------------------------------|:--------------------------------------------------------------| | type | string | string | float | | details | <ul><li>min: 22 tokens</li><li>mean: 136.05 tokens</li><li>max: 256 tokens</li></ul> | <ul><li>min: 12 tokens</li><li>mean: 130.19 tokens</li><li>max: 256 tokens</li></ul> | <ul><li>min: 0.0</li><li>mean: 0.5</li><li>max: 1.0</li></ul> |
—Samples: | theoremscontent | refscontent | score | |:----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:-----------------| | <code>Let $G$ be a [[Definition:Group|group]] whose [[Definition:Identity Element|identity]] is $e$.Let $N$ be a [[Definition:Normal Subgroup|normal subgroup]] of $G$.Let $a \in G$.Then::$\paren {a N}^n$ is the [[Definition:Identity Element|identity]] of the [[Definition:Quotient Group|quotient group]] $G / N${{iff}}::$a^n \in N$</code> | <code>Let $G$ be a [[Definition:Group|group]].Let $N$ be a [[Definition:Normal Subgroup|normal subgroup]] of $G$.Then the [[Definition:Left Coset Space|left coset space]] $G / N$ is a [[Definition:Group|group]], where the [[Definition:Group Operation|group operation]] is defined as::$\paren {a N} \paren {b N} = \paren {a b} N$$G / N$ is called the '''quotient group of $G$ by $N$'''.</code> | <code>1.0</code> | | <code>Let $\omega$ be the [[Definition:Natural Numbers|set of natural numbers]] defined as the [[Definition:Von Neumann Construction of Natural Numbers|von Neumann construction]].Let $m, n \in \omega$.Then::$m < n \iff m \in n$That is, every [[Definition:Natural Numbers|natural number]] is the [[Definition:Set|set]] of all smaller [[Definition:Natural Numbers|natural numbers]].</code> | <code>Let $S \subseteq \R$ be a [[Definition:Countable Set|countable set]].Then $\lambda \left({S}\right) = 0$, where $\lambda$ is [[Definition:Lebesgue Measure|Lebesgue measure]].That is, $S$ is a [[Definition:Null Set|$\lambda$-null set]].</code> | <code>0.0</code> | | <code>Let $\CC$ be a [[Definition:Cartesian Plane|Cartesian plane]].Let $S$ be a [[Definition:Set|set]] of [[Definition:Point|points]] in $\CC$.Let $F$ be the smallest [[Definition:Field (Abstract Algebra)|field]] containing all the [[Definition:Cartesian Coordinate System|coordinates]] of the [[Definition:Point|points]] in $S$.Let $P = \tuple {a, b}$ be a [[Definition:Point|point]] in $\CC$.Then::$P$ is [[Definition:Constructible Point in Plane|constructible]] from $S$ using a [[Definition:Compass and Straightedge Construction|compass and straightedge construction]]{{iff}}::the [[Definition:Cartesian Coordinate System|coordinates]] of $P$ are contained in a [[Definition:Finite Field Extension|finite extension]] $K$ of $F$ whose [[Definition:Degree of Field Extension|degree]] is given by:::$\index K F = 2^m$:for some $m \in \Z_{\ge 0}$.</code> | <code>Let $\mathcal L$ be a [[Definition:Formal Language|formal language]] used in the field of [[:Definition:Symbolic Logic|symbolic logic]].Then the [[Definition:Well-Formed Formula|well-formed formulas]] of $\mathcal L$ are often referred to as '''logical formulas'''.They are symbolic representations of [[Definition:Statement|statements]], and often of [[Definition:Compound Statement|compound statements]] in particular.</code> | <code>0.0</code> |
—Loss: <code>CosineSimilarityLoss</code> with these parameters:

json

  {
      "loss_fct": "torch.nn.modules.loss.MSELoss"
  }

Training Hyperparameters

Non-Default Hyperparameters

—eval_strategy: epoch
—push_to_hub: True
—hub_model_id: TONKKrongyuth/finetune-all-minilm-I6-v2-proofwiki_w-theorem

All Hyperparameters

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

—overwrite_output_dir: False
—do_predict: False
—eval_strategy: epoch
—prediction_loss_only: True
—per_device_train_batch_size: 8
—per_device_eval_batch_size: 8
—per_gpu_train_batch_size: None
—per_gpu_eval_batch_size: None
—gradient_accumulation_steps: 1
—eval_accumulation_steps: None
—torch_empty_cache_steps: None
—learning_rate: 5e-05
—weight_decay: 0.0
—adam_beta1: 0.9
—adam_beta2: 0.999
—adam_epsilon: 1e-08
—max_grad_norm: 1.0
—num_train_epochs: 3
—max_steps: -1
—lr_scheduler_type: linear
—lr_scheduler_kwargs: {}
—warmup_ratio: 0.0
—warmup_steps: 0
—log_level: passive
—log_level_replica: warning
—log_on_each_node: True
—logging_nan_inf_filter: True
—save_safetensors: True
—save_on_each_node: False
—save_only_model: False
—restore_callback_states_from_checkpoint: False
—no_cuda: False
—use_cpu: False
—use_mps_device: False
—seed: 42
—data_seed: None
—jit_mode_eval: False
—use_ipex: False
—bf16: False
—fp16: False
—fp16_opt_level: O1
—half_precision_backend: auto
—bf16_full_eval: False
—fp16_full_eval: False
—tf32: None
—local_rank: 0
—ddp_backend: None
—tpu_num_cores: None
—tpu_metrics_debug: False
—debug: []
—dataloader_drop_last: False
—dataloader_num_workers: 0
—dataloader_prefetch_factor: None
—past_index: -1
—disable_tqdm: False
—remove_unused_columns: True
—label_names: None
—load_best_model_at_end: False
—ignore_data_skip: False
—fsdp: []
—fsdp_min_num_params: 0
—fsdp_config: {'minnumparams': 0, 'xla': False, 'xlafsdpv2': False, 'xlafsdpgrad_ckpt': False}
—fsdp_transformer_layer_cls_to_wrap: None
—accelerator_config: {'splitbatches': False, 'dispatchbatches': None, 'evenbatches': True, 'useseedablesampler': True, 'nonblocking': False, 'gradientaccumulationkwargs': None}
—deepspeed: None
—label_smoothing_factor: 0.0
—optim: adamw_torch
—optim_args: None
—adafactor: False
—group_by_length: False
—length_column_name: length
—ddp_find_unused_parameters: None
—ddp_bucket_cap_mb: None
—ddp_broadcast_buffers: False
—dataloader_pin_memory: True
—dataloader_persistent_workers: False
—skip_memory_metrics: True
—use_legacy_prediction_loop: False
—push_to_hub: True
—resume_from_checkpoint: None
—hub_model_id: TONKKrongyuth/finetune-all-minilm-I6-v2-proofwiki_w-theorem
—hub_strategy: every_save
—hub_private_repo: None
—hub_always_push: False
—gradient_checkpointing: False
—gradient_checkpointing_kwargs: None
—include_inputs_for_metrics: False
—include_for_metrics: []
—eval_do_concat_batches: True
—fp16_backend: auto
—push_to_hub_model_id: None
—push_to_hub_organization: None
—mp_parameters:
—auto_find_batch_size: False
—full_determinism: False
—torchdynamo: None
—ray_scope: last
—ddp_timeout: 1800
—torch_compile: False
—torch_compile_backend: None
—torch_compile_mode: None
—dispatch_batches: None
—split_batches: None
—include_tokens_per_second: False
—include_num_input_tokens_seen: False
—neftune_noise_alpha: None
—optim_target_modules: None
—batch_eval_metrics: False
—eval_on_start: False
—use_liger_kernel: False
—eval_use_gather_object: False
—average_tokens_across_devices: False
—prompts: None
—batch_sampler: batch_sampler
—multi_dataset_batch_sampler: proportional

</details>

Training Logs

Epoch	Step	Training Loss	train loss
1.0	2713	0.037	0.0280
2.0	5426	0.0185	0.0271
3.0	8139	0.0109	0.0259

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

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

<!--

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