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:

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]

Training Details

Training Dataset

train

Dataset: train
Size: 21,701 training samples
Columns: theorems_content, refs_content, and score
Approximate statistics based on the first 1000 samples:
theorems_content refs_content score
type string string float
details
min: 18 tokens
mean: 131.53 tokens
max: 256 tokens
min: 11 tokens
mean: 132.64 tokens
max: 256 tokens
min: 0.0
mean: 0.48
max: 1.0

Samples:

theorems_content	refs_content	score
`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
`There exists only one [[Definition:Strictly Positive Integer`	(strictly) positive integer]] that is exactly twice the [[Definition:Integer Addition	sum]] of its [[Definition:Digit
`Let $p, q \in \R_{\ne 0}$ be non-zero [[Definition:Real Number`	real numbers]] with $p < q$.Let $x_1, x_2, \ldots, x_n \ge 0$ be [[Definition:Real Number	real numbers]].If $p < 0$, then we require that $x_1, x_2, \ldots, x_n > 0$.Then the [[Definition:Hölder Mean

Loss: CosineSimilarityLoss with these parameters:
json
1{ 2 "loss_fct": "torch.nn.modules.loss.MSELoss" 3}

Evaluation Dataset

train

Dataset: train
Size: 5,387 evaluation samples
Columns: theorems_content, refs_content, and score
Approximate statistics based on the first 1000 samples:
theorems_content refs_content score
type string string float
details
min: 22 tokens
mean: 136.05 tokens
max: 256 tokens
min: 12 tokens
mean: 130.19 tokens
max: 256 tokens
min: 0.0
mean: 0.5
max: 1.0

Samples:

theorems_content	refs_content	score
`Let $G$ be a [[Definition:Group`	group]] whose [[Definition:Identity Element	identity]] is $e$.Let $N$ be a [[Definition:Normal Subgroup
`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
`Let $\CC$ be a [[Definition:Cartesian Plane`	Cartesian plane]].Let $S$ be a [[Definition:Set	set]] of [[Definition:Point

Loss: CosineSimilarityLoss with these parameters:
json
1{ 2 "loss_fct": "torch.nn.modules.loss.MSELoss" 3}

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

Click to expand

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: {'min_num_params': 0, 'xla': False, 'xla_fsdp_v2': False, 'xla_fsdp_grad_ckpt': False}
fsdp_transformer_layer_cls_to_wrap: None
accelerator_config: {'split_batches': False, 'dispatch_batches': None, 'even_batches': True, 'use_seedable_sampler': True, 'non_blocking': False, 'gradient_accumulation_kwargs': 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

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

	theorems_content	refs_content	score
type	string	string	float
details	min: 18 tokens mean: 131.53 tokens max: 256 tokens	min: 11 tokens mean: 132.64 tokens max: 256 tokens	min: 0.0 mean: 0.48 max: 1.0