Formal verification of the properties of coreferent resolution model based on decision trees
The paper examines the problem of coreference resolution, which involves identifying objects - words or phrases in a text, that refer to the same real or imaginary entity. The solution of this task is explored for Ukrainianlanguage texts using decision trees, which autonomously structure themselves...
Збережено в:
| Дата: | 2024 |
|---|---|
| Автори: | , , |
| Формат: | Стаття |
| Мова: | Українська |
| Опубліковано: |
PROBLEMS IN PROGRAMMING
2024
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/652 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| _version_ | 1859476791972855808 |
|---|---|
| author | Pogorilyy, S.D. Slynko, M. S. Biletskyi, P.V. |
| author_facet | Pogorilyy, S.D. Slynko, M. S. Biletskyi, P.V. |
| author_sort | Pogorilyy, S.D. |
| baseUrl_str | https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| collection | OJS |
| datestamp_date | 2025-02-15T14:10:47Z |
| description | The paper examines the problem of coreference resolution, which involves identifying objects - words or phrases in a text, that refer to the same real or imaginary entity. The solution of this task is explored for Ukrainianlanguage texts using decision trees, which autonomously structure themselves based on training data. Unlike other machine learning algorithms such as neural networks, decision trees allow for analysis of their internal structure through graphical representation. This feature facilitates explaining individual results produced by the tree, significantly easing formal verification of their properties. To create decision trees, vector representations of words (such as Elmo) and other linguistic features are used. After formation, decision trees are employed for binary classification of input pairs potentially referring to the same coreferent objects. Based on the obtained binary classifier, coreferent objects are grouped into clusters, followed by an evaluation of the clustering accuracy using specialized metrics. The paper provides a detailed description of the implemented application and the structure of the formed decision tree, which serves as the basis for further analysis. Additionally, the use of transition systems is proposed to construct a high-level specification model for coreference resolution. The transition system-based model enables analysis of application behavior on infinite state sequences, ensuring errorfree execution. Formalization is carried out, and automata models along with 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 as well as counterexamples of the analyzed properties are found. The method defined in the paper serves as the foundation for creating automated analyzers for coreference resolution applications based on decision trees.Prombles in programming 2024; 2-3: 319-325 |
| first_indexed | 2025-07-17T09:42:19Z |
| format | Article |
| fulltext |
319
Лінгвістичні системи
УДК 004.8 http://doi.org/10.15407/pp2024.02-03.319
С.Д. Погорілий М. С. Слинько, П.В. Білецький
ФОРМАЛЬНА ВЕРИФІКАЦІЯ ВЛАСТИВОСТЕЙ
МОДЕЛІ ПОШУКУ КОРЕФЕРЕНТНИХ ОБ'ЄКТІВ
НА ОСНОВІ ДЕРЕВ РІШЕНЬ
В роботі розглядається проблема пошуку кореферентних об’єктів, яка полягає в знаходженні об'єктів -
слів або словосполучень в тексті, які посилаються на один і той же реальний чи уявний об'єкт. Розв'я-
зання цієї задачі розглядається для україномовних текстів, використовуючи дерева рішень, які само-
стійно формують свою структуру на основі навчальної вибірки. Завдяки можливості графічного предста-
влення дерева рішень, на відмінну від інших алгоритмів машинного навчання, таких як нейронні мережі,
стає можливим здійснення аналізу внутрішньої структури. ЇЇ можна використовувати для пояснення ок-
ремих результатів роботи дерева, що значно полегшує проведення формальної верифікації їх властивос-
тей. Для створення дерева рішень використовуються векторні представлення слів Elmo та інші лінгвіс-
тичні характеристики. Після формування дерева рішень використовуються для бінарної класифікації вхі-
дної пари потенційно кореферентних об'єктів. На основі отриманого бінарного класифікатора здійсню-
ється об'єднання кореферентних об'єктів в кластери та подальша оцінка правильності кластеризації за
допомогою спеціальних метрик. В роботі проведено детальний опис реалізованого застосунку та струк-
тури сформованого дерева рішень, що є основою для подальшого аналізу. Запропоновано застосування
апарату транзиційних систем для побудови високорівневої специфікації моделі пошуку кореферентних
об’єктів. Модель на основі транзиційних систем дозволяє виконувати аналіз застосунку на нескінченній
послідовності станів, забезпечуючи відсутність помилок в процесі виконання. Проведено формалізацію
та використано автоматні моделі та лінійно-темпоральну логіку для верифікації набору властивостей
отриманої специфікації. Створено автомати Бюхі, що акцептують слова, які підтверджують властивості,
та знайдено приклади та контрприклади властивостей, що аналізуються. Визначений в роботі метод є
основою для створення автоматизованих аналізаторів застосунків пошуку кореферентних об’єктів на ос-
нові дерев рішень.
Ключові слова: штучний інтелект, обробка природних мов, кореферентність, дерева рішень, транзиційні
системи, автомат Бюхі.
S.D. Pogorilyy, M. S. Slynko, P. V. Biletskyi
FORMAL VERIFICATION OF THE PROPERTIES OF
COREFERENT RESOLUTION MODEL BASED ON
DECISION TREES
The paper examines the problem of coreference resolution, which involves identifying objects - words or phrases
in a text, that refer to the same real or imaginary entity. The solution of this task is explored for Ukrainian-
language texts using decision trees, which autonomously structure themselves based on training data. Unlike
other machine learning algorithms such as neural networks, decision trees allow for analysis of their internal
structure through graphical representation. This feature facilitates explaining individual results produced by the
tree, significantly easing formal verification of their properties. To create decision trees, vector representations
of words (such as Elmo) and other linguistic features are used. After formation, decision trees are employed for
binary classification of input pairs potentially referring to the same coreferent objects. Based on the obtained
binary classifier, coreferent objects are grouped into clusters, followed by an evaluation of the clustering accu-
racy using specialized metrics. The paper provides a detailed description of the implemented application and the
structure of the formed decision tree, which serves as the basis for further analysis. Additionally, the use of
transition systems is proposed to construct a high-level specification model for coreference resolution. The tran-
sition system-based model enables analysis of application behavior on infinite state sequences, ensuring error-
free execution. Formalization is carried out, and automata models along with 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 as well as counterexamples
of the analyzed properties are found. The method defined in the paper serves as the foundation for creating
automated analyzers for coreference resolution applications based on decision trees.
Key words: artificial intelligence, natural language processing, coreference resolution, decision trees, transition
systems, Buchi automata.
© С.Д. Погорілий, М. С. Слинько, П.В. Білецький, 2024
ISSN 1727-4907. Проблеми програмування. 2024. №2-3
320
Лінгвістичні системи
Вступ
Пошук кореферентних об’єктів
(Coreferene Resolution) – це задача, яка нале-
жить до обробки природної мови (Natural
Language Processing, NLP). Задача пошуку
кореферентних об’єктів полягає у знахо-
дженні усіх мовленнєвих об’єктів тексту
(таких як іменники, займенники та словос-
получення), що позначають один реальний
чи уявний об’єкт. Результатом розв’язку цієї
задачі є встановлення відповідності між
об’єктами тексту, що вказують на один і той
же об’єкт; така відповідність встановлю-
ється для пари об’єктів чи для їх кластеру.
Приклади кореферентних об’єктів
[1] наведені далі; референт (іменник) виді-
лений жирним шрифтом, займенники - під-
креслені.
- Проста анафора (іменник стоїть пе-
ред займенником в тексті): «Він пе-
рейшов через гору. Вона була висо-
кою.»
- Проста катафора (іменник згаду-
ється після займенника): «Вона ви-
йшла на дорогу, що вела праворуч.
Марія сьогодні мала гарний на-
стрій.»
- Складений референт: «Іван, Ми-
хайло та Остап – всі вони працю-
вали під землею.»
Методи автоматизованого
розв’язання задачі пошуку кореферентних
об’єктів включають в себе алгоритми на ос-
нові строгих правил, що формуються квалі-
фікованими лінгвістами та методи штуч-
ного інтелекту (Artificial Intelligence, AI).
До методів штучного інтелекту відносять
нейронні мережі, мовні моделі та дерева рі-
шень. Дерева рішень, на відмінну від інших
методів штучного інтелекту, мають будову,
що уможливлює відносно легкий аналіз ло-
гіки їх внутрішньої роботи та внесення ко-
рекцій в їхню структуру для зміни логіки
класифікації.
В процесі створення великих, склад-
них програмних систем часто виникають
помилки. Тому актуальним є питання забез-
печення надійності таких систем. Зазвичай
для пошуку помилок у процесі розробки
програмних продуктів виконується його те-
стування. Воно дозволяє знаходити поми-
лки в програмі, але не гарантує їх вияв-
лення. Для детальнішого дослідження на-
дійності застосунків використовують ме-
тоди формальної верифікації системи.
Для проведення формальної верифі-
кації необхідно побудувати формальну мо-
дель системи. Подати систему формально
можна використовуючи розмічені транзи-
ційні системи [2]. Вони дозволяють опи-
сати систему набором дискретних станів,
між якими існують переходи, що здійсню-
ються під час виконання певних умов та по-
значають операції, які виконуються систе-
мою у процесі переходу між станами.
Наступним кроком після створення
формальної моделі необхідно визначити
властивості системи, які будуть аналізува-
тися та подати їх формально.
Після цього, отримавши модель сис-
теми та властивості для її перевірки, вико-
ристовуються формальні методи доведення
виконання (чи невиконання) властивостей.
Для цього використовують автомати Бюхі
[3].
У роботі розглядається проблема по-
шуку кореферентних об’єктів в україномо-
вних текстах, використовуючи дерева рі-
шень. Запропоновано застосування апарату
транзиційних систем для побудови високо-
рівневої специфікації моделі пошуку коре-
ферентних об’єктів. Проведено формаліза-
цію та використано автоматні моделі та лі-
нійно-темпоральну логіку для верифікації
набору властивостей отриманої специфіка-
ції. Створено автомати Бюхі, що акцепту-
ють слова, які підтверджують властивості
та знайдено приклади й контрприклади вла-
стивостей, що аналізуються.
Використання дерев рішень для
пошуку кореферентних об’єктів
Дерево рішень - це ієрархічна стру-
ктура, що складається з вузлів (кореня – по-
чаткового вузла, внутрішніх та кінцевих
вузлів). Кожен некінцевий вузол такого де-
рева посилається на два піддерева (або ву-
зла-нащадка). Формування дерева рішень
321
Лінгвістичні системи
може здійснюється автоматично на основі
набору даних.
Набір даних повинен містити елеме-
нти та мітки класів для них. Кожен елемент
складається з характеристик (features), які
можуть приймати дійсні або булеві значення
(тобто, значення, які підтримують операцію
порівняння, що необхідно для функціону-
вання дерева). В роботі [1] набір даних для
пошуку кореферентних об’єктів складається
із елементів, кожен з яких описує пару поте-
нційно кореферентних об’єктів та мітки, що
вказує, чи ці об’єкти кореферентні. Кожен
елемент містить в собі характеристики пари,
такі як: співпадіння числа, роду, частина
мови першого та другого об’єкту, лематизо-
ваної версії об’єктів, кількість слів між
об’єктами, міру косинусної схожості векто-
рів об’єктів, що розглядаються та інші. Всі
ці характеристики отримані автоматично,
використовуючи бібліотеку UDpipe [4], мо-
дель для створення векторних представлень
слів ELMo [5] та за допомогою власних ал-
горитмів. Набір даних (2500 текстів) був ро-
зділений на навчальну (1500) та перевірочну
(1000) вибірки.
Дерево рішень для пошуку корефе-
рентних об’єктів у роботі [1], створене за до-
помогою бібліотеки scikit-learn [6], форму-
ється шляхом вибору певної характеристики
на кожному кроці в процесі поглиблення. Ця
характеристика обирається таким чином,
щоб найкраще розділити множину, що розг-
лядається в конкретному піддереві, на класи.
Для вибору цієї характеристики використо-
вується коефіцієнт Джині (Gini impurity) [7],
який дозволяє оцінити імовірність невірної
класифікації випадково вибраного об’єкту з
підгрупи. Дерево рішень для пошуку корефе-
рентних об’єктів показане на рис.1, 2.
Рис. 1. Дерево рішень [1]
Рис. 2. Піддерево дерева рішень [1]
Як і іншим методам штучного інте-
лекту, деревам рішень властиве явище пе-
ренавчання (overfitting), яке полягає в над-
мірному пристосуванні структури дерева
до набору даних, що використовується для
його створення. Водночас точність роботи
алгоритму на даних, які не використовува-
лися для навчання, падає. Для подолання
цього явища в роботі [1] використано пара-
метр min_impurity_decrease, який дозволяє
обмежити поглиблення дерева, якщо із по-
дальшим розділенням на підмножини змен-
шення коефіцієнта Джині менше порого-
вого значення.
Створене дерево рішень дозволяє
класифікувати вхідні об’єкти шляхом пере-
ходу в піддерева, починаючи з кореня, у
відповідності із правилом, вказаним у пото-
чному вузлі. Оскільки кожен вхідний
об’єкт описує пару потенційно кореферен-
тних об’єктів, дерево рішень виконує за-
дачу бінарної класифікації.
Кореферентні зв’язки можуть існу-
вати більше ніж між двома об’єктами в тек-
сті, наприклад, включати три, чотири та бі-
льше об’єктів. Тому для отримання резуль-
татів кореферентні об’єкти об’єднуються в
кластери. В роботі [1] початково всі потен-
ційно кореферентні об’єкти вважаються
кластерами. Їх злиття відбувається, якщо
хоча б одна пара потенційно кореферент-
них об’єктів з першого та другого кластерів
розпізнана як кореферентна.
Оцінка якості кластеризації вико-
нується шляхом порівняння отриманих кла-
стерів з оригінальними, використовуючи
спеціальні метрики. Така оцінка викону-
ється на перевірочній вибірці. Отримані в
роботі [1] результати показують високу
322
Лінгвістичні системи
ефективність алгоритиму, близькі до ре-
зультатів моделі на основі нейронних ме-
реж BiLSTM [8].
Формальна верифікація
алгоритмів із використанням
дерев рішень
Як показано в оглядовій статті [9], в
існуючих дослідженнях використання фор-
мальної верифікації для моделей машин-
ного навчання застосовується апарат
розв’язності формул у теоріях (Satisfiability
Modulo Theories, SMT) та лінійної оптимі-
зації (Linear Programming, LP). У роботі
пропонується підхід до верифікації з вико-
ристанням автоматних моделей та лінійно-
темпоральної логіки, що, на відміну від
SMT, дозволяє досліджувати темпоральні
характеристики моделі на потенційно не-
скінченній послідовності станів. Як пра-
вило, математична модель дискретної сис-
теми являє собою граф, вершини якого від-
повідають станам (або класам станів), в
яких може перебувати система в різні мо-
менти часу; а ребрам – переходи між ста-
нами, які можуть мати позначки, що зобра-
жують дії чи події, які виконує система. Фу-
нкціонування системи за такого зобра-
ження представляється послідовностями
переходів від одного стану до іншого. Якщо
ребро має позначку, то ця позначка являє
собою дію системи, що виконується під час
переходу від стану на початку ребра до
стану в його кінці. Далі в роботі використо-
вуються розмічені транзиційні системи (ро-
змічені ТС, або РТС) як дискретна модель
обчислень загального типу [2].
Створення РТС моделей на
високому рівні абстракції
З точки зору моделювання застосу-
нок, що використовує дерева рішень для
пошуку кореферентних об’єктів, можна
представити у вигляді взаємодії таких сис-
тем:
● ТС 1, або “керуюча” система: відпо-
відає за взаємодію з зовнішніми ре-
сурсами;
● ТС 2, або “ядро”: система що пред-
ставляє прохід по дереву рішень.
Керуюча система моделюється ТС
𝑀𝑀 = ({𝑣𝑣0, 𝑣𝑣1, 𝑣𝑣2}, {𝑎𝑎1, 𝑎𝑎2, 𝑎𝑎3}, 𝛼𝛼, 𝛽𝛽, 𝑣𝑣0), (1)
де v0 - система в стані доступності; v1 - стан,
в якому система опрацьовує вхідні дані; v2 -
стан, в якому система видає результат. Пе-
реходи інтерпретуються наступним чином:
a1 - отримання нового набору вхідних да-
них; a2 - формування результату класифіка-
ції; a3 - перехід в стан доступності.
Рис. 3. Представлення ТС моделі керуючої
системи
Для наочності за ядро використаємо
піддерево дерева рішень, отриманого у [1].
Зазначимо, що в процесі створення моделі
до піддерева було додано 2 сурогатні стани:
початковий s0 та кінцевий s6; а також пере-
хід t11 між ними. Це необхідно для предста-
влення дерева рішень як неперервно функ-
ціонуючої системи, що дозволяє викорис-
тання темпоральної логіки для подальшого
аналізу. Кінцева модель визначається як
𝑆𝑆𝐾𝐾 = {𝑠𝑠0, 𝑠𝑠1, 𝑠𝑠2, 𝑠𝑠3, 𝑠𝑠4, 𝑠𝑠5, 𝑠𝑠6}, (2)
𝑇𝑇𝐾𝐾 = {𝑡𝑡1, 𝑡𝑡2, . . . , 𝑡𝑡11}, (3)
𝐾𝐾 = (𝑆𝑆𝐾𝐾, 𝑇𝑇𝐾𝐾, 𝛼𝛼, 𝛽𝛽, 𝑠𝑠0), (4)
а множина пропозиційних формул, асоці-
йованих зі станами, та функція позначок
для кожного стану наведені на рис. 4.
Рис. 4. Представлення ТС підмоделі ядра
323
Лінгвістичні системи
Важливо зазначити, що у обраному
для моделювання піддереві кожен із підм-
ножини станів {s2, s3, s4} фіксує кореферен-
тність вхідних даних. Відповідно, кожен зі
станів {s0, s1, s5} фіксує відсутність корефе-
рентності, а стан s6 зберігає клас корефере-
нтності, визначений раніше.
Для вищенаведених ТС будуємо си-
нхронізовану паралельну композицію (син-
хронний добуток) з глобальними перехо-
дами, що моделює роботу застосунку в ці-
лому. Множина обмежень синхронізації мі-
стить наступні елементи (𝜀𝜀 - тотожна дія,
що означає відсутність переходу в ТС):
𝑇𝑇 = {(𝑎𝑎1, 𝑡𝑡1), (𝑎𝑎1, 𝑡𝑡2), (𝜀𝜀, 𝑡𝑡3), (𝜀𝜀, 𝑡𝑡4),
(𝜀𝜀, 𝑡𝑡5), (𝜀𝜀, 𝑡𝑡6), (𝜀𝜀, 𝑡𝑡7), (𝜀𝜀, 𝑡𝑡8), (𝜀𝜀, 𝑡𝑡9),
(𝜀𝜀, 𝑡𝑡10), (𝑎𝑎2, 𝜀𝜀), (𝑎𝑎3, 𝑡𝑡11)}. (5)
Рис. 5. Синхронний добуток ТС 1 і 2
Верифікація властивостей моделі
автоматами Бюхі
В роботі пропонується викорис-
тання наступного алгоритму перевірки лі-
нійно-темпоральної формули Р, що пред-
ставляє властивість, яка визначає семанти-
чну коректність роботи системи:
1. Створити автомат Бюхі, що акцеп-
тує слова, які підтверджують Р.
2. Побудувати добуток автомата і ТС,
що моделює вихідну систему.
3. Знайти переріз шляхів, які генерує
загальна транзиційна система (ЗТС),
і шляхів, які акцептує автомат. По-
дальший аналіз досяжних станів пе-
рерізу дозволяє знайти як приклади,
так і контрприклади формули Р [3].
Розглянемо використання алгори-
тму на прикладі: нехай існує гіпотеза, що, у
разі аналізу кореферентності двох об’єктів
довжина другого об’єкту є малою, то
об’єкти кореферентні. Така властивість
представляється формулою лінійно-темпо-
ральної логіки
P1 = (len2 ≤ 1.5) → G(F(coref)), (6)
тобто якщо умова справджується, то сис-
тема рано чи пізно перейде в стан, що фік-
сує клас кореферентності, і залишиться в
такому стані.
Рис. 6. Зображення автомата Бюхі, що від-
повідає LT формулі Р1
Автомат Бюхі, що допускає слова,
які відповідають формулі Р1, містить два
стани: початковий p0 та кінцевий p1, перей-
шовши в який, автомат вже не змінює свій
стан незалежно від поданих слів.
Побудуємо перетин автомата Бюхі
(рис. 6) та ТС, що моделює синхронний до-
буток ТС 1 і 2 (рис. 5). Спрощене візуальне
представлення отриманого перетину наве-
дено на рис. 7. Для наочності на рис. 7 при-
ховані недосяжні стани.
Рис. 7. Добуток автомата Бюхі та синхрон-
ного добутку ТС
Отриманий перетин дозволяє прове-
сти низку аналітичних дослідів можливих
шляхів, циклів і трас. Зокрема, він дозволяє
стверджувати, що можливий шлях, за якого
відбувається перехід із стану р1 у стан р0
(кінцевий стан такого переходу виділено
двома концентричними колами), тобто
знайдено контрприклад властивості Р. Дій-
сно, лише інформації про довжину одного з
об’єктів мало, щоб стверджувати про їх ко-
референтність: обхід дерева з вказаним об-
меженням може завершитися як у стані s4,
що фіксує кореферентність, так і в стані s5,
що фіксує її відсутність. Якщо ж розгля-
нути іншу формулу лінійно-темпоральної
логіки, наприклад,
𝑃𝑃2 = (𝑙𝑙𝑙𝑙𝑙𝑙𝑙𝑙 ∧ 1𝑝𝑝𝑝𝑝𝑝𝑝 ∧ 𝑙𝑙𝑙𝑙𝑙𝑙2 ≤ 1.5 ∧
324
Лінгвістичні системи
∧ 𝑙𝑙𝑙𝑙𝑙𝑙1 ≤ 1.5 ∧ 𝑙𝑙𝑛𝑛𝑛𝑛𝑛𝑛𝑛𝑛𝑛𝑛𝑛𝑛 ≤ 58.5) →
𝐺𝐺(𝐹𝐹(𝑐𝑐𝑐𝑐𝑐𝑐𝑙𝑙𝑓𝑓)), (7)
то аналіз добутку автомата Бюхі та синх-
ронного добутку ТС покаже відсутність
шляху-циклу такий, що є доступним із по-
чаткового стану, та який включає в себе
стан із множини недопустимих станів,
тобто формула P2 є істинною, а, отже, влас-
тивість, представлена нею, виконується
завжди.
Висновки
Досліджено використання матема-
тичного апарату транзиційних систем, який
дозволяє отримати формалізовану специфі-
кацію системи, що аналізується. До переваг
сформованої моделі належить можливість
здійснювати формальну верифікацію влас-
тивостей (формул) на потенційно нескін-
ченній послідовності станів, таким чином
гарантуючи відсутність помилок протягом
всього часу функціонування. Це є немож-
ливим за використання інших поширених
апаратів формалізації (як SMT), що вирішу-
ють задачу верифікації лише в конкретний
статичний момент часу.
В роботі виконано перетворення на-
бору властивостей системи пошуку корефе-
рентних об’єктів з використанням дерев рі-
шень у формули лінійно-темпоральної ло-
гіки. Створено автомати Бюхі, що акцепту-
ють слова, які підтверджують формули та
проілюстровано використання частини
отриманої моделі як для знаходження
контрприкладу властивості, що аналізу-
ється, так і для верифікації їх відсутності.
Поданий підхід є базою для створення ав-
томатизованих аналізаторів систем дослі-
дження кореферентності текстів із викори-
станням дерев рішень.
Література
1. С.Д. Погорілий, П.В. Білецький. Алго-
ритм пошуку кореферентних об’єктів в
україномовних текстах із використан-
ням дерев рішень. Проблеми програ-
мування. 2022. № 3-4. с. 85-91.
2. Ю.В. Бойко, С.Л. Кривий, С.Д. Погорі-
лий та ін. Методи та новітні підходи до
проектування, управління і застосу-
вання високопродуктивних ІТ-інфра-
структур. – К.: ВПЦ «Київський уні-
верситет». 2016. 447 с
3. S.L. Kryvyi et al. Method of semantic
application verification in GPGPU
technology. System Research &
Information Technologies, 2020, № 3, pp.
7-22
4. Бібліотека UDpipe. Accessed:
06.04.2024.
https://lindat.mff.cuni.cz/services/udpipe/
5. M. Peters, M. Neumann, M. Iyyer, M.
Gardner, C. Clark, K. Lee, L.
Zettlemoyer.. Deep contextualized word
representations. In Proceedings of the
2018 Conference of the North American
Chapter of the Association for
Computational Linguistics: Human
Language Technologies, 2018, № 1. С.
2227–2237.
6. Scikit learn для дерев рішень. Accessed:
06.04.2024. https://scikit-
learn.org/stable/modules/tree.html
7. S. Tangirala. Evaluating the Impact of
GINI Index and Information Gain on
Classification using Decision Tree
Classifier Algorithm, International
Journal of Advanced Computer Science
and Applications, 2020, pp. 612-619.
8. S. Telenyk, S. Pogorilyy, A. Kramov. The
complex method of coreferent clusters
detection based on a BiLSTM neural
network, Knowledge Based Systems.
2021. C. 205-210
9. M. Krichen et al., Are Formal Methods
Applicable To Machine Learning And
Artificial Intelligence? Proceedings of
2nd International Conference of Smart
Systems and Emerging Technologies
(SMARTTECH), 2022, pp. 48-53.
References
1. S. Pogorilyy, P. Biletskyi, Coreference
resolution algorithm for Ukrainian-
language texts using decision trees,
Problems in programming, 2022, №3-4:
pp. 85-91.
2. BOYKO Yu.V., KRYVYI S.L.,
POGORILYY S.D. et al (2016) Methods
and innovative approaches to designing,
managing, and deploying high-performant
IT infrastructures. PPC “Kyiv University”,
447p. [in Ukrainian]
3. KRYVYI S.L. , POGORILYY S.D.,
SLYNKO M.S., KRAMOV A.A. (2020)
Method of semantic application
verification in GPGPU technology.
325
Лінгвістичні системи
System Research & Information
Technologies № 3, pp. 7-22
4. UDpipe library. Accessed: 06.04.2024.
https://lindat.mff.cuni.cz/services/udpipe/
5. M. Peters, M. Neumann, M. Iyyer, M.
Gardner, C. Clark, K. Lee, L.
Zettlemoyer.. Deep contextualized word
representations. In Proceedings of the
2018 Conference of the North American
Chapter of the Association for
Computational Linguistics: Human
Language Technologies, 2018, № 1. С.
2227–2237.
6. Scikit learn for decision trees. Accessed:
06.04.2024. https://scikit-
learn.org/stable/modules/tree.html
7. S. Tangirala. Evaluating the Impact of
GINI Index and Information Gain on
Classification using Decision Tree
Classifier Algorithm, International Journal
of Advanced Computer Science and
Applications, 2020, pp. 612-619.
8. S. Telenyk, S. Pogorilyy, A. Kramov. The
complex method of coreferent clusters
detection based on a BiLSTM neural
network, Knowledge Based Systems.
2021. C. 205-210.
9. KRICHEN M. et al (2022) Are Formal
Methods Applicable To Machine Learning
And Artificial Intelligence? In
Proceedings of 2nd International
Conference of Smart Systems and
Emerging Technologies (SMARTTECH),
pp. 48-53
Одержано: 10.04.2024
Внутрішня рецензія отримана: 19.04.2024
Зовнішня рецензія отримана: 25.04.2024
Про авторів:
1Погорілий Сергій Дем’янович,
доктор технічних наук,
професор,
sdp77@i.ua ,
https://orcid.org/0000-0002-6497-5056
Слинько Максим Сергійович,
доктор філософії,
maxim.slinko@gmail.com ,
https://orcid.org/0000-0001-9667-8729
1Білецький Павло Володимирович,
аспірант,
асистент,
1234bpv@i.ua ,
https://orcid.org/0000-0001-5425-3706
Місце роботи авторів:
1Факультет радіофізики,
електроніки та комп’ютерних систем,
Київський національний університет
імені Тараса Шевченка,
03187, м. Київ, проспект
Академіка Глушкова, 4г
Тел.: (38)(044) 521-05-32
E-mail: rex@knu.ua
|
| id | pp_isofts_kiev_ua-article-652 |
| institution | Problems in programming |
| keywords_txt_mv | keywords |
| language | Ukrainian |
| last_indexed | 2025-07-17T09:42:19Z |
| publishDate | 2024 |
| publisher | PROBLEMS IN PROGRAMMING |
| record_format | ojs |
| resource_txt_mv | ppisoftskievua/40/309ef86ae2e4a47cd504242d57f44140.pdf |
| spelling | pp_isofts_kiev_ua-article-6522025-02-15T14:10:47Z Formal verification of the properties of coreferent resolution model based on decision trees Формальна верифікація властивостей моделі пошуку кореферентних об’єктів на основі дерев рішень Pogorilyy, S.D. Slynko, M. S. Biletskyi, P.V. artificial intelligence; natural language processing; coreference resolution; decision trees; transition systems; Buchi automata UDC 004.8 штучний інтелект; обробка природних мов; кореферентність; дерева рішень; транзиційні системи; автомат Бюхі УДК 004.8 The paper examines the problem of coreference resolution, which involves identifying objects - words or phrases in a text, that refer to the same real or imaginary entity. The solution of this task is explored for Ukrainianlanguage texts using decision trees, which autonomously structure themselves based on training data. Unlike other machine learning algorithms such as neural networks, decision trees allow for analysis of their internal structure through graphical representation. This feature facilitates explaining individual results produced by the tree, significantly easing formal verification of their properties. To create decision trees, vector representations of words (such as Elmo) and other linguistic features are used. After formation, decision trees are employed for binary classification of input pairs potentially referring to the same coreferent objects. Based on the obtained binary classifier, coreferent objects are grouped into clusters, followed by an evaluation of the clustering accuracy using specialized metrics. The paper provides a detailed description of the implemented application and the structure of the formed decision tree, which serves as the basis for further analysis. Additionally, the use of transition systems is proposed to construct a high-level specification model for coreference resolution. The transition system-based model enables analysis of application behavior on infinite state sequences, ensuring errorfree execution. Formalization is carried out, and automata models along with 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 as well as counterexamples of the analyzed properties are found. The method defined in the paper serves as the foundation for creating automated analyzers for coreference resolution applications based on decision trees.Prombles in programming 2024; 2-3: 319-325 В роботі розглядається проблема пошуку кореферентних об’єктів, яка полягає в знаходженні об'єктів - слів або словосполучень в тексті, які посилаються на один і той же реальний чи уявний об'єкт. Розв'язання цієї задачі розглядається для україномовних текстів, використовуючи дерева рішень, які самостійно формують свою структуру на основі навчальної вибірки. Завдяки можливості графічного представлення дерева рішень, на відмінну від інших алгоритмів машинного навчання, таких як нейронні мережі, стає можливим здійснення аналізу внутрішньої структури. ЇЇ можна використовувати для пояснення окремих результатів роботи дерева, що значно полегшує проведення формальної верифікації їх властивостей. Для створення дерева рішень використовуються векторні представлення слів Elmo та інші лінгвістичні характеристики. Після формування дерева рішень використовуються для бінарної класифікації вхідної пари потенційно кореферентних об'єктів. На основі отриманого бінарного класифікатора здійснюється об'єднання кореферентних об'єктів в кластери та подальша оцінка правильності кластеризації за допомогою спеціальних метрик. В роботі проведено детальний опис реалізованого застосунку та структури сформованого дерева рішень, що є основою для подальшого аналізу. Запропоновано застосування апарату транзиційних систем для побудови високорівневої специфікації моделі пошуку кореферентних об’єктів. Модель на основі транзиційних систем дозволяє виконувати аналіз застосунку на нескінченній послідовності станів, забезпечуючи відсутність помилок в процесі виконання. Проведено формалізацію та використано автоматні моделі та лінійно-темпоральну логіку для верифікації набору властивостей отриманої специфікації. Створено автомати Бюхі, що акцептують слова, які підтверджують властивості, та знайдено приклади та контрприклади властивостей, що аналізуються. Визначений в роботі метод є основою для створення автоматизованих аналізаторів застосунків пошуку кореферентних об’єктів на основі дерев рішень.Prombles in programming 2024; 2-3: 319-325 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2024-12-17 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/652 10.15407/pp2024.02-03.319 PROBLEMS IN PROGRAMMING; No 2-3 (2024); 319-325 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2024); 319-325 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2024); 319-325 1727-4907 10.15407/pp2024.02-03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/652/704 Copyright (c) 2024 PROBLEMS IN PROGRAMMING |
| spellingShingle | artificial intelligence natural language processing coreference resolution decision trees transition systems Buchi automata UDC 004.8 Pogorilyy, S.D. Slynko, M. S. Biletskyi, P.V. Formal verification of the properties of coreferent resolution model based on decision trees |
| title | Formal verification of the properties of coreferent resolution model based on decision trees |
| title_alt | Формальна верифікація властивостей моделі пошуку кореферентних об’єктів на основі дерев рішень |
| title_full | Formal verification of the properties of coreferent resolution model based on decision trees |
| title_fullStr | Formal verification of the properties of coreferent resolution model based on decision trees |
| title_full_unstemmed | Formal verification of the properties of coreferent resolution model based on decision trees |
| title_short | Formal verification of the properties of coreferent resolution model based on decision trees |
| title_sort | formal verification of the properties of coreferent resolution model based on decision trees |
| topic | artificial intelligence natural language processing coreference resolution decision trees transition systems Buchi automata UDC 004.8 |
| topic_facet | artificial intelligence natural language processing coreference resolution decision trees transition systems Buchi automata UDC 004.8 штучний інтелект обробка природних мов кореферентність дерева рішень транзиційні системи автомат Бюхі УДК 004.8 |
| url | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/652 |
| work_keys_str_mv | AT pogorilyysd formalverificationofthepropertiesofcoreferentresolutionmodelbasedondecisiontrees AT slynkoms formalverificationofthepropertiesofcoreferentresolutionmodelbasedondecisiontrees AT biletskyipv formalverificationofthepropertiesofcoreferentresolutionmodelbasedondecisiontrees AT pogorilyysd formalʹnaverifíkacíâvlastivostejmodelípošukukoreferentnihobêktívnaosnovíderevríšenʹ AT slynkoms formalʹnaverifíkacíâvlastivostejmodelípošukukoreferentnihobêktívnaosnovíderevríšenʹ AT biletskyipv formalʹnaverifíkacíâvlastivostejmodelípošukukoreferentnihobêktívnaosnovíderevríšenʹ |