Skip to content

Commit 6b27847

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(metrics): scaffold eight-axis corpus metrics suite with VeriSim sink
Adds metrics/ — umbrella MetricsSuite.jl plus one module per axis: triangulation_rate, alignment_rate, oov_rate, heaps_beta, tactic_cluster_purity, msc_taxonomy_coverage, prover_floor, zipf_s. All metrics share a single corpus_loader.jl pass over the 21 authoritative proof_states_*.jsonl files. Each metric POSTs a typed row to VeriSimDB at /api/v1/metrics via verisim_sink.jl; if the endpoint is unreachable the row is cached to training_data/metrics_<run_id>.jsonl so the run is recoverable. Smoke-tested end-to-end — sample values on current corpus: triangulation_rate 0.73 % (target 15 %) alignment_rate 2.28 % (target 30 %) oov_rate 47.4 % (target ≤ 3 %) heaps_beta 0.79 (target 0.55–0.70) msc_taxonomy_coverage 65 % (target 40 %) prover_floor 5 (target 5 000) zipf_s 0.71 (target 0.9–1.1) Added `just metrics` recipe. Targets documented in metrics/README.md and the strategy note on Desktop. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent ff9a58a commit 6b27847

14 files changed

Lines changed: 856 additions & 0 deletions

‎Justfile‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,13 @@ vocab-canon:
7474
julia scripts/vocabulary_mine_corpus.jl
7575
julia scripts/vocabulary_canonicalize.jl
7676

77+
# Run the eight-axis metrics suite against the current corpus and post
78+
# results to VeriSimDB. Falls back to training_data/metrics_<run_id>.jsonl
79+
# if VERISIM_URL is unreachable. Target values are documented in
80+
# metrics/README.md.
81+
metrics:
82+
julia --project=src/julia metrics/run_all.jl
83+
7784
# Report corpus balance across provers from stats_UNIFIED.json.
7885
corpus-stats:
7986
@julia -e 'using JSON3, Printf; \

‎metrics/MetricsSuite.jl‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
#
4+
# MetricsSuite.jl — Umbrella module wiring every metric against a
5+
# single corpus pass and a single VeriSimDB sink.
6+
7+
module MetricsSuite
8+
9+
include("corpus_loader.jl")
10+
include("verisim_sink.jl")
11+
12+
using .CorpusLoader: load_corpus, CorpusIndex
13+
14+
include("triangulation_rate.jl")
15+
include("alignment_rate.jl")
16+
include("oov_rate.jl")
17+
include("heaps_beta.jl")
18+
include("tactic_cluster_purity.jl")
19+
include("msc_taxonomy_coverage.jl")
20+
include("prover_floor.jl")
21+
include("zipf_s.jl")
22+
23+
using .VeriSimSink: emit_metric, metric_row
24+
using .TriangulationRate
25+
using .AlignmentRate
26+
using .OOVRate
27+
using .HeapsBeta
28+
using .TacticClusterPurity
29+
using .MSCTaxonomyCoverage
30+
using .ProverFloor
31+
using .ZipfS
32+
33+
export run_metrics, METRIC_MODULES
34+
35+
const METRIC_MODULES = (
36+
TriangulationRate,
37+
AlignmentRate,
38+
OOVRate,
39+
HeapsBeta,
40+
TacticClusterPurity,
41+
MSCTaxonomyCoverage,
42+
ProverFloor,
43+
ZipfS,
44+
)
45+
46+
"""
47+
run_metrics(training_dir, run_id; verisim_url) -> Vector{NamedTuple}
48+
49+
Load the corpus once, run each metric, emit each result to VeriSimDB
50+
(with on-disk fallback). Returns the list of metric rows.
51+
"""
52+
function run_metrics(training_dir::AbstractString,
53+
run_id::AbstractString;
54+
verisim_url::AbstractString = VeriSimSink.DEFAULT_URL)
55+
println("Loading corpus from $training_dir …")
56+
idx = load_corpus(training_dir)
57+
n_rec = sum(length, values(idx); init = 0)
58+
println("Loaded $n_rec records across $(length(idx)) provers.")
59+
results = NamedTuple[]
60+
for M in METRIC_MODULES
61+
t0 = time()
62+
r = M.compute(idx)
63+
dt = round(time() - t0; digits = 2)
64+
println("• $(M.NAME) = $(round(r.value; digits = 4)) ($(r.unit), $(dt)s)")
65+
row = metric_row(run_id, M.NAME, r.value; unit = r.unit, context = r.context)
66+
emit_metric(row; verisim_url = verisim_url)
67+
push!(results, (; metric = M.NAME, r.value, r.unit, r.context))
68+
end
69+
return results
70+
end
71+
72+
end

‎metrics/README.md‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# ECHIDNA metrics suite
2+
3+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
4+
5+
Measures the cross-prover corpus along eight axes that together bound
6+
the vocabulary horizon and triangulation capacity. Every metric
7+
writes its result to VeriSimDB via `POST /api/v1/metrics`; the local
8+
JSONL file is a cache, not the source of truth.
9+
10+
## Axes
11+
12+
| Module | Metric | Target |
13+
|---|---|---|
14+
| `triangulation_rate.jl` | % of theorems proved in ≥3 provers | ≥ 15 % |
15+
| `alignment_rate.jl` | RDF-triples linking named theorems across provers | ≥ 30 % |
16+
| `oov_rate.jl` | tokens in corpus not in CANON | ≤ 3 % |
17+
| `heaps_beta.jl` | β from V ≈ k · N^β | 0.55 – 0.70 |
18+
| `tactic_cluster_purity.jl` | per-prover n-gram distinctiveness | ≥ 0.65 |
19+
| `msc_taxonomy_coverage.jl` | MSC categories with ≥ 10 proofs | ≥ 40 % |
20+
| `prover_floor.jl` | proofs in least-represented prover | ≥ 5 000 |
21+
| `zipf_s.jl` | Zipf slope on theorem-name frequencies | 0.9 – 1.1 |
22+
23+
## Running
24+
25+
```bash
26+
julia --project=src/julia metrics/run_all.jl
27+
```
28+
29+
Environment: `VERISIM_URL` (default `http://localhost:8080`),
30+
`METRIC_RUN_ID` (default `metrics-<timestamp>`).
31+
32+
## Design
33+
34+
- Single loader in `corpus_loader.jl` — reads all `proof_states_*.jsonl`
35+
once per run and hands per-prover slices to each metric.
36+
- Sink in `verisim_sink.jl` POSTs metric rows to VeriSimDB. If the API
37+
is unreachable, the row still lands in
38+
`training_data/metrics_<run_id>.jsonl` so no measurement is lost.
39+
- Targets in the table above come from
40+
`Desktop/ECHIDNA-VERISIM-STRATEGY-2026-04-17.md`.

‎metrics/alignment_rate.jl‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
#
4+
# alignment_rate.jl — Fraction of theorems whose normalised name is
5+
# shared by ≥ 2 provers, weighted by cross-prover-pair count.
6+
#
7+
# Informally: how many RDF sameAs-edges could the VeriSim graph carry
8+
# today? Target ≥ 30 % of theorems appear in at least one alignment.
9+
10+
module AlignmentRate
11+
12+
using ..CorpusLoader: CorpusIndex
13+
using ..TriangulationRate: _norm
14+
15+
export compute, NAME
16+
17+
const NAME = "alignment_rate"
18+
19+
function compute(idx::CorpusIndex)
20+
by_name = Dict{String, Set{String}}()
21+
for (prover, recs) in idx
22+
for r in recs
23+
isempty(r.theorem) && continue
24+
n = _norm(r.theorem)
25+
isempty(n) && continue
26+
push!(get!(by_name, n, Set{String}()), prover)
27+
end
28+
end
29+
30+
total = length(by_name)
31+
aligned_names = 0
32+
pair_edges = 0
33+
for s in values(by_name)
34+
k = length(s)
35+
if k >= 2
36+
aligned_names += 1
37+
pair_edges += (k * (k - 1)) ÷ 2
38+
end
39+
end
40+
41+
value = total == 0 ? 0.0 : aligned_names / total
42+
context = Dict{String, Any}(
43+
"total_unique_names" => total,
44+
"aligned_names" => aligned_names,
45+
"prover_pair_edges" => pair_edges,
46+
"target" => 0.30,
47+
)
48+
return (; value, unit = "fraction", context)
49+
end
50+
51+
end

‎metrics/corpus_loader.jl‎

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
#
4+
# corpus_loader.jl — Single authoritative pass over per-prover JSONL.
5+
#
6+
# All metrics share one in-memory index keyed by prover → Vector{Record}.
7+
# This avoids N× re-reading the 286K-proof corpus across eight metrics.
8+
9+
module CorpusLoader
10+
11+
using JSON3
12+
13+
export load_corpus, CorpusRecord, CorpusIndex, PER_PROVER_FILES
14+
15+
# Same list merge_corpus.jl consumes. Intentionally excludes aggregates.
16+
const PER_PROVER_FILES = [
17+
"proof_states_mathlib4_max.jsonl",
18+
"proof_states_coqgym_max.jsonl",
19+
"proof_states_smtlib.jsonl",
20+
"proof_states_metamath.jsonl",
21+
"proof_states_hol_light.jsonl",
22+
"proof_states_hol4.jsonl",
23+
"proof_states_acl2.jsonl",
24+
"proof_states_pvs.jsonl",
25+
"proof_states_why3.jsonl",
26+
"proof_states_dafny.jsonl",
27+
"proof_states_fstar.jsonl",
28+
"proof_states_idris2.jsonl",
29+
"proof_states_mizar.jsonl",
30+
"proof_states_nuprl.jsonl",
31+
"proof_states_minlog.jsonl",
32+
"proof_states_twelf.jsonl",
33+
"proof_states_imandra.jsonl",
34+
"proof_states_minizinc.jsonl",
35+
"proof_states_afp.jsonl",
36+
"proof_states_agda.jsonl",
37+
"proof_states_typechecker_ecosystem.jsonl",
38+
]
39+
40+
struct CorpusRecord
41+
id::Int
42+
prover::String
43+
theorem::String
44+
goal::String
45+
context::Vector{String}
46+
tactic_proof::String
47+
source::String
48+
end
49+
50+
const CorpusIndex = Dict{String, Vector{CorpusRecord}}
51+
52+
function _string_vec(v)::Vector{String}
53+
v isa AbstractVector || return String[]
54+
out = String[]
55+
for x in v
56+
x isa AbstractString && push!(out, String(x))
57+
end
58+
return out
59+
end
60+
61+
function _coerce(rec::AbstractDict)::CorpusRecord
62+
CorpusRecord(
63+
Int(get(rec, "id", 0)),
64+
String(get(rec, "prover", "unknown")),
65+
String(get(rec, "theorem", "")),
66+
String(get(rec, "goal", "")),
67+
_string_vec(get(rec, "context", String[])),
68+
String(get(rec, "tactic_proof", "")),
69+
String(get(rec, "source", "")),
70+
)
71+
end
72+
73+
"""
74+
load_corpus(training_dir) -> CorpusIndex
75+
76+
Read every authoritative per-prover JSONL under `training_dir`.
77+
Returns a dict mapping prover name → records. Missing files are skipped.
78+
"""
79+
function load_corpus(training_dir::AbstractString)::CorpusIndex
80+
idx = CorpusIndex()
81+
for fname in PER_PROVER_FILES
82+
path = joinpath(training_dir, fname)
83+
isfile(path) || continue
84+
open(path, "r") do fh
85+
for line in eachline(fh)
86+
s = strip(line)
87+
isempty(s) && continue
88+
try
89+
rec = JSON3.read(s, Dict{String,Any})
90+
cr = _coerce(rec)
91+
bucket = get!(idx, cr.prover, CorpusRecord[])
92+
push!(bucket, cr)
93+
catch
94+
end
95+
end
96+
end
97+
end
98+
return idx
99+
end
100+
101+
end

‎metrics/heaps_beta.jl‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
#
4+
# heaps_beta.jl — Fit Heap's law V ≈ k · N^β on the flattened corpus.
5+
# Target β ∈ [0.55, 0.70] for identifier-heavy proof text.
6+
#
7+
# Method: sample token stream in log-spaced checkpoints, count unique
8+
# tokens seen so far, least-squares fit log V vs log N.
9+
10+
module HeapsBeta
11+
12+
using ..CorpusLoader: CorpusIndex
13+
using Statistics
14+
15+
export compute, NAME
16+
17+
const NAME = "heaps_beta"
18+
const SPLIT_RE = r"[\s\(\)\[\]\{\},;:.\"'`]+"
19+
20+
function _flatten(idx::CorpusIndex)
21+
out = String[]
22+
for recs in values(idx), r in recs
23+
for raw in split(string(r.theorem, " ", r.goal, " ", r.tactic_proof,
24+
" ", join(r.context, " ")),
25+
SPLIT_RE; keepempty = false)
26+
t = String(strip(raw))
27+
isempty(t) || push!(out, t)
28+
end
29+
end
30+
return out
31+
end
32+
33+
function _checkpoints(n::Int)::Vector{Int}
34+
n <= 1 && return Int[n]
35+
ks = Int[]
36+
k = 100
37+
while k < n
38+
push!(ks, k)
39+
k = Int(round(k * 1.5))
40+
end
41+
push!(ks, n)
42+
return ks
43+
end
44+
45+
function compute(idx::CorpusIndex)
46+
toks = _flatten(idx)
47+
n = length(toks)
48+
n < 200 && return (; value = 0.0, unit = "beta",
49+
context = Dict{String, Any}("reason" => "too_few_tokens",
50+
"total_tokens" => n))
51+
52+
seen = Set{String}()
53+
xs = Float64[]
54+
ys = Float64[]
55+
ckpts = _checkpoints(n)
56+
ci = 1
57+
for (i, t) in enumerate(toks)
58+
push!(seen, t)
59+
if ci <= length(ckpts) && i == ckpts[ci]
60+
push!(xs, log(i))
61+
push!(ys, log(length(seen)))
62+
ci += 1
63+
end
64+
end
65+
66+
# Least-squares slope of log V ~ β · log N + log k.
67+
mx, my = mean(xs), mean(ys)
68+
num = sum((xs .- mx) .* (ys .- my))
69+
den = sum((xs .- mx) .^ 2)
70+
β = den == 0 ? 0.0 : num / den
71+
log_k = my - β * mx
72+
73+
context = Dict{String, Any}(
74+
"total_tokens" => n,
75+
"unique_tokens" => length(seen),
76+
"k" => exp(log_k),
77+
"checkpoints" => length(xs),
78+
"target_low" => 0.55,
79+
"target_high" => 0.70,
80+
)
81+
return (; value = β, unit = "beta", context)
82+
end
83+
84+
end

0 commit comments

Comments
 (0)