A passionate mathematician and coder dedicated to driving impactful research through technical expertise. With an eclectic, creative approach, I excel in collaborative environments, prioritizing trustworthiness, and intellectual rigor.
Recently, I'm delving into the AI safety alignment problem and I regularly spend time into creative theoretical thinking while get in touch with the state of art on this field. I'm also active in AI safety community building (AIS4I, PauseAI Italia) and in the resilience of essential services.
Outside of my academic pursuits, I'm an avid consumer of didattic videos: it's my way to get into most of the fields of the human knowledge and build a personal comphensive understanding of the world.
When I'm not delving into coding and papers, you'll likely find me having deep good talks with friends. Sports also play a significant role in my life: they are a nice way to spend thoughless time with friends while preserving my physical health.
Board and card games are a passion of mine—they're a fantastic blend of entertainment and mental stimulation, providing an opportunity to strategize and having good time.
Reading is finding is way to become an integral part of my routine. Recently, I've been exploring Nassim Nicholas Taleb's "Antifragile," which challenges conventional thinking in a captivating manner, and Benjamin Todd's "80000 Hours," which has been instrumental in shaping my career aspirations toward meaningful impact.
2022 - 2024
The Master in DSSC aims to prepare professionals ready to face the challenges of the modern digital society: experts in the analysis and management of data, in particular Big Data, and in computational modeling with application in engineering and scientific fields.
Link to table of contents: Download File
2019 - 2024
The School for Advanced Studies of the University of Udine is a higher learning institution based on merit. After a very selective admission (including two written and an oral examination), it provides a five-year scholarship covering taxes, board and lodging. During this period, students have to attend extra courses and exams, and in the end, we gain a second-level Master's degree diploma.
Link to table of contents: Download File
Thesis:
Well structured transition systems
2019 - 2022
Link to table of contents: Download File
Development and implementation of advanced methods to support decision-making in emergency scenarios involving critical infrastructure. Supervisor: Prof. Stefano Grimaz - Chairholder of the UNESCO Chair in Intersectoral Safety
R&D: Applying machine modelization techniques to devise strategies for controlling electric furnaces
Here are some of the recent extracurricular activities I pursued
Classified 55/103. Website.
Cryptographic protocols play a fundamental role in securing modern digital infrastructure, but they are often deployed without prior formal verification. This could lead to the adoption of distributed systems vulnerable to attack vectors. Formal verification methods, on the other hand, require complex and time-consuming techniques that lack automatization. In this paper, we introduce a benchmark to assess the ability of Large Language Models (LLMs) to autonomously identify vulnerabilities in new cryptographic protocols through interaction with Tamarin: a theorem prover for protocol verification. We created a manually validated dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents. Our results about the performances of the current frontier models on the benchmark provides insights about the possibility of cybersecurity applications by integrating LLMs with symbolic reasoning systems.
NeurIPS 2024 Workshop: Sys2-Reasoning Poster
A Brunello, C Curaba, L Geatti, M Mignani, A Montanari, N Saccomanno
Accurate translation from Natural Language to First-Order Logic (NL-to-FOL) underpins neurosymbolic AI systems and Natural Language Inference (NLI), making the quality of NL-to-FOL benchmarks essential—yet these datasets have never been rigorously audited. We present a systematic human inspection of FOLIO and MALLS, finding substantial rates of incorrect ground-truth formalizations, and release corrected annotations together with an LLM-assisted framework that directs reviewers toward the most error-prone instances, reaching 90% dataset accuracy after reviewing fewer than 20% of instances.
EMNLP 2026
C Curaba, S Grimaz
In a network of networks, a dependency link runs from a supplier to the node it serves and binds the supplier's failure to the node's failure. Indices computed from the graph topology leave aside the service each edge carries, but in real interdependent systems that service decides how failure propagates. We label each node with the service it provides and measure how far this qualitative input changes the node's vitality ranking: fixing the graph topology, changing only the labels moves the Mean Operativity Loss from 0.023 to 0.114, while a ranking computed from the unlabelled topology is blind to the difference.
Complex Networks 2026
C Curaba, S Grimaz
Modeling cascading failure across interdependent critical infrastructure requires either a costly, data-hungry physical simulator per domain or a topological abstraction that discards quantity awareness. We present a knowledge-driven propagation architecture in which heterogeneous service dependencies are identified by categories: a general logical propagation resolves multi-dependency and redundancy structures from how nodes are categorized, while quantity-aware categories plug in dedicated mechanisms—here, a max-min fair-share flow module for water distribution. Validated against pressure-driven WNTR simulation on eight realistic networks across four failure families, the flow module substantially reduces missed critical junctions compared to a topological-reachability baseline.
Complex Networks 2026
A Brunello, C Curaba, L Geatti, M Mignani, A Montanari, N Saccomanno
Large Language Models (LLMs) have renewed interest in autoformalization. Yet, when First-Order Logic (FOL) is considered as the target formalism, the field still lacks a unified task formulation and a systematic survey. This paper addresses this gap: we provide a principled definition for the FOL-autoformalization task by distinguishing Ontology Extraction from Logical Translation, review existing datasets, evaluation metrics, and LLM-based methods (fine-tuning, prompting, and verification-based refinement), and identify open challenges in benchmarking, semantic evaluation, ontology-aware methods, and end-to-end applications.
EMNLP 2026
We introduce a benchmark for testing how well LLMs can find vulnerabilities in cryptographic protocols. By combining LLMs with symbolic reasoning tools like Tamarin, we aim to improve the efficiency and thoroughness of protocol analysis, paving the way for future AI-powered cybersecurity defenses.
A platform for modelling interdependent critical infrastructure (power, water, heat, digital, personnel) as a graph, then simulating how a failure in one element propagates through the network via a rule-driven, category-typed propagation engine: quantity-aware and purely logical interdependencies share one discrete functionality scale and converge through a single monotonic update rule.
A free, transparent platform collecting the "interpelli" (substitute-teacher call notices) published on Italian state schools' online boards, gathered twice a day and filterable by province and teaching class, with email alerts.
