{"id":"4367b967-de63-4e1d-bdd9-b3fc919f4556","arxiv_id":"2506.05203","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new typed natural deduction calculus defines four grades of trustworthiness for copies of ML systems and proves preservation under logical query composition.","lead":"This paper creates a logic, TNDPQ, for checking whether a machine learning model that is retrained or swapped for another algorithm still preserves the behavior of a trusted original model on relevant outputs. It defines four grades of trustworthiness between an original and a copy, and proves when those grades survive logical combinations of queries.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Counterexample to Lemma 5.1: the two conjunction introduction rules derive the same conclusion with different probabilities from identical leaves, invalidating Theorem 5.1.","rationale":"The reader's weakest assumption was that the trust relations inherit any defect of the original system's probabilities, a limitation the authors acknowledge in Section 6. The reader also noted in the rationale that Lemma 5.1's univocality claim is a proof gap, but did not identify the concrete counterexample. My stress-test found a strictly stronger, internal objection: Lemma 5.1 is not merely unproven but false. The two introduction rules for conjunction allow the same conclusion, σ▷⟨t,u⟩:β×δ, to be derived with different probabilities from the same multiset of leaf judgments. Since Definition 5.3 defines logical construction by existence of a derivation, both derivations qualify, and the equality of leaf probabilities for original and copy does not force equality of the constructed conclusion probabilities. This directly invalidates Theorem 5.1 ('Logical Construction and Deconstruction Preserve JT') and Theorem 5.4, which relies on Lemma 5.1. It also exposes a deeper issue: because the calculus is not confluent, a complex query may have several derivable probabilities, so statements like 'the copy attributes probability r to δ' are ambiguous. This is not a matter of external consensus or of the original being untrustworthy; it is a formal inconsistency in the proof system that the paper's central verification claim depends on. The concrete test—deriving the same conjunction via I×1 and I×2 from fixed leaves and comparing the probabilities—settles the matter directly and can be checked by hand. Given that the central preservation result for Justifiable Trustworthiness is falsified by this counterexample, the paper's main claim as stated does not hold; the framework might be repairable by imposing a canonical derivation strategy or by redefining logical construction relative to a chosen derivation, but that is a substantive revision, not a typographical fix.","tokens_in":34618,"tokens_out":8543,"duration_ms":97660,"concrete_test":"Construct derivations for σ▷⟨t,u⟩:β×δ from the fixed leaf set {σ▷t:β=0.2, σ▷u:δ=0.8, σ,t:β▷u:δ=0.9, σ,u:δ▷t:β=0.4}: apply I×1 to the first and third leaves, obtaining probability 0.18, and I×2 to the second and fourth leaves, obtaining probability 0.32. Under Definition 5.3, both are logical constructions from the same starting judgments. If both derivations are admitted, Lemma 5.1 is false, Theorem 5.1 collapses, and the calculus lacks confluence.","verdict_should_be":"REJECT","load_bearing_attack":"The most load-bearing flaw is internal to the calculus: Lemma 5.1 ('Construction and Deconstruction Preserve Identity') is false as stated. Its proof relies on the claim that the last rule applied can be reconstructed univocally from the conclusion's variable and value. But I×1 and I×2 in Table 2 can both conclude σ▷⟨t,u⟩:β×δ, with different probabilities. Concretely, from leaves σ▷t:β_{0.2} and σ,t:β▷u:δ_{0.9}, I×1 yields 0.18; from σ▷u:δ_{0.8} and σ,u:δ▷t:β_{0.4}, I×2 yields 0.32. These four leaf judgments can be placed in the starting sets A and B with pointwise equal probabilities, satisfying Lemma 5.1's assumptions, yet c and d share the target variable ⟨t,u⟩ and value β×δ with different probabilities. Hence Theorem 5.1, and Theorem 5.4 which invokes Lemma 5.1, do not follow. Moreover, two derivations of the same judgment with different probabilities mean TNDPQ is not confluent; the probability of a complex query is not well-defined, undermining the verification claims. This is distinct from the acknowledged limitation about the original's trustworthiness: it is a correctness problem inside the formalism, not merely a scope restriction.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces TNDPQ, a typed natural deduction calculus for probabilistic queries over machine-learning systems, and uses it to define four notions of trustworthiness for copies of an ML system: Justifiably, Equally, Weakly, and Almost Trustworthy. It studies entailment relations and compositions of these trust notions, and states preservation theorems claiming that logical construction and deconstruction of queries preserve trustworthiness. The central positive claim is that if a copy is trustworthy at the atomic-query level, the logical composition of queries carries that trust to the copy. The paper also includes a decision procedure for mutual exclusivity of outputs and discusses limits of the approach in Section 6.","tokens_in":34832,"tokens_out":12725,"duration_ms":147397,"significance":"If the preservation theorems were correct, the paper would offer a proof-theoretic method for verifying trustworthiness preservation under model copying, a relevant problem for ML reuse and digital twins. The paper has several strengths: it makes the components of an ML system explicit in the syntax, it distinguishes four graded trust notions with clear definitions, it gives negative composition results, and it provides a nontrivial decision procedure for mutual exclusivity. The authors also explicitly acknowledge that they only address output preservation, not fairness or correctness of the original. However, the central preservation results currently rest on a false or at least unproven uniqueness lemma, so the main positive claim is not established as the manuscript stands.","major_comments":[{"comment":"Lemma 5.1 is false as stated. Its proof claims that the last rule applied can be reconstructed univocally from the target variable and value of the conclusion, but Table 2 contains two introduction rules for conjunction, I×1 and I×2, with the same conclusion σ ▷ ⟨t,u⟩ : (β × δ). From the four premises σ ▷ t:β_{0.2}, σ,t:β ▷ u:δ_{0.9}, σ ▷ u:δ_{0.8}, and σ,u:δ ▷ t:β_{0.4}, I×1 derives the conclusion with probability 0.18 while I×2 derives it with probability 0.32. These premises can be included, with identical probabilities, in both starting sets A and B; the two constructions have the same target variable ⟨t,u⟩ and the same value β×δ but different probabilities. Hence g = h is not forced. Since Theorems 5.1, 5.3, and 5.4 rely on Lemma 5.1 or on its univocal-reconstruction reasoning, those preservation results are not established.","section":"§5.2.2, Lemma 5.1"},{"comment":"The same counterexample shows that TNDPQ is not confluent: a single judgment can have two derivations from the same atomic assumptions with different probabilities. Thus the probability of a logically complex query is not well-defined in the calculus as presented. This is a correctness problem internal to the formalism, not the scope limitation acknowledged in Section 6. The authors should either impose and explicitly state a global coherence condition on the probabilities imported by AtQuery so that the two conjunction-introduction rules compute the same joint probability, or modify the definitions of logical construction and deconstruction to record the derivation used, or prove a confluence result under the intended semantics.","section":"§2.2, Table 2; §5.2.2"},{"comment":"Lemma 5.2, used in Theorem 5.2, is also false under the natural reading of the construction relation. For example, take A-premises t:β_{0.1}, σ,t:β▷u:δ_{0.1}, u:δ_{0.9}, σ,u:δ▷t:β_{0.9}, and B-premises with the same values but probabilities 0.05, 0.05, 0.89, 0.89, so that every A-probability is at least the corresponding B-probability. A can construct ⟨t,u⟩:(β×δ) via I×1 with probability 0.01, while B can construct the same judgment via I×2 with probability 0.7921, violating the lemma's conclusion f_{n+1} ≥ g_{n+1}. Unless the authors restrict the construction relation to force the same rule to be used, Theorem 5.2 is unsupported as well.","section":"§5.2.2, Lemma 5.2"}],"minor_comments":[{"comment":"The prose says the subject has a probability of 0.65 of receiving a loan, but the displayed judgment gives 0.60; the numbers should be aligned.","section":"Example 2.2"},{"comment":"The subscript in f^{i+1}_{m+k} = 1/2 f^i_k appears to be a typo for k; as written, the index m+k is unexplained and seems inconsistent with the surrounding equations.","section":"Theorem 4.2, proof"},{"comment":"The prose of Definition 5.4 says 'b is a logical construction' but defines logical deconstruction; the wording should be corrected to 'logical deconstruction'.","section":"Definition 5.4"},{"comment":"There are several typos, e.g., 'behavour' in the abstract and 'maritual status' in Example 1.1; these should be corrected in a revision.","section":"Abstract and Introduction"}],"recommendation":"major_revision","confidential_remarks":"The paper leans heavily on self-citations to the authors' TPTND framework, but the core preservation claim is logically independent of those cited results, so I do not see that as a blocking issue. The blocking issue is technical: the preservation theorems are not sound as stated because of the non-uniqueness of derivations under the two conjunction introduction rules. If the authors can repair this by adding a coherence condition or by making the construction relation derivation-sensitive, the paper could become publishable. As it stands, the main positive results are not yet supported."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Give it a read if you care about formal trust verification for ML. The paper introduces TNDPQ, a natural deduction calculus for probabilistic queries over ML systems, and defines four notions of trustworthiness preservation between an original model and its copies: justifiably, equally, weakly, almost. The problem is real and the four notions are natural; Section 4's entailment and composition results are mostly straightforward but correctly argued. The authors are also honest that the calculus only preserves output behavior, not fairness or correctness of the original.\n\nThe soft spot is load-bearing. The calculus is not confluent. Two different conjunction introductions can derive the same conclusion from the same leaf judgments with different probabilities. Example: from σ▷t:β_{0.2} and σ,t:β▷u:δ_{0.9}, I×1 gives ⟨t,u⟩:(β×δ)_{0.18}; from σ▷u:δ_{0.8} and σ,u:δ▷t:β_{0.4}, I×2 gives the same judgment with probability 0.32. Place all four leaves in both premise sets; Lemma 5.1's assumptions hold and its conclusion fails. The lemma's proof says the last rule is recoverable from the target variable and value—false, since I×1 and I×2 leave identical traces. Theorem 5.1 (JT preservation) and Theorem 5.4 (ET deconstruction) depend on Lemma 5.1 and collapse. The AT and WT preservation theorems (5.2, 5.5) are also in jeopardy because 'the probability of a complex query' is not well-defined without a normalization or canonical derivation strategy. This is not a scope restriction; it is a bug inside the formalism.\n\nMinor issues: Theorem 4.2's statement contains an indexing slip, and the proof sketches in the corollaries are terse. These are easy to fix, unlike the confluence problem.\n\nWho is this for? Researchers working on probabilistic logics, formal verification of ML, and trust/digital twins. The conceptual framing is worth engaging with; the current proof system is not yet a sound basis for verification claims. I would send it to peer review, but flag a major revision: the authors need to either prove confluence, impose a canonical evaluation order, or downgrade the preservation theorems to statements about specific derivation paths. With that, the paper could be solid.","headline":"The paper offers a useful problem setup and four sensible trust notions, but the core preservation theorems rest on a false univocality claim because the calculus is non-confluent.","tokens_in":35382,"tokens_out":4125,"would_cite":false,"duration_ms":48404,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B70","03B48","68T05"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that trustworthiness of a machine-learning system is preserved by its copies under logical construction and deconstruction of probabilistic queries, as certified by the TNDPQ calculus.","keywords":["trustworthiness preservation","probabilistic queries","typed natural deduction","machine learning copies","justifiable trustworthiness","equal trustworthiness","weak trustworthiness","almost trustworthiness"],"falsifier":"Take a concrete pair of probability vectors where the copy dominates the original on all relevant atomic values but, for some formula built from these values using only implication, conjunction, and disjunction, the copy's probability falls below the original's; a single such instance would falsify the Almost Trust and Weak Trust construction theorems. Exhaustively enumerating small finite distributions and all formulas up to a fixed complexity would settle whether the preservation holds without hidden conditions.","tokens_in":34374,"feed_emoji":"🤖","tokens_out":6864,"duration_ms":73587,"temperature":0.7,"pith_summary":"This paper addresses a practical question: when a machine-learning model is copied, either by retraining on different data or by using a different learning algorithm on the same data, does the copy inherit the original's trustworthiness? The authors introduce TNDPQ, a typed natural-deduction calculus that turns an ML system's learned output probabilities into axioms and lets complex queries be decomposed and recomposed logically. They define four degrees of trustworthiness for copies, justifiable, equal, weak, and almost trust, and prove how these notions relate, compose, and behave under logical operations. The central results are preservation theorems: logical construction and deconstruction preserve justifiable trust, construction with implication, conjunction, and disjunction preserves almost and weak trust, and construction and deconstruction preserve equal trust. If these theorems are correct, a copy can inherit trust from an original on logically complex queries without re-evaluating every query from scratch.","feed_headline":"Logic carries trust from ML originals to their copies","feed_subtitle":"A new calculus verifies that justifiable, equal, weak and almost trust survive logical construction of queries.","key_machinery":"The central machinery is the calculus TNDPQ, Typed Natural Deduction for Probabilistic Queries. Its key device is the AtQuery rule, which imports an ML system's learned conditional probability as an axiom, and the logical rules for implication, conjunction, disjunction, and negation, which compose and decompose judgments; the inversion principle generates elimination rules from introduction rules. Logical construction and logical deconstruction are defined as deriving a judgment using only right introduction or right elimination rules. This machinery does the work of stating precisely what it means for a copy to agree with its original on a query and of proving that the four trust relations are closed under those operations.","core_discovery":"The core discovery, in the paper's own terms, is that trustworthiness is a compositional property of probabilistic queries over an ML system. TNDPQ represents each learned conditional probability as an atomic judgment via the AtQuery rule, and its logical rules compose and decompose these judgments. Against this background the paper defines four trust relations between an original and a copy: Justifiably Trustworthy (all output probabilities equal), Equally Trustworthy (equality on a chosen subset of values), Weakly Trustworthy (same support and no lower probability on relevant values), and Almost Trustworthy (no lower probability on relevant values, with support allowed to vary). The preservation theorems state that logical construction and deconstruction preserve Justifiable Trust, construction and deconstruction preserve Equal Trust, construction with implication, conjunction, and disjunction preserves Almost Trust and Weak Trust, while Almost Trust is not preserved under deconstruction and so Weak Trust is not preserved under deconstruction either.","pith_inferences":["Because AtQuery treats the original's output probabilities as axioms, the framework certifies behavioral agreement rather than ground truth; a copy of a biased original is certified as just as biased, which is a limit of the method as much as a feature.","The preservation theorems suggest a feasible verification shortcut: compare atomic output probability vectors between original and copy, then compute trust for complex queries symbolically instead of querying the deployed model for every composite condition.","The same preservation schema could be adapted to other quantitative properties, such as calibration, uncertainty, or robustness bounds, by replacing the four trust relations with analogous inequality relations and re-deriving the lemmas.","The account connects naturally to digital twins: if a simulation is a logical construction of a verified physical-system model, the twin's trustworthiness could be certified from the original without a full independent evaluation."],"forward_implications":["A verified Justifiably Trustworthy copy can be trusted on any query built from trusted atomic queries by logical construction or deconstruction, so complex composite queries inherit trust without renewed model evaluation.","For Almost and Weak Trust, inheritance holds when queries are composed with implication, conjunction, and disjunction, but negation and logical deconstruction break the guarantee, so verification tools must restrict themselves to the permitted constructions.","The hierarchy of trust relations, with Justifiable Trust at the top and Almost Trust at the bottom, gives a graded certification: checking Almost Trust is the weakest guarantee, checking Justifiable Trust the strongest.","Repeatedly composing trust relations never raises the degree of trustworthiness, so conservation, not amplification, is the appropriate expectation when copying systems."],"supporting_citations":[{"why":"Parent calculus TPTND whose trust rules and natural-deduction structure TNDPQ extends to probabilistic queries.","marker":"D’Asaro et al., 2025"},{"why":"Relational semantics for TPTND, providing the trust evaluations that TNDPQ imports as atomic probabilities.","marker":"Kubyshkina and Primiero, 2024"},{"why":"Non-symmetric entropy measures for divergence and bias that motivate the trustworthiness criteria.","marker":"Primiero and D’Asaro, 2022"},{"why":"Formal theory of identity and copy for computational artefacts underlying the notion of copies.","marker":"Angius and Primiero, 2018"},{"why":"Results on preservation of safety and liveness properties by inexact and approximate copies that the trust-preservation theorems generalize.","marker":"Angius and Primiero, 2023"},{"why":"Weak morphisms for ML model copies, which motivate weak forms of trust such as Weak and Almost Trustworthiness.","marker":"Manganini and Primiero, 2025"}],"fun_headline_variants":["Trust survives logical copying of ML models","Calculus verifies trust preservation between ML originals and copies","Four trust notions are compositional for ML copies","Trust preservation by logical construction in ML","A new calculus checks four types of trust in ML copies"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole verification inherits the original system's output probabilities through the AtQuery rule, so if the original is biased, miscalibrated, or wrong, every preserved trust relation merely certifies that the copy behaves like that flawed original.","fun_headline_variants_meta":{"raw":{"variants":["Trust survives logical copying of ML models","Calculus verifies trust preservation between ML originals and copies","Four trust notions are compositional for ML copies","Trust preservation by logical construction in ML","A new calculus checks four types of trust in ML copies"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000434,"raw_usage":{"total_tokens":2192,"prompt_tokens":905,"completion_tokens":1287,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":521,"completion_tokens_details":{"reasoning_tokens":1216}},"tokens_in":521,"tokens_out":1287,"duration_ms":12612,"temperature":1.0,"reasoning_tokens":1216,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T10:22:50.281783+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a concrete pair of probability vectors where the copy dominates the original on all relevant atomic values but, for some formula built from these values using only implication, conjunction, and disjunction, the copy's probability falls below the original's; a single such instance would falsify the Almost Trust and Weak Trust construction theorems. Exhaustively enumerating small finite distributions and all formulas up to a fixed complexity would settle whether the preservation holds without hidden conditions.","supporting_citations":[{"cited_title":"A., Genco, F","cited_arxiv_id":null,"evidence_quote":"Parent calculus TPTND whose trust rules and natural-deduction structure TNDPQ extends to probabilistic queries."},{"cited_title":"and Primiero, G","cited_arxiv_id":null,"evidence_quote":"Relational semantics for TPTND, providing the trust evaluations that TNDPQ imports as atomic probabilities."},{"cited_title":"and D'Asaro, F","cited_arxiv_id":null,"evidence_quote":"Non-symmetric entropy measures for divergence and bias that motivate the trustworthiness criteria."},{"cited_title":"and Primiero, G","cited_arxiv_id":null,"evidence_quote":"Formal theory of identity and copy for computational artefacts underlying the notion of copies."},{"cited_title":"and Primiero, G","cited_arxiv_id":null,"evidence_quote":"Results on preservation of safety and liveness properties by inexact and approximate copies that the trust-preservation theorems generalize."},{"cited_title":"and Primiero, G","cited_arxiv_id":null,"evidence_quote":"Weak morphisms for ML model copies, which motivate weak forms of trust such as Weak and Almost Trustworthiness."}],"review_version":1}