Identifiability of Relational Queries in Multi-View Pretraining
Ratan Bahadur Thapa, Daniel Hernández
cs.DB
Jul 6, 2026 · v1
cs.LG
TL;DR
Main theoretical results (closure certificate, minimax 1/2 error floor, FD/Armstrong correspondence, Fano's inequality, reduction to query determinacy) are machine-checked in a public Lean 4 development.
Abstract
When data sources are integrated through a shared interface, a downstream query may or may not be determined by what the interface exposes: two globally consistent worlds can agree on every shared attribute yet disagree on the query answer. This ambiguity is structural – a property of the interface design, not the data volume – and cannot be resolved by collecting more records or training a larger model. We formalize query identifiability for data integration under interface laws (functional dependencies that hold uniformly across all legal worlds rather than within a single instance) and prove three results. (i) A polynomial-time certificate (CheckCert) decides identifiability via attribute closure, and is exact on instances that expose any residual ambiguity (closure-separable). (ii) Non-identifiable queries face an irreducible 1/2 minimax error floor for any estimator using only interface evidence, bounding multi-view pretraining systems from below. (iii) A minimum-augmentation algorithm (Greedy-MinAug) finds the smallest set of interface additions to certify a query, reducing to Set Cover (logarithmic approximation). Experiments on synthetic benchmarks, real integration datasets spanning three domains (scholarly, product, restaurant), and schemas up to 10^3 attributes confirm CheckCert is exact, both algorithms run in single-digit milliseconds, and ML classifiers exhibit the predicted error floor and abrupt capability gains.
Problem
When data sources are integrated through a shared interface, a downstream query may not be determined by the exposed attributes. Two consistent worlds can agree on all shared views yet give different answers. The paper asks when such queries are identifiable under interface laws, which are functional dependencies that hold across all legal worlds.
Approach
Query identifiability is defined through observational equivalence on closure-augmented overlap projections. The authors prove that a polynomial-time attribute-closure certificate (CheckCert) decides identifiability on closure-separable instances. They also prove a 1/2 minimax error floor for non-identifiable queries, and reduce minimum interface augmentation to Set Cover, solved by Greedy-MinAug. Key results are machine-checked in a Lean 4 development (MultiViewIdentifiability), with queries modeled semantically by their answer invariants.
Results
The closure certificate, the minimax lower bound, the FD/Armstrong correspondence, the reduction to query determinacy and Fano's inequality are verified in Lean; the capability-jump theorem and the MinAug hardness and approximation bounds remain open in the formalization. Experiments on synthetic and real integration datasets confirm that CheckCert is exact, that both algorithms run in milliseconds on schemas with up to 10^3 attributes, and that ML classifiers show the predicted error floor.
| Framework | CQ complexity | Certificate |
|---|
| Query determinacy | Undecidable (general) | Sufficient only |
| Certain answers | coNP-complete | Complete |
| Data exchange | PTIME (chase) | Sound (target-side) |
| CheckCert (this work) | PTIME (closure) | Complete (on closure-separable instances) |
Identifiability vs. related query-answering frameworks (Boolean CQs)
