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 →
Look-Ahead-Freedom as Temporal Non-Interference: A Verifiable Correctness Property for Backtesting and Agentic Trading Pipelines
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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)
- 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.
- §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.
- §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)
- 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.
- 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.
- §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.
- §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.
- 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.
- Typographical: “Π0 1-hard” / “Π⁰₁” formatting is inconsistent across abstract, Theorem 3, and body; unify to Π⁰₁ throughout.
Circularity Check
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
free parameters (2)
- adversarial corpus composition (33 leak / 20 clean; six mechanisms)
- oracle sampling epochs and seeds (e.g. seed 20260702)
axioms (6)
- domain assumption Assumption 1: every value operation f is total and pure—no side-channel access to base data, store, or availability.
- domain assumption Base series are availability-monotone as declared at ingestion; incorrect source stamps are out of scope.
- domain assumption In fragment F, every availability term is drawn from sublanguage A (stamps, constants, max/min, +δ)—never from values.
- standard math Time domain (T, ≤) is a total order; positions (Pos, ⪯) are totally ordered and distinct from availability.
- 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.
- domain assumption Resample/join causal-alignment side conditions (max ρ←(p) ⪯ ι(p); common-position join).
invented entities (2)
-
Time-indexed pipeline calculus with dual coordinates (reference time vs availability) and fragment F
independent evidence
-
Effect as static upper bound on availability of base data flowing into a result
independent evidence
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
Reference graph
Works this paper leans on
-
[1]
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]
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]
É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]
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
doi:10.1090/noti1105 2014
-
[5]
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]
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
2014
-
[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]
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
1992
-
[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]
Dorothy E. Denning. 1976. A Lattice Model of Secure Information Flow.Commun. ACM19, 5 (1976), 236–243. doi:10.1145/360051.360056
-
[11]
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]
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]
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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2606.27462 2026
-
[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]
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]
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
arXiv 1986
-
[17]
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]
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]
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]
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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2410.19364 2024
-
[21]
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
arXiv 1988
-
[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]
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]
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
1992
-
[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]
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]
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]
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
2025
-
[29]
Mohit Tiwari, Hassan M. G. Wassel, Bita Mazloom, Shashidhar Mysore, Frederic T. Chong, and Timothy Sherwood
-
[30]
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]
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]
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]
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]
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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2605.16895 2026
-
[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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2605.23959 2026
-
[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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2602.17234 2026
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.