Training in progress, step 500

model.safetensors

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

runs/Jan08_16-33-07_c156b750c2e0/events.out.tfevents.1704731588.c156b750c2e0.108.0

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

tokenizer.json

@@ -98,38 +98,38 @@
       "w": 34,
       "x": 35,
       "y": 36,
-      "##u": 37,
-      "##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,
-      "##j": 61,
-      "##w": 62,
-      "##1": 63,
-      "##6": 64,
-      "##q": 65,
-      "##0": 66,
-      "##5": 67,
-      "##3": 68,
+      "##x": 37,
+      "##t": 38,
+      "##r": 39,
+      "##e": 40,
+      "##a": 41,
+      "##l": 42,
+      "##_": 43,
+      "##d": 44,
+      "##f": 45,
+      "##v": 46,
+      "##n": 47,
+      "##s": 48,
+      "##m": 49,
+      "##w": 50,
+      "##i": 51,
+      "##c": 52,
+      "##o": 53,
+      "##b": 54,
+      "##p": 55,
+      "##u": 56,
+      "##g": 57,
+      "##2": 58,
+      "##h": 59,
+      "##y": 60,
+      "##.": 61,
+      "##5": 62,
+      "##j": 63,
+      "##1": 64,
+      "##0": 65,
+      "##3": 66,
+      "##6": 67,
+      "##q": 68,
       "##_t": 69,
       "##ac": 70,
       "##_tac": 71,
@@ -199,9 +199,9 @@
       "lt_total": 135,
       "disch_tac": 136,
       "##_sim": 137,
-      "##p_tac": 138,
-      "##rite": 139,
-      "##write": 140,
+      "##rite": 138,
+      "##write": 139,
+      "##p_tac": 140,
       "##write_tac": 141,
       "sr": 142,
       "##bef": 143,
@@ -210,15 +210,15 @@
       "gs": 146,
       "extreal_max": 147,
       "extreal_max_def": 148,
-      "##pe": 149,
-      "##tion": 150,
-      "##e_": 151,
+      "##tion": 149,
+      "##e_": 150,
+      "##ec": 151,
       "##pec": 152,
-      "##ic": 153,
-      "##if": 154,
-      "##ation": 155,
-      "gspec": 156,
-      "##ication": 157,
+      "##ation": 153,
+      "##fi": 154,
+      "##ifi": 155,
+      "##cation": 156,
+      "gspec": 157,
       "##ification": 158,
       "gspecification": 159,
       "##before_def": 160,
@@ -240,14 +240,14 @@
       "##l_sim": 176,
       "full_sim": 177,
       "full_simp_tac": 178,
-      "##_re": 179,
-      "##ab": 180,
+      "##ab": 179,
+      "##_re": 180,
       "##_rewrite_tac": 181,
       "##as": 182,
       "##_space": 183,
       "##_e": 184,
-      "##s_def": 185,
-      "##ep": 186,
+      "##ep": 185,
+      "##s_def": 186,
       "##ets_def": 187,
       "##orel": 188,
       "d_and": 189,
@@ -260,26 +260,26 @@
       "d_or": 196,
       "d_or_def": 197,
       "re": 198,
-      "##_n": 199,
-      "##ar": 200,
+      "##ar": 199,
+      "##_n": 200,
       "##cl": 201,
       "in": 202,
-      "##us": 203,
-      "##ur": 204,
-      "##eas": 205,
-      "##clus": 206,
-      "##urable": 207,
+      "##rable": 203,
+      "##eas": 204,
+      "##us": 205,
+      "##urable": 206,
+      "##clus": 207,
       "##easurable": 208,
       "##_inclus": 209,
       "d_sim": 210,
       "d_inclus": 211,
-      "##ult_def": 212,
-      "##_v": 213,
-      "##iv": 214,
-      "##e_before_def": 215,
+      "##_v": 212,
+      "##ve_": 213,
+      "##ive_": 214,
+      "##ult_def": 215,
       "rewrite_tac": 216,
       "d_simult_def": 217,
-      "d_inclusiv": 218,
+      "d_inclusive_": 218,
       "##_var": 219,
       "d_inclusive_before_def": 220,
       "##m_rewrite_tac": 221,
@@ -290,14 +290,14 @@
       "extension": 226,
       "lb": 227,
       "measurable": 228,
-      "##um": 229,
-      "##of": 230,
-      "extreal_of": 231,
-      "##_sets_def": 232,
-      "##_num": 233,
-      "lborel": 234,
-      "measurable_sets_def": 235,
-      "extreal_of_num": 236,
+      "##f_n": 229,
+      "##m_def": 230,
+      "##of_n": 231,
+      "##um_def": 232,
+      "extreal_of_n": 233,
+      "##_sets_def": 234,
+      "lborel": 235,
+      "measurable_sets_def": 236,
       "extreal_of_num_def": 237,
       "le": 238,
       "le_": 239,
@@ -309,11 +309,11 @@
       "##dep": 245,
       "indep": 246,
       "indep_var": 247,
-      "##ex": 248,
-      "##ists": 249,
-      "asm_rewrite_tac": 250,
-      "q.ex": 251,
-      "##ists_tac": 252,
+      "##xis": 248,
+      "##exis": 249,
+      "##ts_tac": 250,
+      "asm_rewrite_tac": 251,
+      "q.exis": 252,
       "q.exists_tac": 253,
       "dft": 254,
       "dep": 255,
@@ -357,9 +357,9 @@
       "et": 293,
       "se": 294,
       "sig": 295,
-      "##_c": 296,
-      "##ag": 297,
-      "##a_thm": 298,
+      "##ag": 296,
+      "##a_thm": 297,
+      "##_c": 298,
       "##nd": 299,
       "##lect": 300,
       "##et_tac": 301,
@@ -374,21 +374,21 @@
       "sigma_def": 310,
       "select_elim_tac": 311,
       "eq": 312,
-      "##un": 313,
-      "##_m": 314,
-      "##ve": 315,
+      "##_m": 313,
+      "##ve": 314,
+      "##un": 315,
       "prob": 316,
       "eq_tac": 317,
       "on": 318,
       "rand": 319,
       "space": 320,
       "und": 321,
-      "##_before": 322,
-      "##iab": 323,
-      "##table": 324,
-      "##ce_": 325,
-      "##oun": 326,
-      "##finite": 327,
+      "##table": 322,
+      "##_before": 323,
+      "##finite": 324,
+      "##iab": 325,
+      "##ce_": 326,
+      "##oun": 327,
       "##gt": 328,
       "##reimag": 329,
       "##ist": 330,
@@ -409,9 +409,9 @@
       "random_variable_def": 345,
       "##_p": 346,
       "##_as": 347,
-      "##so": 348,
-      "##m_s": 349,
-      "##dd": 350,
+      "##dd": 348,
+      "##so": 349,
+      "##m_s": 350,
       "extreal_le": 351,
       "##_eq": 352,
       "asm_s": 353,
@@ -425,13 +425,13 @@
       "ne": 361,
       "pi": 362,
       "preimag": 363,
-      "##_gt0": 364,
-      "##r_def": 365,
-      "##f_def": 366,
-      "##ext": 367,
-      "##e_le": 368,
-      "##ym": 369,
-      "##not_infty": 370,
+      "##r_def": 364,
+      "##ext": 365,
+      "##e_le": 366,
+      "##_gt0": 367,
+      "##f_def": 368,
+      "##not_infty": 369,
+      "##ym": 370,
       "extreal_mul": 371,
       "gsym": 372,
       "##_not_infty": 373,
@@ -475,28 +475,28 @@
       "not": 411,
       "po": 412,
       "rv": 413,
-      "##ution": 414,
-      "##_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,
+      "##ty": 414,
+      "##rv": 415,
+      "##ri": 416,
+      "##r_thm": 417,
+      "##ai": 418,
+      "##add": 419,
+      "##_l": 420,
+      "##_imag": 421,
+      "##ss": 422,
+      "##mp": 423,
+      "##mul": 424,
+      "##ose": 425,
+      "##bu": 426,
+      "##ge_": 427,
+      "##2rv": 428,
+      "##infty": 429,
+      "##al_ss": 430,
+      "##real_mul": 431,
+      "##real_2rv": 432,
+      "##ispec": 433,
+      "min_comm": 434,
+      "##tion_def": 435,
       "##_emp": 436,
       "events_countable": 437,
       "real": 438,
@@ -512,7 +512,7 @@
       "normal_real_mul": 448,
       "##_sing_emp": 449,
       "##_preimag": 450,
-      "##_pair": 451,
+      "##_pai": 451,
       "mul_not_infty": 452,
       "##_gt0_ninfty": 453,
       "add_assoc": 454,
@@ -522,15 +522,15 @@
       "preimage_extreal_real_2rv": 458,
       "and_inter": 459,
       "countable_imag": 460,
-      "distrib": 461,
+      "distri": 461,
       "image_": 462,
       "mem": 463,
       "not_sing_emp": 464,
       "rv_gt0_ninfty": 465,
-      "##ution_def": 466,
-      "##osed": 467,
+      "##osed": 466,
+      "##bution_def": 467,
       "events_countable_inter": 468,
-      "in_elim_pair": 469,
+      "in_elim_pai": 469,
       "q.ispecl": 470,
       "dft_before_event_gt0": 471,
       "countable_image": 472,

training_args.bin

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:d489df6bad8317b6921b34d38bca438dc1801d66225d7a3a3640b4864b10fddb
+oid sha256:578b7db646b1c5db5a6a20397df1572770ad68c1673c3da073a9e3c3c541807e
 size 4283

vocab.txt

@@ -35,38 +35,38 @@ v
 w
 x
 y
-##u
+##x
+##t
+##r
+##e
+##a
 ##l
 ##_
+##d
+##f
+##v
+##n
 ##s
-##i
 ##m
-##p
-##t
-##a
+##w
+##i
 ##c
-##r
 ##o
 ##b
-##f
-##e
-##x
-##h
-##v
+##p
+##u
 ##g
+##2
+##h
 ##y
 ##.
-##d
-##n
-##2
+##5
 ##j
-##w
 ##1
-##6
-##q
 ##0
-##5
 ##3
+##6
+##q
 ##_t
 ##ac
 ##_tac
@@ -136,9 +136,9 @@ let_trans
 lt_total
 disch_tac
 ##_sim
-##p_tac
 ##rite
 ##write
+##p_tac
 ##write_tac
 sr
 ##bef
@@ -147,15 +147,15 @@ srw_tac
 gs
 extreal_max
 extreal_max_def
-##pe
 ##tion
 ##e_
+##ec
 ##pec
-##ic
-##if
 ##ation
+##fi
+##ifi
+##cation
 gspec
-##ication
 ##ification
 gspecification
 ##before_def
@@ -177,14 +177,14 @@ ful
 ##l_sim
 full_sim
 full_simp_tac
-##_re
 ##ab
+##_re
 ##_rewrite_tac
 ##as
 ##_space
 ##_e
-##s_def
 ##ep
+##s_def
 ##ets_def
 ##orel
 d_and
@@ -197,26 +197,26 @@ d_before_def
 d_or
 d_or_def
 re
-##_n
 ##ar
+##_n
 ##cl
 in
-##us
-##ur
+##rable
 ##eas
-##clus
+##us
 ##urable
+##clus
 ##easurable
 ##_inclus
 d_sim
 d_inclus
-##ult_def
 ##_v
-##iv
-##e_before_def
+##ve_
+##ive_
+##ult_def
 rewrite_tac
 d_simult_def
-d_inclusiv
+d_inclusive_
 ##_var
 d_inclusive_before_def
 ##m_rewrite_tac
@@ -227,14 +227,14 @@ exten
 extension
 lb
 measurable
-##um
-##of
-extreal_of
+##f_n
+##m_def
+##of_n
+##um_def
+extreal_of_n
 ##_sets_def
-##_num
 lborel
 measurable_sets_def
-extreal_of_num
 extreal_of_num_def
 le
 le_
@@ -246,11 +246,11 @@ le_lt
 ##dep
 indep
 indep_var
-##ex
-##ists
+##xis
+##exis
+##ts_tac
 asm_rewrite_tac
-q.ex
-##ists_tac
+q.exis
 q.exists_tac
 dft
 dep
@@ -294,9 +294,9 @@ indep_vars
 et
 se
 sig
-##_c
 ##ag
 ##a_thm
+##_c
 ##nd
 ##lect
 ##et_tac
@@ -311,21 +311,21 @@ select
 sigma_def
 select_elim_tac
 eq
-##un
 ##_m
 ##ve
+##un
 prob
 eq_tac
 on
 rand
 space
 und
+##table
 ##_before
+##finite
 ##iab
-##table
 ##ce_
 ##oun
-##finite
 ##gt
 ##reimag
 ##ist
@@ -346,9 +346,9 @@ once_asm_rewrite_tac
 random_variable_def
 ##_p
 ##_as
+##dd
 ##so
 ##m_s
-##dd
 extreal_le
 ##_eq
 asm_s
@@ -362,13 +362,13 @@ mul
 ne
 pi
 preimag
-##_gt0
 ##r_def
-##f_def
 ##ext
 ##e_le
-##ym
+##_gt0
+##f_def
 ##not_infty
+##ym
 extreal_mul
 gsym
 ##_not_infty
@@ -412,20 +412,19 @@ me
 not
 po
 rv
-##ution
+##ty
+##rv
+##ri
+##r_thm
+##ai
+##add
 ##_l
 ##_imag
 ##ss
-##ir
-##ib
 ##mp
 ##mul
-##ty
-##add
-##air
-##rv
-##rib
 ##ose
+##bu
 ##ge_
 ##2rv
 ##infty
@@ -434,6 +433,7 @@ rv
 ##real_2rv
 ##ispec
 min_comm
+##tion_def
 ##_emp
 events_countable
 real
@@ -449,7 +449,7 @@ finite_countable
 normal_real_mul
 ##_sing_emp
 ##_preimag
-##_pair
+##_pai
 mul_not_infty
 ##_gt0_ninfty
 add_assoc
@@ -459,15 +459,15 @@ dft_event_and_before_preimag
 preimage_extreal_real_2rv
 and_inter
 countable_imag
-distrib
+distri
 image_
 mem
 not_sing_emp
 rv_gt0_ninfty
-##ution_def
 ##osed
+##bution_def
 events_countable_inter
-in_elim_pair
+in_elim_pai
 q.ispecl
 dft_before_event_gt0
 countable_image