61 lines
4.2 KiB
Markdown
61 lines
4.2 KiB
Markdown
# 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](ADR-0131-math-expert-rebench.md), 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](ADR-0119.7-sealed-gsm8k-test.md) 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](file:///Users/kaizenpro/Projects/core/CLAUDE.md#L140-L167), 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.
|