We introduce a novel computational unit for neural networks that features multiple biases, challenging the traditional perceptron structure. This unit emphasizes the importance of preserving uncorrupted information as it is passed from one unit to the next, applying activation functions later in the process with specialized biases for each unit. Through both empirical and theoretical analyses, we show that by focusing on increasing biases rather than weights, there is potential for significant enhancement in a neural network model’s performance. This approach offers an alternative perspective on optimizing information flow within neural networks. See source code [5].

Abstract We present our library for universal algebra in the UniMath framework dealing with multi-sorted signatures, their algebras and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic.

Abstract Static analysis of logic programs by abstract interpretation requires designing abstract operators which mimic the concrete ones, such as unification, renaming, and projection. In the case of goal-driven analysis, where goal-dependent semantics are used, we also need a backward-unification operator, typically implemented through matching. In this paper, we study the problem of deriving optimal abstract matching operators for sharing and linearity properties. We provide an optimal operator for matching in the domain $\mathtt{ShLin}^{\omega }$ , which can be easily instantiated to derive optimal operators for the domains $\mathtt{ShLin}^2$ by Andy King and the reduced product $\mathtt{Sharing} \times \mathtt{Lin}$ .

In the last years almost all families of programming languages, from imperative to functional, logic, object-oriented and machine code, have been subject to static analysis by abstract interpretation. The use of a principled approach to static analysis based on the theory of abstract interpretation provided mathematical tools to reason about program properties and allowed for the rigorous and incremental design of precise and scalable static analyzers, ensuring soundness by construction. The large variety of abstract domains for many different programming languages, the ability to combine and refine them with standard abstract interpretation tools and the availability of mature abstract domain libraries allowed easily porting, reusing and experimenting with techniques born in a specific family to other programming languages and properties.

In the last years, DeepMind algorithm AlphaZero has become the state of the art to efficiently tackle perfect information two-player zero-sum games with a win/lose outcome. However, when the win/lose outcome is decided by a final score difference, AlphaZero may play score-suboptimal moves, because all winning final positions are equivalent from the win/lose outcome perspective. This can be an issue, for instance when used for teaching, or when trying to understand whether there is a better move. Moreover, there is the theoretical quest of the perfect game. A naive approach would be training a AlphaZero-like agent to predict score differences instead of win/lose outcomes. Since the game of Go is deterministic, this should as well produce outcome-optimal play. However, it is a folklore belief that "this does not work".In this paper we first provide empirical evidence to this belief. We then give a theoretical interpretation of this suboptimality in a general perfect information two-player zero-sum game where the complexity of a game like Go is replaced by randomness of the environment. We show that an outcome-optimal policy has a different preference for uncertainty when it is winning or losing. In particular, when in a losing state, an outcome-optimal agent chooses actions leading to a higher variance of the score. We then posit that when approximation is involved, a deterministic game behaves like a nondeterministic game, where the score variance is modeled by how uncertain the position is. We validate this hypothesis in a AlphaZero-like software with a human expert.

Abstract Sharing analysis is used to statically discover data structures which may overlap in object-oriented programs. Using the abstract interpretation framework, we show that sharing analysis greatly benefits from linearity information. A variable is linear in a program state when different field paths starting from it always reach different objects. We propose a graph-based abstract domain which can represent aliasing, linearity, and sharing information and define all the necessary abstract operators for the analysis of a Java-like language.

We develop a new framework for the game of Go to target a high score, and thus a perfect play. We integrate this framework into the Monte Carlo tree search - policy iteration learning pipeline introduced by Google DeepMind with AlphaGo. Training on 9×9 Go produces a superhuman Go player, thus proving that this framework is stable and robust. We show that this player can be used to effectively play with both positional and score handicap. We develop a family of agents that can target high scores against any opponent, recover from very severe disadvantage against weak opponents, and avoid suboptimal moves.

Reasoning on a complex system in the abstract interpretation theory starts with a formal description of the system behavior specified by a collecting semantics. We take the common point of view that a collecting semantics is a very precise semantics from which other abstractions may be derived. We elaborate on both the concepts of precision and derivability, and introduce a notion of adequacy which tell us when a collecting semantics is a good choice for a given family of abstractions. We instantiate this approach to the case of first-order functional programs by considering three common collecting semantics and some abstract properties of functions. We study their relative precision and give a constructive characterization of the classes of abstractions which are adequate for the collecting semantics.

We propose a multiple-komi modification of the AlphaGo Zero/Leela Zero paradigm. The winrate as a function of the komi is modeled with a two-parameters sigmoid function, hence the winrate for all komi values is obtained, at the price of predicting just one more variable. A second novel feature is that training is based on self-play games that occasionaly branch -with changed komi- when the position is uneven. With this setting, reinforcement learning is shown to work on 7×7 Go, obtaining very strong playing agents. As a useful byproduct, the sigmoid parameters given by the network allow to estimate the score difference on the board, and to evaluate how much the game is decided. Finally, we introduce a family of agents which target winning moves with a higher score difference.

Abstract In the analysis of logic programs, abstract domains for detecting sharing properties are widely used. Recently, the new domain ${\mathtt{ShLin}^{\omega}}$ has been introduced to generalize both sharing and linearity information. This domain is endowed with an optimal abstract operator for single-binding unification. The authors claim that the repeated application of this operator is also optimal for multibinding unification. This is the proof of such a claim.

In the theory of abstract interpretation, a domain is complete when abstract computations are as precise as concrete computations. In addition to the standard notion of completeness, we introduce the concept of observational completeness. A domain is

Abstract In the analysis of logic programs, abstract domains for detecting sharing and linearity information are widely used. Devising abstract unification algorithms for such domains has proved to be rather hard. At the moment, the available algorithms are correct but not optimal; i.e., they cannot fully exploit the information conveyed by the abstract domains. In this paper, we define a new (infinite) domainShLinωwhich can be thought of as a general framework from which other domains can be easily derived by abstraction.ShLinωmakes the interaction between sharing and linearity explicit. We provide a constructive characterization of the optimal abstract unification operator onShLinω, and we lift it to two well-known abstractions ofShLinω, namely, to the classicalSharing×Linabstract domain and to the more preciseShLin2abstract domain by Andy King. In the case of single-binding substitutions, we obtain optimal abstract unification algorithms for such domains.

Abstract We face the problems of correctness, optimality, and precision for the static analysis of logic programs, using the theory of abstract interpretation. We propose a framework with a denotational, goal-dependent semantics equipped with two unification operators for forward unification (calling a procedure) and backward unification (returning from a procedure). The latter is implemented through a matching operation. Our proposal clarifies and unifies many different frameworks and ideas on static analysis of logic programming in a single, formal setting. On the abstract side, we focus on the domain sharing by Jacobs and Langen (The Journal of Logic Programming, 1992, vol. 13, nos. 2–3, pp. 291–314) and provide the best correct approximation of all the primitive semantic operators, namely, projection, renaming, and forward and backward unifications. We show that the abstract unification operators are strictly more precise than those in the literature defined over the same abstract domain. In some cases, our operators are more precise than those developed for more complex domains involving linearity and freeness.