fix(pilot): freeze AI labels and enforce auditable execution
This commit is contained in:
@@ -16,16 +16,39 @@ unfaithful formalizations better than a single LLM judge, compile-only, or stati
|
||||
|
||||
## Steps
|
||||
|
||||
cp runs/p85-110/items.jsonl experiments/P0-pilot/data/items.jsonl
|
||||
# Default exports omit source_text. Restore it from the matching private review.
|
||||
python experiments/P0-pilot/prepare_items.py --items runs/p85-110/items.jsonl \
|
||||
--review runs/p85-110/review.json --out experiments/P0-pilot/data/items.jsonl
|
||||
python experiments/P0-pilot/make_sheet.py --items experiments/P0-pilot/data/items.jsonl \
|
||||
--out experiments/P0-pilot/data --key-dir experiments/P0-pilot/labels --seed 7
|
||||
# a person opens data/labelsheet.html, labels all 65 items, downloads labels.json into labels/
|
||||
python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
|
||||
--out experiments/P0-pilot/data/results.jsonl --dry-run
|
||||
python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
|
||||
--out experiments/P0-pilot/data/results.jsonl
|
||||
--out experiments/P0-pilot/data/results.jsonl --labels experiments/P0-pilot/labels/labels.json
|
||||
python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
|
||||
--labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json \
|
||||
--summary experiments/P0-pilot/results/summary.json
|
||||
|
||||
Labeling must be finished before anyone opens `results.jsonl`.
|
||||
|
||||
## Execution safeguards
|
||||
|
||||
- Every item must have a nonempty source passage. `prepare_items.py` restores passages only
|
||||
when all exported fields match the archived review; the exported cohort and Lean code stay intact.
|
||||
- Freeze all labels before the paid run. The owner changed the labeler to the Codex assistant
|
||||
on 2026-10-28. These are **AI labels, not human gold**; see the metadata in `labels/labels.json`.
|
||||
- `--max-calls` counts actual HTTP attempts, including transport and JSON retries, cumulatively
|
||||
across resumes. The hard ceiling is 400. A reservation is saved before each request; an interrupted
|
||||
request may consume a reservation without a known response or token count.
|
||||
- Metadata is stored beside the output as `results.meta.json`. Model, endpoint, temperature,
|
||||
input hash, frozen-label hash and prompt hashes must match on resume. Usage is cumulative.
|
||||
A file lock prevents concurrent writers. A budget stop returns exit status 2.
|
||||
- The nominal successful path uses 130 calls (one source extraction and one judge per item);
|
||||
malformed replies and network retries may increase the actual count.
|
||||
- Scoring requires complete labels and results and no unresolved detector errors. The primary
|
||||
comparison is wrong versus faithful; minor drift is included as positive in the secondary analysis.
|
||||
The complementary-signal PARTIAL rule counts wrong items flagged by role alignment but missed
|
||||
by the judge. No threshold, concept table or detector prompt was tuned for these labels.
|
||||
- Raw passages, labeling HTML and model responses remain in the ignored `data/` directory.
|
||||
Only verdicts, abstract annotation notes, hashes and text-free summaries belong in Git.
|
||||
|
||||
@@ -0,0 +1,427 @@
|
||||
{
|
||||
"labeler": "Codex AI assistant (this chat; exact deployed model identifier unavailable)",
|
||||
"labeler_type": "AI; not human gold",
|
||||
"frozen_at": "2026-10-28T10:42:10.032234+00:00",
|
||||
"items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
|
||||
"key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
|
||||
"method": "Single-pass semantic annotation in shuffled blind-ID order; per-item compiler outcomes and detector outputs hidden. Pure syntax/proof defects are ignored when meaning is recoverable. No compiler/API-name audit. Full extracted-span coverage is assessed; unspecified design tasks or unresolved contextual references are not formalizable.",
|
||||
"limitations": [
|
||||
"Single AI annotator; no human adjudication or inter-annotator agreement.",
|
||||
"The annotator reviewed detector implementation and aggregate compilation counts before labeling; only per-item outputs were hidden.",
|
||||
"AI labels replace the originally planned human/Kimi labels by explicit owner instruction in this chat; the original human-ground-truth protocol is therefore not fully satisfied."
|
||||
],
|
||||
"labels": {
|
||||
"P01": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The field axioms and nontriviality match the stated definition."
|
||||
},
|
||||
"P02": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The whole carrier and identity singleton are the two specified subgroups; API spelling is not assessed."
|
||||
},
|
||||
"P03": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Every integer unit is constrained to the two specified values."
|
||||
},
|
||||
"P04": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Generated subgroup is equated with all integer powers; escaped notation is treated as a syntax defect."
|
||||
},
|
||||
"P05": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Existence of a bijective multiplication-preserving map matches the definition."
|
||||
},
|
||||
"P06": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The theorem statement gives exactly the inverse-of-product identity; proof validity is not assessed."
|
||||
},
|
||||
"P07": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_conclusion",
|
||||
"degenerate"
|
||||
],
|
||||
"notes": "Only already-assumed prime factors are asserted to exist; no recovery from the totient is specified."
|
||||
},
|
||||
"P08": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Both identity preservation and inverse preservation are stated under a multiplicative equivalence."
|
||||
},
|
||||
"P09": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type",
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "The multiplicative ring carrier does not encode the additive cyclic group, and the second extracted exercise is omitted."
|
||||
},
|
||||
"P10": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Both left and right equations have unique solutions."
|
||||
},
|
||||
"P11": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The group cardinality is the exponent, with the correct identity and quantification."
|
||||
},
|
||||
"P12": {
|
||||
"verdict": "not_formalizable",
|
||||
"errors": [
|
||||
"other"
|
||||
],
|
||||
"notes": "The extracted design question provides no formal security or authentication specification for a fidelity comparison."
|
||||
},
|
||||
"P13": {
|
||||
"verdict": "minor_drift",
|
||||
"errors": [
|
||||
"wrong_type"
|
||||
],
|
||||
"notes": "The intended modular identity is retained, but the integer variable is supplied to a natural-number coprimality predicate."
|
||||
},
|
||||
"P14": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "Only existence of a ring structure is stated; the identity and unit characterization are omitted."
|
||||
},
|
||||
"P15": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Unique solvability in both factors expresses the row and column permutation property."
|
||||
},
|
||||
"P16": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Passing to the product representation preserves the order-divisibility claim; capitalization and namespace errors are not semantic changes."
|
||||
},
|
||||
"P17": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "An independent non-field example in the extracted passage is omitted."
|
||||
},
|
||||
"P18": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The norm-one complex carrier and multiplication describe the specified subgroup; bundling/API validity is not assessed."
|
||||
},
|
||||
"P19": {
|
||||
"verdict": "minor_drift",
|
||||
"errors": [
|
||||
"wrong_type"
|
||||
],
|
||||
"notes": "The natural-valued order convention needs an infinite-order convention absent from the cardinality definition."
|
||||
},
|
||||
"P20": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "A single left-identity action on one group element forces equality to the identity."
|
||||
},
|
||||
"P21": {
|
||||
"verdict": "minor_drift",
|
||||
"errors": [
|
||||
"wrong_type"
|
||||
],
|
||||
"notes": "The intended commutativity equivalence is visible, but the left operation lacks the carrier annotation needed to identify G."
|
||||
},
|
||||
"P22": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The two quantified unique-solvability claims express the specified table property."
|
||||
},
|
||||
"P23": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Prime factors, modulus, lcm exponent and coprimality reproduce the extracted claim; no unstated distinctness assumption is introduced."
|
||||
},
|
||||
"P24": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_conclusion",
|
||||
"degenerate"
|
||||
],
|
||||
"notes": "An arbitrary group satisfying an order condition is not identified with the geometric symmetry group."
|
||||
},
|
||||
"P25": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The two declarations cover both cancellation directions."
|
||||
},
|
||||
"P26": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"extra_hypothesis",
|
||||
"missing_hypothesis"
|
||||
],
|
||||
"notes": "The inserted divisibility assumption does not express the RSA relationship required by the argument."
|
||||
},
|
||||
"P27": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "The isomorphism is asserted for a quotient of the ambient group instead of the stabilizer subgroup."
|
||||
},
|
||||
"P28": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type",
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "Natural exponent division fails to express a square root, and the homomorphism target does not encode the specified automorphism."
|
||||
},
|
||||
"P29": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "A bijective homomorphism supplies the isomorphism assumption and both power assertions are retained."
|
||||
},
|
||||
"P30": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type"
|
||||
],
|
||||
"notes": "An unordered finite product is used for an arbitrary semigroup, losing the ordered nonempty product required by the exercise."
|
||||
},
|
||||
"P31": {
|
||||
"verdict": "not_formalizable",
|
||||
"errors": [
|
||||
"other"
|
||||
],
|
||||
"notes": "The isolated instruction refers to an earlier map whose definition is absent; the actual proposition cannot be recovered from this span."
|
||||
},
|
||||
"P32": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_conclusion",
|
||||
"degenerate"
|
||||
],
|
||||
"notes": "The result merely supplies an unspecified ring homomorphism and does not constrain it to evaluation at the matrix parameter."
|
||||
},
|
||||
"P33": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The cardinality assumption and the nonidentity involution conclusion match; the missing instance binder is a compilation defect."
|
||||
},
|
||||
"P34": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The contrasting abelian properties encode the reason these specified groups are not isomorphic."
|
||||
},
|
||||
"P35": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type",
|
||||
"quantifier"
|
||||
],
|
||||
"notes": "One fixed-arity function is applied at incompatible arities instead of specifying a coherent family of products."
|
||||
},
|
||||
"P36": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type",
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "The ring carrier replaces the concrete root-of-unity group, and neither its order nor the specified generator is stated."
|
||||
},
|
||||
"P37": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"degenerate",
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "The declaration has no defining expression for the requested subgroup."
|
||||
},
|
||||
"P38": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"missing_hypothesis"
|
||||
],
|
||||
"notes": "Nonemptiness is missing, so the empty subset satisfies both closure assumptions."
|
||||
},
|
||||
"P39": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type",
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "Laurent series replace finite Laurent polynomials, and the requested units are not characterized."
|
||||
},
|
||||
"P40": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The supplied structure body fixes the function to the canonical integer residue map."
|
||||
},
|
||||
"P41": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"extra_hypothesis"
|
||||
],
|
||||
"notes": "The cardinality assertion is restricted to the range where noncommutativity holds, dropping the smaller symmetric groups."
|
||||
},
|
||||
"P42": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"missing_hypothesis",
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "A necessary closure condition is promoted to sufficiency without inverse closure."
|
||||
},
|
||||
"P43": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Any two groups of the specified size are related by a multiplicative equivalence."
|
||||
},
|
||||
"P44": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The defining field is exactly commutativity of the group operation."
|
||||
},
|
||||
"P45": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"quantifier",
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "Literal uniqueness of a carrier/structure replaces uniqueness up to group isomorphism."
|
||||
},
|
||||
"P46": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type",
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "Univariate polynomials over a product ring replace three-variable real polynomials; the units question is omitted."
|
||||
},
|
||||
"P47": {
|
||||
"verdict": "minor_drift",
|
||||
"errors": [
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "The integer-span equality captures the generated set, but the equality for opposite generators is not explicitly stated."
|
||||
},
|
||||
"P48": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The one-sided inverse hypothesis gives the specified inverse element."
|
||||
},
|
||||
"P49": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The theorem statement is exactly involutivity of group inversion."
|
||||
},
|
||||
"P50": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The custom structure supplies additive commutative group, associative multiplication and both distributive laws without imposing a unit."
|
||||
},
|
||||
"P51": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The carrier, multiplication and identity encode the specified finite group; existence of the chosen API is not audited."
|
||||
},
|
||||
"P52": {
|
||||
"verdict": "minor_drift",
|
||||
"errors": [
|
||||
"wrong_conclusion",
|
||||
"degenerate"
|
||||
],
|
||||
"notes": "Ring structure and unit-to-constant direction are present, but identity characterization is replaced by reflexivity."
|
||||
},
|
||||
"P53": {
|
||||
"verdict": "minor_drift",
|
||||
"errors": [
|
||||
"extra_hypothesis"
|
||||
],
|
||||
"notes": "Cardinality is represented only for finite groups although the definition is not restricted to them."
|
||||
},
|
||||
"P54": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type"
|
||||
],
|
||||
"notes": "Multiplicative subgroup closure of a residue is used in place of the additive cyclic subgroup generated by it."
|
||||
},
|
||||
"P55": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The abelian-property equivalence is stated under an isomorphism."
|
||||
},
|
||||
"P56": {
|
||||
"verdict": "not_formalizable",
|
||||
"errors": [
|
||||
"other"
|
||||
],
|
||||
"notes": "The design question does not specify an authenticity predicate or formal adversarial model."
|
||||
},
|
||||
"P57": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_conclusion"
|
||||
],
|
||||
"notes": "The homomorphism criterion is retained but the separate isomorphism definition is absent."
|
||||
},
|
||||
"P58": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type"
|
||||
],
|
||||
"notes": "A multiplicative equivalence on the full residue ring does not represent the additive cyclic group in the comparison."
|
||||
},
|
||||
"P59": {
|
||||
"verdict": "minor_drift",
|
||||
"errors": [
|
||||
"wrong_type"
|
||||
],
|
||||
"notes": "The inherited-group criterion is recognizable, but operations on the subset are not specified as restricted operations."
|
||||
},
|
||||
"P60": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_type",
|
||||
"missing_hypothesis"
|
||||
],
|
||||
"notes": "Global bijections with local differentiability conditions do not specify self-diffeomorphisms of the open subset."
|
||||
},
|
||||
"P61": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "The homeomorphism type supplies the intended carrier and group structure under composition; notation validity is not assessed."
|
||||
},
|
||||
"P62": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Both least-positive exponent and the bounded-power description are retained, ignoring set-minimum API syntax."
|
||||
},
|
||||
"P63": {
|
||||
"verdict": "faithful",
|
||||
"errors": [],
|
||||
"notes": "Both two-sided identity hypotheses and their equality are stated."
|
||||
},
|
||||
"P64": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"missing_hypothesis",
|
||||
"extra_hypothesis"
|
||||
],
|
||||
"notes": "The exponent relation uses the ciphertext modulus where the RSA exponent modulus is required."
|
||||
},
|
||||
"P65": {
|
||||
"verdict": "wrong",
|
||||
"errors": [
|
||||
"wrong_conclusion",
|
||||
"degenerate"
|
||||
],
|
||||
"notes": "The arbitrary finite group is unrelated to the requested geometric symmetries, with the classification left in a comment."
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -154,6 +154,10 @@ def main() -> int:
|
||||
|
||||
items = [json.loads(line) for line in args.items.read_text(encoding="utf-8").splitlines()
|
||||
if line.strip()]
|
||||
if not items or any(not item.get("source_text", "").strip() for item in items):
|
||||
parser.error("Every item needs nonempty source_text; use a private source-inclusive export.")
|
||||
if len({item["id"] for item in items}) != len(items):
|
||||
parser.error("Item IDs must be unique.")
|
||||
order = list(range(len(items)))
|
||||
random.Random(args.seed).shuffle(order)
|
||||
blind_ids = [f"P{n:02d}" for n in range(1, len(items) + 1)]
|
||||
|
||||
@@ -0,0 +1,45 @@
|
||||
"""Restore source passages from a private archived review without changing the cohort."""
|
||||
from __future__ import annotations
|
||||
|
||||
import argparse
|
||||
import json
|
||||
from pathlib import Path
|
||||
|
||||
|
||||
def restore(items: list[dict], review: dict) -> list[dict]:
|
||||
archived = review["items"]
|
||||
by_id = {row["id"]: row for row in archived}
|
||||
if len(by_id) != len(archived) or len({row["id"] for row in items}) != len(items):
|
||||
raise ValueError("Duplicate item IDs")
|
||||
restored = []
|
||||
for item in items:
|
||||
original = by_id[item["id"]]
|
||||
comparable = dict(original)
|
||||
if isinstance(comparable.get("imports"), str):
|
||||
comparable["imports"] = json.loads(comparable["imports"])
|
||||
if any(comparable.get(k) != v for k, v in item.items()):
|
||||
raise ValueError(f"Archived review does not match item {item['id']}")
|
||||
passage = original.get("source_text", "")
|
||||
if not passage.strip():
|
||||
raise ValueError(f"Missing archived passage for {item['id']}")
|
||||
restored.append({**item, "source_text": passage})
|
||||
return restored
|
||||
|
||||
|
||||
def main() -> None:
|
||||
parser = argparse.ArgumentParser(description=__doc__)
|
||||
parser.add_argument("--items", required=True, type=Path)
|
||||
parser.add_argument("--review", required=True, type=Path)
|
||||
parser.add_argument("--out", required=True, type=Path)
|
||||
args = parser.parse_args()
|
||||
if args.out.parent.name != "data":
|
||||
parser.error("Source-inclusive output must go in a gitignored data/ directory")
|
||||
items = [json.loads(line) for line in args.items.read_text().splitlines() if line.strip()]
|
||||
rows = restore(items, json.loads(args.review.read_text()))
|
||||
args.out.parent.mkdir(parents=True, exist_ok=True)
|
||||
args.out.write_text("".join(json.dumps(row, ensure_ascii=False) + "\n" for row in rows))
|
||||
print(f"Restored {len(rows)} passages; all exported fields are unchanged")
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
@@ -15,8 +15,11 @@ Hard stops: --max-calls bounds API calls; a rerun skips items already in --out.
|
||||
from __future__ import annotations
|
||||
|
||||
import argparse
|
||||
import fcntl
|
||||
import hashlib
|
||||
import inspect
|
||||
import json
|
||||
import os
|
||||
import sys
|
||||
from pathlib import Path
|
||||
|
||||
@@ -24,7 +27,7 @@ from leanbench import srcsimplex
|
||||
from leanbench.align import align
|
||||
from leanbench.config import Settings
|
||||
from leanbench.lint import lint
|
||||
from leanbench.llm import OpenAICompatibleClient
|
||||
from leanbench.llm import OpenAICompatibleClient, Usage
|
||||
from leanbench.project import project
|
||||
|
||||
JUDGE_PROMPT_VERSION = "judge-v1"
|
||||
@@ -41,13 +44,15 @@ def judge(client, passage: str, lean: str) -> dict:
|
||||
{"role": "system", "content": JUDGE_SYSTEM},
|
||||
{"role": "user", "content": f"Passage:\n{passage}\n\nLean:\n{lean}"},
|
||||
])
|
||||
if not isinstance(reply, dict) or "faithful" not in reply:
|
||||
if not isinstance(reply, dict) or type(reply.get("faithful")) is not bool:
|
||||
raise ValueError(f"unusable judge reply: {str(reply)[:200]}")
|
||||
return {"faithful": bool(reply["faithful"]), "confidence": reply.get("confidence"),
|
||||
return {"faithful": reply["faithful"], "confidence": reply.get("confidence"),
|
||||
"reason": str(reply.get("reason", ""))[:300]}
|
||||
|
||||
|
||||
def run_item(client, item: dict) -> dict:
|
||||
if not item.get("source_text", "").strip():
|
||||
raise ValueError("Missing source_text; use a private source-inclusive export")
|
||||
code = item.get("lean_code") or ""
|
||||
row: dict = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}}
|
||||
proj = project(code)
|
||||
@@ -59,51 +64,154 @@ def run_item(client, item: dict) -> dict:
|
||||
al = align(src, proj)
|
||||
row["source"] = [r.__dict__ for r in src.roles]
|
||||
row["role"] = al.as_dict()
|
||||
except CallBudgetExceeded:
|
||||
raise
|
||||
except Exception as error: # a failed extraction is data, not a crash
|
||||
row["errors"]["role"] = str(error)[:300]
|
||||
try:
|
||||
row["judge"] = judge(client, item.get("source_text", ""), code)
|
||||
except CallBudgetExceeded:
|
||||
raise
|
||||
except Exception as error:
|
||||
row["errors"]["judge"] = str(error)[:300]
|
||||
return row
|
||||
|
||||
|
||||
class CallBudgetExceeded(RuntimeError):
|
||||
"""Stop before issuing a request that would exceed the cumulative budget."""
|
||||
|
||||
|
||||
def digest(path: Path) -> str:
|
||||
return hashlib.sha256(path.read_bytes()).hexdigest()
|
||||
|
||||
|
||||
def atomic_json(path: Path, value: dict) -> None:
|
||||
temporary = path.with_suffix(path.suffix + ".tmp")
|
||||
temporary.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n", encoding="utf-8")
|
||||
os.replace(temporary, path)
|
||||
|
||||
|
||||
class AuditedClient(OpenAICompatibleClient):
|
||||
"""Persist reservations before HTTP requests, including transport and JSON retries."""
|
||||
|
||||
def complete(self, *args, **kwargs):
|
||||
try:
|
||||
return super().complete(*args, **kwargs)
|
||||
finally:
|
||||
self.checkpoint()
|
||||
|
||||
|
||||
def execute(args, items, settings) -> int:
|
||||
rows = []
|
||||
if args.out.exists():
|
||||
rows = [json.loads(x) for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()]
|
||||
ids = {item["id"] for item in items}
|
||||
done = {row["id"] for row in rows}
|
||||
if len(done) != len(rows) or not done <= ids:
|
||||
raise ValueError("Results have duplicate or unknown item IDs")
|
||||
hashes = {
|
||||
"source": hashlib.sha256((srcsimplex.SYSTEM_PROMPT + inspect.getsource(srcsimplex.passage_prompt)).encode()).hexdigest(),
|
||||
"judge": hashlib.sha256(JUDGE_SYSTEM.encode()).hexdigest(),
|
||||
}
|
||||
identity = {"model": settings.llm.model, "base_url": settings.llm.base_url,
|
||||
"temperature": settings.llm.temperature, "items_sha256": digest(args.items),
|
||||
"prompt_hashes": hashes,
|
||||
"prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
|
||||
labels = getattr(args, "labels", None)
|
||||
if labels is not None:
|
||||
identity["labels_sha256"] = digest(labels)
|
||||
meta_path = args.out.with_suffix(".meta.json")
|
||||
meta = {**identity, "request_attempts": 0, "usage": Usage().as_dict(), "status": "ready"}
|
||||
if meta_path.exists():
|
||||
meta = json.loads(meta_path.read_text(encoding="utf-8"))
|
||||
if any(meta.get(k) != v for k, v in identity.items()):
|
||||
raise ValueError("Run identity changed; use a new output path instead of mixing runs")
|
||||
elif rows:
|
||||
raise ValueError("Cannot resume results without their audit metadata")
|
||||
todo = [item for item in items if item["id"] not in done]
|
||||
print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
|
||||
f"nominal_calls={len(todo) * 2} request_attempts={meta['request_attempts']} cap={args.max_calls}")
|
||||
print("prompt_hashes:", json.dumps(hashes))
|
||||
if args.dry_run:
|
||||
return 0
|
||||
if settings.llm.model != "qwen-max" or settings.llm.temperature != 0:
|
||||
raise ValueError("P0 is preregistered for qwen-max at temperature 0")
|
||||
client = AuditedClient.from_settings(settings.llm)
|
||||
client.usage = Usage(**meta["usage"])
|
||||
|
||||
def checkpoint():
|
||||
meta["usage"] = client.usage.as_dict()
|
||||
meta["completed_items"] = len(done)
|
||||
atomic_json(meta_path, meta)
|
||||
|
||||
def reserve():
|
||||
if meta["request_attempts"] >= args.max_calls:
|
||||
raise CallBudgetExceeded("Cumulative request cap reached; no further HTTP request was sent")
|
||||
meta["request_attempts"] += 1
|
||||
checkpoint()
|
||||
|
||||
client.checkpoint = checkpoint
|
||||
client.request_guard = reserve
|
||||
meta["max_calls"] = args.max_calls
|
||||
meta["status"] = "running"
|
||||
checkpoint()
|
||||
try:
|
||||
with args.out.open("a", encoding="utf-8") as stream:
|
||||
for item in todo:
|
||||
row = run_item(client, item)
|
||||
stream.write(json.dumps(row, ensure_ascii=False) + "\n")
|
||||
stream.flush()
|
||||
os.fsync(stream.fileno())
|
||||
done.add(item["id"])
|
||||
checkpoint()
|
||||
print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True)
|
||||
meta["status"] = "complete"
|
||||
except CallBudgetExceeded as error:
|
||||
meta["status"] = "budget_exhausted"
|
||||
print(str(error), file=sys.stderr)
|
||||
except BaseException:
|
||||
meta["status"] = "interrupted"
|
||||
raise
|
||||
finally:
|
||||
if args.out.exists():
|
||||
meta["results_sha256"] = digest(args.out)
|
||||
checkpoint()
|
||||
print(json.dumps(meta))
|
||||
return 0 if meta["status"] == "complete" else 2
|
||||
|
||||
|
||||
def main() -> int:
|
||||
ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
|
||||
ap.add_argument("--items", required=True, type=Path)
|
||||
ap.add_argument("--out", required=True, type=Path)
|
||||
ap.add_argument("--max-calls", type=int, default=400)
|
||||
ap.add_argument("--dry-run", action="store_true")
|
||||
ap.add_argument("--labels", type=Path, help="Frozen labels; their hash is bound to the run")
|
||||
args = ap.parse_args()
|
||||
|
||||
if not 1 <= args.max_calls <= 400:
|
||||
ap.error("P0 requires a request cap between 1 and 400")
|
||||
items = [json.loads(x) for x in args.items.read_text(encoding="utf-8").splitlines() if x.strip()]
|
||||
done = set()
|
||||
if args.out.exists():
|
||||
done = {json.loads(x)["id"] for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()}
|
||||
todo = [i for i in items if i["id"] not in done]
|
||||
settings = Settings.from_env()
|
||||
est = len(todo) * 3 # extract (<=2 tries) + judge
|
||||
print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
|
||||
f"est_calls<={est} (extract x2 + judge) cap={args.max_calls}")
|
||||
print("prompts:", srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION,
|
||||
hashlib.sha256((srcsimplex.SYSTEM_PROMPT + JUDGE_SYSTEM).encode()).hexdigest()[:12])
|
||||
if args.dry_run:
|
||||
return 0
|
||||
|
||||
client = OpenAICompatibleClient.from_settings(settings.llm)
|
||||
if not items or len({item["id"] for item in items}) != len(items):
|
||||
ap.error("Input must contain unique item IDs")
|
||||
if any(not item.get("source_text", "").strip() for item in items):
|
||||
ap.error("Every item needs nonempty source_text; use a private source-inclusive export")
|
||||
if not args.dry_run and args.labels is None:
|
||||
ap.error("Freeze all blind labels first, then pass --labels")
|
||||
if args.labels is not None:
|
||||
annotation = json.loads(args.labels.read_text(encoding="utf-8"))
|
||||
key_path = args.labels.with_name("key.json")
|
||||
key = json.loads(key_path.read_text(encoding="utf-8"))["key"]
|
||||
verdicts = {"faithful", "minor_drift", "wrong", "not_formalizable"}
|
||||
if (set(key.values()) != {item["id"] for item in items}
|
||||
or set(annotation["labels"]) != set(key)
|
||||
or any(row.get("verdict") not in verdicts for row in annotation["labels"].values())
|
||||
or annotation.get("items_sha256") != digest(args.items)
|
||||
or annotation.get("key_sha256") != digest(key_path)):
|
||||
ap.error("Frozen labels, key and source-inclusive items must be complete and match")
|
||||
args.out.parent.mkdir(parents=True, exist_ok=True)
|
||||
with args.out.open("a", encoding="utf-8") as fh:
|
||||
for item in todo:
|
||||
if client.usage.calls >= args.max_calls:
|
||||
print("call cap reached; rerun to resume", file=sys.stderr)
|
||||
break
|
||||
fh.write(json.dumps(run_item(client, item), ensure_ascii=False) + "\n")
|
||||
fh.flush()
|
||||
meta = {"model": settings.llm.model, "usage": client.usage.as_dict(),
|
||||
"prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
|
||||
(args.out.parent / "run_meta.json").write_text(json.dumps(meta, indent=2), encoding="utf-8")
|
||||
print(json.dumps(meta))
|
||||
return 0
|
||||
with args.out.with_suffix(args.out.suffix + ".lock").open("w") as lock:
|
||||
fcntl.flock(lock, fcntl.LOCK_EX | fcntl.LOCK_NB)
|
||||
return execute(args, items, Settings.from_env())
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
|
||||
@@ -1,9 +1,9 @@
|
||||
"""Score the pilot: detectors vs. the blind human labels, with the pre-registered decision.
|
||||
"""Score the pilot against frozen blind labels using the pre-registered decision.
|
||||
|
||||
python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
|
||||
--labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json --summary experiments/P0-pilot/results/summary.json
|
||||
|
||||
Positive class = unfaithful. Primary: verdict == "wrong", over ALL labeled items (role alignment and
|
||||
Positive class = unfaithful. Primary: wrong versus faithful, excluding minor drift (role alignment and
|
||||
the judge do not need Lean to accept the code; only 10 of the 65 pilot items compiled, too few to
|
||||
decide on). Secondary: wrong or minor_drift; and the compiled-only subset (the paper's claim, reported
|
||||
with its interval, not used to decide). "not_formalizable" items are excluded. Decision (fixed before
|
||||
@@ -19,22 +19,35 @@ With ~65 items every number carries a wide Wilson interval; the pilot checks for
|
||||
from __future__ import annotations
|
||||
|
||||
import argparse
|
||||
import hashlib
|
||||
import json
|
||||
import math
|
||||
from pathlib import Path
|
||||
|
||||
from leanbench.evalstats import auc, confusion
|
||||
from leanbench.evalstats import auc, confusion, wilson
|
||||
|
||||
|
||||
def load(args):
|
||||
results = {json.loads(x)["id"]: json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()}
|
||||
result_rows = [json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()]
|
||||
results = {row["id"]: row for row in result_rows}
|
||||
labels = json.loads(args.labels.read_text(encoding="utf-8"))["labels"]
|
||||
key = json.loads(args.key.read_text(encoding="utf-8"))["key"]
|
||||
if not key or len(set(key.values())) != len(key):
|
||||
raise ValueError("The blind key must contain unique item IDs")
|
||||
if len(results) != len(result_rows) or set(results) != set(key.values()):
|
||||
raise ValueError("Results must cover every keyed item exactly once")
|
||||
if set(labels) != set(key):
|
||||
raise ValueError("Labels must cover every blind ID exactly once")
|
||||
rows = []
|
||||
for blind, item_id in key.items():
|
||||
lab = labels.get(blind) or {}
|
||||
if item_id in results and lab.get("verdict"):
|
||||
rows.append({**results[item_id], "blind": blind, "verdict": lab["verdict"],
|
||||
"human_errors": lab.get("errors", [])})
|
||||
if lab.get("verdict") not in {"faithful", "minor_drift", "wrong", "not_formalizable"}:
|
||||
raise ValueError(f"Missing or invalid verdict for {blind}")
|
||||
row = results[item_id]
|
||||
if row.get("errors") or "judge" not in row or "role" not in row:
|
||||
raise ValueError(f"Unresolved detector failure for {blind}; no decision can be issued")
|
||||
rows.append({**row, "blind": blind, "verdict": lab["verdict"],
|
||||
"human_errors": lab.get("errors", [])})
|
||||
return rows
|
||||
|
||||
|
||||
@@ -51,19 +64,24 @@ def report(rows, positive):
|
||||
out = {}
|
||||
for name in ("compile_only", "lint", "role", "judge"):
|
||||
out[name] = confusion([flags(r)[name] for r in rows], [positive(r) for r in rows]).as_dict()
|
||||
out[name]["precision_ci"] = wilson(out[name]["tp"], out[name]["tp"] + out[name]["fp"])
|
||||
out["role"]["auc_score"] = auc([-(r.get("role", {}).get("score", 1.0)) for r in rows],
|
||||
[positive(r) for r in rows])
|
||||
out["role"]["complementary_wrong"] = sum(
|
||||
positive(r) and flags(r)["role"] and not flags(r)["judge"] for r in rows
|
||||
)
|
||||
return out
|
||||
|
||||
|
||||
def decide(sub):
|
||||
role, judge = sub["role"], sub["judge"]
|
||||
if role["tp"] + role["fn"] == 0:
|
||||
return "INSUFFICIENT: no wrong items in the labels"
|
||||
if role["tp"] + role["fn"] == 0 or role["fp"] + role["tn"] == 0:
|
||||
return "INSUFFICIENT: both wrong and faithful items are required"
|
||||
go = (role["recall"] >= 0.5 and role["false_flag_rate"] <= 0.2
|
||||
and role["recall"] >= judge["recall"] + 0.10
|
||||
and role["false_flag_rate"] <= judge["false_flag_rate"])
|
||||
partial = (role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
|
||||
partial = ((role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
|
||||
or role.get("complementary_wrong", 0) >= 3)
|
||||
return "GO" if go else "PARTIAL" if partial else "NO-GO"
|
||||
|
||||
|
||||
@@ -75,19 +93,51 @@ def main() -> int:
|
||||
ap.add_argument("--summary", type=Path, default=None,
|
||||
help="also write the (text-free) summary here, e.g. results/summary.json")
|
||||
args = ap.parse_args()
|
||||
rows = [r for r in load(args) if r["verdict"] != "not_formalizable"]
|
||||
compiled = [r for r in rows if r["compiled"]]
|
||||
meta = json.loads(args.results.with_suffix(".meta.json").read_text(encoding="utf-8"))
|
||||
if (meta.get("status") != "complete"
|
||||
or meta.get("labels_sha256") != hashlib.sha256(args.labels.read_bytes()).hexdigest()
|
||||
or meta.get("results_sha256") != hashlib.sha256(args.results.read_bytes()).hexdigest()):
|
||||
ap.error("Scoring requires a complete run with unchanged frozen labels and results")
|
||||
all_rows = load(args)
|
||||
rows = [r for r in all_rows if r["verdict"] != "not_formalizable"]
|
||||
primary = [r for r in rows if r["verdict"] != "minor_drift"]
|
||||
compiled = [r for r in primary if r["compiled"]]
|
||||
summary = {
|
||||
"n_labeled": len(rows), "n_compiled": len(compiled),
|
||||
"run_metadata": meta,
|
||||
"n_labeled": len(all_rows), "n_evaluable": len(rows), "n_primary": len(primary),
|
||||
"n_compiled": len(compiled),
|
||||
"verdicts": {v: sum(r["verdict"] == v for r in rows) for v in
|
||||
("faithful", "minor_drift", "wrong")},
|
||||
("faithful", "minor_drift", "wrong", "not_formalizable")},
|
||||
"compiled_but_wrong": sum(r["verdict"] == "wrong" for r in compiled),
|
||||
"primary_all": report(rows, lambda r: r["verdict"] == "wrong"),
|
||||
"primary_all": report(primary, lambda r: r["verdict"] == "wrong"),
|
||||
"secondary_all": report(rows, lambda r: r["verdict"] in ("wrong", "minor_drift")),
|
||||
"compiled_only": report(compiled, lambda r: r["verdict"] == "wrong"),
|
||||
}
|
||||
summary["verdicts"]["not_formalizable"] = len(all_rows) - len(rows)
|
||||
summary["role_recall_by_error"] = {
|
||||
error: {"flagged": sum(flags(r)["role"] for r in rows
|
||||
if r["verdict"] == "wrong" and error in r["human_errors"]),
|
||||
"total": sum(r["verdict"] == "wrong" and error in r["human_errors"] for r in rows)}
|
||||
for error in sorted({e for r in rows for e in r["human_errors"]})
|
||||
}
|
||||
summary["degenerate_projection"] = {
|
||||
"total": sum(bool(r.get("projection", {}).get("degenerate")) for r in all_rows),
|
||||
"wrong": sum(r["verdict"] == "wrong" and bool(r.get("projection", {}).get("degenerate"))
|
||||
for r in all_rows),
|
||||
}
|
||||
summary["disagreements"] = [
|
||||
{"blind": r["blind"], "verdict": r["verdict"], "flags": flags(r)}
|
||||
for r in primary if any(f != (r["verdict"] == "wrong") for f in flags(r).values())
|
||||
]
|
||||
summary["decision"] = decide(summary["primary_all"])
|
||||
text = json.dumps(summary, indent=2, default=str)
|
||||
def finite_json(value):
|
||||
if isinstance(value, dict):
|
||||
return {k: finite_json(v) for k, v in value.items()}
|
||||
if isinstance(value, (list, tuple)):
|
||||
return [finite_json(v) for v in value]
|
||||
return None if isinstance(value, float) and not math.isfinite(value) else value
|
||||
|
||||
text = json.dumps(finite_json(summary), indent=2, allow_nan=False)
|
||||
if args.summary:
|
||||
args.summary.parent.mkdir(parents=True, exist_ok=True)
|
||||
args.summary.write_text(text + "\n", encoding="utf-8")
|
||||
|
||||
Reference in New Issue
Block a user