|
| 1 | +#!/usr/bin/env julia |
| 2 | +# SPDX-License-Identifier: PMPL-1.0-or-later |
| 3 | +# SPDX-FileCopyrightText: 2026 ECHIDNA Project Team |
| 4 | +# |
| 5 | +# vocabulary_canonicalize.jl — Produce a clean canonical seed vocabulary. |
| 6 | +# |
| 7 | +# vocabulary_UNIFIED.txt and vocabulary_5X.txt are raw-extraction dumps |
| 8 | +# from the proof corpora with no filter — they carry obvious junk (short |
| 9 | +# letter salads like "aabb", pure-repeat runs, concatenated noise) next to |
| 10 | +# real math terms. They are useful as a *survey* of what shows up in |
| 11 | +# proofs, but are NOT suitable as a seed for the training tokenizer: |
| 12 | +# seeding injects tokens that would otherwise be dropped by the |
| 13 | +# min-frequency filter, so any junk in the seed poisons the embedding |
| 14 | +# table. |
| 15 | +# |
| 16 | +# This script builds a curated seed — union of the intentional sources |
| 17 | +# only — and applies a minimal sanity filter: |
| 18 | +# |
| 19 | +# Sources (curated, in merge order): |
| 20 | +# 1. scripts/vocabulary_5x_expansion.jl (prover/math/proof/typechecker) |
| 21 | +# 2. training_data/vocabulary_COMPREHENSIVE.txt |
| 22 | +# 3. training_data/vocabulary_FINAL.txt |
| 23 | +# 4. training_data/vocabulary_ULTIMATE.txt |
| 24 | +# |
| 25 | +# Output: |
| 26 | +# - training_data/vocabulary_CANON.txt |
| 27 | +# - training_data/stats_vocab_canon.json |
| 28 | +# |
| 29 | +# The raw dumps are NOT ingested; frequency-based vocabulary growth |
| 30 | +# happens at training time in src/julia/training/dataloader.jl. |
| 31 | +# |
| 32 | +# Run: julia scripts/vocabulary_canonicalize.jl |
| 33 | + |
| 34 | +using JSON3 |
| 35 | +using Dates |
| 36 | + |
| 37 | +const REPO_ROOT = dirname(dirname(abspath(@__FILE__))) |
| 38 | + |
| 39 | +# Bring curated-set builder functions into scope. The guarded-main change |
| 40 | +# in vocabulary_5x_expansion.jl prevents side effects on include(). |
| 41 | +const _CURATED = joinpath(REPO_ROOT, "scripts", "vocabulary_5x_expansion.jl") |
| 42 | +isfile(_CURATED) && include(_CURATED) |
| 43 | + |
| 44 | +# ── Junk filter ──────────────────────────────────────────────────────────── |
| 45 | + |
| 46 | +""" |
| 47 | + is_valid_token(tok) -> Bool |
| 48 | +
|
| 49 | +Drop tokens that are clearly extraction artefacts. Keep long mathlib-style |
| 50 | +names (they carry real signal) and Unicode math symbols. Reject: |
| 51 | +
|
| 52 | + * Empty or whitespace-only |
| 53 | + * Length < 2 or > 80 |
| 54 | + * Pure digits or pure punctuation |
| 55 | + * Runs of ≥ 4 identical characters anywhere |
| 56 | + * Tokens where > 60 % of characters are a single character |
| 57 | + * Tokens with no letter or non-ASCII math-ish glyph |
| 58 | +
|
| 59 | +The 80-char ceiling is generous: Mathlib names up to ~60 chars exist; past |
| 60 | +80 is almost always concatenated noise. |
| 61 | +""" |
| 62 | +function is_valid_token(tok::AbstractString)::Bool |
| 63 | + s = String(strip(tok)) |
| 64 | + isempty(s) && return false |
| 65 | + chars = collect(s) |
| 66 | + n = length(chars) |
| 67 | + (n < 2 || n > 80) && return false |
| 68 | + |
| 69 | + # Reject pure digits / pure punctuation. |
| 70 | + all(isdigit, chars) && return false |
| 71 | + all(c -> !isletter(c) && !isdigit(c), chars) && return false |
| 72 | + |
| 73 | + # Reject ≥ 3 identical consecutive chars (e.g. "aaa", "---"). Real |
| 74 | + # mathlib identifiers and English/Greek words almost never have a |
| 75 | + # triple-run of the same letter. |
| 76 | + let run = 1, prev = chars[1] |
| 77 | + for c in chars[2:end] |
| 78 | + run = c == prev ? run + 1 : 1 |
| 79 | + run >= 3 && return false |
| 80 | + prev = c |
| 81 | + end |
| 82 | + end |
| 83 | + |
| 84 | + # Reject tokens dominated (> 55 %) by a single character. |
| 85 | + counts = Dict{Char, Int}() |
| 86 | + for c in chars |
| 87 | + counts[c] = get(counts, c, 0) + 1 |
| 88 | + end |
| 89 | + maximum(values(counts)) / n > 0.55 && return false |
| 90 | + |
| 91 | + # Must contain at least one letter (Unicode OK — keeps ∀, λ, ⊥, …). |
| 92 | + any(isletter, chars) || return false |
| 93 | + |
| 94 | + # Latin-alpha vowel density gate. Tokens whose alphabetic content is |
| 95 | + # purely ASCII Latin must have a vowel ratio ≥ 1/6 — this rejects random |
| 96 | + # consonant-runs ("cdbkzuen…") while preserving mathlib names |
| 97 | + # ("cartesianclosedfunctor…") which always carry English roots. |
| 98 | + letters = [c for c in chars if isletter(c)] |
| 99 | + if !isempty(letters) && all(c -> c in 'a':'z' || c in 'A':'Z', letters) |
| 100 | + vowels = count(c -> lowercase(c) in ('a', 'e', 'i', 'o', 'u', 'y'), letters) |
| 101 | + vowels / length(letters) >= (1 / 6) || return false |
| 102 | + # Also reject any run of >=6 consonants. |
| 103 | + let crun = 0 |
| 104 | + for c in letters |
| 105 | + if lowercase(c) in ('a', 'e', 'i', 'o', 'u', 'y') |
| 106 | + crun = 0 |
| 107 | + else |
| 108 | + crun += 1 |
| 109 | + crun >= 6 && return false |
| 110 | + end |
| 111 | + end |
| 112 | + end |
| 113 | + end |
| 114 | + |
| 115 | + return true |
| 116 | +end |
| 117 | + |
| 118 | +# ── Source loading ───────────────────────────────────────────────────────── |
| 119 | + |
| 120 | +function load_if_exists(path::String)::Set{String} |
| 121 | + out = Set{String}() |
| 122 | + isfile(path) || return out |
| 123 | + open(path, "r") do f |
| 124 | + for line in eachline(f) |
| 125 | + tok = strip(line) |
| 126 | + isempty(tok) || push!(out, String(tok)) |
| 127 | + end |
| 128 | + end |
| 129 | + return out |
| 130 | +end |
| 131 | + |
| 132 | +function load_curated_sets()::Set{String} |
| 133 | + isdefined(@__MODULE__, :prover_specific_vocabulary) || return Set{String}() |
| 134 | + return union( |
| 135 | + Base.invokelatest(prover_specific_vocabulary), |
| 136 | + Base.invokelatest(deep_mathematics_vocabulary), |
| 137 | + Base.invokelatest(proof_term_vocabulary), |
| 138 | + Base.invokelatest(typechecker_research_vocabulary), |
| 139 | + ) |
| 140 | +end |
| 141 | + |
| 142 | +# ── Main ─────────────────────────────────────────────────────────────────── |
| 143 | + |
| 144 | +function main() |
| 145 | + println("CANONICAL VOCABULARY BUILD") |
| 146 | + println("=" ^ 60) |
| 147 | + |
| 148 | + td = joinpath(REPO_ROOT, "training_data") |
| 149 | + |
| 150 | + # Curated sources only. Raw-extraction files (5X, UNIFIED) are |
| 151 | + # surveyed separately below for reporting but NOT merged into the |
| 152 | + # seed vocab — they contain too much junk to bypass the freq filter. |
| 153 | + curated = try |
| 154 | + load_curated_sets() |
| 155 | + catch err |
| 156 | + @warn "Curated-set loader failed" err |
| 157 | + Set{String}() |
| 158 | + end |
| 159 | + |
| 160 | + sources = Dict{String, Set{String}}( |
| 161 | + "curated_5x" => curated, |
| 162 | + "COMPREHENSIVE" => load_if_exists(joinpath(td, "vocabulary_COMPREHENSIVE.txt")), |
| 163 | + "FINAL" => load_if_exists(joinpath(td, "vocabulary_FINAL.txt")), |
| 164 | + "ULTIMATE" => load_if_exists(joinpath(td, "vocabulary_ULTIMATE.txt")), |
| 165 | + ) |
| 166 | + |
| 167 | + raw_surveyed = Dict{String, Int}( |
| 168 | + "5X_raw" => length(load_if_exists(joinpath(td, "vocabulary_5X.txt"))), |
| 169 | + "UNIFIED_raw" => length(load_if_exists(joinpath(td, "vocabulary_UNIFIED.txt"))), |
| 170 | + ) |
| 171 | + |
| 172 | + raw_union = Set{String}() |
| 173 | + per_source_raw = Dict{String, Int}() |
| 174 | + for (name, s) in sources |
| 175 | + per_source_raw[name] = length(s) |
| 176 | + union!(raw_union, s) |
| 177 | + end |
| 178 | + println("Sources:") |
| 179 | + for (n, c) in sort(collect(per_source_raw); by = x -> -x[2]) |
| 180 | + println(" $(rpad(n, 14)) → $c tokens") |
| 181 | + end |
| 182 | + println("Raw union total: $(length(raw_union))") |
| 183 | + |
| 184 | + cleaned = Set{String}(t for t in raw_union if is_valid_token(t)) |
| 185 | + dropped = length(raw_union) - length(cleaned) |
| 186 | + println("After filter: $(length(cleaned)) tokens (dropped $dropped)") |
| 187 | + |
| 188 | + per_source_kept = Dict(n => length(Set(t for t in s if is_valid_token(t))) |
| 189 | + for (n, s) in sources) |
| 190 | + |
| 191 | + out_txt = joinpath(td, "vocabulary_CANON.txt") |
| 192 | + open(out_txt, "w") do f |
| 193 | + for tok in sort(collect(cleaned)) |
| 194 | + println(f, tok) |
| 195 | + end |
| 196 | + end |
| 197 | + println("Wrote $out_txt") |
| 198 | + |
| 199 | + stats = Dict{String, Any}( |
| 200 | + "version" => "canon-v1", |
| 201 | + "generated_at" => string(now()), |
| 202 | + "generator" => "scripts/vocabulary_canonicalize.jl", |
| 203 | + "total_tokens" => length(cleaned), |
| 204 | + "raw_union_tokens" => length(raw_union), |
| 205 | + "dropped" => dropped, |
| 206 | + "per_source_raw" => per_source_raw, |
| 207 | + "per_source_kept" => per_source_kept, |
| 208 | + "raw_surveyed_only" => raw_surveyed, |
| 209 | + "filter_rules" => [ |
| 210 | + "2 <= length <= 80", |
| 211 | + "not pure digits / pure punctuation", |
| 212 | + "no run of >=3 identical chars", |
| 213 | + "no single char dominating >55%", |
| 214 | + "must contain at least one letter", |
| 215 | + "ASCII-only tokens: vowel ratio >= 1/6, no >=6 consonant run", |
| 216 | + ], |
| 217 | + "note" => string( |
| 218 | + "CANON is a curated seed. Raw-extraction files (vocabulary_5X.txt, ", |
| 219 | + "vocabulary_UNIFIED.txt) are surveyed but not merged — frequency-based ", |
| 220 | + "vocabulary growth happens at training time in dataloader.jl." |
| 221 | + ), |
| 222 | + ) |
| 223 | + out_json = joinpath(td, "stats_vocab_canon.json") |
| 224 | + open(out_json, "w") do f |
| 225 | + JSON3.pretty(f, stats) |
| 226 | + end |
| 227 | + println("Wrote $out_json") |
| 228 | + |
| 229 | + println("=" ^ 60) |
| 230 | + println("DONE — vocabulary_CANON.txt is the single source of truth.") |
| 231 | +end |
| 232 | + |
| 233 | +main() |
0 commit comments