arXiv subjects

Gianluca Amato

Publications and source records attributed to Gianluca Amato.

15 recordsLinked to original sources

arXiv2026

Experimental evaluation of optimal abstract operators for sharing and linearity analysis

In the field of static analysis of logic programs, the optimality of abstract operators is a valuable theoretical property, as it provides insight into the structure of abstract domains and the maximum precision that can be achieved. However, implementing optimal operators is often complex and may significantly impact performance, giving rise to a trade-off between precision and efficiency. We experimentally investigate this trade-off in the context of sharing and linearity analysis of logic programs. Our experiments build on previous work that proposed several optimal operators for unification and matching. We have implemented these abstract operators and the corresponding abstract domains within the PLAI analyzer, part of the CiaoPP preprocessor, and we report the impact of increasing operator precision on the accuracy and performance of the overall analysis.

cs.LO↗

arXiv2024

Optimal matching for sharing and linearity analysis

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}^ω}$, 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}$.

cs.PL↗

arXiv2024

Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog

This paper introduces a model theory for resolution on Higher Order Hereditarily Harrop formulae (HOHH), the logic underlying the Lambda-Prolog programming language, and proves soundness and completeness of resolution. The semantics and the proof of completeness of the formal system is shown in several ways, suitably adapted to deal with the impredicativity of higher-order logic, which rules out definitions of truth based on induction on formula structure. First, we use the least fixed point of a certain operator on interpretations, in the style of Apt and Van Emden, Then a constructive completeness theorem is given using a proof theoretic variant of the Lindenbaum algebra, which also contains a new approach to establishing cut-elimination.

cs.PL↗

arXiv2024

Increasing biases can be more efficient than increasing weights

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 at https://github.com/CuriosAI/dac-dev.

cs.NE↗

arXiv2023

Artificial intelligence and renegotiation of commercial lease contracts affected by pandemic-related contingencies from Covid-19. The project A.I.A.Co

This paper aims to investigate the possibility of using artificial intelligence (AI) to resolve the legal issues raised by the Covid-19 emergency about the fate of continuing execution contracts, or those with deferred or periodic execution, as well as, more generally, to deal with exceptional events and contingencies. We first study whether the Italian legal system allows for ''maintenance'' remedies to cope with contingencies and to avoid the termination of the contract, while ensuring effective protection of the interests of both parties. We then give a complete and technical description of an AI-based predictive framework, aimed at assisting both the Magistrate (in the course of litigation) and the parties themselves (in out-of-court proceedings) in the redetermination of the rent of commercial lease contracts. This framework, called A.I.A.Co. for Artificial Intelligence for contract law Against Covid-19, has been developed under the Italian grant ''Fondo Integrativo Speciale per la Ricerca''.

cs.AI↗

arXiv2023

Score vs. Winrate in Score-Based Games: which Reward for Reinforcement Learning?

In the last years, the 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 for the perfect game. A naive approach would be training an AlphaZero-like agent to predict score differences instead of win/lose outcomes. Since the game of Go is deterministic, this should as well produce an outcome-optimal play. However, it is a folklore belief that "this does not work". In this paper, we first provide empirical evidence for this belief. We then give a theoretical interpretation of this suboptimality in general perfect information two-player zero-sum game where the complexity of a game like Go is replaced by the 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 score variance. 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 AlphaZero-like software with a human expert.

cs.AI↗

arXiv2020

Universal Algebra in UniMath

We present an ongoing effort to implement Universal Algebra in the UniMath system. Our aim is to develop a general framework for formalizing and studying Universal Algebra in a proof assistant. By constituting a formal system for isolating the invariants of the theory we are interested in -- that is, general algebraic structures modulo isomorphism -- Univalent Mathematics seems to provide a suitable environment to carry on our endeavour.

cs.LO↗

arXiv2019

SAI: a Sensible Artificial Intelligence that plays with handicap and targets high scores in 9x9 Go (extended version)

We develop a new model that can be applied to any perfect information two-player zero-sum game to target a high score, and thus a perfect play. We integrate this model into the Monte Carlo tree search-policy iteration learning pipeline introduced by Google DeepMind with AlphaGo. Training this model on 9x9 Go produces a superhuman Go player, thus proving that it is stable and robust. We show that this model can be used to effectively play with both positional and score handicap, and to minimize suboptimal moves. We develop a family of agents that can target high scores against any opponent, and recover from very severe disadvantage against weak opponents. To the best of our knowledge, these are the first effective achievements in this direction.

cs.AI↗

arXiv2019

SAI, a Sensible Artificial Intelligence that plays Go

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, so that the neural network must predict just one more variable to assess the winrate for all komi values. A second novel feature is that training is based on self-play games that occasionally branch -- with changed komi -- when the position is uneven. With this setting, reinforcement learning is showed to work on 7x7 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.

cs.AI↗

arXiv2018

Primitive weird numbers having more than three distinct prime factors

In this paper we study some structure properties of primitive weird numbers in terms of their factorization. We give sufficient conditions to ensure that a positive integer is weird. Two algorithms for generating weird numbers having a given number of distinct prime factors are presented. These algorithms yield primitive weird numbers of the form $mp_1\dots p_k$ for a suitable deficient positive integer $m$ and primes $p_1,\dots,p_k$ and generalize a recent technique developed for generating primitive weird numbers of the form $2^np_1p_2$. The same techniques can be used to search for odd weird numbers, whose existence is still an open question.

math.NT↗

arXiv2018

Primitive abundant and weird numbers with many prime factors

We give an algorithm to enumerate all primitive abundant numbers (briefly, PANs) with a fixed $Ω$ (the number of prime factors counted with their multiplicity), and explicitly find all PANs up to $Ω=6$, count all PANs and square-free PANs up to $Ω=7$ and count all odd PANs and odd square-free PANs up to $Ω=8$. We find primitive weird numbers (briefly, PWNs) with up to 16 prime factors, improving the previous results of [Amato-Hasler-Melfi-Parton] where PWNs with up to 6 prime factors have been given. The largest PWN we find has 14712 digits: as far as we know, this is the largest example existing, the previous one being 5328 digits long [Melfi]. We find hundreds of PWNs with exactly one square odd prime factor: as far as we know, only five were known before. We find all PWNs with at least one odd prime factor with multiplicity greater than one and $Ω= 7$ and prove that there are none with $Ω< 7$. Regarding PWNs with a cubic (or higher) odd prime factor, we prove that there are none with $Ω\le 7$, and we did not find any with larger $Ω$. Finally, we find several PWNs with 2 square odd prime factors, and one with 3 square odd prime factors. These are the first such examples.

math.NT↗

arXiv2015

Efficiently intertwining widening and narrowing

Non-trivial analysis problems require posets with infinite ascending and descending chains. In order to compute reasonably precise post-fixpoints of the resulting systems of equations, Cousot and Cousot have suggested accelerated fixpoint iteration by means of widening and narrowing. The strict separation into phases, however, may unnecessarily give up precision that cannot be recovered later, as over-approximated interim results have to be fully propagated through the equation the system. Additionally, classical two-phased approach is not suitable for equation systems with infinitely many unknowns---where demand driven solving must be used. Construction of an intertwined approach must be able to answer when it is safe to apply narrowing---or when widening must be applied. In general, this is a difficult problem. In case the right-hand sides of equations are monotonic, however, we can always apply narrowing whenever we have reached a post-fixpoint for an equation. The assumption of monotonicity, though, is not met in presence of widening. It is also not met by equation systems corresponding to context-sensitive inter-procedural analysis, possibly combining context-sensitive analysis of local information with flow-insensitive analysis of globals. As a remedy, we present a novel operator that combines a given widening operator with a given narrowing operator. We present adapted versions of round-robin as well as of worklist iteration, local and side-effecting solving algorithms for the combined operator and prove that the resulting solvers always return sound results and are guaranteed to terminate for monotonic systems whenever only finitely many unknowns (constraint variables) are encountered. Practical remedies are proposed for termination in the non-monotonic case.

cs.PL↗

arXiv2013

Optimal multi-binding unification for sharing and linearity analysis

In the analysis of logic programs, abstract domains for detecting sharing properties are widely used. Recently the new domain $\Linp$ 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 multi-binding unification. This is the proof of such a claim.

cs.PL↗

arXiv2009

On the interaction between sharing and linearity

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) domain ShLin-w which can be thought of as a general framework from which other domains can be easily derived by abstraction. ShLin-w makes the interaction between sharing and linearity explicit. We provide a constructive characterization of the optimal abstract unification operator on ShLin-w and we lift it to two well-known abstractions of ShLin-w. Namely, to the classical Sharing X Lin abstract domain and to the more precise ShLin-2 abstract domain by Andy King. In the case of single binding substitutions, we obtain optimal abstract unification algorithms for such domains. To appear in Theory and Practice of Logic Programming (TPLP).

cs.PL↗

arXiv2009

Optimality in Goal-Dependent Analysis of Sharing

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 and provide the best correct approximation of all the primitive semantic operators, namely, projection, renaming, forward and backward unification. 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. To appear in Theory and Practice of Logic Programming (TPLP)

cs.PL↗