Training in progress, step 500
Browse files- model.safetensors +1 -1
- runs/Jan10_01-30-15_e28f27bc0ed8/events.out.tfevents.1704850216.e28f27bc0ed8.6087.0 +3 -0
- tokenizer.json +64 -64
- training_args.bin +1 -1
- vocab.txt +39 -39
model.safetensors
CHANGED
|
@@ -1,3 +1,3 @@
|
|
| 1 |
version https://git-lfs.github.com/spec/v1
|
| 2 |
-
oid sha256:
|
| 3 |
size 328693404
|
|
|
|
| 1 |
version https://git-lfs.github.com/spec/v1
|
| 2 |
+
oid sha256:632447f0a1072e8c1eeef4f51e8a9d4493df0e4596c34ae998deae08fa59c308
|
| 3 |
size 328693404
|
runs/Jan10_01-30-15_e28f27bc0ed8/events.out.tfevents.1704850216.e28f27bc0ed8.6087.0
ADDED
|
@@ -0,0 +1,3 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
version https://git-lfs.github.com/spec/v1
|
| 2 |
+
oid sha256:1cdf8d843a482a5bfbf0904b4fb7cc036b003b4a25cdf02747742ab5a64d7011
|
| 3 |
+
size 4575
|
tokenizer.json
CHANGED
|
@@ -95,34 +95,34 @@
|
|
| 95 |
"X": 31,
|
| 96 |
"Y": 32,
|
| 97 |
"_": 33,
|
| 98 |
-
"##
|
| 99 |
-
"##
|
| 100 |
-
"##
|
| 101 |
-
"##
|
| 102 |
-
"##
|
| 103 |
"##A": 39,
|
| 104 |
"##C": 40,
|
| 105 |
-
"##
|
| 106 |
-
"##
|
| 107 |
-
"##
|
| 108 |
-
"##
|
| 109 |
-
"##
|
| 110 |
-
"##
|
| 111 |
-
"##
|
| 112 |
-
"##
|
| 113 |
-
"##
|
| 114 |
-
"##
|
| 115 |
-
"##
|
| 116 |
-
"##
|
| 117 |
-
"##
|
| 118 |
-
"##
|
| 119 |
-
"##
|
| 120 |
-
"##
|
| 121 |
-
"##
|
| 122 |
-
"
|
| 123 |
-
"##
|
| 124 |
-
"
|
| 125 |
-
"##
|
| 126 |
"##_T": 62,
|
| 127 |
"##AC": 63,
|
| 128 |
"##_TAC": 64,
|
|
@@ -240,8 +240,8 @@
|
|
| 240 |
"##ID": 176,
|
| 241 |
"DECID": 177,
|
| 242 |
"DECIDE_TAC": 178,
|
| 243 |
-
"##
|
| 244 |
-
"
|
| 245 |
"Q.SPEC": 181,
|
| 246 |
"Q.SPEC_TAC": 182,
|
| 247 |
"ALL_TAC": 183,
|
|
@@ -265,15 +265,15 @@
|
|
| 265 |
"Q.SUBGOAL_THEN": 201,
|
| 266 |
"##CASES_TAC": 202,
|
| 267 |
"HO_MATCH_MP_TAC": 203,
|
| 268 |
-
"##
|
| 269 |
-
"##
|
| 270 |
"##CEPT_TAC": 206,
|
| 271 |
"FR": 207,
|
| 272 |
-
"##
|
| 273 |
-
"##
|
| 274 |
"##UL": 210,
|
| 275 |
-
"##
|
| 276 |
-
"
|
| 277 |
"FRAC_POS_TAC": 213,
|
| 278 |
"##_ASSUM": 214,
|
| 279 |
"RUL": 215,
|
|
@@ -294,9 +294,9 @@
|
|
| 294 |
"HO_MATCH_TAC": 230,
|
| 295 |
"PURE_REWRITE_TAC": 231,
|
| 296 |
"AC": 232,
|
| 297 |
-
"##
|
| 298 |
-
"##
|
| 299 |
-
"##
|
| 300 |
"##RUC": 236,
|
| 301 |
"##ACCEPT_TAC": 237,
|
| 302 |
"ASM_CASES_TAC": 238,
|
|
@@ -308,8 +308,8 @@
|
|
| 308 |
"STRUCT_CASES_TAC": 244,
|
| 309 |
"AP": 245,
|
| 310 |
"NT": 246,
|
| 311 |
-
"##
|
| 312 |
-
"##
|
| 313 |
"##FF": 249,
|
| 314 |
"CASES_TAC": 250,
|
| 315 |
"SUFF": 251,
|
|
@@ -342,43 +342,43 @@
|
|
| 342 |
"MA": 278,
|
| 343 |
"RE": 279,
|
| 344 |
"X_": 280,
|
| 345 |
-
"##
|
| 346 |
-
"##
|
| 347 |
-
"##
|
| 348 |
"##TIS": 284,
|
| 349 |
-
"##
|
| 350 |
-
"##
|
| 351 |
-
"##
|
| 352 |
-
"##
|
| 353 |
-
"##
|
| 354 |
-
"##
|
| 355 |
-
"##
|
| 356 |
-
"##
|
| 357 |
-
"##
|
| 358 |
-
"##
|
| 359 |
-
"##
|
| 360 |
-
"
|
| 361 |
-
"
|
| 362 |
-
"
|
| 363 |
-
"
|
| 364 |
"SUBGOAL": 300,
|
| 365 |
"SUBST_TAC": 301,
|
| 366 |
"IMP_AN": 302,
|
| 367 |
"FIRST_X": 303,
|
| 368 |
"##ERY": 304,
|
| 369 |
"COND_CASES_TAC": 305,
|
| 370 |
-
"
|
| 371 |
"MAP_EV": 307,
|
| 372 |
"REFL": 308,
|
| 373 |
"X_GEN_TAC": 309,
|
| 374 |
"##TISYM_": 310,
|
| 375 |
"##RULE": 311,
|
| 376 |
-
"
|
| 377 |
-
"
|
| 378 |
-
"
|
| 379 |
-
"
|
| 380 |
-
"
|
| 381 |
-
"
|
| 382 |
"MAP_EVERY": 318,
|
| 383 |
"REFL_TAC": 319,
|
| 384 |
"IMP_ANTISYM_RULE": 320
|
|
|
|
| 95 |
"X": 31,
|
| 96 |
"Y": 32,
|
| 97 |
"_": 33,
|
| 98 |
+
"##E": 34,
|
| 99 |
+
"##T": 35,
|
| 100 |
+
"##I": 36,
|
| 101 |
+
"##S": 37,
|
| 102 |
+
"##_": 38,
|
| 103 |
"##A": 39,
|
| 104 |
"##C": 40,
|
| 105 |
+
"##O": 41,
|
| 106 |
+
"##M": 42,
|
| 107 |
+
"##H": 43,
|
| 108 |
+
"##P": 44,
|
| 109 |
+
"##N": 45,
|
| 110 |
+
"##J": 46,
|
| 111 |
+
"##F": 47,
|
| 112 |
+
"##L": 48,
|
| 113 |
+
"##2": 49,
|
| 114 |
+
"##U": 50,
|
| 115 |
+
"##B": 51,
|
| 116 |
+
"##W": 52,
|
| 117 |
+
"##R": 53,
|
| 118 |
+
"##Y": 54,
|
| 119 |
+
"##G": 55,
|
| 120 |
+
"##Q": 56,
|
| 121 |
+
"##D": 57,
|
| 122 |
+
"##.": 58,
|
| 123 |
+
"##X": 59,
|
| 124 |
+
"##1": 60,
|
| 125 |
+
"##V": 61,
|
| 126 |
"##_T": 62,
|
| 127 |
"##AC": 63,
|
| 128 |
"##_TAC": 64,
|
|
|
|
| 240 |
"##ID": 176,
|
| 241 |
"DECID": 177,
|
| 242 |
"DECIDE_TAC": 178,
|
| 243 |
+
"##SP": 179,
|
| 244 |
+
"Q.SP": 180,
|
| 245 |
"Q.SPEC": 181,
|
| 246 |
"Q.SPEC_TAC": 182,
|
| 247 |
"ALL_TAC": 183,
|
|
|
|
| 265 |
"Q.SUBGOAL_THEN": 201,
|
| 266 |
"##CASES_TAC": 202,
|
| 267 |
"HO_MATCH_MP_TAC": 203,
|
| 268 |
+
"##EP": 204,
|
| 269 |
+
"##CEP": 205,
|
| 270 |
"##CEPT_TAC": 206,
|
| 271 |
"FR": 207,
|
| 272 |
+
"##_P": 208,
|
| 273 |
+
"##OS_TAC": 209,
|
| 274 |
"##UL": 210,
|
| 275 |
+
"##AC_P": 211,
|
| 276 |
+
"FRAC_P": 212,
|
| 277 |
"FRAC_POS_TAC": 213,
|
| 278 |
"##_ASSUM": 214,
|
| 279 |
"RUL": 215,
|
|
|
|
| 294 |
"HO_MATCH_TAC": 230,
|
| 295 |
"PURE_REWRITE_TAC": 231,
|
| 296 |
"AC": 232,
|
| 297 |
+
"##ER": 233,
|
| 298 |
+
"##T_ON": 234,
|
| 299 |
+
"##T_CASES_TAC": 235,
|
| 300 |
"##RUC": 236,
|
| 301 |
"##ACCEPT_TAC": 237,
|
| 302 |
"ASM_CASES_TAC": 238,
|
|
|
|
| 308 |
"STRUCT_CASES_TAC": 244,
|
| 309 |
"AP": 245,
|
| 310 |
"NT": 246,
|
| 311 |
+
"##_A": 247,
|
| 312 |
+
"##M_TAC": 248,
|
| 313 |
"##FF": 249,
|
| 314 |
"CASES_TAC": 250,
|
| 315 |
"SUFF": 251,
|
|
|
|
| 342 |
"MA": 278,
|
| 343 |
"RE": 279,
|
| 344 |
"X_": 280,
|
| 345 |
+
"##EQ": 281,
|
| 346 |
+
"##EV": 282,
|
| 347 |
+
"##EV_TAC": 283,
|
| 348 |
"##TIS": 284,
|
| 349 |
+
"##_X": 285,
|
| 350 |
+
"##_EQ": 286,
|
| 351 |
+
"##AN": 287,
|
| 352 |
+
"##PAT": 288,
|
| 353 |
+
"##N_EQ": 289,
|
| 354 |
+
"##FL": 290,
|
| 355 |
+
"##BR": 291,
|
| 356 |
+
"##RUL": 292,
|
| 357 |
+
"##YM_": 293,
|
| 358 |
+
"##GEN_TAC": 294,
|
| 359 |
+
"##P_EV": 295,
|
| 360 |
+
"Q.PAT": 296,
|
| 361 |
+
"DISJ_TAC": 297,
|
| 362 |
+
"FUN_EQ": 298,
|
| 363 |
+
"##_THM": 299,
|
| 364 |
"SUBGOAL": 300,
|
| 365 |
"SUBST_TAC": 301,
|
| 366 |
"IMP_AN": 302,
|
| 367 |
"FIRST_X": 303,
|
| 368 |
"##ERY": 304,
|
| 369 |
"COND_CASES_TAC": 305,
|
| 370 |
+
"ABBR": 306,
|
| 371 |
"MAP_EV": 307,
|
| 372 |
"REFL": 308,
|
| 373 |
"X_GEN_TAC": 309,
|
| 374 |
"##TISYM_": 310,
|
| 375 |
"##RULE": 311,
|
| 376 |
+
"Q.PAT_ASSUM": 312,
|
| 377 |
+
"FUN_EQ_THM": 313,
|
| 378 |
+
"SUBGOAL_TAC": 314,
|
| 379 |
+
"IMP_ANTISYM_": 315,
|
| 380 |
+
"FIRST_X_ASSUM": 316,
|
| 381 |
+
"ABBREV_TAC": 317,
|
| 382 |
"MAP_EVERY": 318,
|
| 383 |
"REFL_TAC": 319,
|
| 384 |
"IMP_ANTISYM_RULE": 320
|
training_args.bin
CHANGED
|
@@ -1,3 +1,3 @@
|
|
| 1 |
version https://git-lfs.github.com/spec/v1
|
| 2 |
-
oid sha256:
|
| 3 |
size 4283
|
|
|
|
| 1 |
version https://git-lfs.github.com/spec/v1
|
| 2 |
+
oid sha256:a3e54757f0a3baa80d1f61d2de060fb50a8609929fe9f38759f5b486814f40f4
|
| 3 |
size 4283
|
vocab.txt
CHANGED
|
@@ -32,34 +32,34 @@ W
|
|
| 32 |
X
|
| 33 |
Y
|
| 34 |
_
|
|
|
|
|
|
|
| 35 |
##I
|
| 36 |
-
##
|
| 37 |
-
##P
|
| 38 |
##_
|
| 39 |
-
##T
|
| 40 |
##A
|
| 41 |
##C
|
| 42 |
-
##E
|
| 43 |
-
##S
|
| 44 |
-
##U
|
| 45 |
-
##F
|
| 46 |
-
##J
|
| 47 |
-
##2
|
| 48 |
##O
|
| 49 |
-
##
|
| 50 |
-
##D
|
| 51 |
-
##R
|
| 52 |
-
##W
|
| 53 |
##H
|
| 54 |
-
##
|
|
|
|
|
|
|
|
|
|
| 55 |
##L
|
|
|
|
|
|
|
| 56 |
##B
|
| 57 |
-
##
|
| 58 |
-
##
|
| 59 |
##Y
|
|
|
|
| 60 |
##Q
|
|
|
|
| 61 |
##.
|
| 62 |
##X
|
|
|
|
|
|
|
| 63 |
##_T
|
| 64 |
##AC
|
| 65 |
##_TAC
|
|
@@ -177,8 +177,8 @@ DEC
|
|
| 177 |
##ID
|
| 178 |
DECID
|
| 179 |
DECIDE_TAC
|
| 180 |
-
##
|
| 181 |
-
|
| 182 |
Q.SPEC
|
| 183 |
Q.SPEC_TAC
|
| 184 |
ALL_TAC
|
|
@@ -202,15 +202,15 @@ PUR
|
|
| 202 |
Q.SUBGOAL_THEN
|
| 203 |
##CASES_TAC
|
| 204 |
HO_MATCH_MP_TAC
|
| 205 |
-
##
|
| 206 |
-
##
|
| 207 |
##CEPT_TAC
|
| 208 |
FR
|
| 209 |
-
##
|
| 210 |
-
##
|
| 211 |
##UL
|
| 212 |
-
##
|
| 213 |
-
|
| 214 |
FRAC_POS_TAC
|
| 215 |
##_ASSUM
|
| 216 |
RUL
|
|
@@ -231,9 +231,9 @@ MATCH_
|
|
| 231 |
HO_MATCH_TAC
|
| 232 |
PURE_REWRITE_TAC
|
| 233 |
AC
|
|
|
|
| 234 |
##T_ON
|
| 235 |
##T_CASES_TAC
|
| 236 |
-
##ER
|
| 237 |
##RUC
|
| 238 |
##ACCEPT_TAC
|
| 239 |
ASM_CASES_TAC
|
|
@@ -245,8 +245,8 @@ ACCEPT_TAC
|
|
| 245 |
STRUCT_CASES_TAC
|
| 246 |
AP
|
| 247 |
NT
|
| 248 |
-
##M_TAC
|
| 249 |
##_A
|
|
|
|
| 250 |
##FF
|
| 251 |
CASES_TAC
|
| 252 |
SUFF
|
|
@@ -279,43 +279,43 @@ AB
|
|
| 279 |
MA
|
| 280 |
RE
|
| 281 |
X_
|
| 282 |
-
##
|
| 283 |
-
##_E
|
| 284 |
-
##_X
|
| 285 |
-
##TIS
|
| 286 |
-
##AN
|
| 287 |
##EV
|
| 288 |
##EV_TAC
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 289 |
##FL
|
| 290 |
-
##
|
| 291 |
##RUL
|
| 292 |
-
##REV_TAC
|
| 293 |
-
##GEN_TAC
|
| 294 |
-
##BREV_TAC
|
| 295 |
##YM_
|
| 296 |
-
##
|
| 297 |
##P_EV
|
| 298 |
Q.PAT
|
| 299 |
DISJ_TAC
|
| 300 |
-
|
|
|
|
| 301 |
SUBGOAL
|
| 302 |
SUBST_TAC
|
| 303 |
IMP_AN
|
| 304 |
FIRST_X
|
| 305 |
##ERY
|
| 306 |
COND_CASES_TAC
|
| 307 |
-
|
| 308 |
MAP_EV
|
| 309 |
REFL
|
| 310 |
X_GEN_TAC
|
| 311 |
##TISYM_
|
| 312 |
##RULE
|
| 313 |
-
##Q_THM
|
| 314 |
Q.PAT_ASSUM
|
| 315 |
FUN_EQ_THM
|
| 316 |
SUBGOAL_TAC
|
| 317 |
IMP_ANTISYM_
|
| 318 |
FIRST_X_ASSUM
|
|
|
|
| 319 |
MAP_EVERY
|
| 320 |
REFL_TAC
|
| 321 |
IMP_ANTISYM_RULE
|
|
|
|
| 32 |
X
|
| 33 |
Y
|
| 34 |
_
|
| 35 |
+
##E
|
| 36 |
+
##T
|
| 37 |
##I
|
| 38 |
+
##S
|
|
|
|
| 39 |
##_
|
|
|
|
| 40 |
##A
|
| 41 |
##C
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 42 |
##O
|
| 43 |
+
##M
|
|
|
|
|
|
|
|
|
|
| 44 |
##H
|
| 45 |
+
##P
|
| 46 |
+
##N
|
| 47 |
+
##J
|
| 48 |
+
##F
|
| 49 |
##L
|
| 50 |
+
##2
|
| 51 |
+
##U
|
| 52 |
##B
|
| 53 |
+
##W
|
| 54 |
+
##R
|
| 55 |
##Y
|
| 56 |
+
##G
|
| 57 |
##Q
|
| 58 |
+
##D
|
| 59 |
##.
|
| 60 |
##X
|
| 61 |
+
##1
|
| 62 |
+
##V
|
| 63 |
##_T
|
| 64 |
##AC
|
| 65 |
##_TAC
|
|
|
|
| 177 |
##ID
|
| 178 |
DECID
|
| 179 |
DECIDE_TAC
|
| 180 |
+
##SP
|
| 181 |
+
Q.SP
|
| 182 |
Q.SPEC
|
| 183 |
Q.SPEC_TAC
|
| 184 |
ALL_TAC
|
|
|
|
| 202 |
Q.SUBGOAL_THEN
|
| 203 |
##CASES_TAC
|
| 204 |
HO_MATCH_MP_TAC
|
| 205 |
+
##EP
|
| 206 |
+
##CEP
|
| 207 |
##CEPT_TAC
|
| 208 |
FR
|
| 209 |
+
##_P
|
| 210 |
+
##OS_TAC
|
| 211 |
##UL
|
| 212 |
+
##AC_P
|
| 213 |
+
FRAC_P
|
| 214 |
FRAC_POS_TAC
|
| 215 |
##_ASSUM
|
| 216 |
RUL
|
|
|
|
| 231 |
HO_MATCH_TAC
|
| 232 |
PURE_REWRITE_TAC
|
| 233 |
AC
|
| 234 |
+
##ER
|
| 235 |
##T_ON
|
| 236 |
##T_CASES_TAC
|
|
|
|
| 237 |
##RUC
|
| 238 |
##ACCEPT_TAC
|
| 239 |
ASM_CASES_TAC
|
|
|
|
| 245 |
STRUCT_CASES_TAC
|
| 246 |
AP
|
| 247 |
NT
|
|
|
|
| 248 |
##_A
|
| 249 |
+
##M_TAC
|
| 250 |
##FF
|
| 251 |
CASES_TAC
|
| 252 |
SUFF
|
|
|
|
| 279 |
MA
|
| 280 |
RE
|
| 281 |
X_
|
| 282 |
+
##EQ
|
|
|
|
|
|
|
|
|
|
|
|
|
| 283 |
##EV
|
| 284 |
##EV_TAC
|
| 285 |
+
##TIS
|
| 286 |
+
##_X
|
| 287 |
+
##_EQ
|
| 288 |
+
##AN
|
| 289 |
+
##PAT
|
| 290 |
+
##N_EQ
|
| 291 |
##FL
|
| 292 |
+
##BR
|
| 293 |
##RUL
|
|
|
|
|
|
|
|
|
|
| 294 |
##YM_
|
| 295 |
+
##GEN_TAC
|
| 296 |
##P_EV
|
| 297 |
Q.PAT
|
| 298 |
DISJ_TAC
|
| 299 |
+
FUN_EQ
|
| 300 |
+
##_THM
|
| 301 |
SUBGOAL
|
| 302 |
SUBST_TAC
|
| 303 |
IMP_AN
|
| 304 |
FIRST_X
|
| 305 |
##ERY
|
| 306 |
COND_CASES_TAC
|
| 307 |
+
ABBR
|
| 308 |
MAP_EV
|
| 309 |
REFL
|
| 310 |
X_GEN_TAC
|
| 311 |
##TISYM_
|
| 312 |
##RULE
|
|
|
|
| 313 |
Q.PAT_ASSUM
|
| 314 |
FUN_EQ_THM
|
| 315 |
SUBGOAL_TAC
|
| 316 |
IMP_ANTISYM_
|
| 317 |
FIRST_X_ASSUM
|
| 318 |
+
ABBREV_TAC
|
| 319 |
MAP_EVERY
|
| 320 |
REFL_TAC
|
| 321 |
IMP_ANTISYM_RULE
|