Coreference Resolution is a task in Natural Language Processing (NLP) that involves finding all the linguistic objects in a text (such as nouns, pronouns, and noun phrases) that refer to the same real or imaginary entity. The result of solving this task is establishing correspondences between text objects that indicate the same entity; such correspondence can be established for a pair of objects or their cluster.
Examples of coreferent objects [1] are provided below; the referent (noun) is highlighted in bold, and pronouns are underlined.
• Simple anaphora (the noun precedes the pronoun in the text): "He crossed the mountain. It was high." • Simple cataphora (the noun is mentioned after the pronoun): "She walked onto the road leading to the right. Maria was in a good mood today."
• Compound referent: "Ivan, Mykhailo, and Ostap -all worked underground." Automated methods for solving the coreference resolution task include algorithms based on strict rules formulated by qualified linguists and artificial intelligence (AI) methods. AI methods include neural networks, language models, and decision trees. Decision trees, unlike other AI methods, have a structure that allows relatively easy analysis of their internal logic and corrections to their structure to change the classification logic.
In the process of creating large complex software systems, errors often arise. Therefore, ensuring the reliability of such systems is relevant. Testing is a common method to find errors in software products during the development. However, testing allows for finding errors in the program but cannot guarantee their absence. For a more detailed analysis of the application reliability, formal verification methods are used.
To conduct formal verification, it is necessary to build a formal model of the system. The system can be formally represented using various methods. We propose using the marked transition systems [2] apparatus, which allows describing the system with a set of discrete states between which transitions occur under certain conditions, indicating the operations that system performs while transitioning from one state to another.
Once the formal model is built, the next step of the analysis is to define the properties of the system to be analyzed and to express them in a formal way -formalize them. After obtaining the system model and the properties for its verification, formal methods are used to prove the verification or falsification of the properties. For this, Petri nets and Büchi automata [3] were used.
The paper considers the problem of coreference resolution in Ukrainian-language texts using decision trees. The application of transition systems is proposed to build a high-level specification model for coreference resolution. Formalization is carried out, and network/automata models and linear-temporal logic are used to verify a set of properties of the obtained specification. Büchi automata are created to accept words confirming the properties, and examples and counterexamples of the analyzed properties are found.
• A decision tree is a hierarchical structure consisting of nodes (the root-the initial node, internal nodes, and leaf nodes). Each non-leaf node of such a tree refers to two subtrees (or child nodes). Decision tree structure can be generated automatically based on a training dataset. • The dataset should contain elements and class labels for them. Each element consists of features that can take real or Boolean values (i.e., values that support comparison operations necessary for the tree's functioning). In the work [1], the dataset for coreference resolution consists of elements describing pairs of potentially coreferent objects and a label indicating whether these objects are coreferent. Each element contains features of the pair, such as: matching number, gender, part of speech of the first and second object, lemmatized versions of the objects, the number of words between the objects, the cosine similarity measure of the vectors of the considered objects, and others. All these features are obtained automatically using the UDpipe library [4], the ELMo model for creating word vector representations [5], and own algorithms. The dataset (2500 texts containing 2.4 million examples) was divided into training (1500) and test (1000) samples. • The decision tree for coreference resolution in the work [1], created using the scikit-learn library [6], is formed by selecting a specific feature at each step in the process of deepening. This feature is chosen in such a way as to best separate the set considered in the specific subtree into classes. The Gini impurity coefficient [7] is used to select this feature, which allows evaluating the probability of incorrect classification of a randomly chosen object from the subgroup. As with other AI methods, decision trees are prone to overfitting, which is the excessive adaptation of the tree structure to the dataset used for its creation. In this case, the algorithm's accuracy on data not used for training decreases. To overcome this phenomenon, the parameter `min_impurity_decrease` is used in the work [1], which allows limiting the tree's depth if further splitting into subsets decreases the Gini coefficient by less than the threshold value. The size of the decision tree from figure 1 is limited by `min_impurity_decrease` set to 0.00005 for illustration purposes (in the final decision tree it was 0.000003).
The created decision tree allows classifying input objects by transitioning into subtrees starting from the root following the rule specified in the current node. Since each input object describes a pair of potentially coreferent objects, the decision tree performs a binary classification task.
Coreferent links can exist between more than two objects in the text, for example, including three, four, or more objects. Therefore, to obtain results, coreferent objects are grouped into clusters. In the work [1], initially, all potentially coreferent objects are considered clusters. Their merging occurs if at least one pair of potentially coreferent objects from the first and second clusters is recognized as coreferent.
The quality of clustering is evaluated by comparing the obtained clusters with the original ones using special metrics. Such an assessment is performed on the test sample. The results obtained in the work [1] show high algorithm efficiency, close to the results of the BiLSTM neural networkbased model [8]. The parts of the decision tree used for further algorithm analysis are shown at figures 2 and 3.
As shown in the review article [9], existing studies use formal verification for machine learning models using Satisfiability Modulo Theories (SMT) and Linear Programming (LP). In this paper we propose an approach to verification using automata models and linear-temporal logic, which allows exploring the temporal characteristics of the model on potentially infinite state sequences. Typically, a mathematical model of a discrete system represents a graph where vertices correspond to states (or state classes) the system can be in at different times, and edges represent transitions between states that may have labels indicating actions or events performed by the system.
The system's functioning is represented by sequences of transitions from one state to another. If an edge has a label, this label represents the system's action performed when transitioning from the state at the beginning of the edge to the state at its end. The work uses marked transition systems (marked TS or MTS) as a discrete model of general-type computations [2].
From the modeling perspective, an application using decision trees for coreference resolution can be represented as the interaction of such systems:
• TS 1 or "control" system: responsible for interaction with external resources;
• TS 2 or "core": system representing the traversal of the decision tree.
The control system is modeled by TS:
) where v 0 is the system in the availability state; v 1 is the state where the system processes input data; v 2 is the state where the system outputs the result. Transitions are interpreted as follows: a 1 is receiving a new set of input data; a 2 is forming the classification result; a 3 is transitioning to the availability state. For clarity, let's use a subtree of the decision tree obtained in [1] as the "core". Note that during the model creation process, two surrogate states were added to the subtree: the initial s 0 and the final s 6 ; as well as the transition t 11 between them. This is necessary to represent the decision tree as a continuously functioning system, allowing the use of temporal logic for further analysis. The final model is defined as: It is important to note that in the subtree, which was selected for modeling, each subset of states {s2, s3, s4} asserts coreference of the input data. Accordingly, each of the states {s0, s1, s5} asserts the absence of coreference, and the state s6 preserves the coreference class determined earlier.
Once the synchronous product of the above TS with global transition constraints is defined, it becomes possible to proceed with its verification. The main models of such a process are automata and network models. The work considers using Petri nets (PN) for which there is a wide range of analysis methods. In [10], it is described that the semantics of the TS product and the PN semantics modeling it are consistent in the sense that the sequence of global transitions t1,...,tk represents the global history of the TS product if and only if it is an acceptable sequence of transitions in the PN. Accordingly, the elements of the set T become PN transitions, and the global states of TS (the set of states of each TS participating in the synchronous product before or after the global transition) become places in the obtained network. According to the set of synchronization constraints T, we build a Petri net modeling the joint operation of the core model and the control system: We will verify the liveliness of such a system. The "liveliness" property means that all transitions in the obtained model will participate in its operation process [2]. If transitions in the PN never fire, it means that the system's design is incorrect or redundant. We will examine the PN for liveliness by solving the state equation of the form 𝐴 𝑥 = 0 where A is the incidence matrix of the PN.
Incidence S 0 -1 0 0 0 0 0 0 -1 0 0 0 1
Solutions to the state equations with the incidence matrix from Table 1 are listed in Table 2. The TSS algorithm [11] was used to solve the state equation.
The incidence matrix and the state equation solutions indicate that all transitions in the PN are covered by positive invariants. Additionally, only transitions corresponding to a single decision tree branch fire at any given time. Analysis of the boundedness PN property is performed by solving the system of equations of the form 𝐴 ! 𝑥 = 0 where 𝐴 ! is the transposed matrix of A. The set of solutions includes vector 𝑥 = {1,1,1,1,1,1,1,1}, that covers all places of the PN with positive values. Therefore, the PN under analysis is bounded, and there are no unreachable places.
Let's consider the Petri net for the presence of deadlocks and traps. Semantically, a deadlock state is a reachable marking of the net from which no transition is possible [12]. A Petri net is structurally live if and only if each of its deadlocks has a trap. The logical dependency system for deadlock detection in Petri nets in Figure 7 is presented as follows:
The system of linear homogeneous Diophantine inequalities (SLHDI), corresponding to this system of logical dependencies, can be represented in the form of the Table 3:
The set of deadlocks in the Petri net under consideration contains the following elements, among which the first deadlock is a combination of basic others:
Let's proceed to investigate the traps of the Petri net depicted in Figure 7. The logical dependency system for trap detection looks like:
The following set of traps is obtained after solving the SLHDI in Table 4:
Since a given Petri net is free-choice, the following statement holds for such nets: a free-choice Petri net is live if and only if every deadlock in such a net includes the trap marked by the initial marking. As evident from the given Petri net, each of its basic deadlock (7) includes at least one of the traps (9), thus the Petri net depicted on Fig 7 is live.
We propose using the following algorithm to verify a linear-temporal formula P representing a property that determines the system's semantic correctness:
1. Create a Büchi automaton that accepts words confirming P.
2. Construct the product of the automaton and the TS modeling the original system.
3. Find the intersection of paths generated by the transition system and the paths accepted by the automaton. Further analysis of the reachable states of the intersection allows finding both examples and counterexamples of the formula P [3]. Let's consider the use of the algorithm with an example: suppose there is a hypothesis that, during the analysis of coreference between two objects, if the length of the second object is small, then the objects are coreferent. Such a property can be represented by a following formula in linear temporal logic:
𝑃 ! = (𝑙𝑒𝑛2 ≤ 1.5) → 𝐺(𝐹(𝑐𝑜𝑟𝑒𝑓)), (10) In other words, if the condition holds true, the system will eventually transition to a state that establishes the coreference class and remain in that state. The Büchi automaton that accepts words corresponding to formula P1 has two states: initial state p0 and final state p1. Once it transitions to p1, the automaton remains in that state regardless of the input words.
Let's construct the intersection of the Büchi automaton (Figure 8) and TS, which models the synchronous product of TS 1 and 2 (Figure 6). A simplified visual representation of the obtained intersection is shown in Figure 9 (for clarity, unreachable states are hidden).
The obtained intersection allows for further analysis of feasible paths, cycles and traces. In particular, we observe that there exists a path where a transition occurs from state p1 to state p0 (the final state of such transition is highlighted by two concentric circles on Fig 9), indicating a counterexample to property P. Indeed, having just the information about the length of one of the objects is insufficient to assert their coreference: traversal of the tree with the specified constraint can end in either state s4, which asserts coreference, or state s5, which asserts its absence.
If we consider another linear temporal logic formula, for example, 𝑃 ! = (𝑙𝑒𝑚𝑆 ∧ 1𝑝𝑟𝑝 ∧ 𝑙𝑒𝑛2 ≤ 1.5 ∧ 𝑙𝑒𝑛1 ≤ 1.5 ∧ 𝑛𝑂𝑏𝑗𝐵𝑡𝑤 ≤ 58.5) → 𝐺(𝐹(𝑐𝑜𝑟𝑒𝑓)), (7) Then the analysis of the Büchi automaton product and the synchronous product of TS will demonstrate the absence of a path-cycle that is accessible from the initial state and includes a state from the set of unreachable states. Thus, formula P2 is true, indicating the property it represents holds true universally.
The study presented in this paper explores the use of decision trees for coreference resolution in Ukrainian-language texts. Decision trees are demonstrated to be an effective method for this task, providing clear and interpretable structures that facilitate the analysis and formal verification of their properties. The application of decision trees allows for binary classification of potentially coreferent object pairs, leading to the formation of coreferent clusters with high accuracy, as evidenced by the experimental results.
A significant contribution of this work is the integration of formal verification methods to ensure the reliability and correctness of the coreference resolution system. By constructing a formal model using marked transition systems, we enable the detailed examination of the system's behavior across potentially infinite state sequences. This approach guarantees the absence of errors during the entire runtime of the system, a feat not achievable with other formalization tools such as SMT, which only address verification at specific static moments.
The use of Petri nets further strengthens the analysis by providing a robust framework for examining the correctness of the model. The synchronous product of the transition systems is analyzed for liveliness, boundedness, and the presence of deadlocks and traps, ensuring the system operates correctly and efficiently without redundancy.
Additionally, the paper proposes using Büchi automata and linear-temporal logic to verify properties of the AI classifiers. This approach allows for the formal verification of semantic correctness by intersecting the paths generated by the transition system with those accepted by the automaton. The approach is illustrated with practical examples, demonstrating both the identification of counterexamples and the verification of property compliance.
Overall, the research lays a solid foundation for creating automated analyzers for coreference resolution applications based on decision trees. The methodologies developed in this work ensure high efficiency, accuracy, and reliability of the system, providing valuable insights for future advancements in the field of natural language processing and formal verification.