Pith. sign in

REVIEW 3 major objections 6 minor 36 references

Look-ahead bias is temporal non-interference: free of future influence when availability is independent of values, and checkable in linear time.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

T0 review · grok-4.5

2026-07-11 10:55 UTC pith:GIWPYUSQ

load-bearing objection Clean formal identification of look-ahead-freedom as temporal non-interference, with a realistic decidable fragment, matching undecidability boundary, and an honest artifact—worth engaging. the 3 major comments →

arxiv 2607.04958 v1 pith:GIWPYUSQ submitted 2026-07-06 cs.CR cs.LOcs.PLcs.SEq-fin.PM

Look-Ahead-Freedom as Temporal Non-Interference: A Verifiable Correctness Property for Backtesting and Agentic Trading Pipelines

classification cs.CR cs.LOcs.PLcs.SEq-fin.PM
keywords look-ahead biasdata leakagenon-interferencetype-and-effect systemsdecidabilitybacktestingagentic systemspoint-in-time correctness
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Backtests and machine-learning evaluations often flatter a system by letting later information shape earlier decisions. The paper claims this failure is not a checklist of local mistakes but a single formal property: fixing a decision epoch, the future must not influence the present. That demand is temporal non-interference over a time-indexed information lattice. The authors build a small pipeline calculus that keeps a datum's availability (when it becomes knowable) separate from its reference time (which instant it describes). On the full language, where availability may be computed from data values, freedom is undecidable: a leak can be exhibited, but absence of leaks cannot be certified. On the value-independent fragment that covers ordinary windowing, resampling, joins, point-in-time and vintage reads, and agentic retrieval, a type-and-effect system accepts only free pipelines and decides acceptance in linear time. An independent oracle finds no leak in any accepted pipeline, and the checker catches planted leaks that differential and tiling detectors miss. The practical conversion is from hoping a pipeline is clean to certifying that it is.

Core claim

Look-ahead-freedom is temporal non-interference over a time-indexed lattice. On pipelines whose availability stamps do not depend on data values, a type-and-effect system soundly certifies the property in linear time; once availability may be computed from values, the property becomes undecidable (Π⁰₁-complete), so leaks are recursively enumerable but freedom is not.

What carries the argument

Temporal non-interference (Definition 8) over a time-indexed lattice, enforced on the value-independent fragment F by a type-and-effect system whose effect is a static upper bound on availability; the single decision obligation is that the body's effect is bounded by the decision epoch.

Load-bearing premise

Real pipelines fix each datum's availability from schema and schedule, never from the numeric values flowing through them, and base series carry honest availability stamps at ingestion.

What would settle it

A pipeline that the checker accepts yet an independent two-run oracle, at some epoch, produces different decisions after only future data is perturbed; or a real backtest pipeline whose availability is value-dependent and still admits a sound, complete certificate.

Watch this falsifier — get emailed when new claim-graph text bears on it.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper identifies look-ahead bias in backtests and agentic trading pipelines as temporal non-interference over a time-indexed information lattice (Definition 8). It introduces a pipeline calculus that separates availability from reference time, isolates a value-independent fragment F covering windowing, scans, joins, resampling, as-of/vintage reads, and agentic retrieval, and proves a type-and-effect system sound for look-ahead-freedom (Theorem 1) and decidable in linear time under bounded availability-term complexity (Theorem 2). On the full language U with value-conditioned availability, look-ahead-freedom is shown Π⁰₁-complete by reduction from the halting problem (Theorem 3): leakage is r.e., freedom is not. An artifact reports linear scaling (log–log slope ≈1.023), oracle agreement on accepted pipelines, and zero false negatives on 33 planted leaks that differential and tiling detectors miss, at a characterized false-positive cost on opaque value operations (Proposition 2).

Significance. If the results hold, the paper converts a pervasive, informally managed evaluation hazard into a checkable correctness property with a sharp decidability boundary. The identification with non-interference is substantive rather than cosmetic: it imports soundness technology, explains why detectors cannot certify absence, and yields a linear-time static discipline on the fragment practitioners actually use. Strengths include an explicit two-run logical relation and Causality Lemma for series operators, an honest relative-completeness ceiling for opaque value ops, a pre-registered empirical plan with bootstrap CIs, and a public clean-room artifact that separates proprietary figures from reproducible qualitative claims. Residual risks (pen-and-paper proofs, modeling gap to production code, trusted source stamps) are disclosed and do not erase the formal contribution.

major comments (3)
  1. Definition 4 (clauses 3–4) and §5.6: acceptance trusts that base series are availability-monotone at ingestion and that each resample rule ρ is causal (max ρ←(p) ⪯ ι(p)), both treated as O(1) local checks. The paper should specify the concrete representation of ρ under which causality is decidable in O(1) (e.g., fixed calendar maps vs. arbitrary functions), and state more explicitly that incorrect source stamps remain out of scope of the certificate. Without that, the linear-time claim and the deployment reading of Theorem 1 rest on an underspecified interface between data sources and the checker.
  2. §7, Theorem 3 (M3 and the reduction): the construction uses countably infinite series and an epoch quantifier over all t, with finite determination of each position by causality. The upper-bound argument that non-look-ahead-freedom is r.e. (finite witness of epoch plus two finite assignments) is plausible but compressed; a short clarification that evaluation of decide_t only inspects a finite prefix under the causal operators would make the Σ⁰₁ membership fully routine and remove any residual doubt about the Π⁰₁-completeness claim.
  3. §8.2–8.3 and the abstract: the empirical claim that the checker catches every planted leak that differential/tiling detectors miss is well supported on the adversarial corpus, but the real-data oracle validation (Table 1) uses non-redistributable proprietary series. The manuscript already ships synthetic stand-ins and carefully separates qualitative from proprietary figures; still, the abstract’s phrasing (“an independent oracle witnesses no leak in any accepted pipeline”) should be scoped to “on the evaluated archetypes / synthetic stand-ins,” so that the soundness corroboration is not read as independently re-runnable on the same market data.
minor comments (6)
  1. Figure 1 and §3: the dual coordinates (reference time vs availability) are central; a one-line example of a restated fundamental (reference t−1, availability t+5) early in §3.1 would make the distinction operational for readers outside information-flow security.
  2. Lemma 2 (effect ordering): the normalisation to max of mins of (t+c or av(x)+c) is sketched; a brief note that unit coefficients and fixed arities keep the comparison finite would help readers who implement the checker.
  3. §4.2 T-Stamp and the intransitive-flow citation [24]: the parallel is apt; a sentence linking the classical “permitted relabelling must not launder high values” slogan to the effect-preserving stamp rule would help non-security readers.
  4. §8.1 Axis 2: the normal-form blow-up at 64–128 literals is useful; stating a practical depth bound observed on the five archetypes (or that realistic as-of/join pipelines stay below, say, depth 4) would make the “bounded complexity” hypothesis concrete.
  5. References: several 2026 arXiv items are contemporaneous; ensure final versions or DOIs are updated at camera-ready, and that the DataFlow citation [27] is consistently positioned as the closest empirical detector rather than a competing formal system.
  6. Typographical: “Π0 1-hard” / “Π⁰₁” formatting is inconsistent across abstract, Theorem 3, and body; unify to Π⁰₁ throughout.

Circularity Check

0 steps flagged

No significant circularity: operational property, independent static discipline, and external undecidability reduction are cleanly separated.

full rationale

The paper defines look-ahead-freedom operationally as two-run agreement under ≈_t (Definition 8), then gives an independent type-and-effect system over a value-independent fragment F and proves soundness via a two-run logical relation plus the Causality Lemma (Theorem 1, Lemmas 4–6). Decidability is a separate linear-time claim (Theorem 2). Undecidability on the full language U is reduced from the external halting problem through value-conditioned availability (Theorem 3, M1–M3), not from any internal fit or self-definition. Relative completeness (Proposition 2) honestly bounds opaque value operations rather than claiming exact semantic completeness. Empirical results (scaling slope, adversarial corpus, dynamic oracle) corroborate the theorems; they do not force them. Self-citations to the author’s related point-in-time and decision-geometry work ([13], [14]) appear only as background in the applied-leakage literature and are not load-bearing premises of any theorem. No step reduces a claimed prediction or first-principles result to its own inputs by construction.

Axiom & Free-Parameter Ledger

2 free parameters · 6 axioms · 2 invented entities

The central theorems rest on a small set of domain modeling choices rather than fitted constants. The load-bearing ones are purity/totality of value operations, value-independence of availability in F, trusted monotone source stamps, and causal alignment of resample/join. Undecidability uses standard TM encoding assumptions on U. No numerical free parameters enter Theorems 1–3; empirical seeds and bootstrap draws affect only reported figures, not the formal claims.

free parameters (2)
  • adversarial corpus composition (33 leak / 20 clean; six mechanisms)
    Hand-designed stress set for Claim B; rates are existence/robustness evidence, not population estimates. Does not enter formal theorems.
  • oracle sampling epochs and seeds (e.g. seed 20260702)
    Affects which dynamic witnesses appear (AR3 case); does not affect static soundness theorem.
axioms (6)
  • domain assumption Assumption 1: every value operation f is total and pure—no side-channel access to base data, store, or availability.
    Licenses opaque treatment of f and relative completeness (Proposition 2); invoked throughout typing and soundness.
  • domain assumption Base series are availability-monotone as declared at ingestion; incorrect source stamps are out of scope.
    Definition 4 clause (3); Lemma 5 preserves Mono only from correct leaves.
  • domain assumption In fragment F, every availability term is drawn from sublanguage A (stamps, constants, max/min, +δ)—never from values.
    Definition 1; justified as matching real pipelines; membership is the decidable scope of Theorems 1–2.
  • standard math Time domain (T, ≤) is a total order; positions (Pos, ⪯) are totally ordered and distinct from availability.
    Section 3.1 and 5.1; standard setup for temporal lattices and series.
  • ad hoc to paper M1–M3 for undecidability: U admits value-conditioned Time terms; Val can encode TM configs; series may be countably infinite with causal operators.
    Section 7 modeling assumptions used only to characterize U, not claimed for F pipelines.
  • domain assumption Resample/join causal-alignment side conditions (max ρ←(p) ⪯ ι(p); common-position join).
    Definition 4 clause (4); turns classic resample leak into an O(1) check.
invented entities (2)
  • Time-indexed pipeline calculus with dual coordinates (reference time vs availability) and fragment F independent evidence
    purpose: Object language in which look-ahead-freedom is defined and checked
    New formal object for this paper; not a physical entity. Independent evidence is the operational semantics and theorems about it.
  • Effect as static upper bound on availability of base data flowing into a result independent evidence
    purpose: Static over-approximation enabling T-Decide obligation φ ⊑ t
    Standard type-and-effect idea specialized to temporal availability; evidence is soundness theorem and checker behavior.

pith-pipeline@v1.1.0-grok45 · 34687 in / 3739 out tokens · 36772 ms · 2026-07-11T10:55:00.596482+00:00 · methodology

0 comments
read the original abstract

Look-ahead bias (using information from after a decision epoch to make the decision at that epoch) is the dominant way a backtest or a machine-learning evaluation flatters a system that will disappoint in deployment. The field manages it with construct-specific recipes and empirical detectors, which are sound only channel by channel and certify nothing by their silence. We show that look-ahead-freedom is a formal property in disguise: fixing an epoch, the demand that the future not influence the present is temporal non-interference over a time-indexed information lattice. From this identification we develop a pipeline calculus separating a datum's availability from its reference time, and settle the problem's boundary. Where availability may depend on data values, look-ahead-freedom is undecidable (indeed Pi-0-1-hard): leakage is recursively enumerable but freedom is not. On the value-independent fragment (covering windowing, resampling, joins, point-in-time and vintage reads, and agentic retrieval) we give a type-and-effect system that is sound and decidable in linear time. An artifact confirms the theory: the check scales linearly, an independent oracle witnesses no leak in any accepted pipeline, and the checker catches every planted leak that differential and tiling detectors miss.

Figures

Figures reproduced from arXiv: 2607.04958 by Xavier Fonseca.

Figure 1
Figure 1. Figure 1: The two ideas the calculus is built on. (a) Every datum carries two independent temporal coordinates: [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Checker scaling. (a) Node-count scaling at bounded availability complexity: median check time versus [PITH_FULL_IMAGE:figures/full_fig_p023_2.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

36 extracted references · 12 canonical work pages · 5 internal anchors

  1. [1]

    Fernández-Moctezuma, Reuven Lax, Sam McVeety, Daniel Mills, Frances Perry, Eric Schmidt, and Sam Whittle

    Tyler Akidau, Robert Bradshaw, Craig Chambers, Slava Chernyak, Rafael J. Fernández-Moctezuma, Reuven Lax, Sam McVeety, Daniel Mills, Frances Perry, Eric Schmidt, and Sam Whittle. 2015. The Dataflow Model: A Practical Approach to Balancing Correctness, Latency, and Cost in Massive-Scale, Unbounded, Out-of-Order Data Processing.Proceedings of the VLDB Endow...

  2. [2]

    Rajeev Alur and David L. Dill. 1994. A Theory of Timed Automata.Theoretical Computer Science126, 2 (1994), 183–235. doi:10.1016/0304-3975(94)90010-8 ACM Trans. Softw. Eng. Methodol., Vol. 0, No. 0, Article 0. Publication date: July 2026. Look-Ahead-Freedom as Temporal Non-Interference: A Verifiable Correctness Property for Backtesting and Agentic Trading ...

  3. [3]

    Étienne André, Didier Lime, Dylan Marinho, and Jun Sun. 2022. Guaranteeing Timed Opacity using Parametric Timed Model Checking.ACM Transactions on Software Engineering and Methodology31, 4 (2022), 1–36. doi:10.1145/3502851

  4. [4]

    Bailey, Jonathan M

    David H. Bailey, Jonathan M. Borwein, Marcos López de Prado, and Qiji Jim Zhu. 2014. Pseudo-Mathematics and Financial Charlatanism: The Effects of Backtest Overfitting on Out-of-Sample Performance.Notices of the American Mathematical Society61, 5 (2014), 458–471. doi:10.1090/noti1105

  5. [5]

    Bailey, Jonathan M

    David H. Bailey, Jonathan M. Borwein, Marcos López de Prado, and Qiji Jim Zhu. 2017. The Probability of Backtest Overfitting.Journal of Computational Finance20, 4 (2017), 39–69. doi:10.21314/JCF.2016.322

  6. [6]

    Bailey and Marcos López de Prado

    David H. Bailey and Marcos López de Prado. 2014. The Deflated Sharpe Ratio: Correcting for Selection Bias, Backtest Overfitting, and Non-Normality.The Journal of Portfolio Management40, 5 (2014), 94–107

  7. [7]

    Mostapha Benhenda. 2026. Look-Ahead-Bench: A Standardized Benchmark of Look-Ahead Bias in Point-in-Time LLMs for Finance. arXiv:2601.13770 [cs.AI] doi:10.48550/arXiv.2601.13770

  8. [8]

    Brown, William Goetzmann, Roger G

    Stephen J. Brown, William Goetzmann, Roger G. Ibbotson, and Stephen A. Ross. 1992. Survivorship Bias in Performance Studies.The Review of Financial Studies5, 4 (1992), 553–580

  9. [9]

    James Cheney, Laura Chiticariu, and Wang-Chiew Tan. 2009. Provenance in Databases: Why, How, and Where. Foundations and Trends in Databases1, 4 (2009), 379–474. doi:10.1561/1900000006

  10. [10]

    Dorothy E. Denning. 1976. A Lattice Model of Secure Information Flow.Commun. ACM19, 5 (1976), 236–243. doi:10.1145/360051.360056

  11. [11]

    Denning and Peter J

    Dorothy E. Denning and Peter J. Denning. 1977. Certification of Programs for Secure Information Flow.Commun. ACM20, 7 (1977), 504–513. doi:10.1145/359636.359712

  12. [12]

    Abdelkader El Mahdaouy, Issam Ait Yahia, Soufiane Oualil, and Ismail Berrada. 2026. Deep Learning for Contextualized NetFlow-Based Network Intrusion Detection: Methods, Data, Evaluation and Deployment. arXiv:2602.05594 [cs.CR] doi:10.48550/arXiv.2602.05594

  13. [13]

    Xavier Fonseca. 2026. The Decision Geometry of Covariance Estimation for the Global Minimum-Variance Portfolio under Heavy Tails. arXiv:2606.27462 [stat.ML] doi:10.48550/arXiv.2606.27462

  14. [14]

    Xavier Fonseca. 2026. Point-in-Time Backtesting of Momentum-Trend Equity Strategies: A Formal Bias Taxonomy, ATR Trailing Stop Analysis, and Investor-Experience Metrics.Mathematics14, 12 (2026), 2182. doi:10.3390/math14122182

  15. [15]

    Guillaume Gardey, John Mullins, and Olivier H. Roux. 2007. Non-Interference Control Synthesis for Security Timed Automata.Electronic Notes in Theoretical Computer Science180, 1 (2007), 35–53. doi:10.1016/j.entcs.2005.05.046

  16. [16]

    Gifford and John M

    David K. Gifford and John M. Lucassen. 1986. Integrating Functional and Imperative Programming. InProceedings of the 1986 ACM Conference on LISP and Functional Programming (LFP ’86). ACM, New York, NY, USA, 28–38. doi:10.1145/ 319838.319848

  17. [17]

    Goguen and José Meseguer

    Joseph A. Goguen and José Meseguer. 1982. Security Policies and Security Models. In1982 IEEE Symposium on Security and Privacy. IEEE Computer Society, Los Alamitos, CA, USA, 11–20. doi:10.1109/SP.1982.10014

  18. [18]

    Shachar Kaufman, Saharon Rosset, Claudia Perlich, and Ori Stitelman. 2012. Leakage in Data Mining: Formulation, Detection, and Avoidance.ACM Transactions on Knowledge Discovery from Data6, 4, Article 15 (2012), 21 pages. doi:10.1145/2382577.2382579

  19. [19]

    Xiangyu Li, Yawen Zeng, Xiaofen Xing, Jin Xu, and Xiangmin Xu. 2025. Profit Mirage: Revisiting Information Leakage in LLM-based Financial Agents. arXiv:2510.07920 [cs.AI] doi:10.48550/arXiv.2510.07920

  20. [20]

    Guojun Liu, Doina Caragea, Xinming Ou, and Sankardas Roy. 2024. The Impact of Train–Test Leakage on Machine Learning-Based Android Malware Detection. arXiv:2410.19364 [cs.CR] doi:10.48550/arXiv.2410.19364

  21. [21]

    Lucassen and David K

    John M. Lucassen and David K. Gifford. 1988. Polymorphic Effect Systems. InProceedings of the 15th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL ’88). ACM, New York, NY, USA, 47–57. doi:10.1145/ 73560.73564

  22. [22]

    Phat Nguyen and Thang Pham. 2026. Toward Reliable Evaluation of LLM-Based Financial Multi-Agent Systems: Taxonomy, Coordination Primacy, and Cost Awareness. arXiv:2603.27539 [cs.MA] doi:10.48550/arXiv.2603.27539

  23. [23]

    1999.Principles of Program Analysis

    Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999.Principles of Program Analysis. Springer, Berlin, Heidelberg. doi:10.1007/978-3-662-03811-6

  24. [24]

    1992.Noninterference, Transitivity, and Channel-Control Security Policies

    John Rushby. 1992.Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02. SRI International, Menlo Park, CA

  25. [25]

    Andrei Sabelfeld and Andrew C. Myers. 2003. Language-Based Information-Flow Security.IEEE Journal on Selected Areas in Communications21, 1 (2003), 5–19. doi:10.1109/JSAC.2002.806121

  26. [26]

    Andrei Sabelfeld and David Sands. 2009. Declassification: Dimensions and Principles.Journal of Computer Security17, 5 (2009), 517–548. doi:10.3233/JCS-2009-0352

  27. [27]

    Giacinto Paolo Saggese and Paul Smith. 2025. DataFlow: A Framework for High-Performance Machine Learning Stream Computing. arXiv:2512.23977 [cs.LG] doi:10.48550/arXiv.2512.23977

  28. [28]

    Sarkar and Keyon Vafa

    Suproteem K. Sarkar and Keyon Vafa. 2025. Lookahead Bias in Pretrained Language Models. InICML 2025 Workshop on Reliable and Responsible Foundation Models (R2-FM). ACM Trans. Softw. Eng. Methodol., Vol. 0, No. 0, Article 0. Publication date: July 2026. 0:30 Xavier Fonseca

  29. [29]

    Mohit Tiwari, Hassan M. G. Wassel, Bita Mazloom, Shashidhar Mysore, Frederic T. Chong, and Timothy Sherwood

  30. [30]

    InProceedings of the 14th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’09)

    Complete Information Flow Tracking from the Gates Up. InProceedings of the 14th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’09). ACM, New York, NY, USA, 109–120. doi:10.1145/1508244.1508258

  31. [31]

    Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996. A Sound Type System for Secure Flow Analysis.Journal of Computer Security4, 2–3 (1996), 167–187. doi:10.3233/JCS-1996-42-304

  32. [32]

    Yihan Xia, Panpan You, Taotao Wang, Fang Liu, Han Qi, Xiaoxiao Wu, and Shengli Zhang. 2026. Agentic Trading: When LLM Agents Meet Financial Markets. arXiv:2605.19337 [cs.AI] doi:10.48550/arXiv.2605.19337

  33. [33]

    Junyi Yao and Zihao Zheng. 2026. Beyond Agent Architecture: Execution Assumptions and Reproducibility in LLM-Based Trading Systems. arXiv:2606.08285 [cs.AI] doi:10.48550/arXiv.2606.08285

  34. [34]

    Yuxuan Ye, Jun Han, Ao Hu, Juncheng Bu, Yiyi Chen, Liangjian Wen, Danilo Mandic, Danny Dongning Sun, Xu Yinghui, and Zenglin Xu. 2026. The Alpha Illusion: Reported Alpha from LLM Trading Agents Should Not Be Treated as Deployment Evidence. arXiv:2605.16895 [cs.CE] doi:10.48550/arXiv.2605.16895

  35. [35]

    Fan Zhang, Zhen Li, Sijia Peng, and Yu Chen. 2026. When Alpha Disappears: A One-Switch Benchmark for Decision- Time Leakage in Financial Backtests. arXiv:2605.23959 [q-fin.RM] doi:10.48550/arXiv.2605.23959

  36. [36]

    Zeyu Zhang, Ryan Chen, and Bradly C. Stadie. 2026. All Leaks Count, Some Count More: Interpretable Temporal Contamination Detection in LLM Backtesting. arXiv:2602.17234 [cs.AI] doi:10.48550/arXiv.2602.17234 ACM Trans. Softw. Eng. Methodol., Vol. 0, No. 0, Article 0. Publication date: July 2026