Training in progress, step 500

config.json

@@ -0,0 +1,27 @@
+{
+  "_name_or_path": "distilroberta-base",
+  "architectures": [
+    "RobertaForMaskedLM"
+  ],
+  "attention_probs_dropout_prob": 0.1,
+  "bos_token_id": 0,
+  "classifier_dropout": null,
+  "eos_token_id": 2,
+  "hidden_act": "gelu",
+  "hidden_dropout_prob": 0.1,
+  "hidden_size": 768,
+  "initializer_range": 0.02,
+  "intermediate_size": 3072,
+  "layer_norm_eps": 1e-05,
+  "max_position_embeddings": 514,
+  "model_type": "roberta",
+  "num_attention_heads": 12,
+  "num_hidden_layers": 6,
+  "pad_token_id": 1,
+  "position_embedding_type": "absolute",
+  "torch_dtype": "float32",
+  "transformers_version": "4.37.0.dev0",
+  "type_vocab_size": 1,
+  "use_cache": true,
+  "vocab_size": 50265
+}

model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:3c1423da4b3a10e9bbf360d7bb66d6a52639aa5b0a72e5e35f1919deb1060163
+size 328693404

runs/Dec29_01-55-53_062f1f1a863d/events.out.tfevents.1703814961.062f1f1a863d.42.0

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:35d7fcdbfa3dba32ea7681d691bba8987deb3bfdf43b8602801922cb21df5ff5
+size 4575

special_tokens_map.json

@@ -0,0 +1 @@
+{"unk_token":"<unk>","sep_token":"</s>","pad_token":"<pad>","cls_token":"<s>","mask_token":"<mask>"}

tokenizer.json

@@ -0,0 +1,544 @@
+{
+  "version": "1.0",
+  "truncation": null,
+  "padding": null,
+  "added_tokens": [
+    {
+      "id": 0,
+      "content": "<s>",
+      "single_word": false,
+      "lstrip": false,
+      "rstrip": false,
+      "normalized": false,
+      "special": true
+    },
+    {
+      "id": 1,
+      "content": "<pad>",
+      "single_word": false,
+      "lstrip": false,
+      "rstrip": false,
+      "normalized": false,
+      "special": true
+    },
+    {
+      "id": 2,
+      "content": "</s>",
+      "single_word": false,
+      "lstrip": false,
+      "rstrip": false,
+      "normalized": false,
+      "special": true
+    },
+    {
+      "id": 3,
+      "content": "<unk>",
+      "single_word": false,
+      "lstrip": false,
+      "rstrip": false,
+      "normalized": false,
+      "special": true
+    },
+    {
+      "id": 4,
+      "content": "<mask>",
+      "single_word": false,
+      "lstrip": false,
+      "rstrip": false,
+      "normalized": false,
+      "special": true
+    }
+  ],
+  "normalizer": null,
+  "pre_tokenizer": {
+    "type": "WhitespaceSplit"
+  },
+  "post_processor": null,
+  "decoder": null,
+  "model": {
+    "type": "WordPiece",
+    "unk_token": "<unk>",
+    "continuing_subword_prefix": "##",
+    "max_input_chars_per_word": 100,
+    "vocab": {
+      "<s>": 0,
+      "<pad>": 1,
+      "</s>": 2,
+      "<unk>": 3,
+      "<mask>": 4,
+      ".": 5,
+      "0": 6,
+      "1": 7,
+      "2": 8,
+      "3": 9,
+      "5": 10,
+      "6": 11,
+      "_": 12,
+      "a": 13,
+      "b": 14,
+      "c": 15,
+      "d": 16,
+      "e": 17,
+      "f": 18,
+      "g": 19,
+      "h": 20,
+      "i": 21,
+      "j": 22,
+      "l": 23,
+      "m": 24,
+      "n": 25,
+      "o": 26,
+      "p": 27,
+      "q": 28,
+      "r": 29,
+      "s": 30,
+      "t": 31,
+      "u": 32,
+      "v": 33,
+      "w": 34,
+      "x": 35,
+      "y": 36,
+      "##u": 37,
+      "##b": 38,
+      "##s": 39,
+      "##e": 40,
+      "##t": 41,
+      "##_": 42,
+      "##d": 43,
+      "##f": 44,
+      "##v": 45,
+      "##n": 46,
+      "##p": 47,
+      "##a": 48,
+      "##c": 49,
+      "##o": 50,
+      "##r": 51,
+      "##g": 52,
+      "##0": 53,
+      "##l": 54,
+      "##i": 55,
+      "##m": 56,
+      "##h": 57,
+      "##w": 58,
+      "##x": 59,
+      "##2": 60,
+      "##y": 61,
+      "##.": 62,
+      "##j": 63,
+      "##3": 64,
+      "##q": 65,
+      "##5": 66,
+      "##6": 67,
+      "##1": 68,
+      "##_t": 69,
+      "##ac": 70,
+      "##_tac": 71,
+      "##ef": 72,
+      "##_d": 73,
+      "##_def": 74,
+      "##re": 75,
+      "##in": 76,
+      "##al": 77,
+      "##al_": 78,
+      "##xt": 79,
+      "##real_": 80,
+      "ext": 81,
+      "extreal_": 82,
+      "lt": 83,
+      "##w_tac": 84,
+      "##_in": 85,
+      "##ft": 86,
+      "##fty": 87,
+      "##le": 88,
+      "##_infty": 89,
+      "##et": 90,
+      "rw_tac": 91,
+      "##is": 92,
+      "##an": 93,
+      "##_s": 94,
+      "met": 95,
+      "##is_tac": 96,
+      "metis_tac": 97,
+      "##ran": 98,
+      "##_tran": 99,
+      "##_trans": 100,
+      "extreal_m": 101,
+      "##lt": 102,
+      "##ax": 103,
+      "##en": 104,
+      "##lt_def": 105,
+      "##_le": 106,
+      "##te": 107,
+      "##le_def": 108,
+      "##ore": 109,
+      "d_": 110,
+      "lt_le": 111,
+      "lt_infty": 112,
+      "extreal_lt_def": 113,
+      "extreal_le_def": 114,
+      "##on": 115,
+      "##im": 116,
+      "##ot": 117,
+      "##ite": 118,
+      "##ion": 119,
+      "##ch": 120,
+      "##in_def": 121,
+      "##isch": 122,
+      "extreal_min_def": 123,
+      "##isch_tac": 124,
+      "min": 125,
+      "max": 126,
+      "##e_trans": 127,
+      "lte_trans": 128,
+      "max_infty": 129,
+      "let": 130,
+      "##_tot": 131,
+      "lt_tot": 132,
+      "min_infty": 133,
+      "let_trans": 134,
+      "lt_total": 135,
+      "disch_tac": 136,
+      "##_sim": 137,
+      "##p_tac": 138,
+      "##rite": 139,
+      "##write": 140,
+      "##write_tac": 141,
+      "sr": 142,
+      "##bef": 143,
+      "srw_tac": 144,
+      "##before": 145,
+      "gs": 146,
+      "extreal_max": 147,
+      "extreal_max_def": 148,
+      "##e_": 149,
+      "##ec": 150,
+      "##tion": 151,
+      "##pec": 152,
+      "##fi": 153,
+      "##ation": 154,
+      "##cation": 155,
+      "##ifi": 156,
+      "gspec": 157,
+      "##ification": 158,
+      "gspecification": 159,
+      "##before_def": 160,
+      "th": 161,
+      "then": 162,
+      "##ul": 163,
+      "then1": 164,
+      "##ts": 165,
+      "##ven": 166,
+      "##d_s": 167,
+      "st": 168,
+      "##pac": 169,
+      "##d_ss": 170,
+      "std_ss": 171,
+      "##or": 172,
+      "##and": 173,
+      "##pace": 174,
+      "ful": 175,
+      "##l_sim": 176,
+      "full_sim": 177,
+      "full_simp_tac": 178,
+      "##_re": 179,
+      "##ab": 180,
+      "##_rewrite_tac": 181,
+      "##as": 182,
+      "##_space": 183,
+      "##_e": 184,
+      "##s_def": 185,
+      "##ep": 186,
+      "##ets_def": 187,
+      "##orel": 188,
+      "d_and": 189,
+      "d_and_def": 190,
+      "##able": 191,
+      "##vents": 192,
+      "##_space_def": 193,
+      "events": 194,
+      "d_before_def": 195,
+      "d_or": 196,
+      "d_or_def": 197,
+      "re": 198,
+      "##_n": 199,
+      "##ar": 200,
+      "##cl": 201,
+      "in": 202,
+      "##us": 203,
+      "##ur": 204,
+      "##eas": 205,
+      "##clus": 206,
+      "##urable": 207,
+      "##easurable": 208,
+      "##_inclus": 209,
+      "d_sim": 210,
+      "d_inclus": 211,
+      "##ult_def": 212,
+      "##_v": 213,
+      "##ve_": 214,
+      "##ive_": 215,
+      "rewrite_tac": 216,
+      "d_simult_def": 217,
+      "d_inclusive_": 218,
+      "##_var": 219,
+      "d_inclusive_before_def": 220,
+      "##m_rewrite_tac": 221,
+      "as": 222,
+      "mp_tac": 223,
+      "##sion": 224,
+      "exten": 225,
+      "extension": 226,
+      "lb": 227,
+      "measurable": 228,
+      "##um": 229,
+      "##f_n": 230,
+      "##of_n": 231,
+      "extreal_of_n": 232,
+      "##_sets_def": 233,
+      "lborel": 234,
+      "measurable_sets_def": 235,
+      "##um_def": 236,
+      "extreal_of_num_def": 237,
+      "le": 238,
+      "le_": 239,
+      "p_space_def": 240,
+      "q.": 241,
+      "##inite": 242,
+      "le_infty": 243,
+      "le_lt": 244,
+      "##dep": 245,
+      "indep": 246,
+      "indep_var": 247,
+      "##ex": 248,
+      "##ists": 249,
+      "asm_rewrite_tac": 250,
+      "q.ex": 251,
+      "##ists_tac": 252,
+      "q.exists_tac": 253,
+      "dft": 254,
+      "dep": 255,
+      "extreal_real_": 256,
+      "##vent": 257,
+      "##_event": 258,
+      "dep_rewrite_tac": 259,
+      "##ub": 260,
+      "##ter": 261,
+      "borel": 262,
+      "sub": 263,
+      "##sets_def": 264,
+      "##ma": 265,
+      "##_inter": 266,
+      "dft_event": 267,
+      "extreal_real_le": 268,
+      "subsets_def": 269,
+      "finite": 270,
+      "m_space_def": 271,
+      "nor": 272,
+      "##mal_": 273,
+      "##ing": 274,
+      "events_def": 275,
+      "normal_": 276,
+      "##ct": 277,
+      "##om": 278,
+      "##real": 279,
+      "##_sing": 280,
+      "gen": 281,
+      "pr": 282,
+      "##lim": 283,
+      "##hm": 284,
+      "##_thm": 285,
+      "##_elim": 286,
+      "normal_real": 287,
+      "gen_tac": 288,
+      "pro": 289,
+      "##ig": 290,
+      "events_inter": 291,
+      "indep_vars": 292,
+      "et": 293,
+      "se": 294,
+      "sig": 295,
+      "##_c": 296,
+      "##nd": 297,
+      "##ag": 298,
+      "##a_thm": 299,
+      "##lect": 300,
+      "##et_tac": 301,
+      "##imag": 302,
+      "##ot_infty": 303,
+      "##ma_def": 304,
+      "dft_event_def": 305,
+      "finite_sing": 306,
+      "##_elim_tac": 307,
+      "eta_thm": 308,
+      "select": 309,
+      "sigma_def": 310,
+      "select_elim_tac": 311,
+      "eq": 312,
+      "##un": 313,
+      "##_m": 314,
+      "##ve": 315,
+      "prob": 316,
+      "eq_tac": 317,
+      "on": 318,
+      "rand": 319,
+      "space": 320,
+      "und": 321,
+      "##table": 322,
+      "##_before": 323,
+      "##finite": 324,
+      "##ce_": 325,
+      "##oun": 326,
+      "##gt": 327,
+      "##iab": 328,
+      "##reimag": 329,
+      "##ist": 330,
+      "##asm_rewrite_tac": 331,
+      "events_space": 332,
+      "in_m": 333,
+      "##_variab": 334,
+      "lborel_le": 335,
+      "##om_variab": 336,
+      "prob_": 337,
+      "once_": 338,
+      "random_variab": 339,
+      "space_def": 340,
+      "undisch_tac": 341,
+      "##ountable": 342,
+      "in_measurable": 343,
+      "once_asm_rewrite_tac": 344,
+      "random_variable_def": 345,
+      "##so": 346,
+      "##_p": 347,
+      "##_as": 348,
+      "##dd": 349,
+      "##m_s": 350,
+      "extreal_le": 351,
+      "##_eq": 352,
+      "asm_s": 353,
+      "##gt0": 354,
+      "##soc": 355,
+      "##_assoc": 356,
+      "extreal_le_eq": 357,
+      "asm_set_tac": 358,
+      "cd": 359,
+      "mul": 360,
+      "ne": 361,
+      "pi": 362,
+      "preimag": 363,
+      "##ext": 364,
+      "##e_le": 365,
+      "##_gt0": 366,
+      "##f_def": 367,
+      "##not_infty": 368,
+      "##r_def": 369,
+      "##ym": 370,
+      "extreal_mul": 371,
+      "gsym": 372,
+      "##_not_infty": 373,
+      "##omm": 374,
+      "##_countable": 375,
+      "##_comm": 376,
+      "##ver_def": 377,
+      "prob_finite": 378,
+      "cdf_def": 379,
+      "never_def": 380,
+      "pie_le": 381,
+      "extreal_mul_def": 382,
+      "pie_lem": 383,
+      "al": 384,
+      "add": 385,
+      "con": 386,
+      "car": 387,
+      "ps": 388,
+      "##se": 389,
+      "##_and": 390,
+      "##l_d": 391,
+      "##inct": 392,
+      "extreal_not_infty": 393,
+      "##e_ext": 394,
+      "dft_event_and": 395,
+      "prove": 396,
+      "##istinct": 397,
+      "preimage_ext": 398,
+      "pie_lemma": 399,
+      "all_d": 400,
+      "conj": 401,
+      "pset_tac": 402,
+      "dft_event_and_before": 403,
+      "preimage_extreal_": 404,
+      "all_distinct": 405,
+      "and": 406,
+      "countable": 407,
+      "dist": 408,
+      "ima": 409,
+      "me": 410,
+      "not": 411,
+      "po": 412,
+      "rv": 413,
+      "##ution": 414,
+      "##bution": 415,
+      "##ss": 416,
+      "##ty": 417,
+      "##_l": 418,
+      "##_imag": 419,
+      "##pty": 420,
+      "##ai": 421,
+      "##add": 422,
+      "##ose": 423,
+      "##rv": 424,
+      "##ri": 425,
+      "##r_thm": 426,
+      "##ge_": 427,
+      "##mul": 428,
+      "##mpty": 429,
+      "##2rv": 430,
+      "##infty": 431,
+      "##al_ss": 432,
+      "##real_mul": 433,
+      "##real_2rv": 434,
+      "##ispec": 435,
+      "min_comm": 436,
+      "##_empty": 437,
+      "events_countable": 438,
+      "real": 439,
+      "real_ss": 440,
+      "##_ninfty": 441,
+      "in_elim": 442,
+      "q.ispec": 443,
+      "dft_before": 444,
+      "extreal_real_lt": 445,
+      "##_event_gt0": 446,
+      "finite_def": 447,
+      "finite_countable": 448,
+      "normal_real_mul": 449,
+      "##_sing_empty": 450,
+      "##_preimag": 451,
+      "##_pai": 452,
+      "mul_not_infty": 453,
+      "##_gt0_ninfty": 454,
+      "add_assoc": 455,
+      "card": 456,
+      "conj_assoc": 457,
+      "dft_event_and_before_preimag": 458,
+      "preimage_extreal_real_2rv": 459,
+      "and_inter": 460,
+      "countable_imag": 461,
+      "distri": 462,
+      "image_": 463,
+      "mem": 464,
+      "not_sing_empty": 465,
+      "rv_gt0_ninfty": 466,
+      "##bution_def": 467,
+      "##osed": 468,
+      "events_countable_inter": 469,
+      "in_elim_pai": 470,
+      "q.ispecl": 471,
+      "dft_before_event_gt0": 472,
+      "countable_image": 473,
+      "distribution_def": 474,
+      "image_finite": 475,
+      "rv_gt0_ninfty_def": 476,
+      "in_elim_pair_thm": 477
+    }
+  }
+}

training_args.bin

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:44b6f047acbbba00d78e5d1b6224750b5505a5ff60d96b458381bef293b8b769
+size 4283

vocab.txt

@@ -0,0 +1,478 @@
+<s>
+<pad>
+</s>
+<unk>
+<mask>
+.
+0
+1
+2
+3
+5
+6
+_
+a
+b
+c
+d
+e
+f
+g
+h
+i
+j
+l
+m
+n
+o
+p
+q
+r
+s
+t
+u
+v
+w
+x
+y
+##u
+##b
+##s
+##e
+##t
+##_
+##d
+##f
+##v
+##n
+##p
+##a
+##c
+##o
+##r
+##g
+##0
+##l
+##i
+##m
+##h
+##w
+##x
+##2
+##y
+##.
+##j
+##3
+##q
+##5
+##6
+##1
+##_t
+##ac
+##_tac
+##ef
+##_d
+##_def
+##re
+##in
+##al
+##al_
+##xt
+##real_
+ext
+extreal_
+lt
+##w_tac
+##_in
+##ft
+##fty
+##le
+##_infty
+##et
+rw_tac
+##is
+##an
+##_s
+met
+##is_tac
+metis_tac
+##ran
+##_tran
+##_trans
+extreal_m
+##lt
+##ax
+##en
+##lt_def
+##_le
+##te
+##le_def
+##ore
+d_
+lt_le
+lt_infty
+extreal_lt_def
+extreal_le_def
+##on
+##im
+##ot
+##ite
+##ion
+##ch
+##in_def
+##isch
+extreal_min_def
+##isch_tac
+min
+max
+##e_trans
+lte_trans
+max_infty
+let
+##_tot
+lt_tot
+min_infty
+let_trans
+lt_total
+disch_tac
+##_sim
+##p_tac
+##rite
+##write
+##write_tac
+sr
+##bef
+srw_tac
+##before
+gs
+extreal_max
+extreal_max_def
+##e_
+##ec
+##tion
+##pec
+##fi
+##ation
+##cation
+##ifi
+gspec
+##ification
+gspecification
+##before_def
+th
+then
+##ul
+then1
+##ts
+##ven
+##d_s
+st
+##pac
+##d_ss
+std_ss
+##or
+##and
+##pace
+ful
+##l_sim
+full_sim
+full_simp_tac
+##_re
+##ab
+##_rewrite_tac
+##as
+##_space
+##_e
+##s_def
+##ep
+##ets_def
+##orel
+d_and
+d_and_def
+##able
+##vents
+##_space_def
+events
+d_before_def
+d_or
+d_or_def
+re
+##_n
+##ar
+##cl
+in
+##us
+##ur
+##eas
+##clus
+##urable
+##easurable
+##_inclus
+d_sim
+d_inclus
+##ult_def
+##_v
+##ve_
+##ive_
+rewrite_tac
+d_simult_def
+d_inclusive_
+##_var
+d_inclusive_before_def
+##m_rewrite_tac
+as
+mp_tac
+##sion
+exten
+extension
+lb
+measurable
+##um
+##f_n
+##of_n
+extreal_of_n
+##_sets_def
+lborel
+measurable_sets_def
+##um_def
+extreal_of_num_def
+le
+le_
+p_space_def
+q.
+##inite
+le_infty
+le_lt
+##dep
+indep
+indep_var
+##ex
+##ists
+asm_rewrite_tac
+q.ex
+##ists_tac
+q.exists_tac
+dft
+dep
+extreal_real_
+##vent
+##_event
+dep_rewrite_tac
+##ub
+##ter
+borel
+sub
+##sets_def
+##ma
+##_inter
+dft_event
+extreal_real_le
+subsets_def
+finite
+m_space_def
+nor
+##mal_
+##ing
+events_def
+normal_
+##ct
+##om
+##real
+##_sing
+gen
+pr
+##lim
+##hm
+##_thm
+##_elim
+normal_real
+gen_tac
+pro
+##ig
+events_inter
+indep_vars
+et
+se
+sig
+##_c
+##nd
+##ag
+##a_thm
+##lect
+##et_tac
+##imag
+##ot_infty
+##ma_def
+dft_event_def
+finite_sing
+##_elim_tac
+eta_thm
+select
+sigma_def
+select_elim_tac
+eq
+##un
+##_m
+##ve
+prob
+eq_tac
+on
+rand
+space
+und
+##table
+##_before
+##finite
+##ce_
+##oun
+##gt
+##iab
+##reimag
+##ist
+##asm_rewrite_tac
+events_space
+in_m
+##_variab
+lborel_le
+##om_variab
+prob_
+once_
+random_variab
+space_def
+undisch_tac
+##ountable
+in_measurable
+once_asm_rewrite_tac
+random_variable_def
+##so
+##_p
+##_as
+##dd
+##m_s
+extreal_le
+##_eq
+asm_s
+##gt0
+##soc
+##_assoc
+extreal_le_eq
+asm_set_tac
+cd
+mul
+ne
+pi
+preimag
+##ext
+##e_le
+##_gt0
+##f_def
+##not_infty
+##r_def
+##ym
+extreal_mul
+gsym
+##_not_infty
+##omm
+##_countable
+##_comm
+##ver_def
+prob_finite
+cdf_def
+never_def
+pie_le
+extreal_mul_def
+pie_lem
+al
+add
+con
+car
+ps
+##se
+##_and
+##l_d
+##inct
+extreal_not_infty
+##e_ext
+dft_event_and
+prove
+##istinct
+preimage_ext
+pie_lemma
+all_d
+conj
+pset_tac
+dft_event_and_before
+preimage_extreal_
+all_distinct
+and
+countable
+dist
+ima
+me
+not
+po
+rv
+##ution
+##bution
+##ss
+##ty
+##_l
+##_imag
+##pty
+##ai
+##add
+##ose
+##rv
+##ri
+##r_thm
+##ge_
+##mul
+##mpty
+##2rv
+##infty
+##al_ss
+##real_mul
+##real_2rv
+##ispec
+min_comm
+##_empty
+events_countable
+real
+real_ss
+##_ninfty
+in_elim
+q.ispec
+dft_before
+extreal_real_lt
+##_event_gt0
+finite_def
+finite_countable
+normal_real_mul
+##_sing_empty
+##_preimag
+##_pai
+mul_not_infty
+##_gt0_ninfty
+add_assoc
+card
+conj_assoc
+dft_event_and_before_preimag
+preimage_extreal_real_2rv
+and_inter
+countable_imag
+distri
+image_
+mem
+not_sing_empty
+rv_gt0_ninfty
+##bution_def
+##osed
+events_countable_inter
+in_elim_pai
+q.ispecl
+dft_before_event_gt0
+countable_image
+distribution_def
+image_finite
+rv_gt0_ninfty_def
+in_elim_pair_thm