Skip to content

Commit 5a708f5

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(corpus): expand to 138k trainable examples (pkg5a)
Ran extract_afp.jl, extract_agda.jl, extract_hol_light.jl, extract_hol4.jl against the provisioned external_corpora/, then re-merged via scripts/merge_corpus.jl and re-aligned via scripts/align_premises.jl. Trainable set (premise-joined proof_states) grew from ~82k to **138,071**: Lean: 71,267 HOL4: 29,299 HOLLight: 25,908 Coq: 11,353 Agda: 206 Isabelle: 38 Bulk contribution from HOL Light (328,825 new premise records) and HOL4 (139,796 new records); AFP + Agda add proof_state coverage but thin premise signal until their extractors gain deeper parsing. proof_states_UNIFIED.jsonl (703,029 proofs, 39 provers) regenerated by merge_corpus — gitignored; vocabulary_UNIFIED.txt and stats_UNIFIED.json updated to match. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent fe3239b commit 5a708f5

9 files changed

Lines changed: 628599 additions & 272916 deletions

‎training_data/premises_ALIGNED_stats.json‎

Lines changed: 76 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,5 @@
11
{
22
"per_source": {
3-
"premises_isabelle_zf.jsonl": {
4-
"dropped": 0,
5-
"written": 0
6-
},
7-
"premises_nitpick.jsonl": {
8-
"dropped": 0,
9-
"written": 0
10-
},
113
"premises_arend.jsonl": {
124
"dropped": 0,
135
"written": 0
@@ -16,10 +8,6 @@
168
"dropped": 0,
179
"written": 0
1810
},
19-
"premises_proverif.jsonl": {
20-
"dropped": 0,
21-
"written": 0
22-
},
2311
"premises_prism.jsonl": {
2412
"dropped": 0,
2513
"written": 0
@@ -28,122 +16,158 @@
2816
"dropped": 158,
2917
"written": 0
3018
},
31-
"premises_all.jsonl": {
19+
"premises_boogie.jsonl": {
3220
"dropped": 0,
33-
"written": 300
21+
"written": 0
3422
},
35-
"premises_uppaal.jsonl": {
23+
"premises_spin.jsonl": {
3624
"dropped": 0,
3725
"written": 0
3826
},
39-
"premises_boogie.jsonl": {
27+
"premises_framac.jsonl": {
4028
"dropped": 0,
4129
"written": 0
4230
},
43-
"premises_spin.jsonl": {
31+
"premises_key.jsonl": {
4432
"dropped": 0,
4533
"written": 0
4634
},
47-
"premises_framac.jsonl": {
35+
"premises_tlc.jsonl": {
4836
"dropped": 0,
4937
"written": 0
5038
},
51-
"premises_matita.jsonl": {
39+
"premises_naproche.jsonl": {
5240
"dropped": 0,
5341
"written": 0
5442
},
55-
"premises_abc.jsonl": {
43+
"premises_abella.jsonl": {
44+
"dropped": 42,
45+
"written": 0
46+
},
47+
"premises_mathlib4_max.jsonl": {
48+
"dropped": 0,
49+
"written": 2083077
50+
},
51+
"premises_nusmv.jsonl": {
5652
"dropped": 0,
5753
"written": 0
5854
},
59-
"premises_coqgym_max.jsonl": {
55+
"premises_tamarin.jsonl": {
6056
"dropped": 0,
6157
"written": 0
6258
},
63-
"premises_key.jsonl": {
59+
"premises_isabelle_zf.jsonl": {
6460
"dropped": 0,
6561
"written": 0
6662
},
67-
"premises_kissat.jsonl": {
63+
"premises_abc.jsonl": {
6864
"dropped": 0,
6965
"written": 0
7066
},
7167
"premises_coqgym.jsonl": {
7268
"dropped": 0,
7369
"written": 76705
7470
},
75-
"premises_seahorn.jsonl": {
71+
"premises_tlaps.jsonl": {
7672
"dropped": 0,
7773
"written": 0
7874
},
79-
"premises_tlc.jsonl": {
75+
"premises_typed_wasm.jsonl": {
8076
"dropped": 0,
8177
"written": 0
8278
},
83-
"premises_tlaps.jsonl": {
79+
"premises_lambda_prolog.jsonl": {
8480
"dropped": 0,
8581
"written": 0
8682
},
87-
"premises_typed_wasm.jsonl": {
83+
"premises_minisat.jsonl": {
8884
"dropped": 0,
8985
"written": 0
9086
},
91-
"premises_naproche.jsonl": {
87+
"premises_cbmc.jsonl": {
9288
"dropped": 0,
9389
"written": 0
9490
},
95-
"premises_lambda_prolog.jsonl": {
91+
"premises_nunchaku.jsonl": {
9692
"dropped": 0,
9793
"written": 0
9894
},
99-
"premises_minisat.jsonl": {
95+
"premises_viper.jsonl": {
10096
"dropped": 0,
10197
"written": 0
10298
},
103-
"premises_cbmc.jsonl": {
99+
"premises_mathlib4.jsonl": {
100+
"dropped": 1,
101+
"written": 43
102+
},
103+
"premises_athena.jsonl": {
104104
"dropped": 0,
105105
"written": 0
106106
},
107-
"premises_nunchaku.jsonl": {
107+
"premises_hol4.jsonl": {
108+
"dropped": 0,
109+
"written": 139796
110+
},
111+
"premises_agda.jsonl": {
112+
"dropped": 0,
113+
"written": 354
114+
},
115+
"premises_nitpick.jsonl": {
108116
"dropped": 0,
109117
"written": 0
110118
},
111-
"premises_acl2s.jsonl": {
119+
"premises_uppaal.jsonl": {
112120
"dropped": 0,
113121
"written": 0
114122
},
115-
"premises_abella.jsonl": {
116-
"dropped": 42,
123+
"premises_matita.jsonl": {
124+
"dropped": 0,
117125
"written": 0
118126
},
119-
"premises_viper.jsonl": {
127+
"premises_kissat.jsonl": {
120128
"dropped": 0,
121129
"written": 0
122130
},
123-
"premises_mathlib4_max.jsonl": {
131+
"premises_coqgym_max.jsonl": {
124132
"dropped": 0,
125-
"written": 2083077
133+
"written": 0
126134
},
127-
"premises_mathlib4.jsonl": {
135+
"premises_acl2s.jsonl": {
128136
"dropped": 0,
129137
"written": 0
130138
},
131-
"premises_athena.jsonl": {
139+
"premises_afp.jsonl": {
140+
"dropped": 0,
141+
"written": 39
142+
},
143+
"premises_cameleer.jsonl": {
132144
"dropped": 0,
133145
"written": 0
134146
},
135-
"premises_nusmv.jsonl": {
147+
"premises_proverif.jsonl": {
136148
"dropped": 0,
137149
"written": 0
138150
},
139-
"premises_tamarin.jsonl": {
151+
"premises_cadical.jsonl": {
140152
"dropped": 0,
141153
"written": 0
142154
},
143-
"premises_cameleer.jsonl": {
155+
"premises_all.jsonl": {
156+
"dropped": 0,
157+
"written": 300
158+
},
159+
"premises_COMPLETE_pre_align.jsonl": {
160+
"dropped": 0,
161+
"written": 2160082
162+
},
163+
"premises_seahorn.jsonl": {
144164
"dropped": 0,
145165
"written": 0
146166
},
167+
"premises_hol_light.jsonl": {
168+
"dropped": 0,
169+
"written": 328825
170+
},
147171
"premises_mercury.jsonl": {
148172
"dropped": 0,
149173
"written": 0
@@ -152,27 +176,26 @@
152176
"dropped": 10434,
153177
"written": 0
154178
},
155-
"premises_cadical.jsonl": {
156-
"dropped": 0,
157-
"written": 0
158-
},
159179
"premises_alloy.jsonl": {
160180
"dropped": 0,
161181
"written": 0
162182
}
163183
},
164184
"dropped_no_theorem": 10634,
165-
"dropped_no_match": 0,
185+
"dropped_no_match": 1,
166186
"dropped_malformed": 0,
167-
"written": 2160082,
168-
"match_rate_percent": 99.51011555634177,
187+
"written": 4789221,
188+
"match_rate_percent": 99.77843085292558,
169189
"unified_path": "/var/mnt/eclipse/repos/verification-ecosystem/echidna/training_data/proof_states_UNIFIED.jsonl",
170190
"output_path": "/var/mnt/eclipse/repos/verification-ecosystem/echidna/training_data/premises_COMPLETE.jsonl",
171-
"unified_index_size": 871731,
191+
"unified_index_size": 703029,
172192
"sources": [
193+
"premises_COMPLETE_pre_align.jsonl",
173194
"premises_abc.jsonl",
174195
"premises_abella.jsonl",
175196
"premises_acl2s.jsonl",
197+
"premises_afp.jsonl",
198+
"premises_agda.jsonl",
176199
"premises_all.jsonl",
177200
"premises_alloy.jsonl",
178201
"premises_arend.jsonl",
@@ -186,6 +209,8 @@
186209
"premises_dedukti.jsonl",
187210
"premises_dreal.jsonl",
188211
"premises_framac.jsonl",
212+
"premises_hol4.jsonl",
213+
"premises_hol_light.jsonl",
189214
"premises_isabelle_zf.jsonl",
190215
"premises_key.jsonl",
191216
"premises_kissat.jsonl",

‎training_data/premises_afp.jsonl‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
{"prover":"Isabelle","source":"afp","premise":"i","theorem":"index_of_pqueueD3","proof_id":224645}
2+
{"prover":"Isabelle","source":"afp","premise":"impl_model_check","theorem":"impl_model_check_correct","proof_id":229476}
3+
{"prover":"Isabelle","source":"afp","premise":"res","theorem":"fun_evaluate_length","proof_id":231123}
4+
{"prover":"Isabelle","source":"afp","premise":"of","theorem":"in_id_succg_rel_iff","proof_id":234726}
5+
{"prover":"Isabelle","source":"afp","premise":"trace","theorem":"eq_trace_conv","proof_id":237595}
6+
{"prover":"Isabelle","source":"afp","premise":"trace","theorem":"self_conv","proof_id":237596}
7+
{"prover":"Isabelle","source":"afp","premise":"quotient_of","theorem":"farey_fractions_bij","proof_id":245982}
8+
{"prover":"Isabelle","source":"afp","premise":"x","theorem":"ad_agr_map","proof_id":248550}
9+
{"prover":"Isabelle","source":"afp","premise":"not_not","theorem":"fut_terminate","proof_id":253710}
10+
{"prover":"Isabelle","source":"afp","premise":"x","theorem":"map_graph_preserves_restricted","proof_id":256736}
11+
{"prover":"Isabelle","source":"afp","premise":"h","theorem":"frees_tm","proof_id":259916}
12+
{"prover":"Isabelle","source":"afp","premise":"h","theorem":"consts_tm","proof_id":259917}
13+
{"prover":"Isabelle","source":"afp","premise":"h","theorem":"subst_tm","proof_id":259918}
14+
{"prover":"Isabelle","source":"afp","premise":"a","theorem":"case_prod_cong","proof_id":267430}
15+
{"prover":"Isabelle","source":"afp","premise":"b","theorem":"case_prod_cong","proof_id":267430}
16+
{"prover":"Isabelle","source":"afp","premise":"f","theorem":"check_values_neq_NoneI","proof_id":275499}
17+
{"prover":"Isabelle","source":"afp","premise":"right","theorem":"subtract_shifted","proof_id":275693}
18+
{"prover":"Isabelle","source":"afp","premise":"x","theorem":"automation","proof_id":280856}
19+
{"prover":"Isabelle","source":"afp","premise":"x","theorem":"monomial_poly_split","proof_id":287604}
20+
{"prover":"Isabelle","source":"afp","premise":"a b x assume A","theorem":"Pring_smult_l_distr","proof_id":287649}
21+
{"prover":"Isabelle","source":"afp","premise":"a x y m assume A","theorem":"Pring_smult_r_distr","proof_id":287650}
22+
{"prover":"Isabelle","source":"afp","premise":"a b x m assume A","theorem":"Pring_smult_assoc1","proof_id":287651}
23+
{"prover":"Isabelle","source":"afp","premise":"x show","theorem":"coeff_simp","proof_id":287726}
24+
{"prover":"Isabelle","source":"afp","premise":"x","theorem":"trms_of_deg_leq_iter","proof_id":287920}
25+
{"prover":"Isabelle","source":"afp","premise":"of_nat_power","theorem":"solution_of_nat_of_nat","proof_id":289182}
26+
{"prover":"Isabelle","source":"afp","premise":"distinction","theorem":"maintain_S_precise_and_connected","proof_id":292125}
27+
{"prover":"Isabelle","source":"afp","premise":"x","theorem":"rel_prod_simp_asym","proof_id":293182}
28+
{"prover":"Isabelle","source":"afp","premise":"1","theorem":"imp_sim","proof_id":295162}
29+
{"prover":"Isabelle","source":"afp","premise":"1","theorem":"nand_sim","proof_id":295165}
30+
{"prover":"Isabelle","source":"afp","premise":"1","theorem":"HC_contrapos_nn","proof_id":295166}
31+
{"prover":"Isabelle","source":"afp","premise":"1","theorem":"not_imp","proof_id":295169}
32+
{"prover":"Isabelle","source":"afp","premise":"branch_gen","theorem":"get_all_valuations_alt","proof_id":297143}
33+
{"prover":"Isabelle","source":"afp","premise":"nat_of_string","theorem":"inj_show_nat","proof_id":309480}
34+
{"prover":"Isabelle","source":"afp","premise":"int_of_string","theorem":"inj_show_int","proof_id":309481}
35+
{"prover":"Isabelle","source":"afp","premise":"a","theorem":"generalized_sfw_simps","proof_id":310397}
36+
{"prover":"Isabelle","source":"afp","premise":"polC","theorem":"nv2L_simps","proof_id":312136}
37+
{"prover":"Isabelle","source":"afp","premise":"d","theorem":"traverse_tree_simps","proof_id":313563}
38+
{"prover":"Isabelle","source":"afp","premise":"of","theorem":"noreps_singleton","proof_id":316640}
39+
{"prover":"Isabelle","source":"afp","premise":"ti","theorem":"TBOUND_VEBT_case","proof_id":322133}

0 commit comments

Comments
 (0)