Agentin verifikasiyası
Agentin verifikasiyası — süni agentlərin öz spesifikasiyalarına uyğun fəaliyyət göstərdiyinə dair təminat əldə etmək məqsədilə həyata keçirilən fəaliyyətlər toplusudur. Qeyri-üzvi agentlərin ilkin formaları əsrlər boyu istehsalatda istifadə olunsa da, süni agentlərin elmi tədqiqi yalnız XX əsrin ortalarında başlamışdır. Bu sahədə aparılan fundamental tədqiqatlar süni intellektin akademik elm sahəsi kimi formalaşması ilə sıx bağlı olmuşdur. Sənaye idarəetmə sistemilərində və kompüter sistemlərində tətbiq edilən ilk agentlər adətən süni intellektdən istifadə etməyən, sadə məntiq qaydalarına əsaslanan idarəetmə mexanizmləri ilə işləyirdi.
Belə agentlər çoxagentli sistemlərin tərkibində istifadə edildikdə, onların kollektiv davranışını ənənəvi proqram təminatının sınaq üsulları ilə yoxlamaq çətin olduğundan agentyönümlü xüsusi test metodlarına ehtiyac yaranmışdır. Agentlərin təhlükəli davranış nümayiş etdirməyəcəyinə təminat vermək problemi isə xüsusilə böyük dil modeli (LLM) əsaslı agentlərin meydana çıxmasından və 2025-ci ildən etibarən onların geniş tətbiq olunmasından sonra daha da aktuallaşmışdır.
Agent davranışının verifikasiyası formal və ya qeyri-formal üsullarla həyata keçirilə bilər. Qeyri-formal verifikasiya daha az riyazi bilik tələb edir. Lakin agentlər insan həyatı, ətraf mühit və ya böyük maliyyə itkiləri ilə bağlı yüksək riskli sistemlərin tərkib hissəsi olduqda, adətən formal verifikasiyaya üstünlük verilir. Həm tənzimləyici qurumlar, həm də sistem layihələndiriciləri formal verifikasiyanı yüksək səviyyədə riyazi etibarlılıq təmin etdiyi üçün üstün hesab edirlər.
Bununla belə, xüsusilə yeni nəsil LLM əsaslı agentlərin yüksək avtonomluq səviyyəsinə görə onların davranışının bütün aspektlərini formal üsullarla yoxlamaq həmişə mümkün olmur. Buna görə də aşağı riskli tətbiqlərdə agentlərin verifikasiyası yalnız qeyri-formal metodlarla aparıla bilər, yüksək riskli tətbiqlərdə isə formal və qeyri-formal metodların kombinasiyasından istifadə olunur.[1]
Ümumi təyinatlı mühakimə agentləri
[redaktə | vikimətni redaktə et]Böyük dil modelinin (LLM) meydana çıxması süni agentlərin tətbiq imkanlarını əhəmiyyətli dərəcədə genişləndirdi, çünki bu modellərə əsaslanan agentlər ümumi təyinatlı koqnitiv qabiliyyətlərə malik ola bilirdilər. LLM-lər (və bəzi hallarda LLM olmayan təməl modellər) əsasında işləyən agentlər, qərar ağacı modelləri ilə idarə olunan agentlər kimi, adversarial hücumlara qarşı oxşar həssaslığa malikdirlər. Bununla yanaşı, LLM agentlərinin daha geniş fəaliyyət imkanları klassik agentlərlə müqayisədə verifikasiya sahəsində yeni problemlər yaratmışdır. Məsələn, LLM-in neyron şəbəkəsi ona sonsuz domenlər üzərində işləmək imkanı verdiyindən, bu xüsusiyyət ənənəvi formal verifikasiya metodları üçün xüsusi çətinlik yaradır.
Akademik tədqiqatçılar LLM agentlərinin verifikasiyası ilə bağlı problemləri 2018-ci ildən araşdırmağa başlamışdırlar. Belə agentlərin tətbiqi 2023-cü ilin sonlarında OpenAI tərəfindən təqdim edilən “function-calling” API-sindən sonra sürətlə artmağa başladı. Xüsusilə Anthropic şirkətinin 2024-cü ilin sonlarında təqdim etdiyi Model Context Protocol (MCP) standartı bu prosesi daha da sürətləndirdi. MCP LLM agentlərinə kontekst məlumatlarını əldə etməyə və müxtəlif xarici alətləri çağırmaqla real dünyada fəaliyyət göstərməyə imkan verən standartlaşdırılmış mexanizmdir. MCP-nin təqdim edilməsindən sonra LLM agentlərinin sürətli yayılması agentlərin verifikasiyasına həm akademik dairələrdə, həm də özəl sektorda marağı əhəmiyyətli dərəcədə artırdı. Artan tələbatı qarşılamaq məqsədilə 2024 və 2025-ci illərdə həm Avropada, həm də ABŞ-də LLM agentlərinin verifikasiyası üzrə ixtisaslaşmış bir sıra startaplar yaradıldı.[2][3][4][5]
Yanaşmalar
[redaktə | vikimətni redaktə et]Formal verifikasiya
[redaktə | vikimətni redaktə et]
Formal verifikasiya sistemin bütün və ya müəyyən xüsusiyyətlərinin düzgünlüyünü riyazi metodlarla sübut etmə prosesidir. Bu metodlar əl ilə aparılan formal sübutlardan tutmuş, Isabelle kimi avtomatlaşdırılmış teorem isbatlayıcılarından istifadə etməklə həyata keçirilən yoxlamalara qədər müxtəlif ola bilər.
Agentlərin verifikasiyasında ən geniş istifadə olunan formal metod model yoxlanılmasıdır (model checking). LLM-dən əvvəlki agent modellərində bu metod tez-tez hesablama ağacı məntiqi (CTL) əsaslı üsullarla tamamlanırdı. Digər geniş yayılmış yanaşma isə teorem isbatıdır. Formal verifikasiya qeyri-formal üsullarla müqayisədə daha yüksək etibarlılıq səviyyəsi təmin etsə də, hətta mümkün olduğu hallarda belə həmişə tətbiq edilmir. Bunun səbəbi proqram agentlərini hazırlayan şəxslərin və ya təşkilatların lazımi ixtisasa malik olmaması və ya agentlərin nasaz işləməsinin ciddi nəticələr doğurmayacağı hallarda bu prosesi əlavə əmək tələb edən iş hesab etmələridir.
Agentlər səhvlərinin ciddi nəticələrə səbəb ola biləcəyi sistemlərdə istifadə edildikdə, formal verifikasiyanın riyazi zəmanət verməsi həm tənzimləyici qurumlar, həm də sistem layihələndiriciləri tərəfindən üstün tutulur. Bununla belə, yüksək riskli sistemlər üçün belə formal verifikasiyanın həyata keçirilməsi çətin ola bilər.[4][6][7]
Hazırlayıcılar agent əsaslı sistemləri elə layihələndirə bilərlər ki, onların xüsusiyyətlərinin daha böyük hissəsinin formal şəkildə yoxlanılması mümkün olsun. Buna həm agenti idarə edən əsas koqnitiv modelin agent scaffolding strukturunun xüsusi şəkildə qurulması, həm də LLM və digər təməl modellərin təlim prosesinin dəyişdirilməsi ilə nail olmaq mümkündür.
Bu yanaşmanın nümunələrindən biri əsas qərarvermə modelinin qəbul etdiyi qərarları ləğv edə bilən idarəedici (governor) və ya arbitraj agentlərinin tətbiqidir. Belə agentlər adətən daha sadə quruluşa malik olduqları üçün onların formal verifikasiyası da asan olur. Bu yanaşma ən azı 2009-cu ildən istifadə olunsa da, 2018-ci ildən sonra LLM-as-a-Judge paradiqmasının meydana çıxması ilə onun əhəmiyyəti daha da artmışdır.
Bununla belə, bu üsullar tətbiq edildikdə belə formal verifikasiya həmişə mümkün olmur. Hesablama tələbləri son dərəcə yüksək ola bilər və bunun üçün bütöv məlumat mərkəzlərinin illərlə işləməsi tələb oluna bilər. Bəzi hallarda isə problemi riyazi baxımdan formalaşdırmaq belə çox çətin olur. Məsələn, çoxagentli sistemdə (MAS) işləmə zamanı agentlərin sayının qeyri-müəyyən şəkildə dəyişməsi halında ümumi problem adətən qərarverilməz olur, baxmayaraq ki, müəyyən xüsusi hallar üçün həll üsulları mövcuddur. LLM agentləri üçün isə verifikasiya problemlərinin bəzi hissələri formal riyaziyyat baxımından tamamilə qərarverilməz və ya ən azı NP-çətin ola bilər. Buna görə də formal verifikasiya çox vaxt qeyri-formal metodlarla tamamlanır.[6][5][8][4]
Kimliyin verifikasiyası
[redaktə | vikimətni redaktə et]LLM agentlərinin sürətlə yayılması onların rəqəmsal kimliyinin təsdiqlənməsini aktual problemə çevirmişdir, çünki bu proses ənənəvi üsullarla həmişə etibarlı və geniş miqyasda həyata keçirilə bilmir. Kimliyin verifikasiyası hər zaman formal verifikasiyanın tərkib hissəsi hesab edilməsə də, onun ciddi şəkildə həyata keçirilməsi müqayisə edilə biləcək səviyyədə etibarlılıq təmin edə bilər. Kimliyin verifikasiyası həlləri təqdim edən Vouched şirkəti 2025-ci ildə LLM agentlərinin kimliyinin verifikasiyası sahəsinə daxil olan şirkətlərdən biridir.[9][10]
Qeyri-formal verifikasiya
[redaktə | vikimətni redaktə et]Agentlərin qiymətləndirilməsi üçün müxtəlif qeyri-formal metodlardan istifadə edilə bilər. Bunlar arasında proqram təminatının inspeksiyası və heuristik qiymətləndirmə ən qeyri-formal üsullardan hesab olunur. Bununla belə, sadə və kiçik həcmli kodun yoxlanıldığı hallardan başqa, yüksək etibarlılıq səviyyəsinə nail olmaq üçün qiymətləndiricilərdən böyük təcrübə və peşəkarlıq tələb olunur.
Proqram təminatının sınağı sahəsi formal verifikasiyada olduğu kimi ciddi riyazi sübut tələb etməyən, lakin adətən sistemli şəkildə həyata keçirilən müxtəlif sınaq metodlarını, o cümlədən funksional testi əhatə edir. Agentlərin verifikasiyasında isə ənənəvi qeyri-formal metodların əsas çətinliyi bütün mümkün ssenariləri əhatə edən test nümunələrinin hazırlanmasının mürəkkəbliyidir. Sistemin ümumi məqsədlərinə nail olmaq üçün müxtəlif agentlərin qarşılıqlı fəaliyyət göstərməsi tələb olunduqda, hətta agentlərin hər biri ayrıca sadə olsa belə, mümkün vəziyyətlərin sayı son dərəcə böyük ola bilər.
Ənənəvi proqram təminatının verifikasiyası metodlarının icra vaxtı verifikasiyası (runtime verification)[note 1] ilə tamamlanması agent əsaslı sistemlərin spesifikasiyaya uyğun işlədiyinə olan inamı daha da artırır.[11][6]
Simulyasiya
[redaktə | vikimətni redaktə et]Agent əsaslı modellər və ya geniş yayılmış adı ilə agent əsaslı simulyasiyalar (ABM) 1980-ci illərdən mövcuddur. Lakin ilk dövrlərdə onlar əsasən xəstəliklərin yayılması və ya maliyyə bazarlarındakı proseslər kimi makrosəviyyəli hadisələrin modelləşdirilməsi üçün istifadə olunurdu, agentlərin öz davranışlarını öyrənmək üçün deyil.
Bu vəziyyət 1990-cı illərdə dəyişməyə başladı. Java əsasında hazırlanmış JAMES platforması mobil agentlərin davranışının verifikasiyası üçün simulyasiyadan istifadə edən ilk sistemlərdən biri olmuşdur. Bununla belə, təməl modellər (foundation models) meydana çıxana qədər simulyasiya üsullarından bu məqsədlə istifadə geniş yayılmamışdı.
2020-ci illərdə LLM əsaslı agentlərin sürətlə tətbiq olunması simulyasiya metodlarına marağı əhəmiyyətli dərəcədə artırdı. Simulyasiya formal sübut qədər yüksək riyazi zəmanət verməsə də, formal və digər qeyri-formal metodlarla həlli mümkün olmayan və ya çox çətin olan LLM agentlərinin verifikasiyası problemlərinin bir hissəsinin qiymətləndirilməsi üçün əlverişli vasitə hesab olunur.
Agentlərin verifikasiyası üçün rəqəmsal simulyasiya platformaları təqdim edən şirkətlərdən biri Daniel J. Hulme və Calum Chace tərəfindən yaradılmış Conscium şirkətidir. Şirkətin VerifyAX platforması agentlərin davranışını standart etalonlarla yanaşı siyasətlərə uyğunluq, adversarial və ya qeyri-müəyyən giriş məlumatlarına qarşı dayanıqlılıq, həmçinin zaman keçdikcə davranış sabitliyinin qorunması kimi meyarlar əsasında yoxlamağa imkan verir.[2][12][6]
Alətlər
[redaktə | vikimətni redaktə et]- MCMAS — zaman, epistemik və strateji məntiqləri dəstəkləyən çoxagentli sistemlər üçün simvolik model yoxlayıcısıdır.[13]
- MCMAS-OP — agentlərin icra zamanı sistemə qoşula və ya sistemi tərk edə bildiyi açıq çoxagentli sistemlər üçün hazırlanmış MCMAS genişləndirməsidir. (Açıq mənbəli.)[8]
- AJPF (Agent JPF) — agent proqramlaşdırma dillərinin model yoxlanılması üçün Java Pathfinder platformasının genişləndirilməsidir.[14]
- VerifyAX — süni intellekt agentlərinin simulyasiya əsaslı verifikasiyası üçün platformadır.[2]
Həmçinin bax
[redaktə | vikimətni redaktə et]Qeydlər
[redaktə | vikimətni redaktə et]- ↑ İcra vaxtı verifikasiyası konkret tətbiq üsulundan asılı olaraq həm formal, həm də qeyri-formal verifikasiya kateqoriyasına aid edilə bilər.
İstinadlar
[redaktə | vikimətni redaktə et]- ↑ Bordini RH, Visser W, Fisher M, Wooldridge M. "Verifying Multi-agent Programs by Model Checking". Autonomous Agents and Multi-Agent Systems. 12 (2). 2006: 239–256. doi:10.1007/s10458-006-5955-7.
- 1 2 3 Éanna Kelly. "The startups chasing rogue AI agents: 'They could cost your company billions of dollars'". Sifted. 9 dekabr 2025. İstifadə tarixi: 22 fevral 2026.
- ↑ Cole Stryker. "The evolution of AI agents". IBM. 2025. 13 yanvar 2026 tarixində arxivləşdirilib. İstifadə tarixi: 22 fevral 2026.
- 1 2 3 Hinchey M, Steffen B, redaktorlar The Combined Power of Research, Education, and Dissemination: Essays Dedicated to Tiziana Margaria on the Occasion of Her 60th Birthday. Springer Nature. 2025. 202–215, 302–325, 328. ISBN 978-3031738869.
- 1 2 Kouvaros, Panagiotis. Towards Formal Verification of Neuro-symbolic Multi-agent Systems. International Joint Conference on Artificial Intelligence. 2023. doi:10.24963/ijcai.2023/800.
- 1 2 3 4 Louise D, Michael F. Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines. Cambridge University Press. 2023. 8, 24–26, 42–45. ISBN 1108484999.
- ↑ Bakar NA, Selamat A. "Agent systems verification : systematic literature review and mapping". Appl Intell (48). 2018: 1251–1274. doi:10.1007/s10489-017-1112-z.
- 1 2 Kouvaros P, Lomuscio A, Pirovano E, Punchihewa H. Formal Verification of Open Multi-Ag (PDF). [International Conference on Autonomous Agents and Multiagent Systems]. 17 may 2019. 8 fevral 2026 tarixində arxivləşdirilib (PDF). İstifadə tarixi: 14 fevral 2026.
- ↑ "Vouched Launches "Know Your Agent" Verification to Bring Trust and Identity to the Next Generation of AI Agents". Businesswire. 22 may 2025. 18 yanvar 2026 tarixində arxivləşdirilib. İstifadə tarixi: 22 fevral 2026.
- ↑ A Formal Verification-Based Risk Assessment Framework for the Authentication of Self-driving Vehicles Arxiv surəti 15 iyul 2026 tarixindən Wayback Machine saytında DOI 10.1109/ICCT62929.2024.10875011
- ↑ Fisher M, Dennis L, Webster M. "Verifying Autonomous Systems". Communications of the ACM. 56 (9). 2013: 84–93. doi:10.1145/2494558.
- ↑ Davoust A, və b. "An Architecture for Integrating BDI Agents with a Simulation Environment" (PDF). Carleton University. 2019. 28 avqust 2025 tarixində arxivləşdirilib (PDF). İstifadə tarixi: 22 fevral 2026.
- ↑ Lomuscio, A., Qu, H. & Raimondi, F. (2017). "MCMAS: an open-source model checker for the verification of multi-agent systems." International Journal on Software Tools for Technology Transfer, 19(1), 9–30. doi:10.1007/s10009-015-0378-x
- ↑ Dennis, L.A., Fisher, M., Webster, M.P. & Bordini, R.H. (2012). "Model checking agent programming languages." Automated Software Engineering, 19(1), 5–63. doi:10.1007/s10515-011-0088-x