ABSTRACT. Computational Origami is an interdisciplinary field that combines mathematics, geometry, symbolic computation, and computer science to study origami through formal and computational methods. In 2020, I published An Introduction to Computational Origami with Springer, which summarized the state of the art of the field, with a particular focus on the Eos (E-Origami System) project that I have been developing since the early 2000s. The field has continued to evolve, and I am currently preparing a substantially revised second edition of the book.

The work on the second edition has coincided with the rapid emergence of large language models (LLMs). Although these systems were not originally designed for symbolic reasoning or mathematical research, they have proved to be surprisingly useful assistants in many aspects of research activity, including writing, revising manuscripts, organizing ideas, exploring related literature, and discussing technical concepts.

In this talk, I will revisit the development of Computational Origami and present some experiences and observations gained through the preparation of the second edition. Rather than focusing on AI technology itself, I will discuss how these new tools are beginning to interact with a long-established research workflow centered on symbolic computation and mathematical knowledge. Drawing on concrete examples from my own research and writing activities, I will reflect on both the opportunities and the limitations of LLMs in mathematical and symbolic-computation-oriented research environments, and conclude with some thoughts on future directions.

ABSTRACT. In this talk, I will introduce the small-step operational semantics we developed for the Core Erlang language and implemented in the Rocq proof assistant. I will discuss the various design decisions we explored and adopted, including variable and binding representations, substitutions versus environments, and the validation of the mechanised semantics. I will also explain how we defined notions of program equivalence that coincide with behavioural equivalence. Then, I will highlight several applications of the semantics that contribute to trustworthy software tools for Erlang, including the verification of refactoring correctness, the formalization of software vulnerabilities, and a verifier for property-based tests. Finally, I will present the early but promising results of our most recent effort: the development of a proven-correct optimizing compiler for Erlang.

ABSTRACT. Block-term decompositions (BTDs) are structured low-rank models that represent multiway data as an additive decomposition of components with possibly different multilinear rank. The recoverability of such models--that is, under which conditions can the latent components be recovered from the original tensor--is one of their key properties. However, current results make it very difficult to verify it beyond classical settings with low numbers of components. This paper proposes a Jacobian rank-based certificate for generic recoverability of BTDs. The method first removes a continuous blockwise change-of-basis ambiguity of the decomposition by working on local affine charts of the factor subspaces, yielding an explicit polynomial parametrization with the effective number of parameters. Then, we leverage the links between geometric properties of polynomial maps and the existence of a so-called witness with full-column-rank Jacobian in order to certify the generic finite-to-one recoverability of the charted model. Moreover, the same computation also gives information about the dimension of algebraic varieties associated with BTD formats. Numerical experiments classify selected non-defective and rank-defective BTD formats and compare the recoverability guarantees given by the proposed certificate with existing sufficient identifiability criteria.

ABSTRACT. The original SciGMark benchmark adapted the SciMark numerical suite to measure the cost of generic programming in scientific computing. In the twenty years since, generics have become ordinary features of mainstream languages, but their implementation strategies have diversified. This paper reports SciGMark 1.5, a benchmark study of specialized and generic implementations in modern languages. The study has three aims. First, it examines the consequences of the wide variety of generic-realization strategies used in current widely used languages. Second, it extends the benchmark toward symbolic computation by adding finite-field linear algebra, finite-field FFT, and a naive Groebner basis computation. Third, it asks how the original floating-point scientific kernels behave in the new language settings. The measurements cover Rust, Java, Go, and TypeScript for the main suite, with additional C++ and Julia measurements for the Groebner basis benchmark. The study also records representative output artifact sizes, since code generation and runtime packaging are part of the cost model of generic programming.

The results confirm that the cost of generic programming is not inherent in abstraction itself, but depends strongly on when type information is resolved, how arithmetic values are represented, and whether the compiler or runtime can recover specific operations in the inner loops. Ahead-of-time monomorphization usually makes generic code close to specialized code in the numerical tests. Erased or object-based generic arithmetic can introduce substantial overhead, especially in arithmetic- and allocation-intensive code. Runtime specialization occupies an intermediate position, offering flexibility and good steady-state performance when type inference and representation choices are favourable.

ABSTRACT. We report on GPU implementations of block-level addition, subtraction, multiplication and division for midsize integers, with operands of 2^15 to 2^18 bits using the high-level functional language Futhark. Comparing with hand-written C++/CUDA versions and cgbn, we identify which functional constructs compile well, where memory placement and sequentialization are effective, and what compiler support is needed. The results show that high-level code can express the algorithms compactly while approaching competitive performance after certain compiler improvements.

ABSTRACT. Automatic tools that bound the round-off error of a straight-line program are common nowadays. But the obtained bounds may be too large compared to the user expectations. The question is therefore whether the tool is too coarse or the program has indeed a large maximal error. Our objective is threefold: answer this question, evaluate the tightness of the provided bounds, and build trust in the tool. We therefore present the Pathogen tool that generates guaranteed pathological inputs, that is to say inputs that create a high error formally verified, hopefully near the obtained bound. The idea is both to randomly sample and to split the domain guided by the Gappa tool bounds. We have successfully tested its efficiency, reproductibility, and quality of the pathological inputs on a benchmark of 77 programs, taken from the FPBench benchmark and the literature.

ABSTRACT. Multi-camera pedestrian detectors fuse synchronized views into a common ground-plane occupancy estimate, but in real deployments individual cameras degrade independently due to weather, illumination, or transmission artifacts. We address this problem through a coordinated framework in which per-camera assessment and adaptive action selection determine whether each degraded view should be kept, restored, or discarded before multi-view fusion. The framework combines distributed per-camera degradation assessment with coordinated decision-making and is evaluated on the Wildtrack dataset using four state-of-the-art multi-view detectors (EarlyBird, MVDet, GMVD, and MVDeTr) under five degradation types (gamma,fog, noise, JPEG, and rain). Results show that no single action is universally optimal: the best decision depends on both the degradation characteristics and the fusion architecture. In particular, discarding degraded views improves detection by up to +45.2 MODA under dense fog, whereas blind restoration can reduce performance. We further distinguish between a diagnostic action space that estimates the upper bound of adaptive intervention and a deployable action space based on practical restoration methods. Cross-scene experiments demonstrate that a zero-shot VLM-based degradation assessor transfers more consistently than scene-specific classifiers, while a temporal-differential feature improves cross-scene routing accuracy by +9.3 percentage points. These findings highlight the importance of adaptive per-camera intervention for robust multi-view pedestrian detection under heterogeneous sensor degradations.

ABSTRACT. Automatic segmentation of brain tumors from multimodal MRI images is affected in practice by the lack of one or more imaging modalities, although most studies evaluate models only under ideal conditions. In this paper, a Segmentation Robustness Assessment Framework (SRAF) is proposed to systematically assess the robustness of segmentation models in scenarios with missing MRI modalities. The framework adopts an agent-oriented architecture, coordinated by an Evaluation Orchestrator, in which specialized agents perform baseline performance evaluation, robustness analysis in the absence of MRI modalities, analysis of MRI modality importance, comparison of training strategies, and selective prediction evaluation. The methodology is validated on the BraTS2020 dataset using representative CNN-based segmentation architectures. The results show that FLAIR and T1ce modalities have the greatest influence on the segmentation of different tumor regions and demonstrate that modality dropout-based training significantly improves the robustness of models in scenarios with incomplete information. The proposed framework provides a unified, modular, and architecture-independent methodology for evaluating and comparing the robustness of segmentation models.

ABSTRACT. Debugging concurrent Multi-Agent Systems (MAS) is inherently challenging due to non-determinism, asynchronous scheduling, and the tight interleaving of multi-threaded shared states. Traditional debugging methods often fail to capture the semantic intent of agent interactions or introduce significant performance overhead, known as the “Probe Effect.” This research proposes a generalized Hybrid Observability Framework for concurrent agent environments. The proposed methodology combines a low-overhead, asynchronous data ingestion layer with a neuro-symbolic analysis engine powered by Large Language Models (LLMs). Empirical results gathered via the FLASH-MAS platform demonstrate that an event-driven, lock-free buffering strategy allows for high-fidelity data capture with negligible impact on simulation timing. Furthermore, we formalize and evaluate an adaptive simulation protocol via a Reactive Hot-Swap by Cascade Propagation mechanism, designed to dynamically isolate non-deterministic cognitive entities while compressing global computational execution costs.

ABSTRACT. Hospital scheduling is a critical operational problem. Patient demand, staff availability, clinical priorities, bed capacity, and diagnostic resources change continuously. Centralized schedulers may scale poorly. They may also react slowly to urgent admissions, delayed procedures, or temporary resource shortages. This paper presents a multi-agent system implemented as a microservices architecture for hospital scheduling and resource allocation. The framework decomposes the process into five autonomous services: Patient Agent, Scheduling Agent, Prediction Agent, Resource Agent, and Notification Agent. The Prediction Agent is developed on the MIMIC-III critical-care dataset. The prediction task focuses on length of stay (LOS) and high resource-demand classification. Five machine-learning algorithms are compared: Logistic Regression, Decision Tree, Support Vector Machine, Random Forest, and XGBoost. In the prototype, XGBoost obtains the best performance, with 0.92 accuracy, 0.90 precision, 0.90 recall, 0.90 F1-score, and 0.94 ROC-AUC. The results suggest that distributed predictive services can support hospital scheduling. However, the operational effect on waiting time and resource use should be validated through simulation or prospective studies.

ABSTRACT. In this talk we present a view of Artificial Consciousness (called SP-Consciousness) as an interplay between sequential and parallel computation in complex computing networks. The main gain from this view is a design methodology which keep under control the complexity of a hierarchy of systems of systems. Modern studies on understanding consciousness have exploded after 1953 when Ibsen established the first Intensive Care Unit. Now, we know that a body and a brain can “live” even when their connection is interrupted, putting great pressure on deciding when a person is conscious or not, alive or dead.

First, we review two leading theories on finding the neural correlates of consciousness: Integrated Information Theory (IIT) and Global Workspace Theory (GWT). The IIT approach puts more emphasis on the structure of a network supporting consciousness, while GWT is more suited to explain the interaction with a conscious network.

Then, we go to the technical part of the talk. We incorporate suggestions from IIT and GWT theories into the Mixed Network Algebra formalism (MixNA), described below.

Symmetric monoidal category with feedback (a.k.a. traced monoidal category), introduced by Stefanescu in 1986, is a versatile algebraic structure. Initially, an additive interpretation of the monoidal operation was considered, aiming to model control structures like flowchart schemes or finite automata. Later on, with a multiplicative interpretation of the monoidal operation, the structure was successfully used to capture parallel computing models, in particular data-flow networks. Classical sequential programs have limited parallelism, while parallel data-flow networks have limited control. Hence, it is desirable to have a setting freely mixing control and parallelism. Symmetric semiringal categories (having two monoidal operations: addition and multiplication) with feedback has been proposed as an algebraic candidate to study this complicated setting. Agapia programming model and Virtual Organisms are two instances of the MixNA formalism.

Finally, we illustrate the approach with a design of a hierarchy of virtual organisms. Within each virtual organism the processing is massively parallel, in concordance with the IIT theory. When we compose virtual organisms, GWT suits better, with its emphasis on selecting one action at a time and broadcasting the choice within the virtual organism. These steps are repeated at the next level of the hierarchy keeping the full network design at a desirable complexity scale.

ABSTRACT. The axiomatization of the theory of hereditarily finite sets in first-order classical logic is systematically explored and formalized in Isabelle/HOL. The formalization uses a hierarchy of locales, each corresponding to a fragment of the theory given by a particular An inductive definition of first-order definable predicates is introduced and used to formalize axiom schemata. Special attention is paid to several equivalent axioms of finiteness, as well as to several equivalent ways of expressing regularity. The work also formalizes several facts about independence of an axiom from a system of axioms by defining appropriate models.

ABSTRACT. A polyhedral set can be represented by a system of inequalities (including equalities) called the H-representation. In this paper, we show how to compute the H-representation of the topological closure of the convex hull of finitely many polyhedral sets given in H-representation. Our proposed algorithm avoids completely the computation of the V-representation of its input and intermediary polyhedral sets. Therefore, it extends previous works on the computation of convex hulls. Moreover, all computations of our proposed algorithm, except linear algebra, reduce to linear programming.

ABSTRACT. The goal of this work is to discover more NP-complete quandles to color knots within the Tait--Rolfsen Knot Table. This presents a randomized algorithm along with two ways in which this algorithm was improved to discover more quandles. The first improvement was to develop a formula for the size of Sharac quandles to tighten the search to acceptable size limits. The second method limits the space of the randomly-selected generator for the quandle to so-called involutory products. Eight new and relevant NP-complete quandles were discovered through these improvements.

ABSTRACT. We present a computer-aided study of the diminished Euler Sombor index, the degree-based graph descriptor obtained by applying the diminishing operation to Gutman's Euler Sombor index. It is the one diminished geometric Sombor index not previously isolated. We give initial results on its structure: a symbolic second-moment identity for the underlying edge kernel and the tight global bounds it yields around an irregularity measure; a separation result showing that the index is not an affine function of the diminished Sombor index, with the gap between the two controlled by the same irregularity; and an estimate of the index from the edge count alone, with a worst-case relative error of about seven percent, reflecting the narrow range of its scale-invariant kernel. The bounds and their equality cases are certified by exhaustive computation over all connected graphs on at most ten vertices and by random sampling at larger orders, and the kernel identities are verified symbolically. We end by setting out the main open problems.

ABSTRACT. The Frobenius method is the most common method for computing a basis of linearly independent series which are the solutions to a linear ordinary differential equation at a regular singular point. When implemented, the classical formulas of the Frobenius method have significant computational shortcomings. In this paper we propose various techniques to improve the computational footprint of the Frobenius method, improving the classification of roots of the indicial polynomial, reducing output size and increasing readability, and decreasing execution time

ABSTRACT. Predicting the biological function of uncharacterized proteins remains a major challenge in bioinformatics. This paper presents a practical, resource-efficient ensemble pipeline developed for the CAFA 6 competition. Our system integrates: (i) embeddings from pre-trained protein language models (ESM-2 and ProtT5-XL) with KNN classifiers, (ii) DIAMOND-based homology transfer, (iii) Rank-Sum ensembling, (iv) BFS-based GO DAG propagation to enforce the true-path rule and score monotonicity, and (v) an SQLite-backed chunked streaming engine that processes multi-gigabyte prediction files under a strict 2 GB memory limit on standard workstations. On the public CAFA 6 leaderboard, the pipeline achieves an IC-weighted Fmax of 0.250. We provide detailed ablations showing the contribution of each component, a biological analysis across GO sub-ontologies (BPO, MFO, CCO), and characterization of success/failure cases. The proposed modular architecture offers a reproducible and accessible solution for researchers with limited computational resources while maintaining strict ontological correctness. Index Terms—Protein function prediction, Gene Ontology, ESM-2, ProtT5, DIAMOND, ensemble learning, BFS propagation, resource-efficient bioinformatics.

ABSTRACT. This paper presents Ami, a prototype conversational system designed to provide accessible emotional support for Romanian-speaking users. The system leverages a fine-tuned large language model integrated into a modular well-being platform that includes journaling, mood tracking, music, and cognitive distraction games. The model is trained using open-source conversational data augmented with cognitive behavioral therapy-inspired examples and adapted for Romanian language and cultural context. Performance is evaluated using BERTScore, with the best results obtained by a quantized Gemma 2 9B model. A user study with 20 participants indicates high usability and positive perceived usefulness, suggesting that the system can effectively support emotional self-reflection and well-being activities. The results demonstrate the feasibility of integrating fine-tuned conversational AI with complementary digital well-being tools into a unified support system.

ABSTRACT. This paper investigates how different routing behaviours affect urban evacuation performance under partial compliance. The study compares centralized, selfish, and collaborative evacuation strategies on a directed road network of Timisoara, Romania, extracted from OpenStreetMap and modeled as a capacity-constrained transportation network. Congestion is represented with a Bureau of Public Roads volume–delay function, while evacuees are simulated as agents moving through the network under finite edge capacities and FIFO queueing. The experiments evaluate 13 routing-composition configurations across three population sizes: 10,000, 20,000, and 40,000 agents, for a total of 780 simulation runs. Performance is measured using total evacuation time, 95th percentile evacuation time, average delay, and Compliance Efficiency Ratio. At 10,000 agents, centralized routing performs best, selfish routing performs worst, and collaborative routing remains between them. Increasing centralized or collaborative participation improves evacuation outcomes, although no sharp tipping point is observed. At higher demand, collaborative routing gains relative advantage for clearance-based metrics, showing that static planning and dynamic rerouting can behave differently under severe congestion.

ABSTRACT. Ensuring safe software updates in safety-critical systems without interrupting operation and without provisioning and activating cold spare hardware poses a fundamental challenge due to the conflict between system availability and update execution. In this paper, we present a bounded SMT encoding for synthesizing fixed global-time update schedules for timed-games with linear update automata and a fixed number of update transitions. We model the interaction between the system and the update as a two-player timed game. Our key contribution is the synthesis of global time points that define a fixed update schedule which guarantees safe and complete deployment of the update independently of the autonomous system behavior. To this end, we reduce the scheduling problem to a reachability and safety objective and encode it as a quantified SMT problem. We demonstrate it on an example system of a trajectory planner for autonomous driving, showing that the synthesized schedule ensures safe deployment under all admissible executions.

ABSTRACT. A resolvable network is a directed-graph representation of SAT: every SAT instance can be translated into an RN, and every RN has an associated CNF formula. A reach is an ordered pair of disjoint variable sets representing one clause: its head contains the variables occurring negatively in the clause, and its tail contains the variables occurring positively. RN-Solver is a proof-of-concept SAT solver based on this representation. Its all-positive clauses are represented by white reaches, and its token distributions are the inclusion-minimal hitting sets of the current white tails, generated by monotone CNF--DNF dualization. RN-Solver learns new white reaches by private-pivot resolution, a structured resolution sequence that uses old white reaches as pivot witnesses. In the original algorithm, every candidate white reach generated by such a chain was followed by a global subsumption test against the current network. Profiling showed that this subsumption test can dominate the runtime on random 3-SAT instances. We show that this check is unnecessary when the mixed reach used for learning is falsified by the current token distribution, meaning that the distribution makes all variables in the head true and all variables in the tail false. The key invariant is simple: the resulting white tail is disjoint from the triggering token distribution, while the same distribution intersects every old white tail. Hence no old white reach can subsume the generated reach. This structural observation allows us to construct a simpler, snapshot-based, subsumption-free variant of RN-Solver, where each main-loop iteration uses a fixed set of old reaches and installs newly generated white reaches only at the end of the iteration. We prove soundness of the revised algorithm. Preliminary experiments confirm that the targeted old-white subsumption checks drop to zero and that the revised solver improves over the original implementation on the tested small random 3-SAT subset.

ABSTRACT. Kubernetes (K8s) is a widely-used container orchestration platform that brings significant complexity when it comes to ensuring correctness, security, and compliance in multitenant clusters. Tools like role-based access control and policies help enforce isolation, while audit logging helps detect misconfigurations. However, they often miss deeper correctness properties and are difficult to maintain at scale. Formal methods provide techniques that offer stronger guaranties and could be applied in this context. In distributed systems, formal methods are usually used at design time through model-checking by specifying an abstract model of the system and then exhaustively checking all possible behaviors. TLA+ is commonly used in this way as a specification language, together with the TLC model checker. In this paper, we present a monitoring tool that, at its core, utilizes TLA+ specifications: the tool utilizes a TLA+ trace-checking specification to detect violations in behavior inferred from K8s audit logs. Our primary use case focuses on multitenancy violations; however, the pipeline is not limited to that setting. Specifically, it demonstrates how formal reasoning can be incorporated into live K8s environments to improve monitoring and correctness checking.

ABSTRACT. Fast (fast.xyz) is a verifiable settlement infrastructure for AI-native work: humans, agents, services, and merchants coordinating work and settling outcomes, including payments, programmatically. This talk presents recent progress on Fast at Pi Squared Labs (pi2labs.org), starting with the FastSet weak consensus protocol that powers the Fast network. Unlike traditional systems that serialize transactions into one global order, FastSet processes independent claims in parallel, avoiding unnecessary consensus bottlenecks while preserving precise settlement semantics.

A central theme of the talk is verification. Fast does not treat correctness as an afterthought or a layer of audits around an implementation. The protocol is designed so that critical behavior can be specified, executed, and checked with formal methods. This gives stronger guarantees about what the system is allowed to accept, not just whether the network accepted it. The talk will also connect the protocol to real products: fast.xyz as the user and developer entry point, app.fast.xyz as an app for holding user and agent accounts and signing transactions, and shop.fast.xyz as a working example of agent-first commerce, where AI agents can discover merchants, prepare purchases, and participate in checkout flows.

ABSTRACT. We introduce a multimodal dataset of 4,069 ques- tions spanning all seven Romanian driving license categories to evaluate Llama 4 Scout, Gemma 3-27B, and Qwen3.6-35B. While the top model achieves 70.98% overall accuracy, all evaluated architectures suffer a severe performance collapse on multi- answer questions, highlighted by a 28.28 percentage point drop in the leading model. An automated taxonomy analysis of over 4,300 errors reveals that more than 80% of failures stem from systemic reasoning dependencies—specifically the misapplication of correct traffic rules rather than factual knowledge gaps. Per- formance peaks on text-based technical mechanics within heavy vehicle classifications (Categories C and D) but bottoms out on the mixed regulatory settings of License Reacquisition (Category R), demonstrating that future domain alignment must prioritize contextual reasoning consistency over factual knowledge scaling.

ABSTRACT. Large Language Models (LLMs) have become highly performant at solving mathematical problems on established datasets; yet the question of authentic reasoning versus pattern memorization remains open. We introduce RoJBMO, a benchmark of 508 problems from the Junior Balkan Mathematical Olympiad (JBMO), its official shortlists, and the Romanian Team Selection Tests-sources underrepresented in existing benchmarks. We evaluate 11 LLMs using an automated pipeline combining solution generation with LLM-as-a-Judge evaluation across five scoring dimensions. Reasoning models substantially outperform instruction-tuned ones: Kimi-K2.5 and Qwen3 235B A22B jointly lead with 6.97/10 and 6.90/10, respectively, while Llama 3.3 70B scores 3.75/10, with nearly all pairwise differences statistically significant. Scores are 3- 4.5 points lower than on the MATH benchmark under identical evaluation conditions, and a negative score- year correlation provides evidence of training data contamination.

ABSTRACT. Phishing email detection remains a critical challenge in cybersecurity, with existing datasets suffering from outdated vocabulary, monolingual coverage, and non-representative negative samples. This paper presents an end-to-end pipeline for generating and detecting multilingual synthetic phishing emails that combines Large Language Models (LLMs), Retrieval-Augmented Generation (RAG), and a self-correction quality gate. The pipeline produces a dataset of 16,818 emails across five European languages (Romanian, English, German, French, Italian). We evaluate five classification architectures, namely TF-IDF+LR, mDistilBERT, XLM-RoBERTa, mDeBERTa-v3, and ModernBERT, coupled with a systematic analysis of scaling laws. All models reach F1~1.0 from only 500 training examples. Cross-domain evaluation reveals a severe generalization gap (FNR=97.8%+/-0.5%, 3 seeds) when training exclusively on synthetic data; mixing in as little as 17\% real examples resolves it (FNR$->3.8%+/-1.3%), and a real-only control shows this gain comes mainly from having any real data at all, with mixed training's distinct value being that it retains full multilingual synthetic coverage that a real-only classifier cannot. Phishing generated by Qwen2.5-7B-Instruct evades a classifier trained on standard phishing in 40--44% of cases regardless of Group Relative Policy Optimization (GRPO) fine-tuning (base: 40.2%+/-12.9%, GRPO: 43.5%+/-11.0%, 3 seeds), indicating the adversarial advantage stems from generator stylistic diversity rather than reward-optimized evasion; an adversarial iterative game further shows the defender adapts completely after a single retraining round with 200 examples. Explainability analyses using LIME and Integrated Gradients confirm that classifiers learn relevant semantic phishing features rather than stylistic artifacts.

ABSTRACT. Relation extraction (RE) for low-resource languages is typically constrained by the lack of annotated corpora. We investigate the feasibility of cross-lingual RE for Romanian by combining automatic dataset translation with large language model (LLM) inference. We translate the SemEval-2010 Task 8 benchmark from English to Romanian using an LLMbased translation pipeline and evaluate two open-weight LLMs, Gemma 4 31B and Qwen 2.5 32B, under zero-shot, few-shot, and QLoRA fine-tuned configurations, against four encoder baselines spanning 125M to 560M parameters: XLM-RoBERTa (base and large), Romanian BERT, and RoBERT-large. We assess two task formulations: relation classification with marked entities and end-to-end extraction. Our results over the two large language models show that the cross-lingual gap in prompt-only settings is not distinguishable from zero when taking into account exemplar sampling variance, that few-shot prompting provides no consistent gains for Gemma, while Qwen shows a larger but variable improvement, particularly at k=5, and that QLoRA finetuning improves macro F1-Score by more than 22 percentage points in both languages while reducing the cross-lingual gap to 1.4pp for Gemma and 2.6pp for Qwen. The encoder baselines come within 0.8–4.3pp of QLoRA Gemma on Romanian despite being 50–250 times smaller, with monolingual Romanian BERT at 125M parameters matching multilingual XLM-R at 278M. Regarding end-to-end relation extraction, we find that a pipeline consisting of two 560M encoders (a span detector and a relation classifier) matches the stronger LLM on exact match and exceeds both on entity match, so the 31B LLMs may not be warranted when compute matters. We release the translated dataset, evaluation code, and trained models.

ABSTRACT. The rapid development of Large Language Models (LLMs) has raised interest in their ability to translate natural language descriptions of optimisation problems into formulations that can be passed to a solver. However, little attention has been paid to the requirements from industrial applications: guaranteeing solution validity and creating reusable formulations, often in languages that companies do not want to make public.

We study two LLM-based approaches to formulate industrial optimisation problems in a language without public documentation when the LLM was trained. A first case study indicates that LLMs can generate correct and competitive formulations that, in some cases, outperform manually crafted formulations. We observe a trade-off between allowing unconstrained formulation generation and enforcing structural constraints that support reusability and automated validation. These findings highlight both the potential and the limitations of an LLM-driven formulation of industrial optimisation problems.

ABSTRACT. Short-Term Load Forecasting (STLF) research often relies on proprietary data, limiting reproducibility, an issue especially acute for Central and Eastern European grids, where open load data are scarce despite demand patterns differing from Western Europe and North America. Prior Romanian load forecasting work used public TSO data but covered only the COVID-19 period and released no reusable dataset. We address this gap by releasing a multi-year, 15-minute resolution Romanian national load dataset, harmonized with population-weighted weather and holiday covariates, built entirely from open sources. We complement it with an exploratory analysis of temporal, climatic, and calendar-driven demand structure, plus a reproducible benchmark, from classical baselines to gradient-boosted trees, testing whether open-data models can match performance reported with proprietary data.

ABSTRACT. Extremal graph theory over vertex-degree-based topological indices increasingly relies on computation: to scope conjectures, to catch errors before proofs, and to settle instances that resist closed forms. We describe a verification-first pipeline developed inside a research programme on the inverse degree index, the sum over all vertices of the reciprocal of the degree. The pipeline combines exhaustive-first enumeration of graph classes, a two-tier isomorphism-reduction discipline with explicitly reported approximation caveats, exhaustive realization enumeration for fixed degree sequences, unbiased edge-swap walks where enumeration is infeasible, and two counting layers (realizability-aware Burnside counts and Ehrhart quasipolynomial fits). We report three case studies. First, a replication study of a real in-project false negative: an independence-number-guided search, a heuristic steered by intermediate independence-number evaluations, once produced a wrong optimality claim by missing a realization, but a controlled study shows guided heuristics robust on the four validated instances at the tested scales, so the defensible rule is exhaustive-first with full-band scans rather than a blanket distrust of guidance. Second, we settle seven instances of an open extremal problem, the deficiency-one optimum of the independence-constrained maximization of the index at cyclomatic numbers four through eight, exhaustively: the clean closed-form candidate provably fails realizability from cyclomatic number four on, two shape conjectures fitted to the accumulating data were each falsified live by the next out-of-sample instance, and the optimum shape keeps shifting through cyclomatic number eight. The instances stand as sharp boundary data for the open problem. Third, we show the pipeline operating at theorem scale, as the falsification layer behind recently proved dichotomy and trichotomy theorems for all strictly convex underlying functions. All numbers in this paper were regenerated from scratch for this submission.

ABSTRACT. A vertex-degree-based topological index assigns a number to every graph by summing a fixed function of the vertex degrees. The extremal-graph literature asks which member of a family maximizes or minimizes such an index; we ask the stronger question of when the index is injective on the family, ordering even its structurally close interior pairs. Taking the banana trees of fixed order as a testbed, we give a computational criterion: the completely monotone indices order the family if and only if an explicit integer-coefficient separation polynomial attached to each pair of members has no root in the open unit interval. Two consequences follow. Negatively, no smoothness class of index functions, up to and including complete monotonicity, orders the banana trees at all orders: one tuned exponential collides a pair already at twenty-five vertices. Positively, a simple decay condition orders the standard decreasing indices, with an exact reach on the scale families and a computer-assisted census locating the catalogue. We also abstract the criterion into a positive/negative test and settle eight worked families with it. Both sides transfer to edge indices. All results are computer-assisted but hand-checkable, and a companion script regenerates them. One open problem is posed.

ABSTRACT. Large Language Models (LLMs) frequently produce confident but incorrect answers, commonly called hallucinations, which limit their reliability in high stakes domains. We study this problem in the setting of multiple choice question answering, where it becomes a selective prediction task: the goal is to recognise when an answer is likely wrong and to replace it with an explicit abstention. Across four benchmarks (MMLU Pro, ARC Challenge, MedQA, TruthfulQA) and the gpt-4o-mini model, we first show that no single confidence signal, namely self reported confidence, answer token log probabilities, or multi sample consistency, reliably separates correct from incorrect answers on its own. Combining the signals in a multi signal detector reaches a cross validated AUROC of 0.79-0.81 on MMLU Pro and 0.78-0.88 when transferred to an unseen benchmark, and reduces the error rate among the retained half of the answers by 33-41%. The log probability features carry almost all of this performance and the five sample consistency features add nothing. We then analyse cost based abstention policies and the effect of prompting style on calibration and detector transfer. Finally, for the open weight Qwen 2.5 7B model, we train lightweight classifiers on hidden state activations and attention entropy collected in a single forward pass, reaching an AUROC of 0.72 from a single layer of the 4 bit model and 0.76 from all layers of the uncompressed model, on par with a SAPLMA style probe and with the model's own answer token probability (0.74), and far above its verbalised confidence (0.63) and sampling consistency (0.60), without any additional generation. Within the scope of multiple choice question answering, the probabilities and hidden states a model computes are thus more informative about the correctness of its answers than what it says about them. Open ended generation is left for future work.

ABSTRACT. The gravitational N-body problem is a fundamental and challenging topic in physics and computational science, involving the prediction of the motion of N interacting bodies under mutual gravitational forces. While the two-body problem admits analytical solutions, systems with three or more bodies exhibit highly nonlinear behavior, and no general analytical solution is known. This work explores the use of neural networks to predict the dynamics of N-body systems, using an N-body simulator developed from scratch to generate ground-truth data. A systematic comparative study is then performed across five neural network architectures: a baseline Multilayer Perceptron, a temporal Long Short-Term Memory network, a standard Graph Neural Network, and two physics-constrained models, Graph Neural Ordinary Differential Equation (GNODE) and Physics-Informed Graph Neural Network (PI-GNN). The models are evaluated on trajectory prediction accuracy, zero-shot generalization, conservation of physical quantities, and inference runtime. The results show that GNODE and PI-GNN achieve the best overall performance among the evaluated models, highlighting the importance of integrating physical knowledge into deep learning models for physically consistent simulations.

ABSTRACT. Detection of code smells plays a significant role in the software engineering domain, aiming to enhance code quality by identifying potential issues and improving the maintainability of software systems. With the current boost of machine learning methods applied to software engineering problems, several scientific contributions exist in the domain, raising a need for assessing their suitability and performance. This contribution is an evaluation experiment study that assesses evaluating eight artificial intelligent models including seven machine learning approaches (Decision Trees, Support Vector Machines, Naive Bayes, Random Forests, k-Nearest Neighbors), neural networks such as Long Short-Term Memory (LSTM) and Convolutional Neural Networks (CNNs), alongside with Genetic Algorithms, on a dataset comprised of 23 Python projects. The purpose is to find out the performance and suitability of the intelligent models in detecting code smells. The results show that kNN and Naive Bayes are the best performing models for classifying code smells, each having the best score for 5 out of 10 code smells classified, closely followed by Decision Trees. In terms of suitability, kNN seems appropriate for less complex code smells like Long Method, Long Parameter List and Large Class, while Naive Bayes gives best results for the rest of the code smells. The findings of our evaluation also showed that the performance and suitability is very dependent on model configuration and the representativeness of code smells in the dataset.

ABSTRACT. This paper introduces a novel wireframe parsing framework based on geometrically guided graphs built from local corner structures. Unlike current methods that treat wireframe parsing as a learned end-to-end problem, the proposed method takes a bottom-up approach that uses a novel corner descriptor able to directly guide the construction of a structured graph whose topology is supported by local geometric evidence. By grounding graph construction in local geometric context, the method promotes structurally plausible matches and suppresses inconsistent corner to corner associations.

ABSTRACT. This paper presents the formalization in Dafny of the Omega Test, an algorithm used to decide the satisfiability of a system of inequalities. The implementation defines executable representations for rational numbers, linear expressions, inequalities, and systems of constraints, together with their semantic interpretation through valuations. The verified elimination procedure combines real shadow, dark shadow, and grey-shadow branches in order to obtain variable-free projections and reason about satisfiability over integers. This paper focuses on connecting the mathematical structures and operations used in the Omega Test to the Dafny representations and proof obligations required to verify their correctness.

ABSTRACT. Solving a problem using an effective procedure or computability is a crucial concept when it comes to analyzing the inner workings of a program. This article proposes formalizations of two famous computational models, Turing machines and Lambda Calculus, in Dafny, a verification-aware programming language. Furthermore, it offers an application that proves the termination of a simple Turing Machine, a demo for the proof of the Church Encoding, and a mechanical proof of the famous Church-Rosser theorem

ABSTRACT. The large safety instrumentation & control (I&C) systems in civil nuclear power plants (NPPs) are mainly safe-shutdown systems (reactor protection) or limitation and control systems. Framatome’s established TELEPERM XS (TXS Core) product family is a digital I&C system platform to cover all these applications. We illustrate the role of verification in the different stages of the software production toolchain, focus on the formal compilation process, and discuss the contribution of the CompCert certified compiler to the safety case of the product. Scrutinizing the object code produced by this compiler has exhibited suboptimal run-time performance in a certain simple but recurring generated code pattern. We explain how formal methods allow us to address this issue in the compiler while simultaneously reducing its trusted computing base (TCB), thereby strengthening the safety case rather than merely preserving it.

ABSTRACT. Doubly Linked Lists (DLLs) are notoriously difficult to formalise for verification. A second layer of difficulty comes from implementing this type of self-referential data structure in Rust, a language with its own constraints: aliasing, ownership, and lifetimes. Even with modern tools for formal verification, such as Verus, DLL verification demands substantial effort and time. Weak specifications result from the excessive use of unproven assumptions, modeled by assumed statements and axiomatic lemmas. We investigate whether LLM agents can synthesize strong DLL specifications while minimising these trusted bases. The analysis follows three different approaches: manual verification, property-specific verification, and a defined skill for the specific case of DLLs and certain properties of this type of data structure. The skill encodes domain knowledge and a task-decomposition strategy. We show that an LLM agent equipped with a carefully designed verification skill can generate strong, low-trust specifications for DLLs in Verus.

ABSTRACT. AI systems increasingly operate between flexible input representations and formal objects used by downstream tools. A key challenge is recognizing when an unfamiliar formulation denotes a known formal object. We study this challenge through theorem recognition: given an equivalence-preserving transformation of a theorem condition, a model must recover the theorem identity associated with the standard statement. We introduce TREAT, a benchmark for evaluating whether large language models can recover known theorem identities from equivalence-preserving formula-level transformations. Rather than paraphrasing theorem text, TREAT changes the mathematical form of theorem conditions themselves, expressing known results through residual equations, witness statements, optimization identities, set relations, operator forms, and proof-intermediate characterizations. Starting from scraped theorem pages, we filter for entries with usable mathematical expression forms, extract canonical theorem conditions, and generate transformed variants with recorded assumptions and inverse mappings. The final corpus contains 737 theorem identities and 29,480 transformed rows. On a test panel, the best model retrieves the correct theorem identity in only 60.73\% of cases. Other systems reveal different failure modes, including abstention, wrong detection, and malformed outputs. These suggest that theorem knowledge can be fragile under equivalent changes in representation. TREAT therefore provides a controlled testbed for evaluating representation-robust access to formal knowledge, with broader relevance to domains that require stable target objects, explicit equivalence relations, validation procedures, and auditable scoring.

ABSTRACT. Automatic segmentation of brain tumors from MRI scans is a critical task at the intersection of medical imaging and deep learning. This paper investigates two multimodal fusion strategies for adapting the TransResU-Net architecture to multi-sequence MRI input: early fusion, where modalities are concatenated at the input level, and intermediate fusion, where each modality is processed by a dedicated ResNet50 encoder before feature-level integration. Both strategies are evaluated on three publicly available datasets that cover different pathological contexts: BrainMetShare (brain metastases), REMBRANDT (adult primary tumors), and BraTS-PED (pediatric primary tumors). The results show that multimodal models consistently outperform unimodal baselines, with Dice score gains of up to 6.1 percentage points. Among individual modalities, FLAIR and T2 emerge as the most informative for whole-tumor binary segmentation. The FLAIR+T2 early fusion configuration achieves competitive or superior results compared to using all four modalities, suggesting that a well-selected subset of modalities can offer a favorable trade-off between performance and computational cost. Intermediate fusion yields the best overall result on BrainMetShare (Dice 83.6%), but does not consistently outperform early fusion on the other datasets, indicating that the benefit of dedicated per-modality encoders is conditioned on dataset characteristics.

ABSTRACT. Text-to-SQL systems translate a natural-language question into an SQL query. In practice, users often evaluate the execution rate (ER): the share of generated queries that run without error. Since queries can run and still return wrong answers, the BIRD benchmark defines execution accuracy (BEX): the returned result must exactly match the gold result. We measure how database metadata affects BEX for six large language models from three providers on the PostgreSQL BIRD Mini-Dev benchmark (500 questions, 11 databases, 21,000 evaluations). We organize and derive context into four metadata dimensions: data dictionary, query patterns, business context, and domain knowledge. We compare prompts that add these dimensions one at a time, remove them one at a time from the full set, or replace them with irrelevant distractor text. Full metadata raises BEX by 16.7-21.0% over the distractor control across all models. The benefit is real but not sufficient: at full metadata, ER still exceeds BEX by 30 to 38 points on every model, so a query that runs is often still wrong. The dimensions contribute unequally and by metric: query patterns protect execution, and business context improves value correctness, with statistically confirmed effects on two of the three ablation models. We present the controlled multi-dimensional ablation, a released reproduction package, and practical guidance for evaluating text-to-SQL applications using benchmarks and metrics such as execution accuracy.

ABSTRACT. The Internet of Things (IoT) is a rapidly growing field, with billions of devices connected to the internet. The Matter protocol is a new standard for IoT devices that aims to provide interoperability and security. In this paper, we propose a method for detecting the class of Matter devices based on their encrypted network traffic using tree-based machine learning techniques. We evaluate the performance of Decision Tree, Random Forest, and XGBoost models in classifying the device classes. Our best model achieves over 89% accuracy in identifying 7 classes of devices, outperforming the only available solution in this field (Schlett et al.), which only identifies 4 classes of devices. We also analyze the impact of different features on the performance of the models, and we test their resource consumption on a real router, proving that the models can be deployed in real-world scenarios.

ABSTRACT. Although multi-layered verification frameworks, such as that proposed by Rabhi et al., have shown promise against grey-box threats, their resilience in white-box scenarios and their ability to generalize to unseen data remain underexplored. This paper implements a hybrid ResNet18 + Bi-GRU discriminator alongside a speech-to-text (STT) validation layer, and evaluates its performance against a white-box attacker with full gradient and dataset access. We show a critical 'phonetic boundary': perturbations that are successful against the detector corrupt the linguistic coherence required by the STT layer in the vast majority of cases, neutralizing the attack. The STT layer can also serve as a generalization tool, increasing Bonafide Recall from 1.75% to 81% on external, non-homogeneous data. These results show that multi-layering can be used for practical, generalizable deepfake detection.

ABSTRACT. Biometric systems are becoming more accurate and portable as time goes by, but one of the challenges that persists for voice-based biometric extraction/detection systems is the background noise that disrupts the performance. This study presents a portable sound processing framework to prevent noise distortions that enhances speech prior to speaker embedding extraction, integrating a multi-head attention module to our Full-band and Sub-band Path Extension Network baseline model, that plays a crucial role in feature detection. Our solution is designed with the computational constraints of portable health monitoring devices in mind, such as hearing aids, improving robustness under noisy conditions. The results highlight potential improvements in speaker recognition systems by processing the frequencies of the audio signal in a multispectral manner.

ABSTRACT. For deep learning to be used in fields such as healthcare, we need to be able to build trust and interpretability in the specific model. To solve this problem, a series of explainable artificial intelligence (XAI) methods have been created. In this study, we conducted a comparative analysis of the effect that the architecture of a deep learning model for anomaly detection has on the results of an XAI algorithm. We employed the capabilities of SHAP, LIME and Grad-CAM and used those methods on a trained (convolutional) autoencoder and a variational variant. The study demonstrated that the methods indeed struggle more on anomalous regions. Furthermore, the change in architecture improved the agreement between SHAP and Grad-CAM.

ABSTRACT. Correctly identifying engine-bay components is the first step in most automotive service workflows, yet it remains largely manual and there is no public object-detection dataset whose taxonomy matches the diagnostic and spare-parts use case. We address this gap with two contributions. First, we build a consolidated, eight-class engine-component detection dataset of roughly 2900 images by merging and normalising two public sources onto a common taxonomy, deduplicating on a per-source basis using perceptual hashing, and verifying a leakage-free train/validation/test partition (2013/440/445 images) with no source appearing in more than one split. Second, we use this dataset to run an in-domain comparison of three YOLOv11 variants (n, s and m) trained under identical conditions, together with a controlled augmentation ablation. The deployed model reaches mAP@0.5 = 0.879 on the leakage-checked test set, while the in-domain variant comparison shows the small variant matching the medium one at less than half the size, indicating that added capacity is not converted into accuracy on this dataset. A per-class analysis shows that small, visually distinctive parts photographed in isolation are detected far more reliably than large components embedded in cluttered engine-bay scenes; for the latter, the dominant error is missed detection rather than inter-class confusion. We release the consolidation pipeline, the dataset and the trained baselines to support reproducible work on this detection task.

ABSTRACT. Most medical record management systems work as repositories for clinical documents: they store and display files, but do not correlate them or help interpret the information accumulated over time. This paper presents MyMed, a web platform that pairs patient-centered medical record management with AI-assisted laboratory report analysis, bringing together secure communication, appointment scheduling, centralized document storage, and an asynchronous AI pipeline that extracts structured data, normalizes laboratory parameters to a common canonical name, and generates plain-language summaries. Document management and AI processing are decoupled through internal events, so a failed analysis never breaks an upload. Every AI-generated summary passes an automated faithfulness check before it reaches the user; summaries that fail it are replaced by a deterministic template-based version, and the physician keeps the final say through an accept/edit/reject step. On a benchmark of twenty complete blood count (CBC) reports, every value the pipeline did extract was correct, which is a consequence of a conservative design that omits uncertain values rather than guessing, with OCR recall on scanned documents as the main limitation: values were missed rather than misread. The results argue for a rule-based, audit-friendly extraction pipeline paired with a necessary faithfulness safeguard for LLM-generated content, keeping transparency, auditability, and patient control over sensitive data.

ABSTRACT. This paper addresses a critical trade-off in modern digital security: the lack of auditable data transit in standard, secure-by-design elliptic curve cryptography (ECC) primitives. While widely adopted commercial standards, such as NIST P-256 and Curve25519, exhibit high performance and robust privacy, their mathematical opacity prevents legitimate data monitoring without exposing the long-term private keys of the end-to-end communication nodes. To resolve this issue, we evaluate the feasibility of a malleable, trapdoored Naccache-Stern-type elliptic curve scheme defined over the ring Zn. By configuring a smooth group order, an authorized auditor holding the factorization of the modulus can bypass the Elliptic Curve Discrete Logarithm Problem (ECDLP) using a local Pohlig-Hellman reduction. We present a custom implementation in Python and perform a comparative analysis between the auditable Naccache-Stern setup and standard opaque curves in terms of computation time, memory payload, and theoretical security. Furthermore, we assess the vulnerability of these primitives in the post-quantum era by simulating Shor’s period-finding algorithm on noisy simulators and executing it on real 156-qubit physical IBM Quantum hardware (ibm marrakesh), analyzing how NISQ physical noise degrades quantum fidelity.

ABSTRACT. We present a domain-theoretical formalization of interaction trees in the Rocq prover. Unlike existing formalizations, ours does not rely on Rocq’s built-in coinduction. Hence, we avoid complications occuring in earlier works, such as artificially including silent steps to comply with Rocq's productivity checker, treating monad laws as weak bisimulations, and coinductive bisimulation reasoning.

We define an inductive program equivalence relation as the congruence closure of a base relation on primitive effects with respect to action sequencing and least upper bounds. This enables reasoning about possibly non-terminating programs by reducing their equivalences to equivalences of their terminating approximations, which are then proved by induction.

This relation is proved correct: provided the base relation is correct, equivalent computations have equal denotations in any monad that faithfully implements the effects.

We illustrate the framework by showing the equivalence of two programs encoding the Syracuse sequence, whose termination is an open mathematical conjecture.

ABSTRACT. This is a case study on a specific version of the Patience Sort algorithm in which we illustrate the evolution of it from an intuitive but inefficient nested recursion into a more complex but more efficient tail recursion, together with its formal certification in two distinct systems: Theorema and Rocq (formerly Coq). We identify some general principles of algorithm transformation, and we develop the necessary background theory and domain-specific proof methods needed for the natural style certification process. As a significant distinctive aspect, the approach in Theorema uses multisets, which simplifies the whole process and makes it more intuitive. The certification process reveals significant differences between the Theorema and Rocq frameworks, particularly in terms of proof style, automation, and structure. We provide a comparative analysis of these with respect to algorithm definition, proof development, and proof effort. This analysis offers insights into how algorithm design influences the complexity and structure of formal proofs, contributes to a better understanding of cross-system certification and demonstrates how non-trivial algorithms can be effectively verified across different formal frameworks.