core-labs/core
1
0
Fork 0
Code Issues Pull requests 1 Projects Releases Packages Wiki Activity Actions
core/docs/decisions/ADR-0131.1.S-sealed-holdout.md

4.2 KiB
Raw Permalink Blame History

ADR-0131.1.S — Sealed Holdout for Benchmark 1 (Symbolic Equivalence v1)

Status: Accepted Date: 2026-05-23 Author: CORE agents + reviewers Depends on: ADR-0131 (composite math expert promotion), ADR-0119.7 (sealed GSM8K test set), #167 (symbolic equivalence v1)

Context

Benchmark 1 of ADR-0131, merged in PR #167, tests whether the engine can determine algebraic equivalence of univariate integer polynomials under exact recall. The benchmark has a 100% baseline correct rate on a curated set of 30 public cases in cases.jsonl.

To make the benchmark's claims externally credible, we must prevent the development team from "peeking" at or optimizing against the evaluation cases used to measure expert promotion. Per the methodology proven in ADR-0119.7 for GSM8K, we introduce a sealed holdout split for Benchmark 1 using pyrage age-encryption.

Decision

We establish the Benchmark 1 sealed holdout split:

  1. Crypto Keypair: Generate a dedicated X25519 key pair for the B1 sealed holdout. The public key is stored in the repo at evals/math_symbolic_equivalence/v1/sealed_holdout.pubkey. The private key stays off-repo per the seal discipline of ADR-0119.7.
  2. Sealed Holdout Cases: Hand-curated 14 new evaluation cases strictly within the v1 univariate integer polynomial scope. The categories strictly match the public cases (e.g. commutative_add, distributive, square_of_binomial, difference_of_squares, collect_like_terms, zero_cancellation, repeated_addition, exponent_combine, different_constant, sign_flipped, distributive_miss, out_of_scope_variable, out_of_scope_division).
  3. Disjointness Invariant: The holdout cases are guaranteed to be disjoint from the public cases — they do not duplicate any case_id or any (expression_a, expression_b) pair.
  4. Sealed File: The plaintext cases are encrypted with the public key and written to evals/math_symbolic_equivalence/v1/sealed_holdout.age. No plaintext representation of the holdout cases resides in the repository.
  5. Sealed Runner: We ship evals/math_symbolic_equivalence/v1/sealed_runner.py which decrypts the sealed file using the age identity file provided by the CORE_SEALED_KEY environment variable. If the environment variable is unset or missing, it fails cleanly with an EnvironmentError.
  6. Pass Criterion: The sealed runner writes its results to sealed_report.json and gates the split on:
    • wrong == 0 (no confabulation)
    • correct_rate >= 0.95 (statistical threshold matching public splitter)

Security and Trust Boundaries

Per Security and Trust Boundaries in CLAUDE.md, we enforce strict trust boundaries on holdout decryption:

  • No plaintext companion files are written to disk during the runner's execution (only memory-based decryption).
  • No logging or echos of the decrypted plaintext cases to stdout or stderr are allowed.
  • The decryption key CORE_SEALED_KEY is never set in standard CI runs; tests requiring decryption gracefully skip when the key is absent to avoid blocking standard pull request flows.

Invariants

adr_0131_1_s_sealed_file_present_and_age_formatted

evals/math_symbolic_equivalence/v1/sealed_holdout.age exists, is non-empty, and begins with the age-encryption.org/ magic header.

adr_0131_1_s_no_plaintext_leaks

No plaintext companion files (cases_plaintext.jsonl, etc.) exist in the holdout directory.

adr_0131_1_s_runner_refuses_without_key

The sealed runner fails with EnvironmentError when CORE_SEALED_KEY is not configured, preventing silent fallback or execution.

adr_0131_1_s_decrypted_disjointness

When decrypted, all holdout cases have distinct case_id values and distinct expression pairs compared to the public cases.jsonl set.

Consequences

  • Credentialed Claims: Benchmark 1's validation claims are now externally reviewable and immune to developer-level overfitting.
  • Zero-Confabulation Gate: wrong == 0 is strictly enforced against the sealed holdout. Any algebraic regression that triggers a wrong verdict on held-out cases rejects the build.