Introduction

Knowledge Representation and Reasoning (KRR) formalisms, such as Datalog and its extensions, are gathering increasing attention in industrial contexts. This is particularly evident in the financial sector, with applications in the so-called Decentralized Finance (DeFi), a novel financial paradigm that leverages distributed ledger technologies to offer services without intermediaries. Logical languages such as Datalog effectively balance expressive power and computational complexity, enabling, thanks to their extension to the temporal dimension, the creation of concise and efficiently executable formalizations of smart contracts, i.e., executable scripts that implement a financial asset [1,2,3]. Additionally, the inherent step-by-step nature of logical reasoning aligns closely with concepts of explainability, thereby supporting transparency in decision-making activities. The declarative paradigm promotes simplicity, trustworthiness, compactness, and code comprehensibility, making it algorithm-independent and more aligned with high-level specifications, policies, and standards. Among these, the recent Markets in Crypto-Assets Regulation (MiCAR) of the European Union [4] introduces rules for crypto-activity issuers, such as the requirements for white papers, i.e., semi-structured documents containing all information about the crypto assets being offered or admitted to trading. The availability of such Information on the reserve of assets 7

Table 1

Templates for e-money (left) and asset-references (right) token white paper contents.

templates is appealing if combined with the impressive power of state-of-the-art Large Language Models (LLMs), which have proved to be capable of understanding and manipulating complex unstructured data as text. One of the most promising applications is using LLMs to analyze white papers, their compliance with rules, and their features, which may impact financial markets, raising the interest of financial authorities. Leveraging Large Language Models for the automatic translation of natural language descriptions into executable code on a blockchain is a novel and unexplored field due to the challenges of (i) converting text to programming languages an LLM has rarely seen, and (ii) ensuring the fidelity and quality of the translated content [5]. Recent works, such as SolMover [6], build frameworks that, by employing LLMs, try to understand coding concepts and use them to translate from a code like Solidity into a non-trained source language. While results are promising, this approach is a code-to-code translation, thus not directly a natural language (NL)-to-code translation. Other works are based on a human-LLM continuous dialogue, such as via ChatGPT, that supports the writing of Solidity code for smart contracts, although human intervention and correction are still required [7].

Contribution.

In this short work, we present our preliminary approach that aims at translating white papers into an executable and inherently transparent language as DatalogMTL. Our approach leverages the semi-structured format enforced by the MiCAR to build a pipeline that supports a pre-trained LLM agent in the translation task by (i) reducing the amount of information passed to the model, filtering in only specific sections of the white paper, and (ii) implementing token-specific pre-and post-processing steps that help the LLM achieve an executable output.

Background

In this section, we briefly recall DatalogMTL foundations required for its use in crypto-activity modelling, i.e., to model smart contracts. Then, we outline the main aspects of interest introduced by the MiCAR.

DatalogMTL. DatalogMTL [8,9] is a recently developed extension of Datalog with operators from Metric Temporal Logic (MTL) interpreted over the rational timeline and with stratified negation under stable model semantics. In [10], we showed how the only required temporal operator for implementing financial markets in DatalogMTL is the use of ⊟ [𝑡 1 ,𝑡 2 ] over a punctual interval, i.e., up to 𝑡 1 = 𝑡 2 . Informally speaking, given the rule ⊟ [𝑡 1 ,𝑡 2 ] 𝐴 1 → 𝐴 2 and a time interval [𝑥, 𝑦], the ⊟ operator defines the satisfaction of an atom 𝐴 2 within the interval [𝑥 + 𝑡 2 , 𝑦 + 𝑡 1 ], based on the continuous satisfaction of an atom 𝐴 1 within the interval [𝑥, 𝑦], where 𝑥 + 𝑡 2 ≤ 𝑦 + 𝑡 1 . The idea is that, by considering punctual intervals, we can model the evolving market at any timestamp and create rules that react in case an event occurs, such as a transfer of assets between two market participants.

The MiCA Regulation in the EU. The Markets in Crypto-Assets (MiCA) regulation, enacted by the European Union, covers three categories: asset-referenced tokens, e-money tokens, and other crypto-assets. Since the scope of the third category is broader, in this work we will focus only on the first two more specific tokens. For each crypto asset category, the MiCAR contains norms regarding the content of the white paper. While no official template has been published yet, we report in Table 1 the likely structure of the templates, following the consultations that are in progress [11].

LLM-based White Paper Translation Pipeline

The problem of translating an arbitrary NL whitepaper into a DatalogMTL specification is inherently complex and our experience shows that pure machine translation approaches, where the LLM is directly tasked with the NL-to-DatalogMTL translation goal (even when fine-tuning is involved) are not effective and lead to arbitrary programs, highly affected by hallucinations and overall incorrect. To overcome these difficulties, we suggest a paradigm shift and follow a template-based technique, implemented in the pipeline shown in Figure 1. Overview. We pre-define a set of market mechanisms ℳ that represent standard "functional components" of a market, such as creation (minting), selling of a token (redemption), and so on. For each pattern, we feature pre-built templatized (i.e., with formal variables) DatalogMTL rules decorated with a natural language description. Examples are in Figure 2. Then, given a white paper, we can first select the templatized rules according to the token type, and iteratively prompt the LLM with all the information required to specialize the rules to the white paper content. LLM-based Rules Specialization. Algorithm 1 describes the process we developed to adapt the generic rules to the token-specific features. Based on a custom input MiCAR-compliant white paper, the corresponding set of templatized rules Σ, either e-money token or asset-referenced token, is considered. Then, for each market mechanism 𝑀 of the set ℳ of mechanisms (line 1), we consider the set of templatized rules 𝑅, their description 𝐷 that we have pre-defined, and we extract the portion 𝐼 of the white paper that contains relevant information for the mechanism (lines 2-4). Each mechanism is also decorated with a set of keywords 𝒦, which describe the content of the mechanism and activate optional pre-processing steps (lines 5-7). Thus, if the mechanism deals with one of the topics defined by the keywords, a pre-processing LLM call will be performed to rewrite the information that was inserted in the white paper fields. The aim of this step is to support the LLM-translation task by simplifying, if possible, the textual input. For instance, this is the case of temporal information such as the specification of market opening days, which can be defined in multiple formats, e.g., the market is closed on weekends. Then, the LLM is provided 𝑅, 𝐷 and 𝐼 and is prompted to perform the actual specification (line 8): "These are Datalog rules: {R} where {D}. Modify them according to this information: {I}" Finally, the LLM generates the translated rules, and we perform post-processing checks (line 9-11), such as detection of syntax or programmatically identifiable errors. In case checks are not passed, the LLM is asked to repeat the task until they are passed. Minting 𝑞 is the minimum quantity that it's possible to hold 𝑞 is the minimum quantity that it's possible to hold ⊟ , 𝐵𝑎𝑙𝑎𝑛𝑐𝑒 𝑢, 𝑛 , 𝑅𝑒𝑑𝑒𝑒𝑚𝑂𝑟𝑑𝑒𝑟 𝑢, 𝑞 , 𝑞 ≤ 𝑛 → 𝑅𝑒𝑑𝑒𝑒𝑚(𝑢, 𝑞) ⊟ , 𝐵𝑎𝑙𝑎𝑛𝑐𝑒 𝑢, 𝑛 , 𝑅𝑒𝑑𝑒𝑒𝑚𝑂𝑟𝑑𝑒𝑟 𝑢, 𝑞 , 𝑞 ≤ 𝑛 → 𝑅𝑒𝑑𝑒𝑒𝑚(𝑢, 𝑞)

Redemption

The rule describes that you need enough units in balance for redeeming The rule describes that you need enough units in balance for redeeming ⊟ , 𝐵𝑎𝑙𝑎𝑛𝑐𝑒 𝑠, 𝑜 , 𝑇𝑟𝑎𝑛𝑠𝑓𝑒𝑟 𝑠, 𝑟, 𝑢, 𝑏 , 𝑏 = 𝑏 , 𝑜 ≥ 𝑢 → 𝑇𝑟𝑎𝑛𝑠𝑓𝑒𝑟𝐴𝑝𝑝𝑟𝑜𝑣𝑒𝑑(𝑠, 𝑟, 𝑢, 𝑏) ⊟ , 𝐵𝑎𝑙𝑎𝑛𝑐𝑒 𝑠, 𝑜 , 𝑇𝑟𝑎𝑛𝑠𝑓𝑒𝑟 𝑠, 𝑟, 𝑢, 𝑏 , 𝑏 = 𝑏 , 𝑜 < 𝑢 → 𝑇𝑟𝑎𝑛𝑠𝑓𝑒𝑟𝐷𝑒𝑛𝑖𝑒𝑑(𝑠, 𝑟, 𝑢, 𝑏) ⊟ , 𝐵𝑎𝑙𝑎𝑛𝑐𝑒 𝑠, 𝑜 , 𝑇𝑟𝑎𝑛𝑠𝑓𝑒𝑟 𝑠, 𝑟, 𝑢, 𝑏 , 𝑏 = 𝑏 , 𝑜 ≥ 𝑢 → 𝑇𝑟𝑎𝑛𝑠𝑓𝑒𝑟𝐴𝑝𝑝𝑟𝑜𝑣𝑒𝑑 𝑠, 𝑟, 𝑢, 𝑏 ⊟ , 𝐵𝑎𝑙𝑎𝑛𝑐𝑒 𝑠, 𝑜 , 𝑇𝑟𝑎𝑛𝑠𝑓𝑒𝑟 𝑠, 𝑟, 𝑢, 𝑏 , 𝑏 = 𝑏 , 𝑜 < 𝑢 → 𝑇𝑟𝑎𝑛𝑠𝑓𝑒𝑟𝐷𝑒𝑛𝑖𝑒𝑑(𝑠, 𝑟, 𝑢, 𝑏)

Transfer

𝑏 is a supported blockchain for the token 𝑏 is a supported blockchain for the token Figure 2: Examples of templatized rules Σ of some relevant token mechanisms, namely, the collateral acceptance terms, minting and redemption, and transfer conditions. Each mechanism is defined as a pair of DatalogMTL rules -NL description that illustrates some relevant aspects of the rules, i.e., either the role of the variables or a generic description. The number of pre-defined rules in the mechanism is arbitrary and, as we shall see, will help the translation mechanism. Possible differences between e-money tokens and asset-referenced ones might refer either to the rules or to the descriptions and depend on the different nature of the token.

Algorithm 1 Rules Specialization. ◁ LLM is asked to rewrite the information 7: end if 8:

𝑅 * ← LLMPrompt(𝑅, 𝐷, 𝐼)

◁ LLM is prompted to adapt the rules R according to I 9: while 𝑅 * .𝑐ℎ𝑒𝑐𝑘𝑠 not passed do 10:

𝑅 * ← 𝐿𝐿𝑀 𝑃 𝑟𝑜𝑚𝑝𝑡(𝑅, 𝐷, 𝐼)

◁ LLM is asked to repeat the task 11: end while 12: end for For our preliminary experiments and tests, we employed a pre-trained LLaMA 3 70B as our reference LLM. The model was prompted with system content providing a generic DatalogMTL adaptation example. We opted not to perform fine-tuning since (i) few-shot learning demonstrated promising results in our initial trials, and (ii) there is a current lack of large-scale datasets of DatalogMTL rules.

Example 1 (X-Coin -Supported Blockchain). Consider the market mechanism 𝑀 = Transfer for a hypothetical e-money token named X-Coin. It defines the conditions required by the white paper for the approval of a transfer of tokens between a Sender 𝑠 and a

Receiver 𝑟 of 𝑢 units on the blockchain 𝑏. For instance, suppose the only main conditions for approving a transfer are (i) having enough tokens in the sender's balance, and (ii) that the transfer occurs on a supported blockchain. Figure 3 illustrates the pipeline in action for the Transfer mechanism. In this example, the variable 𝑏 1 (refer to Figure 2) has been instantiated and the model has also created additional rules to account for the multiple blockchains, i.e., inserting OR conditions. To achieve this, the input has been automatically pre-processed: since the mechanism referred to the supported blockchain technology, a step to separate each blockchain type has been activated. Then, post-processing checks have controlled the syntax in the output, such as the presence of all initial predicates and the absence of additional undesired predicates.

DatalogMTL Market Formalization.

By collecting all the rules that have been generated or modified in Algorithm 1, we can create a DatalogMTL program that formalizes the token's specific market that, if extensional facts are injected, is executable in a DatalogMTL engine. Full examples of our approach over existing crypto activities, converting natural language white papers into a DatalogMTL formalization, can be found in our repository [12]. Such programs are executable if the required extensional facts are provided and replicate the conditions laid out in the white papers.

Discussion and Limitations. We developed the pipeline with the goal of producing DatalogMTL programs that are executable in any reasoner engine that supports the MTL extension of Datalog. Thus, engines like the MeTeoR [13] and Vadalog [14] systems can execute the generated programs. However, in all cases, the extensional database to practically run the program should be manually (or semi-automatically) generated, in the scenario you aim to reproduce or test the market for particular use cases, which is our goal for future work. In particular, any interested user might inject a market scenario and run the corresponding DatalogMTL program to see what the consequences of such a scenario would be.

Finally, while the semantic correctness of the resulting programs can be evaluated using rule-based checks or domain-specific constraints, which involve detecting rule-specific features, assessing the content correctness is more challenging. Specifically, verifying that the translated rules, including potential errors introduced by the LLM, accurately replicate the mechanisms of a specific token remains difficult, particularly in an automated way. In fact, although employing human evaluators seems like a straightforward solution, automatic checks and correctness experiments would require a gold standard, i.e., the true sets of market rules, which is so far unavailable. Nevertheless, our pipeline is strictly guided, with the presence of specific regulations and pre-defined rule templates that mitigate the issue of creating unreliable DatalogMTL representations of crypto-markets.

Conclusion and Future Work

In this work, we presented the first approach that, by employing the enormous power of pre-trained LLMs in a controlled fashion, tries to model crypto activity markets in a tractable and inherently transparent formal language, i.e., DatalogMTL. Preliminary results show that we can automatically generate executable DatalogMTL programs starting from white papers in natural language by carefully instructing the LLM to perform the translation task and by leveraging the semi-structured nature of the MiCAR. In future works, we will expand on this approach and industrialize it on a larger scale, allowing stakeholders to get a DatalogMTL formalization of any MiCAR-compliant token. We will also test whether such programs fully replicate the markets by simulating their evolution and comparing it with the real market they aim to represent.