SearcharxivSearch

arXiv subjects

Simone Severini

Publications and source records attributed to Simone Severini.

At least 19 recordsLinked to original sources

The minimum of the graph likelihood

The likelihood of a finite simple undirected graph $G$ on $n$ vertices is the probability that the uniform sequential attachment process, which at each step joins a new vertex to a uniformly random subset of uniformly random size of the vertices already present, outputs a graph isomorphic to $G$. Dervovic, Mocherla and Severini conjectured that the likelihood is minimised by the balanced complete bipartite graph. We prove that, among complete bipartite graphs of a given order, the balanced one uniquely minimises the likelihood. Exact computation shows that it also minimises over all graphs for every order from $6$ through $14$, and that the first counterexample occurs at $n=15$. The blow-up of the five cycle by independent sets of size three, equivalently the circulant on fifteen vertices with connection set $\{1,4,6\}$, has likelihood $0.20128\ldots$ times that of $K_{7,8}$, and it is again triangle-free. We show that the failure is not sporadic by proving that the likelihood of the balanced complete bipartite graph is $2^{-(1/2-1/(8\ln 2)+o(1))n^2}$, whereas the minimum over all graphs of order $n$ is $2^{-(1/2+o(1))n^2}$, so the conjectured minimiser exceeds the minimum by a factor exponential in $n^2$. We also determine the Shannon entropy of the process to leading order, namely $n^2/(4\ln 2)$ bits, which shows that the conjectured minimiser is in fact more likely than a typical output of the process. The proofs rest on a vertex deletion recurrence which evaluates the likelihood in time $O(n\,2^n)$ and which closes on the blow-ups of any fixed base graph.

math.CO

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. LEAP leverages foundation model capabilities, such as informal reasoning, instruction following, and iterative self-refinement. By decomposing complex problems into smaller units, the system bridges formal proof construction with informal blueprints through continuous interaction with the Lean compiler. To provide a rigorous evaluation beyond increasingly saturated benchmarks, we introduce Lean-IMO-Bench, a benchmark of IMO-style problems formalized in Lean, with short statements yet highly non-routine and multi-step proofs across a wide range of difficulty levels. Empirically, on the latest 2025 Putnam Competition, an annual mathematics competition for undergraduate students in North America, LEAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models. On Lean-IMO-Bench, LEAP boosts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70%, notably surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system. Furthermore, we demonstrate LEAP's research-level utility by autonomously formalizing complex proofs for open combinatorial challenges, including a verified proof for a key subproblem in Knuth's Hamiltonian decomposition of even-order Cayley graphs.

cs.AI

The Network Structure of Mathlib

The ongoing development of Lean 4's Mathlib has produced a macroscopic structural complexity that interweaves logical, mathematical, and infrastructural dependencies. We present a network analysis of this library, extracting its dependency structure into a multilayer graph of 308,129 declarations, 8.4 million edges, and 7,563 modules. By introducing graph decompositions that isolate explicit edges from those synthesized by the compiler or driven by proofs, we quantify the structural properties of formalized mathematics. Our analysis reveals three findings. First, taxonomies designed by humans diverge from logical structures, exhibiting a 50.9% coupling across namespaces. Second, developers utilize a median of 1.6% of the imported scope. Third, formalization compresses semantic hierarchies, with network centrality capturing language infrastructure rather than mathematical relevance.

cs.LO

Computocene: Notes from an Age of Observation

This piece plays with the idea of the Computocene: an era defined not merely by the ubiquity of computers, but by their deepening role in how we observe, interpret, and make sense of the world. Rather than emphasizing automation, speed, scale, or intelligence, computation is reframed as a mode of attention: filtering information, guiding inquiry, reframing questions, and shaping the very conditions under which knowledge emerges. I invite the reader to consider computers not simply as tools of calculation, but as epistemic instruments that participate in the formation of knowledge. This perspective reconfigures not only scientific practice but the epistemological foundations of understanding itself. The Computocene thus names a shift: from computation as calculation to computation as a form of attunement to the world. It is a speculative essay, offered without technical formality, and intended for a general, curious readership.

cs.CY

The impact of CAP subsidies on the productivity of cereal farms in six European countries

Total factor productivity (TFP) is a key determinant of farm development, a sector that receives substantial public support. The issue has taken on great importance today, where the conflict in Ukraine has led to repercussions on the cereal markets. This paper investigates the effects of different subsidies on the productivity of cereal farms, accounting that farms differ according to the level of TFP. We relied on a three-step estimation strategy: i) estimation of production functions, ii) evaluation of TFP, and iii) assessment of the relationship between CAP subsidies and TFP. To overcome multiple endogeneity problems, the System-GMM estimator is adopted. The investigation embraces farms in France, Germany, Italy, Poland, Spain and the United Kingdom using the FADN samples from 2008 to 2018. Adding to previous analyses, we compare results from different countries and investigate three subsets of farms with varying levels of TFP. The outcomes confirm how CAP negatively impacts farm TFP, but the extent differs according to the type of subsidies, the six countries and, within these, among farms with different productivity groups. Therefore there is room for policy improvements in order to foster the productivity of cereal farms.

econ.GN

Can Machine Learning discover the determining factors in participation in insurance schemes? A comparative analysis

Identifying factors that affect participation is key to a successful insurance scheme. This study's challenges involve using many factors that could affect insurance participation to make a better forecast.Huge numbers of factors affect participation, making evaluation difficult. These interrelated factors can mask the influence on adhesion predictions, making them misleading.This study evaluated how 66 common characteristics affect insurance participation choices. We relied on individual farm data from FADN from 2016 to 2019 with type 1 (Fieldcrops) farming with 10,926 observations.We use three Machine Learning (ML) approaches (LASSO, Boosting, Random Forest) compare them to the GLM model used in insurance modelling. ML methodologies can use a large set of information efficiently by performing the variable selection. A highly accurate parsimonious model helps us understand the factors affecting insurance participation and design better products.ML predicts fairly well despite the complexity of insurance participation problem. Our results suggest Boosting performs better than the other two ML tools using a smaller set of regressors. The proposed ML tools identify which variables explain participation choice. This information includes the number of cases in which single variables are selected and their relative importance in affecting participation.Focusing on the subset of information that best explains insurance participation could reduce the cost of designing insurance schemes.

econ.GN

The role of Common Agricultural Policy (CAP) in enhancing and stabilising farm income: an analysis of income transfer efficiency and the Income Stabilisation Tool

Since its inception, the E.U.'s Common Agricultural Policy (CAP) aimed at ensuring an adequate and stable farm income. While recognizing that the CAP pursues a larger set of objectives, this thesis focuses on the impact of the CAP on the level and the stability of farm income in Italian farms. It uses microdata from a high standardized dataset, the Farm Accountancy Data Network (FADN), that is available in all E.U. countries. This allows if perceived as useful, to replicate the analyses to other countries. The thesis first assesses the Income Transfer Efficiency (i.e., how much of the support translate to farm income) of several CAP measures. Secondly, it analyses the role of a specific and relatively new CAP measure (i.e., the Income Stabilisation Tool - IST) that is specifically aimed at stabilising farm income. The assessment of the potential use of Machine Learning procedures to develop an adequate ratemaking in IST. These are used to predict indemnity levels because this is an essential point for a similar insurance scheme. The assessment of ratemaking is challenging: indemnity distribution is zero-inflated, not-continuous, right-skewed, and several factors can potentially explain it. We address these problems by using Tweedie distributions and three Machine Learning procedures. The objective is to assess whether this improves the ratemaking by using the prospective application of the Income Stabilization Tool in Italy as a case study. We look at the econometric performance of the models and the impact of using their predictions in practice. Some of these procedures efficiently predict indemnities, using a limited number of regressors, and ensuring the scheme's financial stability.

econ.GN

The direct and indirect effect of CAP support on farm income enhancement:a farm-based econometric analysis

We assess the correlation between CAP support provided to farmers and their income and use of capital and labour in the first year of the new CAP regime. This is done applying three regression models on the Italian FADN farms controlling for other farm characteristics. CAP annual payments are positively correlated with farm income and capital but are negatively correlated with labour use. Farm investment support provided by RDP measures is positively correlated to the amount of capital. Results suggest that CAP is positively affecting farm income directly but also indirectly by supporting the substitution of labour with capital

econ.GN

Quantum State Discrimination Using Noisy Quantum Neural Networks

Near-term quantum computers are noisy, and therefore must run algorithms with a low circuit depth and qubit count. Here we investigate how noise affects a quantum neural network (QNN) for state discrimination, applicable on near-term quantum devices as it fulfils the above criteria. We find that when simulating gradient calculation on a noisy device, a large number of parameters is disadvantageous. By introducing a new smaller circuit ansatz we overcome this limitation, and find that the QNN performs well at noise levels of current quantum hardware. We also show that networks trained at higher noise levels can still converge to useful parameters. Our findings show that noisy quantum computers can be used in applications for state discrimination and for classifiers of the output of quantum generative adversarial networks.

quant-ph

Graph Cut Segmentation Methods Revisited with a Quantum Algorithm

The design and performance of computer vision algorithms are greatly influenced by the hardware on which they are implemented. CPUs, multi-core CPUs, FPGAs and GPUs have inspired new algorithms and enabled existing ideas to be realized. This is notably the case with GPUs, which has significantly changed the landscape of computer vision research through deep learning. As the end of Moores law approaches, researchers and hardware manufacturers are exploring alternative hardware computing paradigms. Quantum computers are a very promising alternative and offer polynomial or even exponential speed-ups over conventional computing for some problems. This paper presents a novel approach to image segmentation that uses new quantum computing hardware. Segmentation is formulated as a graph cut problem that can be mapped to the quantum approximate optimization algorithm (QAOA). This algorithm can be implemented on current and near-term quantum computers. Encouraging results are presented on artificial and medical imaging data. This represents an important, practical step towards leveraging quantum computers for computer vision.

cs.CV

Modelling Non-Markovian Quantum Processes with Recurrent Neural Networks

Quantum systems interacting with an unknown environment are notoriously difficult to model, especially in presence of non-Markovian and non-perturbative effects. Here we introduce a neural network based approach, which has the mathematical simplicity of the Gorini-Kossakowski-Sudarshan-Lindblad master equation, but is able to model non-Markovian effects in different regimes. This is achieved by using recurrent neural networks for defining Lindblad operators that can keep track of memory effects. Building upon this framework, we also introduce a neural network architecture that is able to reproduce the entire quantum evolution, given an initial state. As an application we study how to train these models for quantum process tomography, showing that recurrent neural networks are accurate over different times and regimes.

quant-ph

Unitary equivalence between the Green's function and Schr\"odinger approaches for quantum graphs

In a previous work [Andrade \textit{et al.}, Phys. Rep. \textbf{647}, 1 (2016)], it was shown that the exact Green's function (GF) for an arbitrarily large (although finite) quantum graph is given as a sum over scattering paths, where local quantum effects are taken into account through the reflection and transmission scattering amplitudes. To deal with general graphs, two simplifying procedures were developed: regrouping of paths into families of paths and the separation of a large graph into subgraphs. However, for less symmetrical graphs with complicated topologies as, for instance, random graphs, it can become cumbersome to choose the subgraphs and the families of paths. In this work, an even more general procedure to construct the energy domain GF for a quantum graph based on its adjacency matrix is presented. This new construction allows us to obtain the secular determinant, unraveling a unitary equivalence between the scattering Schr\"odinger approach and the Green's function approach. It also enables us to write a trace formula based on the Green's function approach. The present construction has the advantage that it can be applied directly for any graph, going from regular to random topologies.

quant-ph

Adversarial quantum circuit learning for pure state approximation

Adversarial learning is one of the most successful approaches to modelling high-dimensional probability distributions from data. The quantum computing community has recently begun to generalize this idea and to look for potential applications. In this work, we derive an adversarial algorithm for the problem of approximating an unknown quantum pure state. Although this could be done on universal quantum computers, the adversarial formulation enables us to execute the algorithm on near-term quantum computers. Two parametrized circuits are optimized in tandem: One tries to approximate the target state, the other tries to distinguish between target and approximated state. Supported by numerical simulations, we show that resilient backpropagation algorithms perform remarkably well in optimizing the two circuits. We use the bipartite entanglement entropy to design an efficient heuristic for the stopping criterion. Our approach may find application in quantum state tomography.

quant-ph

Universal discriminative quantum neural networks

Quantum mechanics fundamentally forbids deterministic discrimination of quantum states and processes. However, the ability to optimally distinguish various classes of quantum data is an important primitive in quantum information science. In this work, we train near-term quantum circuits to classify data represented by non-orthogonal quantum probability distributions using the Adam stochastic optimization algorithm. This is achieved by iterative interactions of a classical device with a quantum processor to discover the parameters of an unknown non-unitary quantum circuit. This circuit learns to simulates the unknown structure of a generalized quantum measurement, or Positive-Operator-Value-Measure (POVM), that is required to optimally distinguish possible distributions of quantum inputs. Notably we use universal circuit topologies, with a theoretically motivated circuit design, which guarantees that our circuits can in principle learn to perform arbitrary input-output mappings. Our numerical simulations show that shallow quantum circuits could be trained to discriminate among various pure and mixed quantum states exhibiting a trade-off between minimizing erroneous and inconclusive outcomes with comparable performance to theoretically optimal POVMs. We train the circuit on different classes of quantum data and evaluate the generalization error on unseen mixed quantum states. This generalization power hence distinguishes our work from standard circuit optimization and provides an example of quantum machine learning for a task that has inherently no classical analogue.

quant-ph

Quantum Walk Search on Kronecker Graphs

Kronecker graphs, obtained by repeatedly performing the Kronecker product of the adjacency matrix of an "initiator" graph with itself, have risen in popularity in network science due to their ability to generate complex networks with real-world properties. In this paper, we explore spatial search by continuous-time quantum walk on Kronecker graphs. Specifically, we give analytical proofs for quantum search on first-, second-, and third-order Kronecker graphs with the complete graph as the initiator, showing that search takes Grover's $O(\sqrt{N})$ time. Numerical simulations indicate that higher-order Kronecker graphs with the complete initiator also support optimal quantum search.

quant-ph

Hierarchical quantum classifiers

Quantum circuits with hierarchical structure have been used to perform binary classification of classical data encoded in a quantum state. We demonstrate that more expressive circuits in the same family achieve better accuracy and can be used to classify highly entangled quantum states, for which there is no known efficient classical method. We compare performance for several different parameterizations on two classical machine learning datasets, Iris and MNIST, and on a synthetic dataset of quantum states. Finally, we demonstrate that performance is robust to noise and deploy an Iris dataset classifier on the ibmqx4 quantum computer.

quant-ph

Approximating Hamiltonian dynamics with the Nystr\"om method

Simulating the time-evolution of quantum mechanical systems is BQP-hard and expected to be one of the foremost applications of quantum computers. We consider classical algorithms for the approximation of Hamiltonian dynamics using subsampling methods from randomized numerical linear algebra. We derive a simulation technique whose runtime scales polynomially in the number of qubits and the Frobenius norm of the Hamiltonian. As an immediate application, we show that sample based quantum simulation, a type of evolution where the Hamiltonian is a density matrix, can be efficiently classically simulated under specific structural conditions. Our main technical contribution is a randomized algorithm for approximating Hermitian matrix exponentials. The proof leverages a low-rank, symmetric approximation via the Nystr\"om method. Our results suggest that under strong sampling assumptions there exist classical poly-logarithmic time simulations of quantum computations.

quant-ph

Constructing graphs with limited resources

We discuss the amount of physical resources required to construct a given graph, where vertices are added sequentially. We naturally identify information -- distinct into instructions and memory -- and randomness as resources. Not surprisingly, we show that, in this framework, threshold graphs are the simplest possible graphs, since the construction of threshold graphs requires a single bit of instructions for each vertex and no use of memory. Large instructions without memory do not bring any advantage. With one bit of instructions and one bit of memory for each vertex, we can construct a family of perfect graphs that strictly includes threshold graphs. We consider the case in which memory lasts for a single time step, and show that as well as the standard threshold graphs, linear forests are also producible. We show further that the number of random bits (with no memory or instructions) needed to construct any graph is asymptotically the same as required for the Erd\H{o}s-R\'enyi random graph. We also briefly consider constructing trees in this scheme. The problem of defining a hierarchy of graphs in the proposed framework is fully open.

cs.DM