arXiv subjects

Marco Giunti

Publications and source records attributed to Marco Giunti.

9 recordsLinked to original sources

arXiv2026

The Transformer Revolution, Part 1: Dynamic Processing through Output-Weight Interconnections

We reinterpret Transformer inference by developing a functionally equivalent mechanical-structural description of its functional architecture. Parameterized transformations of token representations, or transforming concepts, are identified with simple neural networks organized through output-input and output-weight interconnections. This redescription makes explicit an organizational feature that is not equally salient in the standard matrix description: during inference, the outputs of some networks determine the weights, and hence the transformations, of others. These output-weight interconnections generate prompt-dependent dynamic transformations and give rise to Sequence-level Interactive Dynamic Parallel Processing (SIDPP). We show that the number of dynamic parameters grows linearly with prompt length and may become comparable to, or exceed, the number of static parameters fixed through training, a phenomenon we call strong prompt sensitivity. Philosophically, this shifts the conceptual picture of the Transformer from one centered on the static structure acquired through training to one that also treats the prompt-dependent transformations dynamically constructed during inference as constitutive features of its operation. GPT-4.5's recent Turing test results provide a behavioral illustration of this phenomenon. Finally, we identify biological mechanisms morphologically and functionally correspondent to output-weight interconnections, supporting the in-principle neural realizability of SIDPP and motivating Conjecture T: human neural systems may realize a functional architecture relevantly similar to that of the Transformer.

cs.AI↗

arXiv2025

ChatGPT-4 and other LLMs in the Turing Test: A Critical Analysis

This paper critically examines the recent publication "ChatGPT-4 in the Turing Test" by Restrepo Echavarría (2025), challenging its central claims regarding the absence of minimally serious test implementations and the conclusion that ChatGPT-4 fails the Turing Test. The analysis reveals that the criticisms based on rigid criteria and limited experimental data are not fully justified. More importantly, the paper makes several constructive contributions that enrich our understanding of Turing Test implementations. It demonstrates that two distinct formats, the three-player and two-player tests, are both valid, each with unique methodological implications. The work distinguishes between absolute criteria for passing the test--the machine's probability of incorrect identification equals or exceeds the human's probability of correct identification--and relative criteria--which measure how closely a machine's performance approximates that of a human--, offering a more nuanced evaluation framework. Furthermore, the paper clarifies the probabilistic underpinnings of both test types by modeling them as Bernoulli experiments--correlated in the three-player version and uncorrelated in the two-player version. This formalization allows for a rigorous separation between the theoretical criteria for passing the test, defined in probabilistic terms, and the experimental data that require robust statistical methods for proper interpretation. In doing so, the paper not only refutes key aspects of the criticized study but also lays a solid foundation for future research on objective measures of how closely an AI's behavior aligns with, or deviates from, that of a human being.

cs.AI↗

arXiv2025

Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report

Most works on session types take an equi-recursive approach and do not distinguish among a recursive type and its unfolding. This becomes more important in recent type systems which do not require global types, also known as generalised multiparty session types (GMST). In GMST, in order to establish properties as deadlock-freedom, the environments which type processes are assumed to satisfy extensional properties holding in all infinite sequences. This is a problem because: (1) the mechanisation of GMST and equi-recursion in proof assistants is utterly complex and eventually requires co-induction; and (2) the implementation of GMST in type checkers relies on model checkers for environment verification, and thus the program analysis is not self-contained. In this paper, we overcome these limitations by providing an iso-recursive typing system that computes the behavioural properties of environments. The type system relies on a terminating function named compliance that computes all final redexes of an environment, and determines when these redexes do not contain mismatches or deadlocks: compliant environments cannot go wrong. The function is defined theoretically by introducing the novel notions of deterministic LTS of environments and of environment closure, and can be implemented in mainstream programming languages and compilers. We showcase an implementation in OCaml by using exception handling to tackle the inherent non-determinism of synchronisation of branching and selection types. We assess that the implementation provides the desired properties, namely absence of mismatches and of deadlocks in environments, by resorting to automated deductive verification performed in tools of the OCaml ecosystem relying on Why3.

cs.PL↗

arXiv2023

Sound Atomicity Inference for Data-Centric Synchronization

Data-Centric Concurrency Control (DCCC) shifts the reasoning about concurrency restrictions from control structures to data declaration. It is a high-level declarative approach that abstracts away from the actual concurrency control mechanism(s) in use. Despite its advantages, the practical use of DCCC is hindered by the fact that it may require many annotations and/or multiple implementations of the same method to cope with differently qualified parameters. Moreover, the existing DCCC solutions do not address the use of interfaces, precluding their use in most object-oriented programs. To overcome these limitations, in this paper we present AtomiS, a new DCCC model based on a rigorously defined type-sound programming language. Programming with AtomiS requires only (atomic)-qualifying types of parameters and return values in interface definitions, and of fields in class definitions. From this atomicity specification, a static analysis infers the atomicity constraints that are local to each method, considering valid only the method variants that are consistent with the specification, and performs code generation for all valid variants of each method. The generated code is then the target for automatic injection of concurrency control primitives, by means of the desired automatic technique and associated atomicity and deadlock-freedom guarantees, which can be plugged-into the model's pipeline. We present the foundations for the AtomiS analysis and synthesis, with formal guarantees that the generated program is well-typed and that it corresponds behaviourally to the original one. The proofs are mechanised in Coq. We also provide a Java implementation that showcases the applicability of AtomiS in real-life programs.

cs.PL↗

arXiv2023

On using VeriFast, VerCors, Plural, and KeY to check object usage

Typestates are a notion of behavioral types that describe protocols for stateful objects, specifying the available methods for each state, in terms of a state machine. Usually, objects with protocol are either forced to be used in a linear way, which restricts what a programmer can do, or deductive verification is required to verify programs where these objects may be aliased. To evaluate the strengths and limitations of static verification tools for object-oriented languages in checking the correct use of shared objects with protocol, we present a survey on four tools for Java: VeriFast, VerCors, Plural, and KeY. We describe the implementation of a file reader and of a linked-list, check for each tool its ability to statically guarantee protocol compliance as well as protocol completion, even when objects are shared in collections, and evaluate the programmer's effort in making the code acceptable to these tools.

cs.LO↗

arXiv2022

Anticipation of Method Execution in Mixed Consistency Systems -- Technical Report

Distributed applications often deal with data with different consistency requirements: while a post in a social network only requires weak consistency, the user balance in turn has strong correctness requirements, demanding mutations to be synchronised. To deal efficiently with sequences of operations on different replicas of the distributed application, it is useful to know which operations commute with others and thus, when can an operation not requiring synchronisation be anticipated wrt other requiring it, thus avoiding unnecessary waits. Herein we present a language-based static analysis to extract at compile-time from code information on which operations can commute with which other operations and thus get information that can be used by the run-time support to decide on call anticipations of operations in replicas without compromising consistency. We illustrate the formal analysis on several paradigmatic examples and briefly present a proof-of-concept implementation in Java.

cs.SC↗

arXiv2015

Unlocking Blocked Communicating Processes

We study the problem of disentangling locked processes via code refactoring. We identify and characterise a class of processes that is not lock-free; then we formalise an algorithm that statically detects potential locks and propose refactoring procedures that disentangle detected locks. Our development is cast within a simple setting of a finite linear CCS variant â although it suffices to illustrate the main concepts, we also discuss how our work extends to other language extensions.

cs.PL↗

arXiv2012

Hide and New in the Pi-Calculus

In this paper, we enrich the pi-calculus with an operator for confidentiality (hide), whose main effect is to restrict the access to the object of the communication, thus representing confidentiality in a natural way. The hide operator is meant for local communication, and it differs from new in that it forbids the extrusion of the name and hence has a static scope. Consequently, a communication channel in the scope of a hide can be implemented as a dedicated channel, and it is more secure than one in the scope of a new. To emphasize the difference, we introduce a spy context that represents a side-channel attack and breaks some of the standard security equations for new. To formally reason on the security guarantees provided by the hide construct, we introduce an observational theory and establish stronger equivalences by relying on a proof technique based on bisimulation semantics.

cs.PL↗

arXiv2011

A type checking algorithm for qualified session types

We present a type checking algorithm for establishing a session-based discipline in the pi calculus of Milner, Parrow and Walker. Our session types are qualified as linear or unrestricted. Linearly typed communication channels are guaranteed to occur in exactly one thread, possibly multiple times; afterwards they evolve as unrestricted channels. Session protocols are described by a type constructor that denotes the two ends of one and the same communication channel. We ensure the soundness of the algorithm by showing that processes consuming all linear resources are accepted by a type system preserving typings during the computation and that type checking is consistent w.r.t. structural congruence.

cs.PL↗