|
| 1 | +#!/usr/bin/env julia |
| 2 | +# SPDX-License-Identifier: PMPL-1.0-or-later |
| 3 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 4 | +# |
| 5 | +# vocabulary_mine_corpus.jl — Mine proof corpora for a frequency-filtered |
| 6 | +# identifier vocabulary to complement the hand-curated CANON seed. |
| 7 | +# |
| 8 | +# Context |
| 9 | +# ------- |
| 10 | +# vocabulary_UNIFIED.txt is a raw frequency dump that carried junk |
| 11 | +# (sub-trigrams like "aabb", 100-char letter runs). The CANON seed |
| 12 | +# deliberately ignores it. But we still need a way to pick up real |
| 13 | +# identifiers — Mathlib theorem names, Isabelle tactic names, Agda |
| 14 | +# constructor names, TPTP predicates — that *do* appear in the corpus |
| 15 | +# but are missing from the curated lists. |
| 16 | +# |
| 17 | +# Strategy |
| 18 | +# -------- |
| 19 | +# Walk the per-prover authoritative proof_states_*.jsonl files (the |
| 20 | +# same list merge_corpus.jl consumes), tokenise every theorem / goal / |
| 21 | +# context entry, count frequencies, apply the same shared filter as |
| 22 | +# vocabulary_canonicalize.jl, and keep everything with a count at or |
| 23 | +# above `MIN_FREQ`. Frequency is a strong junk filter: random |
| 24 | +# extraction artefacts almost never repeat. |
| 25 | +# |
| 26 | +# Output |
| 27 | +# ------ |
| 28 | +# training_data/vocabulary_mined.txt |
| 29 | +# training_data/stats_vocab_mined.json |
| 30 | +# |
| 31 | +# Downstream: vocabulary_canonicalize.jl folds the mined file into the |
| 32 | +# CANON seed. |
| 33 | +# |
| 34 | +# Run: julia scripts/vocabulary_mine_corpus.jl |
| 35 | + |
| 36 | +using JSON3 |
| 37 | +using Dates |
| 38 | + |
| 39 | +const REPO_ROOT = dirname(dirname(abspath(@__FILE__))) |
| 40 | +const TRAINING_DIR = joinpath(REPO_ROOT, "training_data") |
| 41 | +const OUTPUT_FILE = joinpath(TRAINING_DIR, "vocabulary_mined.txt") |
| 42 | +const STATS_FILE = joinpath(TRAINING_DIR, "stats_vocab_mined.json") |
| 43 | + |
| 44 | +# Share the sanity filter with the canonicalizer. |
| 45 | +include(joinpath(REPO_ROOT, "scripts", "vocabulary_canonicalize.jl")) |
| 46 | +# The canonicalizer auto-runs its main() on include; that is harmless |
| 47 | +# here — it writes the existing CANON, which we'll regenerate downstream. |
| 48 | + |
| 49 | +# Frequency threshold. Tokens that appear at least this many times in |
| 50 | +# the combined corpus graduate into the mined vocabulary. 3 is strict |
| 51 | +# enough to reject extraction noise while admitting domain-specific |
| 52 | +# identifiers that recur across proofs in a family. |
| 53 | +const MIN_FREQ = 3 |
| 54 | + |
| 55 | +# Per-prover authoritative corpus files — mirrors merge_corpus.jl. |
| 56 | +# Aggregate/merged files (UNIFIED, COMPLETE, BALANCED, ULTIMATE, etc.) |
| 57 | +# are excluded deliberately to avoid double-counting. |
| 58 | +const CORPUS_FILES = [ |
| 59 | + "proof_states_mathlib4_max.jsonl", |
| 60 | + "proof_states_coqgym_max.jsonl", |
| 61 | + "proof_states_smtlib.jsonl", |
| 62 | + "proof_states_metamath.jsonl", |
| 63 | + "proof_states_hol_light.jsonl", |
| 64 | + "proof_states_hol4.jsonl", |
| 65 | + "proof_states_acl2.jsonl", |
| 66 | + "proof_states_pvs.jsonl", |
| 67 | + "proof_states_why3.jsonl", |
| 68 | + "proof_states_dafny.jsonl", |
| 69 | + "proof_states_fstar.jsonl", |
| 70 | + "proof_states_idris2.jsonl", |
| 71 | + "proof_states_mizar.jsonl", |
| 72 | + "proof_states_nuprl.jsonl", |
| 73 | + "proof_states_minlog.jsonl", |
| 74 | + "proof_states_twelf.jsonl", |
| 75 | + "proof_states_imandra.jsonl", |
| 76 | + "proof_states_minizinc.jsonl", |
| 77 | + "proof_states_isabelle.jsonl", |
| 78 | + "proof_states_afp.jsonl", |
| 79 | + "proof_states_agda.jsonl", |
| 80 | + "proof_states_tptp.a2ml", |
| 81 | + "proof_states_typechecker_ecosystem.jsonl", |
| 82 | + "proof_states_mathlib4.jsonl", |
| 83 | + "proof_states_coqgym.jsonl", |
| 84 | + "proof_states_2026-03-20.jsonl", |
| 85 | +] |
| 86 | + |
| 87 | +# --------------------------------------------------------------------------- |
| 88 | +# Tokenisation |
| 89 | +# --------------------------------------------------------------------------- |
| 90 | + |
| 91 | +# Same splitter as src/julia/models/encoder.jl:tokenize_text so the mined |
| 92 | +# vocabulary matches what the trainer actually sees. |
| 93 | +const SPLIT_RE = r"[\s\(\)\[\]\{\},;:.\"'`]+" |
| 94 | + |
| 95 | +""" |
| 96 | + tokenise(text) -> Vector{String} |
| 97 | +
|
| 98 | +Split text into candidate tokens. Also splits Agda-style compound |
| 99 | +identifiers on a short set of interior delimiters we care about. |
| 100 | +""" |
| 101 | +function tokenise(text::AbstractString)::Vector{String} |
| 102 | + out = String[] |
| 103 | + for raw in split(text, SPLIT_RE; keepempty = false) |
| 104 | + t = String(strip(raw)) |
| 105 | + isempty(t) || push!(out, t) |
| 106 | + end |
| 107 | + return out |
| 108 | +end |
| 109 | + |
| 110 | +function fold_record!(counts::Dict{String, Int}, rec::AbstractDict) |
| 111 | + for key in ("theorem", "goal", "tactic_proof") |
| 112 | + if haskey(rec, key) && rec[key] isa AbstractString |
| 113 | + for tok in tokenise(rec[key]) |
| 114 | + counts[tok] = get(counts, tok, 0) + 1 |
| 115 | + end |
| 116 | + end |
| 117 | + end |
| 118 | + if haskey(rec, "context") && rec["context"] isa AbstractVector |
| 119 | + for item in rec["context"] |
| 120 | + item isa AbstractString || continue |
| 121 | + for tok in tokenise(item) |
| 122 | + counts[tok] = get(counts, tok, 0) + 1 |
| 123 | + end |
| 124 | + end |
| 125 | + end |
| 126 | +end |
| 127 | + |
| 128 | +# --------------------------------------------------------------------------- |
| 129 | +# Main |
| 130 | +# --------------------------------------------------------------------------- |
| 131 | + |
| 132 | +function mine() |
| 133 | + println("MINE CORPUS VOCABULARY") |
| 134 | + println("=" ^ 60) |
| 135 | + |
| 136 | + counts = Dict{String, Int}() |
| 137 | + files_seen = 0 |
| 138 | + files_miss = 0 |
| 139 | + records_in = 0 |
| 140 | + |
| 141 | + for fname in CORPUS_FILES |
| 142 | + path = joinpath(TRAINING_DIR, fname) |
| 143 | + if !isfile(path) |
| 144 | + files_miss += 1 |
| 145 | + @info "Skipping absent file" file=fname |
| 146 | + continue |
| 147 | + end |
| 148 | + files_seen += 1 |
| 149 | + open(path, "r") do fh |
| 150 | + for line in eachline(fh) |
| 151 | + s = strip(line) |
| 152 | + isempty(s) && continue |
| 153 | + try |
| 154 | + rec = JSON3.read(s, Dict{String,Any}) |
| 155 | + fold_record!(counts, rec) |
| 156 | + records_in += 1 |
| 157 | + catch |
| 158 | + # Non-JSON line (e.g. partial a2ml) — ignore. |
| 159 | + end |
| 160 | + end |
| 161 | + end |
| 162 | + println(" + $(rpad(fname, 44)) running unique=$(length(counts))") |
| 163 | + end |
| 164 | + |
| 165 | + println("Files consumed: $files_seen (missing: $files_miss)") |
| 166 | + println("Records ingested: $records_in") |
| 167 | + println("Raw unique tokens: $(length(counts))") |
| 168 | + |
| 169 | + kept = String[] |
| 170 | + for (tok, c) in counts |
| 171 | + c >= MIN_FREQ || continue |
| 172 | + is_valid_token(tok) || continue |
| 173 | + push!(kept, tok) |
| 174 | + end |
| 175 | + sort!(kept) |
| 176 | + println("After freq>=$MIN_FREQ + filter: $(length(kept)) tokens") |
| 177 | + |
| 178 | + open(OUTPUT_FILE, "w") do fh |
| 179 | + for t in kept |
| 180 | + println(fh, t) |
| 181 | + end |
| 182 | + end |
| 183 | + println("Wrote $OUTPUT_FILE") |
| 184 | + |
| 185 | + stats = Dict{String, Any}( |
| 186 | + "version" => "mined-v1", |
| 187 | + "generated_at" => string(now()), |
| 188 | + "generator" => "scripts/vocabulary_mine_corpus.jl", |
| 189 | + "min_freq" => MIN_FREQ, |
| 190 | + "files_seen" => files_seen, |
| 191 | + "files_missing" => files_miss, |
| 192 | + "records_ingested" => records_in, |
| 193 | + "raw_unique_tokens" => length(counts), |
| 194 | + "kept_tokens" => length(kept), |
| 195 | + ) |
| 196 | + open(STATS_FILE, "w") do fh |
| 197 | + JSON3.pretty(fh, stats) |
| 198 | + end |
| 199 | + println("Wrote $STATS_FILE") |
| 200 | + println("=" ^ 60) |
| 201 | +end |
| 202 | + |
| 203 | +mine() |
0 commit comments