{"id":"b65634c4-159e-4f0f-9b36-047ee28b2c8c","arxiv_id":"2501.00169","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":3.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A sketch showing how petri-net-style control flow and API resources of a deep learning training phase can be encoded as linear logic implications, with a proof of one reachability property.","lead":"This paper proposes using Linear Logic to model the control flow and resource usage of deep learning experiments, with a small hand-coded example showing how a training phase can be represented as a linear logic proof. It might matter because it sketches a lightweight way to statically check for resource misuse and data leakage in ML pipelines, though the full model is left for future work.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The model proves only control-flow reachability; the advertised data-provenance analysis is not representable in the propositional formulas, so the central validation claim is unsupported.","rationale":"The reader's weakest assumption is that the shallow petri-net/linear-logic model is a faithful abstraction of real DL experiment behavior, including data-provenance properties such as train/validation isolation, and that properties provable in the model transfer to the Python program. My stress-test confirms that this is the load-bearing gap. The formal proof in the paper is internally correct: the petri-net-to-propositional-linear-logic correspondence is well established in the cited literature, and the derivation of Π, M ⊢ e in Figure 3 is valid for the toy graph. The problem is not the logic but the expressiveness of the abstraction. The paper's own Section 2.1 admits that the propositional model must be extended to predicate linear logic, and Section 4 lists that extension as future work. Because the only resource token m carries no identity for the different dataset slices, the formulas cannot distinguish a correct experiment from one with training/validation leakage, even though that is the paper's central motivating scenario. The abstract's claim that artifacts are 'proofs in Linear Logic that can be readily verified by off-the-shelf reasoners' is therefore true only of the reachability proof, not of any data-provenance property. My concrete test would settle the concern by constructing a minimal buggy program that the current model provably cannot distinguish from a correct one. This supports the reader's REJECT verdict; no verdict adjustment is needed.","tokens_in":7333,"tokens_out":3010,"duration_ms":31307,"concrete_test":"Take the Figure 1 program and introduce a data-leak bug, e.g. make load_validation_slice return training data or augment the dataset before slicing so validation information enters training. Apply the Section 2.1 translation literally to both the buggy and the correct program. If, as the formal model suggests, the two translations produce the same Π and M (because slice identity is not represented), the analysis cannot detect the paper's motivating failure mode. The check is settled by implementing the translation in Celf and asking whether any proof differs between the two programs; if no proof differs, the central claim of data-provenance validation fails on this minimal case.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 2.1's translation (Figure 1) maps every place to one proposition: e, t, f1, f2, m. The three dataset slices named in the code—training_slice, validation_slice, testing_slice—are never given distinct formulas; the only data-related resource is the single token m. Consequently the sequent Π, M ⊢ e proved in Figure 3 is a reachability statement about a four-node control-flow graph, not a statement about data provenance. The abstract's claim that the model expresses 'reasoning rules about the correct consumption of resources during experiments' is not instantiated for the dataset-isolation property that motivates the paper; a program that leaks validation data into training would be encoded with the same formulas as a correct one. The paper itself defers the needed enrichment: 'a more detailed approach requires us to describe this model in predicate rather than propositional Linear Logic' (Section 2.1), and Section 4 lists the predicate model as future work. With no soundness theorem and no implementation of the predicate model, the central claim that the artifacts are verifiable proofs of DL experiment properties is unsupported; at most, a known encoding of petri-net reachability in propositional linear logic has been rehearsed.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes using a small fragment of propositional Linear Logic (⊗, &, ⊸, !) to model the control flow and resource usage of a deep learning experiment. It translates a toy Python training snippet into a Petri net and then into formulas π1–π4, and uses a sequent calculus to prove the reachability sequent Π, M ⊢ e. The paper claims that this yields a lightweight, visually understandable model whose artifacts are Linear Logic proofs that can be verified by off-the-shelf reasoners, and it defers a richer predicate-level model to future work. The main evidence is the single hand-constructed example in Figures 1 and 3.","tokens_in":7551,"tokens_out":6144,"duration_ms":62194,"significance":"If the method were realized as described, it would address a real reproducibility problem: preventing data leakage between training, validation, and testing slices and detecting incorrect API usage on accelerators. The paper is readable and honest about the toy nature of its example, and it explicitly acknowledges the need for a predicate-level model in future work. However, the current contribution is essentially a standard encoding of a Petri net into propositional Linear Logic applied to one snippet. The motivating data-provenance property is not representable in the formulas, no soundness or automation is given, and no verifier output is shown. The significance as a research contribution is therefore limited, though the direction may be worth exploring in a longer paper with a predicate model and a soundness argument.","major_comments":[{"comment":"The toy encoding does not model the data-provenance property that motivates the paper. The Python snippet introduces training_slice, validation_slice, and testing_slice, but the linear-logic formulas contain only the single resource token m; no formula distinguishes the dataset slices. Consequently, the same formulas and the same proof in Figure 3 describe a program that trains on validation data and one that does not. The paper itself acknowledges at the end of Section 2.1 that a 'more detailed approach requires us to describe this model in predicate rather than propositional Linear Logic', and Section 4 lists the predicate model as future work, confirming that the central validation claim is not established by the present example.","section":"Section 2.1, Figure 1"},{"comment":"The paper claims that the analysis abstracts a program into linear-logic expressions 'automatically derived from the program's source code' and that execution of the derived linear-logic program 'produces a proof (or disproof) of the experimental properties under investigation'. However, the translation in Figure 1 is manual, no algorithm is given for deriving formulas from Python source, and no soundness theorem relates provability in the logic to properties of the source program. Without such a theorem, the sequent Π, M ⊢ e only shows reachability inside the hand-built model, not a property of the actual experiment.","section":"Section 1, Section 2.1"},{"comment":"The paper claims that the artifacts are proofs that can be 'readily verified by off-the-shelf reasoners', but the calculus in Figure 2 is incomplete for the proofs shown. It omits the right-introduction rules for ⊸ and & and any rule for !, yet the formulas π1–π4 are !-boxed and the proof in Figure 3 uses them as antecedents. As printed, Figure 3 is not a derivation in the stated calculus. No Celf or other reasoner input/output is provided, so the claim of verifiability by off-the-shelf tools is not demonstrated.","section":"Section 3, Figure 2"}],"minor_comments":[{"comment":"The caption and the code annotations are visually confusing: the labels e, t, f1, f2, and m are placed next to code lines without explaining that they denote places in the Petri net; a table mapping code elements to propositions would help.","section":"Figure 1"},{"comment":"The simplified proof notation that omits Π from the left and the constant right-hand side is not formally defined as an inference relation, making it unclear how the simplified derivations relate to the sequent calculus of Figure 2.","section":"Section 3.1"},{"comment":"The proof in Figure 3 uses only π1, π2, and π3 for the f1 path; the f2 case is asserted to be symmetric, but the paper does not display how the &l(f1) choice is made, so the all-paths claim is not fully demonstrated.","section":"Section 3.1"},{"comment":"There are several typographical errors, including 'permance' for 'permanence' in Section 3.1, 'essense' for 'essence' in Section 3, and 'nowdays' for 'nowadays' in Section 4; these should be corrected.","section":"Throughout"}],"recommendation":"reject","confidential_remarks":"The paper is a short idea note rather than a complete research contribution. The central claims in the abstract go beyond what the toy example supports, and the manuscript itself identifies the needed predicate model as future work. If the journal accepts position papers, a major revision that substantially weakens the claims might be considered, but as a regular research submission the lack of soundness, automation, and data-provenance modeling is a blocking issue."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a clear, correct toy example, but the paper's central claim outruns what is actually modeled. The propositional encoding collapses the three dataset slices into a single token m, so the data-provenance problem that motivates the paper cannot even be expressed, let alone verified.\n\nWhat is new: the domain application. The paper takes the well-known Petri-net-to-propositional-linear-logic correspondence (Martí-Oliet and Meseguer 1989, properly cited) and maps a simplified DL training phase with its API resource m into a sequent. The exposition is genuinely clear: Figure 1 gives an easy visual and symbolic story, Figure 2 has the small sequent calculus, and Figure 3's proof is correct. The simplified rewriting notation in Section 3.1 is a nice touch. The motivation section honestly describes the data-leakage problem in DL experiments.\n\nThe soft spots are serious. The four propositions e, t, f1, f2 and the single resource m cannot represent training, validation, and testing slices as distinct entities. A program that trains on validation data would be encoded with the same formulas. The paper itself concedes the point in Section 2.1, deferring a predicate model, and Section 4 lists that as future work. The abstract's claim that the approach 'statically validates' experimental properties is therefore unsupported. There is also no automatic derivation from source code and no soundness theorem connecting the Petri-net abstraction to Python semantics. The reachability proof in Figure 3 shows that the hand-built model follows the intended path, which is a sanity check, not a validation of the approach.\n\nWho gets value: people thinking about what lightweight formal tools might do for ML reproducibility, and reading groups wanting an accessible example of linear logic applied outside pure theorem proving. As a research contribution it is a position statement with a toy demonstration; nothing here advances the theory or provides a usable tool.\n\nRecommendation: for a formal-methods journal this is a desk reject unless the predicate model is actually developed. For a workshop or short-paper track, it deserves a referee, because the core idea is worth airing and the writing is careful. If it is reviewed, the referee should press on Section 2.1 and ask what properties the propositional fragment can actually decide.","headline":"A clean, correct toy encoding of a DL training loop in propositional linear logic, but the advertised data-provenance validation is absent because the model cannot distinguish dataset slices.","tokens_in":8064,"tokens_out":3343,"would_cite":false,"duration_ms":35715,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B70","68Q85","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper argues that a small fragment of Linear Logic ($\\otimes$, $\\&$, $\\multimap$, $!$) can model the control flow, resources, and resource-consumption rules of deep learning experiments, turning verification questions into checkable…","keywords":["linear logic","deep learning experiments","petri nets","resource consumption","data provenance","program verification","proof search","static analysis"],"falsifier":"A concrete test is to take the paper's training template, deliberately let validation data flow into the training slice, translate the modified program by the same method, and run proof search on the resulting sequent. If a proof of $\\Pi, M \\vdash e$ still exists for the leaky version, the model fails to detect the data-provenance violation it was designed to prevent. A second test is to remove the resource token $m$ for the model or API from the initial state and check that the target sequent no longer proves; if it still proves, resource consumption is not being enforced.","tokens_in":7099,"feed_emoji":"🧠","tokens_out":7402,"duration_ms":68322,"temperature":0.7,"pith_summary":"The paper tries to establish that a small fragment of Linear Logic, built from multiplicative conjunction, additive choice, linear implication, and the bang operator, can serve as a lightweight formal model of deep learning experiments. It claims that this model expresses the control flow of an experiment, the resources it needs (dataset slices, model state, and API calls that touch accelerator hardware), and rules for how those resources may be consumed. A property such as “the training phase can complete and return control” becomes a sequent whose proof is the artifact of analysis, and off-the-shelf reasoners can verify that proof. The proposal matters because dataset leakage between training, validation, and test sets, and incorrect API usage that wastes or corrupts accelerator work, are common and expensive failures in practice.","feed_headline":"Linear logic models deep learning experiments as checkable proofs","feed_subtitle":"Control flow and accelerator API usage become resource formulas whose proofs verify whether an experiment is sound.","key_machinery":"The central object is a translation of a Petri net into propositional Linear Logic, relying on the known correspondence between Petri nets and Linear Logic. Petri net places become linear propositions, transitions become permanent linear implications (instructions), and the current state together with available APIs becomes a multiset of resources. The bang operator $!$ marks instructions that persist after use; $\\otimes$ groups the resources consumed on the left of an implication; $\\multimap$ expresses that one multiset of resources is replaced by another; and $\\&$ expresses a choice between alternative paths. Verification is then proof search: finding a derivation of the target sequent $\\Pi, M \\vdash e$ demonstrates that the experiment can reach the desired state with the available resources.","core_discovery":"The central claim is that control flow and resource consumption in a deep learning experiment can be represented as a propositional Linear Logic theory. In the running example, program statements become permanent linear implications such as $!(e \\multimap t)$ and $!(t \\otimes m \\multimap f_1\\&f_2)$, while the current execution point and the available model resources become a multiset of propositions $e, m$. The question of whether the training phase can successfully return becomes the reachability sequent $\\Pi, M \\vdash e$, where $\\Pi$ is the multiset of permanent implications; a derivation of this sequent is a proof that the property holds. The paper displays such a derivation for both execution paths, using the additive connective $\\&$ to enumerate the alternatives, and it argues that the same intuition extends to predicate Linear Logic for tracking the execution stack and consumed resources.","pith_inferences":["The paper leaves implicit that data-isolation requirements become non-reachability facts: a leaky path that consumes the validation token should make the clean sequent unprovable, a property that can be tested by extending the running example with a leaky transition.","A natural extension, not taken here, is to automate the source-to-formula translation; the paper builds the model by hand from one small program, so scaling depends on making the mapping compositional.","The model represents API and hardware calls as tokens in a single multiset, whereas real accelerator usage is concurrent and batched; adopting the full concurrent logical framework the paper points to as future work would be needed to catch overlap and race-style bugs."],"forward_implications":["Data-provenance requirements, such as keeping validation samples out of training, can be encoded as resource-consumption constraints and checked by proof search.","Every successful analysis produces a formal proof object, so a small, independently trusted prover can certify experimental properties without re-running the experiment.","Because permanent implications correspond to program statements and transient resources to memory and API state, the same mechanism covers control flow and resource accounting in one pass.","The Petri net rendering gives practitioners a visual counterpart of the logical model, making the analysis understandable without reading sequent calculus.","Moving from propositional to predicate Linear Logic, as the paper outlines, could track the execution stack and log which path was taken, extending the method to larger experiments."],"supporting_citations":[{"why":"Explains why Linear Logic models resources: contraction and weakening are disallowed, so facts are consumed rather than duplicated or dropped.","marker":"[5]"},{"why":"Introduces Linear Logic, the system the paper applies to deep learning experiments.","marker":"[6]"},{"why":"Supplies the formal correspondence between Petri nets and propositional Linear Logic that underlies the translation of the running example.","marker":"[11]"},{"why":"Defines Petri nets, the graphical model that gives the approach its visual component and its reachability reading.","marker":"[12]"},{"why":"Provides an off-the-shelf reasoner that can check the generated Linear Logic proofs, limiting the trusted software base.","marker":"[17]"},{"why":"The concurrent logical framework whose sequent calculus the paper adapts for its fragment of Linear Logic.","marker":"[20]"}],"fun_headline_variants":["Linear logic turns deep learning runs into verifiable proofs","Deep learning experiments as linear-logic proof obligations","Checkable proofs for deep learning via linear logic","Linear logic proof theory for sound deep learning","Modeling deep learning resource use with linear logic"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that properties proved in the linear-logic model are true of the actual Python experiment; the paper does not provide a formal soundness theorem connecting the source-code translation to the logical formulas.","fun_headline_variants_meta":{"raw":{"variants":["Linear logic turns deep learning runs into verifiable proofs","Deep learning experiments as linear-logic proof obligations","Checkable proofs for deep learning via linear logic","Linear logic proof theory for sound deep learning","Modeling deep learning resource use with linear logic"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000664,"raw_usage":{"total_tokens":3007,"prompt_tokens":897,"completion_tokens":2110,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":513,"completion_tokens_details":{"reasoning_tokens":2039}},"tokens_in":513,"tokens_out":2110,"duration_ms":14913,"temperature":1.0,"reasoning_tokens":2039,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T22:56:54.334812+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A concrete test is to take the paper's training template, deliberately let validation data flow into the training slice, translate the modified program by the same method, and run proof search on the resulting sequent. If a proof of $\\Pi, M \\vdash e$ still exists for the leaky version, the model fails to detect the data-provenance violation it was designed to prevent. A second test is to remove the resource token $m$ for the model or API from the initial state and check that the target sequent no longer proves; if it still proves, resource consumption is not being enforced.","supporting_citations":[{"cited_title":"Di Cosmo and D","cited_arxiv_id":null,"evidence_quote":"Explains why Linear Logic models resources: contraction and weakening are disallowed, so facts are consumed rather than duplicated or dropped."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces Linear Logic, the system the paper applies to deep learning experiments."},{"cited_title":"Martí-Oliet and J","cited_arxiv_id":null,"evidence_quote":"Supplies the formal correspondence between Petri nets and propositional Linear Logic that underlies the translation of the running example."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines Petri nets, the graphical model that gives the approach its visual component and its reachability reading."},{"cited_title":"Schack-Nielsen and C","cited_arxiv_id":null,"evidence_quote":"Provides an off-the-shelf reasoner that can check the generated Linear Logic proofs, limiting the trusted software base."},{"cited_title":"Watkins, I","cited_arxiv_id":null,"evidence_quote":"The concurrent logical framework whose sequent calculus the paper adapts for its fragment of Linear Logic."}],"review_version":1}