{"id":"8b8d4e95-c96f-4e7c-8120-0bf7fc7e35aa","arxiv_id":"2412.16864","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"PredTrace is a lineage inference system that uses predicate pushdown, optional intermediate materialization, and iterative refinement to trace row-level lineage across SQL and Pandas pipelines, with broad operator and UDF coverage.","lead":"PredTrace infers which input rows produced a given output row by pushing a row-selection predicate down through a pipeline to the source tables, saving intermediate results only when precise lineage requires it. A generalist would read this to see how a classic database optimization trick, predicate pushdown, is repurposed to make data lineage fast and usable on complex SQL and Pandas pipelines with user-defined functions.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 3.1 equates predicate selectivity with lineage minimality, but the paper's own Table 2 shows groupby max can return a superset; the precise-lineage guarantee is therefore unproven.","rationale":"The reader's weakest assumption and my stress-test converge on the same point: PredTrace's correctness proof assumes that the external predicate pushdown module returns the most selective predicate, and that this predicate selects exactly the minimal lineage set as defined in Definition 3.1. The paper does not provide a formal theorem about MagicPush's output, and Lemma 3.1's proof steps from 'most conjunctions' to 'most selective' to 'minimal lineage' are not valid in general. This is the single most load-bearing concern because it undermines the theoretical contribution—the claimed guarantee of precise lineage—even if the empirical evaluation is promising. The paper's own Table 2 exposes the issue with GroupBy(max), where the default fallback returns the entire group rather than the precise row set. Since the central claim is 'always computes the precise lineage,' and the proof of that claim relies on an unverified external guarantee, the conditional acceptance recommended by the reader is appropriate. No stronger action is warranted because the system may still work in practice and the gap could be closed by a more careful formal treatment or by stating the external module's guarantees as an assumption.","tokens_in":22291,"tokens_out":8865,"duration_ms":78232,"concrete_test":"Construct a table with group g containing values (1,2,5) and target output row (g,5). Use the MagicPush module described in Section 2 to push the row-selection predicate (group==g AND max==5) through a GroupBy(max) operator. Check whether the returned G is (group==g AND value==5), which selects the precise lineage, or (group==g), which returns the entire group. If the latter, the claim that PredTrace always computes precise lineage is contradicted. Additionally, re-derive Lemma 3.1 without the footnoted equivalence; if the proof cannot be completed, the formal guarantee is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central formal claim—that pushing a row-selection predicate down through a pipeline with materialized intermediates always yields precise lineage—rests on Lemma 3.1. The proof of Lemma 3.1 uses two unjustified steps. First, the footnote (Section 3.2) asserts that since G_row is a conjunction of equal comparisons, 'the predicate with the most conjunctions is the most selective.' But selectivity in terms of syntactic conjunctions does not imply semantic minimality: functional dependencies can make extra conjuncts redundant, and G_row for operators like RowTransform or RowExpand includes function equalities or disjunctions, so the syntactic argument does not apply. Second, even if G_row is the most selective predicate satisfying Op(G_row(T)) ⊇ F_row(Op(T)), this does not imply G_row selects the lineage as defined in Definition 3.1 (union of all minimal subsets). The most selective G_row could pick one minimal subset rather than their union, or it could include rows that are necessary for the equivalence to hold on all tables but are not part of the lineage of the actual output row. The paper's own Table 2 acknowledges this: for GroupBy with max, the default G_row 'selects the entire group,' which is a strict superset of the precise lineage. While the authors state that MagicPush never fell back to this default in their experiments, the formal 'always' claim requires a guarantee from the external module that is neither stated nor proven. Consequently, the strongest claim—'pushing it down through a pipeline assisted by saving intermediate results always computes the precise lineage'—is not established by the paper's arguments.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes PredTrace, a lazy row-level lineage inference system that constructs a row-selection predicate for a target output row and pushes it down through a data-processing pipeline using an external predicate-pushdown module (specifically MagicPush). When a non-row-selection predicate cannot be pushed down equivalently, PredTrace materializes a small intermediate result; when materialization is not feasible, it uses a push-up/iterative-refinement procedure to reduce false positives. The system is evaluated on all 22 TPC-H queries and 70 real-world Jupyter/pandas pipelines, with comparisons to Trace, GProM, Panda, and SMOKE, reporting low pipeline overhead, lineage query times around hundreds of milliseconds when intermediates are saved, and up to 10x speedups over prior lazy systems.","tokens_in":22574,"tokens_out":5919,"duration_ms":58376,"significance":"If the formal claims were fully established, PredTrace would be a meaningful advance: it applies lazy lineage inference to a much broader class of pipelines than prior SPJA-focused systems, including UDFs and non-relational operators, while keeping lineage querying efficient. The evaluation is broad and transparent, the system has no data-dependent free parameters, and the SMT-based verification gives reproducible, derived lineage results rather than fitted ones. The main weakness is the proof of the central 'always precise lineage' claim, which currently conflates syntactic predicate selectivity with semantic minimality and does not handle non-unique minimal lineage sets; the paper's own Table 2 shows a concrete case (GroupBy with max) where the default pushed-down predicate selects a strict superset. The iterative no-intermediate-result algorithm and its FPR evaluation are interesting, but their correctness also depends on this unproven foundation.","major_comments":[{"comment":"The proof's claim that the pushed-down predicate selects the precise lineage is not established. The footnote equates 'most conjunctions' with 'most selective', but this is only syntactic: functional dependencies, disjunctions in G_row (e.g., RowExpand in Table 2), and function equalities (RowTransform) can make larger conjunction counts unrelated to row-set minimality. More importantly, Definition 3.1 defines lineage as the union of all minimal subsets when the minimal subset is not unique; a most-selective G satisfying Op(G(T)) superset of {t_o} may select only one minimal subset, or may include rows that are needed only to make the pushdown identity hold for all tables, not to produce t_o. Table 2 itself gives a counterexample: for GroupBy with max, the default G_row 'selects the entire group', a strict superset of the precise lineage. The statement that MagicPush did not fall back to this default in the experiments does not prove the formal 'always' claim, so the guarantee in contribution 1 and the decision to skip materialization in Algorithm 1 (Line 5) rest on an unproven assertion.","section":"Section 3.2, Lemma 3.1"},{"comment":"The proof of property (1) is invalid. It argues that any other subset of T_i that produces the target output T*_{i+1} must be a superset of T*_i, but T*_i is defined in Definition 3.1 as the union of all minimal subsets. A producing subset need not contain every minimal subset; for example, if two disjoint minimal subsets both produce the target, a third subset containing only one of them still produces the target but is not a superset of the union. Thus Lemma 3.2 does not prove that naive pushdown returns a superset of the precise lineage; it may return an incomparable set. This matters directly for Section 6, where Algorithm 3's iterative refinement is justified as reducing the size of a 'meaningful superset', and for the FPR numbers in Table 6.","section":"Section 3.2, Lemma 3.2"},{"comment":"The manuscript does not state precisely what property the external pushdown module must guarantee for PredTrace's correctness, nor does it formalize the decision procedure behind Algorithm 1's Line 5. The verification in Section 4.2 checks equivalence of row-exist expressions on bounded symbolic tables and asserts soundness via MagicPush's bounded-size symbolic verification, but the paper never states the resulting contract as a theorem (e.g., 'G_row is the minimal row set whose image contains t_o') nor proves that G_i equivalent to G_row implies precise lineage under Definition 3.1. Given that Table 2 lists operators for which the default G_row is a superset, the verifier can only be as strong as the property it checks; as written, the reader cannot tell whether the verifier would certify a non-minimal G_row as precise.","section":"Section 4.2 and Algorithm 1"}],"minor_comments":[{"comment":"The statement that a cardinality estimator is unnecessary because 'the predicate with the most conjunctions is the most selective' should be removed or replaced with a semantic argument; as noted in the major comments, it is not generally true.","section":"Section 3.2, footnote"},{"comment":"Line 1 of Algorithm 2 contains a formatting artifact ('1 t] input :') that should be corrected.","section":"Algorithm 2"},{"comment":"The default G_row entries for Pivot and UnPivot appear to be broken across lines ('col_index == v_i∧' with no continuation); the table should be reformatted so each predicate is complete and readable.","section":"Table 2"},{"comment":"The claim that a unique index implies set semantics is under-specified: a unique index makes rows distinguishable at the physical level, but PredTrace's row-selection predicates are value-based and may still treat two rows with identical projected values as indistinguishable.","section":"Section 4.3"},{"comment":"The text in Section 7.1.2 describes Trace as iterating over input rows, while Figure 4 shows Trace as an inner join; these descriptions should be reconciled.","section":"Figure 4"},{"comment":"The text refers to 'Eqn (1)' but the displayed equation is not numbered in the manuscript; adding a number or a pointer to the displayed formula would improve readability.","section":"Section 6.1"}],"recommendation":"major_revision","confidential_remarks":"The paper is within scope for cs.DB and the experimental contribution is substantial. The main blocker is the formal correctness argument: Lemma 3.1 and Lemma 3.2 contain load-bearing gaps, and the paper's own Table 2 undermines the unconditional 'always precise' claim. This is repairable—the authors could state the external pushdown module's required guarantee as an explicit assumption, restrict the precise-lineage claim to operators where G_row is proven minimal, or weaken the contribution accordingly. The self-citation to MagicPush is appropriate here because MagicPush has its own evaluation and is not tuned to the lineage task; it does not make the paper circular."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nTwo things to know about this paper. First, the core trick is genuine and the experimental work is broad: PredTrace handles all 22 TPC-H queries and 70 real-world Pandas pipelines, with lineage query times orders of magnitude better than the lazy baselines. Second, the paper's headline formal claim — that pushing a row-selection predicate through a pipeline with materialized intermediates always computes precise lineage — is not actually established by the proof. The stress-test note is right: Lemma 3.1 has a real gap.\n\nWhat is new: using predicate pushdown as a lineage inference mechanism. Prior lazy systems either rewrite queries (Perm, GProM) or require hand-specified attribute maps (Panda). PredTrace gets pushdown from an external module (MagicPush), which extends to UDFs and non-relational operators. The selective materialization of intermediate results and the iterative pushup-pushdown refinement for the no-materialization case are also nice engineering. The evaluation is the real strength: 1GB TPC-H, 70 real pipelines, up to 98x faster lineage querying than the best lazy baseline, and false-positive reduction from 70.7% to 6.6% on the iterative method. The baselines are the right ones, and the SMOKE comparison is honestly caveated.\n\nThe soft spots, in proportion. Lemma 3.1 is the main one. The footnote claims that because G_row is a conjunction of equal comparisons, the predicate with the most conjuncts is the most selective. That is not generally true: functional dependencies can make conjuncts redundant, and for RowTransform or RowExpand the pushed predicate is not a pure conjunction of equalities. Even a genuinely most-selective predicate satisfying the equivalence condition need not select the union of all minimal lineage subsets — it could pick one minimal subset, or include rows needed for the equivalence on all tables but not for the actual output row. The paper's own Table 2 shows the default G_row for groupby max selects the entire group, which is a superset. The authors say MagicPush never fell back to that default in their runs, but that is an empirical observation, not a proof of the \"always\" claim. This is fixable: state the required guarantee from the external module as an explicit condition, or weaken the claim to \"precise lineage conditional on that guarantee.\"\n\nThe dependency on MagicPush is a real limitation but not a flaw; the paper inherits its restrictions (deterministic, symbolically executable UDFs, SMT timeouts) and says so. The missing code and data is a weakness for a systems paper, but not a correctness defect. The set-semantics limitation is also stated clearly.\n\nBottom line: this is a solid systems paper with a genuine new idea and a strong evaluation. The formal soundness claim needs a fix before publication, but the paper deserves referee time. I would recommend conditional acceptance — no need to redo the experiments, but repair the lemma or qualify the claim, and consider releasing the prototype.\n\nRecommendation: send to peer review, expecting revision on the soundness gap.","headline":"Predicate pushdown for lineage is a real idea, and the evaluation is strong, but the 'always precise' guarantee rests on a proof gap that needs repair before publication.","tokens_in":23087,"tokens_out":3378,"would_cite":true,"duration_ms":29079,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that row-level lineage can be computed by pushing a row-selection predicate through a data pipeline, saving intermediate results only where pushdown loses precision.","keywords":["row-level lineage","predicate pushdown","data provenance","lazy lineage inference","intermediate result materialization","data science pipelines","TPC-H"],"falsifier":"Run PredTrace on a small groupby-max pipeline whose group contains values 3, 4, and 5 and trace the output row for max = 5: if the returned lineage includes the rows with 3 or 4, the precise-lineage claim is falsified. On the no-intermediate-results variant, trace SELECT sum(R.a) FROM R WHERE R.a > (SELECT avg(S.b) FROM S); any returned R row with R.a <= avg(S.b) is a false positive that the iterative refinement claims to remove.","tokens_in":22096,"feed_emoji":"🔍","tokens_out":8132,"duration_ms":74529,"temperature":0.7,"pith_summary":"The paper's central claim is that row-level lineage can be obtained by reusing predicate pushdown, a standard query optimization. Instead of instrumenting operators or rewriting the whole query, PredTrace encodes the target output row as a row-selection predicate and pushes it down through the pipeline to the source tables, treating the selected rows as lineage. For a single operator the pushed-down predicate is claimed to select exactly the minimal input subset, and with a few saved intermediate results the same guarantee is claimed for an entire pipeline. When intermediate results cannot be saved, PredTrace still returns a lineage superset and iteratively refines it, cutting the average false-positive rate on TPC-H from 70.7% to 6.6%. The payoff is broad coverage: all 22 TPC-H queries and 70 real-world data-processing pipelines, with lineage queries answered in seconds and up to 98x faster than prior lazy lineage systems in the paper's experiments.","feed_headline":"Predicate pushdown traces lineage for all 22 TPC-H queries","feed_subtitle":"Precise lineage comes from pushing row predicates down; even without saved intermediate results, false positives average 6.6%.","key_machinery":"The central object is the row-selection predicate $F_{row}(t)=(col_1=v_1 \\land \\dots \\land col_k=v_k)$, constructed from a concrete output row. The argument rides on the predicate-pushdown equivalence $Op(G(T))=F(Op(T))$, or the relaxed $Op(G(T))\\supseteq F(Op(T))$: pushing $F_{row}$ through each operator rewrites it into a source-table predicate. When pushing an arbitrary predicate $F_i$ is not equivalent to pushing a row-selection predicate, PredTrace materializes the operator's output and pushes a row-selection predicate from there; equivalence is checked on fixed-size symbolic tables with an SMT solver. When no intermediate result can be saved, row-value predicates containing sets of column values are pushed upward and then downward in an iterative refinement until the value sets reach a fixpoint, removing non-joinable rows from the lineage superset.","core_discovery":"The core discovery is a formal connection: if $t_o$ is an output row and $F_{row}$ is the conjunction of equalities that picks exactly $t_o$, then pushing $F_{row}$ through an operator $Op$ yields a predicate $G_{row}$ whose selected rows are the minimal input subset that can produce $t_o$. The paper proves this for a single operator and shows that for a pipeline, materializing an intermediate result precisely at the operators where pushdown fails makes the same guarantee hold for the whole pipeline. It also proves that pushing the final predicate all the way down without intermediates yields a meaningful superset, and introduces an iterative push-up/push-down refinement that eliminates most false positives. On its evaluation, the method covers all 22 TPC-H queries and 70 sampled real-world pipelines, supports user-defined functions and non-relational operators, and answers lineage queries in about 0.23 seconds on average when intermediate results are available.","pith_inferences":["Beyond the paper: because the logical inference phase is system-independent and runs once per pipeline, the same technique could be exposed as a non-invasive service on any engine that already supports predicate pushdown, not only the prototype's SQL and Python front ends.","Beyond the paper: the precise-lineage guarantee is stated under set semantics, so duplicate output rows with identical values are traced together; adding unique row identifiers through the pipeline would extend the method to view-update-style row deletion, which the paper leaves open.","Beyond the paper: the push-up/push-down exchange that drives the iterative refinement could be reused as a general way to optimize data-debugging queries over arbitrary join graphs, since it effectively computes join-reachable row sets without materializing the full join."],"forward_implications":["For a single operator, lineage is exactly what a pushed-down row-selection predicate selects, so lineage querying reduces to running a predicate rather than re-executing the pipeline.","When intermediate results are materialized at the operators where pushdown loses precision, pipeline-level lineage is exact, and the saved results can be kept small by column projection and by deferring materialization to a later, smaller output.","When materialization is impossible, iterative push-up/push-down refinement returns a lineage superset, with zero false positives on inner-join and semi-join-heavy workloads and an average false-positive rate of 6.6% across TPC-H in the paper's evaluation.","Supported pipelines include Pandas-style data science pipelines with user-defined functions, pivots, windows, grouped maps, and subqueries, not just SQL SPJA queries.","Logical lineage inference runs once per pipeline, independent of the data system, so lineage queries for arbitrary output rows can reuse the same pushed-down predicates without repeating the inference work."],"supporting_citations":[{"why":"Supplies the external predicate pushdown module that handles non-relational operators and UDFs; PredTrace's precision guarantee depends on this module returning the most selective pushed-down predicate.","marker":"[36]"},{"why":"Provides the logical provenance model and attribute-mapping/filter specification that PredTrace extends from relational queries to pipelines.","marker":"[22]"},{"why":"A lazy lineage baseline for general transformations that PredTrace compares against and whose coverage it exceeds.","marker":"[11]"},{"why":"Contributes provenance query rewriting for nested subqueries, used as a baseline technique and for subquery coverage.","marker":"[17]"},{"why":"Provides provenance-aware query optimization used by a baseline system in the evaluation.","marker":"[29]"},{"why":"An eager lineage tracking system used as the comparison point for query-execution overhead and lineage-query latency.","marker":"[31]"}],"fun_headline_variants":["PredTrace: 10x faster lineage via predicate pushdown","Lineage in seconds through pushed-down predicates","Predicate pushdown yields lineage for all TPC-H queries","Pushdown predicates make lineage queries up to 10x faster"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The method assumes that the external predicate-pushdown module returns the most selective predicate that selects exactly the minimal input-row set, and that having more equality conditions always means selecting fewer rows; if the module can only return a safe superset, the precise-lineage guarantee degrades to a superset.","fun_headline_variants_meta":{"raw":{"variants":["PredTrace: 10x faster lineage via predicate pushdown","Lineage in seconds through pushed-down predicates","Predicate pushdown yields lineage for all TPC-H queries","Pushdown predicates make lineage queries up to 10x faster"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000397,"raw_usage":{"total_tokens":2108,"prompt_tokens":1004,"completion_tokens":1104,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":620,"completion_tokens_details":{"reasoning_tokens":1037}},"tokens_in":620,"tokens_out":1104,"duration_ms":9027,"temperature":1.0,"reasoning_tokens":1037,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T06:01:41.569565+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run PredTrace on a small groupby-max pipeline whose group contains values 3, 4, and 5 and trace the output row for max = 5: if the returned lineage includes the rows with 3 or 4, the precise-lineage claim is falsified. On the no-intermediate-results variant, trace SELECT sum(R.a) FROM R WHERE R.a > (SELECT avg(S.b) FROM S); any returned R row with R.a <= avg(S.b) is a false positive that the iterative refinement claims to remove.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the external predicate pushdown module that handles non-relational operators and UDFs; PredTrace's precision guarantee depends on this module returning the most selective pushed-down predicate."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the logical provenance model and attribute-mapping/filter specification that PredTrace extends from relational queries to pipelines."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"A lazy lineage baseline for general transformations that PredTrace compares against and whose coverage it exceeds."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Contributes provenance query rewriting for nested subqueries, used as a baseline technique and for subquery coverage."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides provenance-aware query optimization used by a baseline system in the evaluation."}],"review_version":1}