{"id":"a5476f3d-9f31-424f-b564-9da779d074ef","arxiv_id":"2607.26997","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"APS-Estimator gives an (ε,δ)-approximation of the union of Delphic sets in a stream with space O(R log|Ω|) and update time linear in dimension for Klee’s measure, settling a PODS 2012 open problem.","lead":"A simple adaptive sampling algorithm estimates the size of a union of implicitly presented sets in a data stream, with tight resource bounds. It settles a decade-old open question on multi-dimensional Klee’s measure and unifies coverage testing and DNF counting under one abstraction.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified","rationale":"The reader correctly flags Observation 4.1 as the messiest step in the write-up: APS thins the count N_i before sampling while Naive samples then thins, so a naïve shared-tape coupling does not automatically give identical control flow or identical surviving sets. That is a genuine presentational gap (and the surrounding paragraph contains clear editing artifacts). It is not, however, load-bearing for the theorem. The concentration analysis never needs pathwise identity with Naive; it only needs that, conditioned on DistinctSample succeeding, the pair (X,p) maintained by APS is distributed exactly as an independent p-sample of the current union. That invariant is elementary from the definitions of Binomial thinning and DistinctSample and is already the invariant claimed for Naive. Consequently Pr[Bad_APS]≤Pr[concentration failure]+Pr[FailSample]≤δ follows verbatim, the space/update bounds are immediate from |X|<thr_0, and Cor 1.7 (linear-in-d streaming Klee) is a direct instantiation. The claimed Lean 4 formalization, if it discharges the invariant, eliminates even the residual doubt. No other soft spot (Delphic implementations, Chernoff thresholds, coupon-collector tail, or the retracted prior claim) threatens the headline result. Verdict remains ACCEPT.","tokens_in":21638,"tokens_out":691,"duration_ms":82712,"concrete_test":"Inspect the public Lean 4 development (github.com/meelgroup/delphic21lean) and confirm it proves the independent-sampling invariant for APS-Estimator itself (or an equivalent pathwise coupling) together with the exact δ-budget split; if the invariant lemma is absent or relies on an unproved axiom about postponed vs immediate thinning, re-derive the invariant on paper for one full iteration with k≥1 halvings and check that final inclusion probabilities remain exactly p.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim (Thm 1.6 / Cor 1.7) holds under a direct invariant argument that does not require the Naive coupling. After the remove step, X is an independent p-sample of S^(i-1)\\S_i. Cascaded Bin(N_i,1/2) updates together with the X-thinning steps preserve that N_i~Bin(|S_i|,p_current) and X is an independent p_current-sample; a successful DistinctSample then restores an independent p-sample of the full union. Concentration and the thr_0 thresholds therefore apply verbatim to APS-Estimator, with the only additive error Pr[FailSample]≤2δ/3 from the coupon-collector bound (Thm 3.1). The Observation 4.1 coupling write-up is sloppy (control flow for the number of halvings differs between APS and Naive; the published text also contains typos), but that is presentational, not load-bearing: the same invariant already used for Naive applies directly to APS. Lean formalization further reduces residual risk. Delphic lemmas for rectangles, Cov_t and DNF terms are routine and give the linear-in-d update time.","agreement_with_reader":"partial"},"referee_report":{"model":"grok-4.5","summary":"The paper introduces Delphic sets—families closed under efficient membership, uniform sampling, and counting—and gives a simple adaptive sampling algorithm (APS-Estimator) that returns an (ε,δ)-approximation of the cardinality of the union of a stream of such sets. Space is O(R log|Ω|) and per-item update time is O(R log R · log(M/δ) · log|Ω|) with R = O(log(M/δ)·ε^{-2}). The framework specializes to discrete streaming Klee’s measure (first algorithm whose update time is linear in dimension d for d>1, settling an open question of Tirthapura–Woodruff), combinatorial test-coverage estimation, and streaming DNF model counting. A second, hashing-based estimator for coverage trades near-optimal space for P^NP update time. The revised manuscript reports a Lean 4 formalization of the main algorithm and its correctness argument.","tokens_in":21833,"tokens_out":971,"duration_ms":38558,"significance":"If correct, the result is a clean and practically usable advance: it unifies three previously separate streaming problems under a single black-box interface, supplies the first linear-in-d update-time algorithm for multi-dimensional discrete Klee’s measure, and does so with an elementary sampling analysis rather than range-efficient sketches. The explicit Lean 4 machine-checked proof of APS-Estimator and the transparent constant derivation for thr_0 are genuine strengths that lower residual risk and make the work easy to reuse. The time–space trade-off for coverage estimation is a useful secondary contribution. Overall the paper is a strong candidate for a theory journal that values simple, implementable streaming algorithms with rigorous guarantees.","major_comments":[{"comment":"§4.1, Observation 4.1 and the surrounding coupling: the written argument equates APS-Estimator with Naive under a shared random tape, yet the control flow for when p is halved differs (APS thins the pending binomial N_i before DistinctSample; Naive samples immediately and then thins). The published text also contains garbled phrasing (“after the loop 5–7). Naive”). While a direct invariant (after the remove step X is an independent p-sample of the prior union minus S_i; cascaded Bin(·,1/2) and X-thinning preserve the invariant; a successful DistinctSample restores an independent p-sample of the full union) already justifies the same Chernoff/coupon-collector bounds, the manuscript should either repair the coupling carefully or replace it by the direct invariant so that the published proof matches what the Lean development discharges.","section":"§4.1 (Observation 4.1, Algorithms 1–3)"}],"minor_comments":[{"comment":"Several local typos remain from the PODS revision (e.g., “seminar work” → “seminal work” in §2; “ofcount sketch”; missing spaces and punctuation around the Naive coupling paragraph). A careful pass would help.","section":"§2, §4.1"},{"comment":"Corollary 1.7’s update-time expression hides an extra log(1/ε) factor relative to the generic bound of Theorem 1.6; a one-line remark explaining the origin (DistinctSample’s coupon-collector loop) would avoid reader confusion.","section":"Corollary 1.7"},{"comment":"In the appendix proof of Lemma 4.6 the constants 4.92, 10.84, 20.68, 62.5 appear without intermediate arithmetic; expanding one Chebyshev/Paley–Zygmund calculation would make the 1/4-style bound easier to check.","section":"Appendix (Lemma 4.6)"},{"comment":"The Lean repository is cited only by URL in the footnote; adding a short “Artifact” paragraph (what is formalized, which axioms remain, how to replay) would strengthen the reproducibility claim.","section":"Front matter / §1"}],"recommendation":"minor_revision","confidential_remarks":"This is a substantially cleaned revision of a PODS’21 paper with an added Lean formalization. The core technical contribution is solid and the open-problem resolution is real; the only load-bearing textual weakness is the coupling write-up, which is fixable without changing the result. Good fit for a journal that accepts polished streaming/algorithms papers."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The thing worth knowing is that this revised PODS piece gives the first streaming algorithm for discrete Klee’s measure whose per-item update time is linear in dimension d, not exponential. That was a stated open problem after Tirthapura–Woodruff’s earlier claim was retracted. The same sampler also covers combinatorial-test coverage and streaming #DNF once you accept the Delphic interface (count / uniform sample / membership in O(log |Ω|) time).\n\nWhat is new is less a deep new probabilistic idea than a clean packaging: start with p = 1, maintain a thr0-sized sketch that is notionally an independent p-sample of the union so far, remove-then-resample on each arriving set so elements that appear in many sets are not over-weighted, and halve p (and thin the sketch) when the bucket overflows. Space is O(R log |Ω|) with R = O(log(M/δ) ε^{-2}); update is O(R log R · log(M/δ) · log |Ω|). The Delphic lemmas for axis-aligned rectangles (and arithmetic progressions), Cov_t, and DNF terms are routine and immediately give the three corollaries. The near-optimal-space HashingEstimator that spends P^NP update time is a secondary but honest time–space trade-off for coverage.\n\nThe analysis is elementary Chernoff + coupon-collector with an explicit δ split. The published coupling to an idealized “Naive” process is a bit sloppy on control flow (when halvings happen relative to sampling), but it is not load-bearing: the same independent-p-sample invariant already used for Naive applies directly to APS-Estimator after the remove step and the cascaded Bin(·,1/2) thinnings. FailSample is just the classical coupon-collector tail. Lean 4 formalization of the algorithm and correctness argument further lowers residual risk; that is real evidence, not decoration.\n\nSoft spots are minor and presentational: the coupling write-up could be tighter, constants are the usual loose Chernoff ones, and the paper does not chase M-independent bounds or turnstile deletions (both flagged as future work). Citation pattern is appropriate; self-cites are to prior counting/hashing work that the argument actually uses.\n\nThis is for streaming-algorithms and combinatorial-geometry people, and for anyone who needs a practical union-size monitor when the sets are implicitly given. I would bring it to reading group, I would cite the KMP corollary and the Delphic framing, and a serious editor should send it to referees rather than desk-reject. Engage with it.","headline":"Clean adaptive sampler that actually settles the linear-in-d update-time open problem for streaming discrete Klee, with a Lean-checked analysis and a useful unifying abstraction.","tokens_in":22526,"tokens_out":653,"would_cite":true,"duration_ms":17156,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68W27","68W20","68Q25"],"pacs":[],"model":"grok-4.5","headline":"A simple adaptive sampler estimates the size of a stream of union-of-sets whenever each set can be counted, sampled, and tested for membership quickly.","keywords":["streaming algorithms","union of sets","Delphic sets","Klee's measure problem","DNF model counting","combinatorial testing","adaptive sampling","F0 estimation"],"falsifier":"Implement APS-Estimator on a stream of random d-dimensional boxes for moderate d and M, compute the true union volume exactly (or by a slower exact method), and check whether the fraction of runs whose relative error exceeds ε is at most δ; a systematic excess would falsify the claimed concentration.","tokens_in":22476,"feed_emoji":"📐","tokens_out":986,"duration_ms":16919,"temperature":0.7,"pith_summary":"Many streaming problems amount to estimating how many distinct elements appear across a long sequence of implicitly defined sets. The paper isolates a clean sufficient condition—called Delphic sets—under which three black-box operations (size, uniform sample, membership) run in logarithmic time, and shows that three classical tasks fall inside this class: discrete Klee’s measure (volume of axis-aligned boxes), combinatorial test-coverage, and DNF model counting. It then gives a single adaptive-sampling algorithm, APS-Estimator, that maintains a small random sketch of the union seen so far, thinning the sketch whenever it grows too large. The algorithm returns an (ε,δ)-approximation using space linear in the sketch size and update time that is only linear in dimension for boxes. Because the same routine works for all three problems, the paper simultaneously settles an open question on multi-dimensional streaming volume and supplies practical streaming estimators for coverage and DNF counting.","feed_headline":"One adaptive sampler sizes streaming unions of sets","feed_subtitle":"Linear-in-dimension updates for box volumes, plus free algorithms for coverage and DNF counting","key_machinery":"APS-Estimator: an adaptive sketch that keeps every element of the current union independently with a dynamically halved probability p, removing then re-sampling on each new set so that the invariant is restored, and thinning the entire sketch by 1/2 whenever its size exceeds a Chernoff threshold.","core_discovery":"There exists a streaming algorithm APS-Estimator that, given any stream of Delphic sets, outputs an (ε,δ)-approximation of the cardinality of their union using worst-case space O(R log|Ω|) and update time O(R log R · log(M/δ) · log|Ω|), where R = O(log(M/δ)·ε^{-2}). Instantiated on axis-aligned boxes this is the first algorithm whose update time depends only linearly on dimension.","pith_inferences":["Because the analysis treats the three Delphic primitives as black boxes, the same sampler can be dropped into any domain (geometric, combinatorial, logical) once those primitives are supplied, suggesting a reusable library pattern.","The residual logarithmic dependence on stream length M is inherited from the adaptive thinning schedule; removing it would simultaneously improve distinct-elements, coverage, and DNF counting.","The Lean 4 formalization already discharged the coupling step; any later extension to turnstile streams or higher frequency moments can reuse that verified core."],"forward_implications":["Discrete Klee’s measure in the streaming model now admits update time linear in dimension, closing the exponential-in-d gap left by earlier sketching approaches.","The same black-box routine immediately yields streaming (ε,δ)-approximators for combinatorial t-way coverage and for the number of models of a DNF formula whose terms arrive one-by-one.","A second hashing-based estimator for coverage trades the linear-in-log(M) space for near-optimal space at the price of NP-oracle calls per update, exhibiting an explicit time–space trade-off.","Any future problem whose sets support fast size/sample/membership queries inherits the same space and update bounds without further algorithmic work."],"fun_headline_variants":["APS-Estimator approximates streaming Delphic set unions","Linear-in-d updates settle streaming Klee measure open problem","Simple sampler sizes unions of boxes, coverage, and DNF models","Space O(R log|Ω|) stream algorithm for Delphic union cardinality","Near-optimal coverage space via P^NP update trade-off"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"The argument that the real algorithm and an idealized immediate-sample version stay coupled on the same random bits, so that any failure of the real algorithm is already charged either to a coupon-collector abort or to a concentration failure of the idealized process.","fun_headline_variants_meta":{"raw":{"variants":["APS-Estimator approximates streaming Delphic set unions","Linear-in-d updates settle streaming Klee measure open problem","Simple sampler sizes unions of boxes, coverage, and DNF models","Space O(R log|Ω|) stream algorithm for Delphic union cardinality","Near-optimal coverage space via P^NP update trade-off"]},"model":"grok-4.5","effort":"low","cost_usd":0.003539,"raw_usage":{"total_tokens":1263,"prompt_tokens":901,"num_sources_used":0,"completion_tokens":74,"cost_in_usd_ticks":35388000,"prompt_tokens_details":{"text_tokens":901,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":288,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":901,"tokens_out":74,"duration_ms":5054,"temperature":1.0,"reasoning_tokens":288,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-30T14:31:45.292505+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Implement APS-Estimator on a stream of random d-dimensional boxes for moderate d and M, compute the true union volume exactly (or by a slower exact method), and check whether the fraction of runs whose relative error exceeds ε is at most δ; a systematic excess would falsify the claimed concentration.","supporting_citations":[],"review_version":1}