Training in progress, step 500

model.safetensors

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

runs/Jan08_14-24-07_c6d825a30e68/events.out.tfevents.1704723848.c6d825a30e68.42.0

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

tokenizer.json

@@ -99,37 +99,37 @@
       "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,
+      "##l": 38,
+      "##_": 39,
+      "##s": 40,
+      "##i": 41,
+      "##m": 42,
+      "##p": 43,
+      "##t": 44,
+      "##a": 45,
+      "##c": 46,
+      "##r": 47,
+      "##o": 48,
+      "##b": 49,
+      "##f": 50,
+      "##e": 51,
+      "##x": 52,
+      "##h": 53,
+      "##v": 54,
+      "##g": 55,
+      "##y": 56,
+      "##.": 57,
+      "##d": 58,
+      "##n": 59,
       "##2": 60,
-      "##y": 61,
-      "##.": 62,
-      "##j": 63,
-      "##3": 64,
+      "##j": 61,
+      "##w": 62,
+      "##1": 63,
+      "##6": 64,
       "##q": 65,
-      "##5": 66,
-      "##6": 67,
-      "##1": 68,
+      "##0": 66,
+      "##5": 67,
+      "##3": 68,
       "##_t": 69,
       "##ac": 70,
       "##_tac": 71,
@@ -210,15 +210,15 @@
       "gs": 146,
       "extreal_max": 147,
       "extreal_max_def": 148,
-      "##e_": 149,
-      "##ec": 150,
-      "##tion": 151,
+      "##pe": 149,
+      "##tion": 150,
+      "##e_": 151,
       "##pec": 152,
-      "##fi": 153,
-      "##ation": 154,
-      "##cation": 155,
-      "##ifi": 156,
-      "gspec": 157,
+      "##ic": 153,
+      "##if": 154,
+      "##ation": 155,
+      "gspec": 156,
+      "##ication": 157,
       "##ification": 158,
       "gspecification": 159,
       "##before_def": 160,
@@ -275,11 +275,11 @@
       "d_inclus": 211,
       "##ult_def": 212,
       "##_v": 213,
-      "##ve_": 214,
-      "##ive_": 215,
+      "##iv": 214,
+      "##e_before_def": 215,
       "rewrite_tac": 216,
       "d_simult_def": 217,
-      "d_inclusive_": 218,
+      "d_inclusiv": 218,
       "##_var": 219,
       "d_inclusive_before_def": 220,
       "##m_rewrite_tac": 221,
@@ -291,13 +291,13 @@
       "lb": 227,
       "measurable": 228,
       "##um": 229,
-      "##f_n": 230,
-      "##of_n": 231,
-      "extreal_of_n": 232,
-      "##_sets_def": 233,
+      "##of": 230,
+      "extreal_of": 231,
+      "##_sets_def": 232,
+      "##_num": 233,
       "lborel": 234,
       "measurable_sets_def": 235,
-      "##um_def": 236,
+      "extreal_of_num": 236,
       "extreal_of_num_def": 237,
       "le": 238,
       "le_": 239,
@@ -358,9 +358,9 @@
       "se": 294,
       "sig": 295,
       "##_c": 296,
-      "##nd": 297,
-      "##ag": 298,
-      "##a_thm": 299,
+      "##ag": 297,
+      "##a_thm": 298,
+      "##nd": 299,
       "##lect": 300,
       "##et_tac": 301,
       "##imag": 302,
@@ -383,13 +383,13 @@
       "rand": 319,
       "space": 320,
       "und": 321,
-      "##table": 322,
-      "##_before": 323,
-      "##finite": 324,
+      "##_before": 322,
+      "##iab": 323,
+      "##table": 324,
       "##ce_": 325,
       "##oun": 326,
-      "##gt": 327,
-      "##iab": 328,
+      "##finite": 327,
+      "##gt": 328,
       "##reimag": 329,
       "##ist": 330,
       "##asm_rewrite_tac": 331,
@@ -407,31 +407,31 @@
       "in_measurable": 343,
       "once_asm_rewrite_tac": 344,
       "random_variable_def": 345,
-      "##so": 346,
-      "##_p": 347,
-      "##_as": 348,
-      "##dd": 349,
-      "##m_s": 350,
+      "##_p": 346,
+      "##_as": 347,
+      "##so": 348,
+      "##m_s": 349,
+      "##dd": 350,
       "extreal_le": 351,
       "##_eq": 352,
       "asm_s": 353,
       "##gt0": 354,
-      "##soc": 355,
-      "##_assoc": 356,
-      "extreal_le_eq": 357,
-      "asm_set_tac": 358,
+      "##_asso": 355,
+      "extreal_le_eq": 356,
+      "asm_set_tac": 357,
+      "##_assoc": 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,
+      "##_gt0": 364,
+      "##r_def": 365,
+      "##f_def": 366,
+      "##ext": 367,
+      "##e_le": 368,
+      "##ym": 369,
+      "##not_infty": 370,
       "extreal_mul": 371,
       "gsym": 372,
       "##_not_infty": 373,
@@ -450,9 +450,9 @@
       "con": 386,
       "car": 387,
       "ps": 388,
-      "##se": 389,
+      "##l_d": 389,
       "##_and": 390,
-      "##l_d": 391,
+      "##se": 391,
       "##inct": 392,
       "extreal_not_infty": 393,
       "##e_ext": 394,
@@ -476,67 +476,67 @@
       "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,
+      "##_l": 415,
+      "##_imag": 416,
+      "##ss": 417,
+      "##ir": 418,
+      "##ib": 419,
+      "##mp": 420,
+      "##mul": 421,
+      "##ty": 422,
+      "##add": 423,
+      "##air": 424,
+      "##rv": 425,
+      "##rib": 426,
+      "##ose": 427,
+      "##ge_": 428,
+      "##2rv": 429,
+      "##infty": 430,
+      "##al_ss": 431,
+      "##real_mul": 432,
+      "##real_2rv": 433,
+      "##ispec": 434,
+      "min_comm": 435,
+      "##_emp": 436,
+      "events_countable": 437,
+      "real": 438,
+      "real_ss": 439,
+      "##_ninfty": 440,
+      "in_elim": 441,
+      "q.ispec": 442,
+      "dft_before": 443,
+      "extreal_real_lt": 444,
+      "##_event_gt0": 445,
+      "finite_def": 446,
+      "finite_countable": 447,
+      "normal_real_mul": 448,
+      "##_sing_emp": 449,
+      "##_preimag": 450,
+      "##_pair": 451,
+      "mul_not_infty": 452,
+      "##_gt0_ninfty": 453,
+      "add_assoc": 454,
+      "card": 455,
+      "conj_assoc": 456,
+      "dft_event_and_before_preimag": 457,
+      "preimage_extreal_real_2rv": 458,
+      "and_inter": 459,
+      "countable_imag": 460,
+      "distrib": 461,
+      "image_": 462,
+      "mem": 463,
+      "not_sing_emp": 464,
+      "rv_gt0_ninfty": 465,
+      "##ution_def": 466,
+      "##osed": 467,
+      "events_countable_inter": 468,
+      "in_elim_pair": 469,
+      "q.ispecl": 470,
+      "dft_before_event_gt0": 471,
+      "countable_image": 472,
+      "distribution_def": 473,
+      "image_finite": 474,
+      "not_sing_empty": 475,
       "rv_gt0_ninfty_def": 476,
       "in_elim_pair_thm": 477
     }

training_args.bin

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

vocab.txt

@@ -36,37 +36,37 @@ w
 x
 y
 ##u
-##b
-##s
-##e
-##t
+##l
 ##_
-##d
-##f
-##v
-##n
+##s
+##i
+##m
 ##p
+##t
 ##a
 ##c
-##o
 ##r
-##g
-##0
-##l
-##i
-##m
-##h
-##w
+##o
+##b
+##f
+##e
 ##x
-##2
+##h
+##v
+##g
 ##y
 ##.
+##d
+##n
+##2
 ##j
-##3
+##w
+##1
+##6
 ##q
+##0
 ##5
-##6
-##1
+##3
 ##_t
 ##ac
 ##_tac
@@ -147,15 +147,15 @@ srw_tac
 gs
 extreal_max
 extreal_max_def
-##e_
-##ec
+##pe
 ##tion
+##e_
 ##pec
-##fi
+##ic
+##if
 ##ation
-##cation
-##ifi
 gspec
+##ication
 ##ification
 gspecification
 ##before_def
@@ -212,11 +212,11 @@ d_sim
 d_inclus
 ##ult_def
 ##_v
-##ve_
-##ive_
+##iv
+##e_before_def
 rewrite_tac
 d_simult_def
-d_inclusive_
+d_inclusiv
 ##_var
 d_inclusive_before_def
 ##m_rewrite_tac
@@ -228,13 +228,13 @@ extension
 lb
 measurable
 ##um
-##f_n
-##of_n
-extreal_of_n
+##of
+extreal_of
 ##_sets_def
+##_num
 lborel
 measurable_sets_def
-##um_def
+extreal_of_num
 extreal_of_num_def
 le
 le_
@@ -295,9 +295,9 @@ et
 se
 sig
 ##_c
-##nd
 ##ag
 ##a_thm
+##nd
 ##lect
 ##et_tac
 ##imag
@@ -320,13 +320,13 @@ on
 rand
 space
 und
-##table
 ##_before
-##finite
+##iab
+##table
 ##ce_
 ##oun
+##finite
 ##gt
-##iab
 ##reimag
 ##ist
 ##asm_rewrite_tac
@@ -344,31 +344,31 @@ undisch_tac
 in_measurable
 once_asm_rewrite_tac
 random_variable_def
-##so
 ##_p
 ##_as
-##dd
+##so
 ##m_s
+##dd
 extreal_le
 ##_eq
 asm_s
 ##gt0
-##soc
-##_assoc
+##_asso
 extreal_le_eq
 asm_set_tac
+##_assoc
 cd
 mul
 ne
 pi
 preimag
-##ext
-##e_le
 ##_gt0
-##f_def
-##not_infty
 ##r_def
+##f_def
+##ext
+##e_le
 ##ym
+##not_infty
 extreal_mul
 gsym
 ##_not_infty
@@ -387,9 +387,9 @@ add
 con
 car
 ps
-##se
-##_and
 ##l_d
+##_and
+##se
 ##inct
 extreal_not_infty
 ##e_ext
@@ -413,21 +413,20 @@ not
 po
 rv
 ##ution
-##bution
-##ss
-##ty
 ##_l
 ##_imag
-##pty
-##ai
+##ss
+##ir
+##ib
+##mp
+##mul
+##ty
 ##add
-##ose
+##air
 ##rv
-##ri
-##r_thm
+##rib
+##ose
 ##ge_
-##mul
-##mpty
 ##2rv
 ##infty
 ##al_ss
@@ -435,7 +434,7 @@ rv
 ##real_2rv
 ##ispec
 min_comm
-##_empty
+##_emp
 events_countable
 real
 real_ss
@@ -448,9 +447,9 @@ extreal_real_lt
 finite_def
 finite_countable
 normal_real_mul
-##_sing_empty
+##_sing_emp
 ##_preimag
-##_pai
+##_pair
 mul_not_infty
 ##_gt0_ninfty
 add_assoc
@@ -460,19 +459,20 @@ dft_event_and_before_preimag
 preimage_extreal_real_2rv
 and_inter
 countable_imag
-distri
+distrib
 image_
 mem
-not_sing_empty
+not_sing_emp
 rv_gt0_ninfty
-##bution_def
+##ution_def
 ##osed
 events_countable_inter
-in_elim_pai
+in_elim_pair
 q.ispecl
 dft_before_event_gt0
 countable_image
 distribution_def
 image_finite
+not_sing_empty
 rv_gt0_ninfty_def
 in_elim_pair_thm