Pith. sign in

REVIEW 3 major objections 4 minor 28 references

Trustworthiness Preservation by Copies of Machine Learning Systems

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2506.05203 v1 pith:SATLLSHO submitted 2025-06-05 cs.LO cs.LG

Leonardo Ceragioli , Giuseppe Primiero This is my paper
classification cs.LOcs.LG MSC 03B7003B4868T05
keywords trustworthinesspreservationprobabilisticqueriestypednaturaldeductionmachinelearningcopiesjustifiableequalweakalmost
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

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.

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 (3)
  1. [§5.2.2, Lemma 5.1] 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.
  2. [§2.2, Table 2; §5.2.2] 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.
  3. [§5.2.2, Lemma 5.2] 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.
minor comments (4)
  1. [Example 2.2] 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.
  2. [Theorem 4.2, proof] 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.
  3. [Definition 5.4] The prose of Definition 5.4 says 'b is a logical construction' but defines logical deconstruction; the wording should be corrected to 'logical deconstruction'.
  4. [Abstract and Introduction] There are several typos, e.g., 'behavour' in the abstract and 'maritual status' in Example 1.1; these should be corrected in a revision.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: trust-preservation theorems follow algebraically from the trust definitions; the acknowledged original-trust assumption is a scope limit, and the main risk is a correctness ambiguity in Lemma 5.1, not a circular derivation.

full rationale

The trust relations are defined directly as equalities or inequalities of output probabilities (Definitions 3.1-3.8, 5.5-5.11), and Theorems 5.1-5.5 are proved by composing those pointwise constraints through the deterministic probability functions of the I/E rules. No parameter is fitted to a subset of data and then renamed a prediction, and no theorem is obtained by assuming its own conclusion. The AtQuery rule imports learned probabilities as axioms, so the framework inherits any defect of the original system, but this is explicitly acknowledged as a scope limitation in Section 6: 'we have not discussed specific properties of the original system that we want to preserve in the copy... focusing only on the preservation of the output.' That is an input assumption, not a circular step. The paper does cite prior TPTND work by the same authors, but those citations (rule inspiration, implemented verification tools, related semantics) are not load-bearing for the preservation results, which are derived within the present calculus. The skeptic's counterexample is a proof-correctness concern, not a circularity: the proof of Lemma 5.1 claims that the last rule can be reconstructed univocally from the conclusion, while I×1 and I×2 in Table 2 can both yield σ▷⟨t,u⟩:(β×δ) with different probabilities from different leaves. If sustained, this would undermine the proof of Theorem 5.1 and hence Theorem 5.4, but it is a failure of the uniqueness argument, not a reduction of the theorem to its input. For these reasons the circularity finding is essentially clean, with only minor non-load-bearing self-citation.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

The framework has no fitted free parameters and introduces no new empirical entities. Its main assumptions are the standard probability axioms, the axiomatic import of ML output probabilities, the finite exhaustive mutually exclusive atomic value space, nonzero conditioning probabilities, independence for conjunction closure, and the external trustworthiness of the original.

assumptions (7)
  • standard math Probabilities satisfy the Kolmogorov axioms and the conditional probability identities used in the I/E rules.
    Used to justify the rules I/E for implication, conjunction, disjunction on the left, and negation on the left in Section 2.2.
  • domain assumption AtQuery: the ML system's output probabilities are axioms representing learned conditional probabilities.
    Table 1 imports the probabilities without checking them; the calculus verifies logical consequences and preservation, not the original's correctness.
  • domain assumption Each atomic target variable has a finite set of possible atomic values, assumed exhaustive and mutually exclusive.
    Stated at the start of Section 3 and used in Definitions 3.1 to 3.8; without exhaustivity and mutual exclusivity, the trust relations are not well-defined.
  • domain assumption Conditional probability rules require conditioning events with nonzero probability.
    The E-rules for conjunction in Table 2 carry provisos g != 0; zero-probability conditions would make divisions undefined.
  • domain assumption When closing target variables under conjunction, the target variables are mutually independent and do not occur in the query list.
    Corollaries 5.1 to 5.4 require this restriction to keep the same antecedent across the rule, limiting the generality of the preservation results.
  • domain assumption Atomic values for different atomic variables are always mutually disjoint.
    Appendix A assumes disjointness to define mutual exclusivity and the decision procedure for complex values.
  • domain assumption The original system is trustworthy or reliable as an external input.
    The paper transfers trust from original to copy; Section 6 acknowledges that specific properties of the original are not verified within the framework.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Trustworthiness Preservation by Copies of Machine Learning Systems." pith.science (2026). https://pith.science/paper/SATLLSHO

@misc{pith2026250605203,
  author       = {Pith},
  title        = {Pith review of: Trustworthiness Preservation by Copies of Machine Learning Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SATLLSHO}},
  note         = {Machine review of arXiv:2506.05203}
}
read the original abstract

A common practice of ML systems development concerns the training of the same model under different data sets, and the use of the same (training and test) sets for different learning models. The first case is a desirable practice for identifying high quality and unbiased training conditions. The latter case coincides with the search for optimal models under a common dataset for training. These differently obtained systems have been considered akin to copies. In the quest for responsible AI, a legitimate but hardly investigated question is how to verify that trustworthiness is preserved by copies. In this paper we introduce a calculus to model and verify probabilistic complex queries over data and define four distinct notions: Justifiably, Equally, Weakly and Almost Trustworthy which can be checked analysing the (partial) behaviour of the copy with respect to its original. We provide a study of the relations between these notions of trustworthiness, and how they compose with each other and under logical operations. The aim is to offer a computational tool to check the trustworthiness of possibly complex systems copied from an original whose behavour is known.

Figures

Figures reproduced from arXiv: 2506.05203 by the authors.

Figure 1
Figure 1. Components of an ML system and its application [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Entailment relations between notions of Trust and complementary conditions [PITH_FULL_IMAGE:figures/full_fig_p019_2.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages

  1. [1]

    and Jacobs, B

    Adams, R. and Jacobs, B. (2015). A type theory for probabilistic and bayesian reasoning. In Uustalu, T., editor, 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia , volume 69 of LIPIcs , pages 1:1--1:34. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik

    work page 2015

  2. [2]

    and Primiero, G

    Angius, N. and Primiero, G. (2018). The logic of identity and copy for computational artefacts. J. Log. Comput. , 28(6):1293--1322

    work page 2018

  3. [3]

    and Primiero, G

    Angius, N. and Primiero, G. (2023). Copying safety and liveness properties of computational artefacts. J. Log. Comput. , 33(5):1089--1117

    work page 2023

  4. [4]

    Bacci, G., Furber, R., Kozen, D., Mardare, R., Panangaden, P., and Scott, D. S. (2018). Boolean-valued semantics for the stochastic \( \) -calculus. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018 , pages 669--678

    work page 2018

  5. [5]

    Benk, M., Kerstan, S., von Wangenheim, F., and Ferrario, A. (2024). Twenty-four years of empirical research on trust in ai: A bibliometric review of trends, overlooked issues, and future directions. AI and Society , pages 1--24

    work page 2024

  6. [6]

    D., Gordon, A

    Borgstr \" o m, J., Lago, U. D., Gordon, A. D., and Szymczak, M. (2016). A lambda-calculus foundation for universal probabilistic programming. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 , pages 33--46

    work page 2016

  7. [7]

    Bori c i \'c , M. (2016). Inference rules for probability logic. Publications de l'Institut Math \'e matique , 100(114):77--86

    work page 2016

  8. [8]

    Bori c i \'c , M. (2017). Suppes-style sequent calculus for probability logic. Journal of Logic and Computation , 27(4):1157--1168

    work page 2017

Show all 28 references
  1. [9]

    Bori c i \'c , M. (2019). Sequent calculus for classical logic probabilized. Archive for Mathematical Logic , 58(1-2):119--136

    2019

  2. [10]

    and Giaretta, P

    Carrara, M. and Giaretta, P. (2001). Identity criteria and sortal concepts. In Proceedings of the international conference on Formal Ontology in Information Systems-Volume 2001 , pages 234--243

    2001

  3. [11]

    and Soavi, M

    Carrara, M. and Soavi, M. (2010). Copies, replicas, and counterfeits of artworks and artefacts. The Monist , 93(3):414--432

    2010

  4. [12]

    A., Genco, F

    Coraglia, G., D'Asaro, F. A., Genco, F. A., Giannuzzi, D., Posillipo, D., Primiero, G., and Quaggio, C. (2023). Brioxalkemy: a bias detecting tool. In Boella, G., D'Asaro, F. A., Dyoub, A., Gorrieri, L., Lisi, F. A., Manganini, C., and Primiero, G., editors, Proceedings of the...

    2023

  5. [13]

    A., Piantadosi, P., Bagli, E., Giuffrida, P., Posillipo, D., and Primiero, G

    Coraglia, G., Genco, F. A., Piantadosi, P., Bagli, E., Giuffrida, P., Posillipo, D., and Primiero, G. (2024). Evaluating ai fairness in credit scoring with the brio tool

    2024

  6. [14]

    Dastile, X., Celik, T., and Potsane, M. (2020). Statistical and machine learning models in credit scoring: A systematic literature survey. Applied Soft Computing , 91:106263

    2020

  7. [15]

    de Amorim, P. H. A., Kozen, D., Mardare, R., Panangaden, P., and Roberts, M. (2021). Universal semantics for the stochastic \( \) -calculus. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021 , pages 1--12

    2021

  8. [16]

    Di Pierro, A. (2020). A type theory for probabilistic--calculus. In From Lambda Calculus to Cybersecurity Through Program Analysis: Essays Dedicated to Chris Hankin on the Occasion of His Retirement , pages 86--102. Springer

    2020

  9. [17]

    A., Genco, F

    D’Asaro, F. A., Genco, F. A., and Primiero, G. (2025). Checking trustworthiness of probabilistic computations in a typed natural deduction system. Journal of Logic and Computation , page exaf003

    2025

  10. [18]

    Ghilezan, S., Iveti \'c , J., Ka s terovi \'c , S., Ognjanovi \'c , Z., and Savi \'c , N. (2018). Probabilistic reasoning about simply typed lambda terms. In International Symposium on Logical Foundations of Computer Science , pages 170--189. Springer

    2018

  11. [19]

    and Vickers, J

    Grieves, M. and Vickers, J. (2017). Digital twin: Mitigating unpredictable, undesirable emergent behavior in complex systems. Transdisciplinary perspectives on complex systems: New findings and approaches , pages 85--113

    2017

  12. [20]

    Henrique, B. M. and Santos, E. (2024). Trust in artificial intelligence: Literature review and main path analysis. Computers in Human Behavior: Artificial Humans , 2(1):100043

    2024

  13. [21]

    J., and Durresi, A

    Kaur, D., Uslu, S., Rittichier, K. J., and Durresi, A. (2022). Trustworthy artificial intelligence: A review. ACM Comput. Surv. , 55(2)

    2022

  14. [22]

    and Primiero, G

    Kubyshkina, E. and Primiero, G. (2024). A possible worlds semantics for trustworthy non-deterministic computations. International Journal of Approximate Reasoning , 172:109212

    2024

  15. [23]

    and Primiero, G

    Manganini, C. and Primiero, G. (2025). Philosophy of science for machine learning: Core issues and new perspectives , chapter Defining Formal Validity Criteria for Machine Learning Models. Springer

    2025

  16. [24]

    and D'Asaro, F

    Primiero, G. and D'Asaro, F. A. (2022). Proof-checking bias in labeling methods. In Boella, G., D'Asaro, F. A., Dyoub, A., and Primiero, G., editors, Proceedings of 1st Workshop on Bias, Ethical AI, Explainability and the Role of Logic and Logic Programming (BEWARE 2022) co-lo...

    2022

  17. [25]

    O., Angerschmid, A., Saranti, A., Schneeberger, D., Röttger, R., Müller, H., and Holzinger, A

    Retzlaff, C. O., Angerschmid, A., Saranti, A., Schneeberger, D., Röttger, R., Müller, H., and Holzinger, A. (2024). Post-hoc vs ante-hoc explanations: xai design guidelines for data scientists. Cognitive Systems Research , 86:101243

    2024

  18. [26]

    Semeraro, C., Lezoche, M., Panetto, H., and Dassisti, M. (2021). Digital twin paradigm: A systematic literature review. Computers in Industry , 130:103469

    2021

  19. [27]

    Termine, A., Primiero, G., and D'Asaro, F. A. (2021). Modelling accuracy and trustworthiness of explaining agents. In Ghosh, S. and Icard, T., editors, Logic, Rationality, and Interaction , pages 232--245, Cham. Springer International Publishing

    2021

  20. [28]

    Warrell, J. H. (2016). A probabilistic dependent type system based on non-deterministic beta reduction. CoRR , abs/1602.06420

    2016 arXiv

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.