R12 Active Verifier Query No-Go

Status: valid active-learning theorem, rejected as a new closed reasoning mechanism. Target-coupled verifier feedback is an oracle; target-independent verification adds no information.

1. Access model

Let a candidate be theta=(M,s), a compact residual machine and current state. An experiment supplies an event word, query, and proposed witness. The verifier returns one bit

V_theta(x) in {0,1}.

Two candidates are verifier-equivalent when every possible experiment receives the same bit. No adaptive policy can distinguish candidates in one verifier fiber. Hidden-state conjugacies remain in the same fiber; only the behavioral quotient can be identified.

2. Strongest positive theorem

Let the current quotient version space have size N. If every non-singleton version space has a polynomial-time experiment that leaves at least a beta fraction on either side, greedy disagreement identifies the class within

ceil(log(N)/-log(1-beta)) = O(log(N)/beta)

verifier calls. Binary information requires at least ceil(log_2 N) calls in the best geometry. With independent verifier error eta<1/2, majority repetition adds the standard

O((1-2 eta)^-2 log(T/delta))

factor. This can exponentially beat passive sampling, as threshold search does.

3. Fatal limits

1. A public target-independent verifier has zero mutual information with the unknown target.
2. A target-coupled accept/reject verifier is a membership oracle; a returned counterexample is an equivalence oracle.
3. Final-answer verification identifies accepted behavior, not internal transitions or a unique reasoning path.
4. Extrapolation is justified only when every surviving candidate agrees.
5. Current-state recovery needs separating experiments, resets, cloning, or an adaptive homing sequence; experiments can otherwise merge states irreversibly.
6. Query count does not imply computational efficiency. Finding a disagreement input for succinct circuits can be SAT-hard, balancing a version space can require model counting, and unrestricted program equivalence is undecidable.
7. Active experiments learn a model but do not reduce the exact online residual memory lower bound.

4. Compact exponential obstruction

On X={0,1}^d, take

H = {h_bottom} union {h_z : z in X},
h_bottom(x)=0,
h_z(x)=1[x=z].

Every hypothesis has an O(d) description and a small DFA. Against h_bottom, each membership query eliminates at most one h_z, so exact identification needs 2^d calls. Compactness, determinism, and self-generated disagreement do not imply polynomial identification.

5. Prior-art boundary

Membership plus equivalence queries are exact automata learning. Balanced version-space splitting is generalized binary search. Candidate synthesis with verifier counterexamples is CEGIS/OGIS. Self-play chooses experiments and hypotheses; all target information still comes from the verifier. Verifiable reward changes search and optimization, not the oracle information boundary.

6. Decision

Actively generated disagreement tests remain useful data-engineering doctrine. They are not a new latent-reasoning mechanism. No CPU falsifier is authorized without a concrete nonlinear hypothesis class with polynomial consistency and separator synthesis, polynomial target-coupled queries without latent-axis labels, joint action-state identification up to behavioral conjugacy, and an exponential separation from matched active-automata and synthesis controls.