කෝක්, රොක්, ලීන් වැනි පරිභාෂා‑මූලික භාෂා, කේතයේ නිරුපිත නියමයන් සෘජුවම පරීක්ෂා කරන හැකියාවක් දෙනවා. නමුත් එම වාසියට අමතරව, සාක්ෂි ලිවීමේ කාලය ඉතා වැඩිවන බැවින්, බොහෝ සංවර්ධකයින්ට ඒවා අත්යවශ්ය නොවනවා වගේ පෙනේ.
මෙම ගැටළුවට නව විසඳුමක් ලෙස, කෘතිම බුද්ධිය (LLM) සමඟ සාක්ෂි ස්වයංක්රීය කිරීමේ අත්දැකීම අලුත් තරඟයක් ගෙන එයි. මූලික අදහස වන්නේ, සාක්ෂිය නිවැරදි නම්, ඒ සාක්ෂියේ තත්ත්වය වැදගත් නොවන අතර, එය පවතින බව පමණක් ප්රමාණවත් වීමයි. එම නිසා LLM මගින් සාක්ෂි ලිවීමේ බර අඩු කර, තේරුම් ගත යුතු වැඩ පමණක් ඉතිරි වේ.
මෙම සංකල්පය පරීක්ෂා කිරීමට, ලේඛකයා ලීන් භාෂාවෙන් Zstandard (ZSTD) සංඛ්යාතකරණයේ ඩිකම්ප්රෙස්සර් එකක් සාදා ඇත. ZSTD යනු gzip කෙරෙහි තරඟකරන නවතම සම්පීඩකයකි, ඒත් එය ලීන් මඟින් ලියන ලද විශාල කේතයක් ලෙස සැලකේ. මෙම පරීක්ෂණය මඟින්, LLM භාවිතයෙන් සාක්ෂි ලේඛන 20 පාරක් අඩු කළ හැකි බව පෙන්වා දී ඇත.
කොඩ් එකේ වෙනස්කම් සිදුවූ විට, සාක්ෂි නැවත සකස් කිරීමේ පිරිවැය අඩු වීම, තාක්ෂණික වශයෙන් නව පරමාර්ථයක් වේ. එමෙන්ම, ලීන් පරිසරය තුළ අධික මතක භාවිතය නොවන පරිදි LLM මගින් පරික්ෂා කළ හැකි බව පරීක්ෂා කර ඇත.
ශ්රී ලංකාවට ඇති වැදගත්කම
ශ්රී ලංකාවේ තාක්ෂණ ශිෂ්යයන්, සංවර්ධකයින්, ව්යාපාරිකයින් සඳහා මෙම නවෝත්පාදනය විශාල අවස්ථාවක් වේ:
- ශ්රේෂ්ඨ අධ්යාපනය: විශ්වවිද්යාලයන්ට dependent types සහ proof automation පාඨමාලා ඇතුළත් කිරීමේ හැකියාව ලැබේ.
- විකසිත සංවර්ධනය: කෝඩ් පදනම මත අඩු සාක්ෂි පිරිවැය නිසා, නව යෙදුම් ඉක්මනින් නිර්මාණය කර ගත හැක.
- ව්යාපාරික ප්රතිලාභ: සුරක්ෂිත හා කාර්යක්ෂම සොෆ්ට්වේයාර් නිර්මාණය කිරීමෙන්, දත්ත ආරක්ෂාව සහ ක්රියාකාරී කාලය අඩු වේ.
අනාගතයේදී, LLM‑අධිෂ්ඨිත සාක්ෂි ස්වයංක්රීය කිරීම, ශ්රී ලංකාවේ තාක්ෂණික පදනම වඩා ශක්තිමත් කර, ගෝලීය තරඟකාරිත්වයට අපව ගෙන යාමට මඟ පෙන්වයි.
කොඩ් ලේඛන වල සංකීර්ණතාවය අඩු කර, නිර්මාණය සහ නවීකරණය අතර ඇති දුර කෙටි කිරීම, තාක්ෂණික ප්රගතියේ නව මංපොළක් විවෘත කරයි. මෙය සාර්ථකව පවත්වාගෙන යාමට, LLM සහ dependent types අතර සම්බන්ධතාවය තවත් අධ්යයනය කළ යුතුය.
