Neapolis University Paphos

Certified program synthesis (aka vericoding) is the process of automatically generating a program, its formal specification, and a machine-checkable proof of their alignment from a natural-language description. Two challenges make vericoding difficult. First, specifications synthesised from natural language are often either too weak to be meaningful or too strong to be implementable, yet existing approaches lack systematic means to detect such defects. Second, the landscape of program verifiers is fragmented: each tool supports a particular reasoning mode – auto-active (e.g., Dafny, Verus) or interactive (e.g., Coq, Lean) – with its own trade-off between automation and expressivity. This forces every synthesis methodology to be tailored to a single verification paradigm, limiting the class of tasks it can handle effectively. We overcome both challenges by structuring the certified synthesis workflow around a multi-modal verifier – a single tool combining dynamic validation, automated proofs, and interactive proof scripting in one foundational framework. We realise this idea in LeetProof, an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean. Multi-modality enables LeetProof to validate generated specifications via randomised property-based testing before any code is synthesised, decompose the synthesis task into sub-problems guided by verification conditions, and delegate residual proof obligations to frontier AI provers specialised for Lean. We evaluate LeetProof on benchmarks derived from prior work on certified synthesis. Our specification validation uncovers defects in existing reference benchmarks, and LeetProof's staged pipeline achieves a significantly higher rate of fully certified solutions than a single-mode baseline at the same budget – consistently across two frontier LLM backends.

The quality of subword tokenization is critical for Large Language Models, yet evaluating tokenizers for morphologically rich Uralic languages is hampered by the lack of clean morpheme lexicons. We introduce SampoNLP, a corpus-free toolkit for morphological lexicon creation using MDL-inspired Self-Referential Atomicity Scoring, which filters composite forms through internal structural cues - suited for low-resource settings. Using the high-purity lexicons generated by SampoNLP for Finnish, Hungarian, and Estonian, we conduct a systematic evaluation of BPE tokenizers across a range of vocabulary sizes (8k-256k). We propose a unified metric, the Integrated Performance Score (IPS), to navigate the trade-off between morpheme coverage and over-splitting. By analyzing the IPS curves, we identify the "elbow points" of diminishing returns and provide the first empirically grounded recommendations for optimal vocabulary sizes (k) in these languages. Our study not only offers practical guidance but also quantitatively demonstrates the limitations of standard BPE for highly agglutinative languages. The SampoNLP library and all generated resources are made publicly available: https://github.com/AragonerUA/SampoNLP

We present Velvet—a Dafny-style verifier for imperative programs embedded in the Lean proof assistant. Like Dafny, Velvet supports reasoning about effectful programs featuring mutable state, loops, and non-determinism. Unlike Dafny, Velvet seamlessly combines automated SMT-based proofs with the interactive proof mode of the Lean proof assistant, in which it is embedded, thus enabling multi-modal proofs. Implemented as a Lean library, Velvet enjoys interaction with the rest of the Lean ecosystem, and in particular, with its automation tactics and rich library of mathematical theories. In this paper, we give a tour of Velvet ’s features, outline the techniques underlying its implementation, and evaluate its performance and expressivity in comparison with Dafny.

In this study, we examine the impact of residence-by-investment programs on collaborative economy platforms, particularly in the context of Greece’s tourism sector. Recent policy interventions have introduced significant restrictions on these programs, aiming to address housing shortages, but have inadvertently affected the short-term rental market. Our findings suggest that residence-by-investment programs play a crucial role in sustaining the growth of collaborative economy platforms, as investors often engage in short-term rentals to generate returns on their properties. These results underscore the importance of carefully balancing regulatory changes with economic incentives. Restrictive policies could dampen investment-driven tourism growth, while well-structured residence-by-investment programs may provide a pathway for sustainable tourism development. Our findings contribute to the broader discussion on tourism, digital business models, and the evolving regulatory landscape surrounding the collaborative economy.

Bit addition arises virtually everywhere in digital circuits: arithmetic operations, increment/decrement operators, computing addresses and table indices, and so on. Since bit addition is such a basic task in Boolean circuit synthesis, a lot of research has been done on constructing efficient circuits for various special cases of it. A vast majority of these results are devoted to optimizing the circuit depth (also known as delay). In this paper, we investigate the circuit size (also known as area) over the full binary basis of bit addition. Most of the known circuits are built from Half Adders and Full Adders as suggested by Dadda in 1965 for designing multiplier circuits. Applying these ideas to the bit addition function, one gets a 5n - 3m upper bound on its circuit size, where n is the number of input bits and m is the number of output bits. We prove an upper bound 4.5n - 2m. In the regimes where m is small compared to n (for example, for computing the sum of n bits or multiplying two n-bit integers), this leads to 10% improvement. We also show that it is provably impossible to improve the two upper bounds above to 5n - 3.01m or 4.5n - 2.51m. We achieve this by establishing that the circuit size of the increment function (a special case of the bit addition function with m = n + 1) is equal to 2n. We complement our theoretical result by an open-source implementation of generators producing circuits for bit addition and multiplication. The generators allow one to produce the corresponding circuits in two lines of code and to compare them to existing designs.