SILICA Certified Counterfactual Evaluation of Identifiability in Unseen-Language Induction

The languages are invented for the benchmark, so knowing real languages cannot help. Everything a model needs is in the prompt: a short program that reads only the prompt gets puzzles right. And there is a twist. You never need to work out exactly which language it is. You only need to check whether all the languages that are still possible give the same answer.

A SILICA record describes a small, closed world. binary features, four lexical swaps and four grammar settings, give candidate languages, drawn below as a  ×  grid: one square per language, columns set by the lexical bits and rows by the grammar bits. The record publishes a Boolean program that keeps half of them, reveals three dictionary facts, and asks one query. The gold action is ANSWER when every language still compatible with the evidence gives the same answer, and ABSTAIN when two of them disagree.

This is the paper's worked example, a released parity-guard pair (items and ), replayed one public filter at a time. Step through it, or press play. Every square's state is computed from the released public row with the silica package and checked against the sealed certificates; nothing is drawn by hand.

The two queries of a pair share the same program and the same three observations, and only the query changes; yet one must be answered and the other abstained from. So a policy that does not consult the evidence cannot separate them. Picture one that answers each row at a fixed rate α and, when it answers, picks a payload without reading the observations. Move the slider to choose α.

AR

answerable decision recall: how often the policy answers when the evidence determines the answer.

FCR

false-certainty rate: how often it answers when the evidence does not.

UR, EAR

abstention recall on underdetermined rows, and exact answerable recall (answer plus the canonical payload).

BDA, BJA

balanced decision accuracy, the mean of AR and UR, and balanced strict joint accuracy, the mean of EAR and UR.

The policy answers at the same rate whatever the gold action, so AR equals FCR and BDA stays at one half. Its evidence-blind payload is right on exactly one of the two answerable rows of every four-cell unit, because those two rows carry different canonical payloads. BJA therefore slides between the always-ABSTAIN constant () and the always-ANSWER constant (), while the exact oracle reaches .

Reporting UR, EAR or BJA alone therefore cannot distinguish a competent model from a differently tuned constant.

The rows are nested views of a much smaller number of logical objects, and the nesting is what makes the test hard to game. Below is one real route group from the release, the one that contains the worked example: four evidence states, each queried on both coordinates. Every column is a same-state pair with opposite gold actions; every row is a four-cell unit with two answers and two abstentions.

The construction was accepted only after constant-cardinality, paired-query, learned-probe and independent clean-room gates were fixed, before any direct-model inference. Two oracles must be exact, and every query-masked control and learned probe must sit exactly at chance; a solver that reads only the rendered user message reproduces every gold label. The strongest query-masked control keeps the raw program and evidence and is exactly at chance because every state receives both labels.

The sealed panel was frozen before any output was inspected: , each on the same -row common cohort, with greedy decoding, at most new tokens, no worked example, and the instruction to reason silently. Hover or focus a point for its full row of the paper's sealed-panel table.

Each pair changes one factor on a fixed checkpoint: a visible reasoning trace for two reasoning models (a -token budget, with only the final content scored), or a visible <think> scratchpad with a -token budget for two panel models. Flip the factor and watch which rows move.

Four renderings of the same cohort were served to two panel checkpoints: the released prompt (verbatim); a <think> scratchpad (scratchpad); a shorter user message that keeps the feature-value declaration (lean); and the guarded-switch route in place of the enumeration (compact_rule, an upper bound on what relieving the stated procedure can buy, not a matched control). Every arm stays on or right next to the diagonal: the answer rate changes a lot, the decision signal barely at all.

The stated enumerate-and-filter route costs declared-universe assignments times the published program's operator count (median , range ): a median of operator evaluations per row. The minimal sufficient decision is a Boolean function of the three revealed bits with minimal formula size (median), at most ; of the programs need none at all.

Install the package, download the dataset, check it, render the exact prompts, run your model, and score it. The common cohort is the one used in the paper; --cohort full renders every row.

The public row is the released model-facing record; the prompt renderer projects its routing fields, identifiers and hashes away before a model sees it. The gold record is evaluator-only and joined by id. Nested fields start collapsed.