This paper addresses the problem of coreference resolution, which involves identifying words or phrases in a text that refer to the same real or imaginary entity. The solution for this task is developed for Ukrainian-language texts using decision trees, which autonomously structure themselves based on training data. Decision trees, unlike other machine learning algorithms such as neural networks, allow for the analysis of their internal structure through graphical representation, significantly easing the formal verification of their properties. Vector representations of words (such as ELMo) and other linguistic features are used to create decision trees. These trees are employed for the binary classification of input pairs potentially referring to the same coreferent objects. Based on the binary classifier, coreferent objects are grouped into clusters, followed by an evaluation of clustering accuracy using specialized metrics. To guarantee the reliability of large, complex software systems, formal verification methods are applied. A formal model of the coreference resolution system is constructed using marked transition systems. This model describes the system with a set of discrete states and transitions between them under certain conditions. The properties of the system are formalized and verified using network models, automata models and linear-temporal logic, ensuring error-free execution on infinite state sequences. The work explores the use of Petri nets for analyzing the correctness of the system model. The synchronous product of transition systems is verified for liveliness, boundedness, deadlocks, and traps, ensuring that the model operates correctly without redundancy. Büchi automata are created to accept words confirming the properties, with examples and counterexamples found during the analysis. The proposed method serves as a foundation for creating automated analyzers for coreference resolution applications based on decision trees, demonstrating high efficiency and accuracy. The approach allows for the formal verification of system properties on potentially infinite state sequences, ensuring the reliability and correctness of the coreference resolution system throughout its runtime. artificial intelligence, natural language processing, coreference resolution, decision trees, transition systems, Büchi automata, Petri nets, formal verification 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
[
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 [
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 [
The decision tree for coreference resolution in the work [
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 [
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 [
The parts of the decision tree used for further algorithm analysis are shown at figures 2 and 3.
As shown in the review article [
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 [
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:
= ({!, !, !}, {!, !, !}, , , !), (1) where v0 is the system in the availability state; v1 is the state where the system processes input data; v2 is the state where the system outputs the result. Transitions are interpreted as follows: a1 is receiving a new set of input data; a2 is forming the classification result; a3 is transitioning to the availability state.
For clarity, let's use a subtree of the decision tree obtained in [
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. For the above TS, we construct a synchronized parallel composition (synchronous product) with global transitions modeling the application's operation as a whole. The set of synchronization constraints includes the following elements (ε - identical action indicating no transition in TS): = {(!, !), (!, !), (, !), (, !), , ! , , ! , , ! , , ! , , ! , (, !"), (!, ), (!, !!)}. (5)
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 [
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 [
Solutions to the state equations with the incidence matrix from Table 1 are listed in Table 2. The
TSS algorithm [
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 [
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: 1 1 1 1
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: ! = {!, !, !, !, !, !, !, !}, ! = {!, !, !}, ! = {!, !, !}, ! = {!, !, !}, ! = {!, !, !}, ! = {!, !, !}, ! = {!, !, !}. 0 0 0 0 0 0 -1
Let's proceed to investigate the traps of the Petri net depicted in Figure 7. The logical dependency system for trap detection looks like:
! → ! ∧ !; ! → ! ∧ !; ! → ! ∧ !; ! → !; ! → !; ! → !; ! → !. (8) The following set of traps is obtained after solving the SLHDI in Table 4: ! = {!, !, !, !, !}, ! = !, !, !, ! , ! = {!, !, !, !}, (9) ! = {!, !, !}, ! = {!, !, !}.
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 [
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 that 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.