Claude, Lean மொழியில் ஃபெர்மாவின் கடைசித் தேற்றத்தை முறைப்படுத்துகிறது
Anthropic சமீபத்தில் ஒரு பிரம்மாண்டமான ஆராய்ச்சிப் பணியை முடித்துள்ளது. Lean 4 நிரூபண மொழியைப் பயன்படுத்தி ஃபெர்மாவின் கடைசித் தேற்றத்தை முறைப்படுத்த ஒரு உள்முறை மாதிரி (internal model) 11 நாட்கள் உழைத்தது.
இது ஒரு புதிய கணிதக் கண்டுபிடிப்பு அல்ல. ஆண்ட்ரூ வைல்ஸ் 1995-இல் இந்தத் தேற்றத்தை நிரூபித்தார். Anthropic செய்ததெல்லாம் அந்த ஏற்கனவே உள்ள நிரூபணத்தை குறியீடாக (code) மாற்றியதுதான். இது கணினி ஒவ்வொரு தர்க்கரீதியான படிநிலையையும் முழுமையான உறுதியுடன் சரிபார்க்க அனுமதிக்கிறது.
இந்தத் திட்டத்தின் அளவு பிரம்மாண்டமானது: • இந்த மாதிரி 13 மில்லியன் வரிகள் கொண்ட Lean குறியீட்டை உருவாக்கியது. • இது 30,300 இடைநிலைத் தேற்றங்களை நிரூபித்தது. • இது கிட்டத்தட்ட 6 பில்லியன் வெளியீட்டு டோக்கன்களைப் பயன்படுத்தியது.
இந்த மாதிரி பெரும்பாலும் தானாகவே இயங்கியது. மனிதர்கள் அவ்வப்போது உயர்நிலை வழிகாட்டுதல்களை மட்டுமே வழங்கினர். யாரும் கவனிக்காத நள்ளிரவில் இந்தச் செயல்முறை முடிவடைந்தது. இந்த வெற்றி தானாகவே கணினியில் பதிவு செய்யப்பட்டது.
கவனிக்க வேண்டிய இரண்டு முக்கியமான விஷயங்கள்:
- இந்த மாதிரி ஒரு உள் ஆராய்ச்சி கருவி. இதை நீங்கள் இன்னும் API மூலம் அணுக முடியாது. இது நீங்கள் இன்று பயன்படுத்தும் Claude மாதிரிகளைப் போன்றது அல்ல.
- டெவலப்பர்களுக்கான உண்மையான மதிப்பு Prove2Me எனப்படும் ஒருங்கிணைப்பு அடுக்கில் உள்ளது.
Prove2Me என்பது ஒரு திறந்த மூலக் கருவி. இது பணிகளை நிர்வகிக்க ஒரு சார்பு வரைபடத்தைப் (dependency graph) பயன்படுத்துகிறது. ஒரு சாதாரண சரிபார்ப்புப் பட்டியலுக்குப் பதிலாக, நிரூபணங்கள் ஒன்றுடன் ஒன்று எவ்வாறு இணைகின்றன என்பதற்கான வரைபடத்தை இது உருவாக்குகிறது.
இந்த அமைப்பு ஏஜென்ட் பணிப்பாய்வுகளுக்கு (agent workflows) இரண்டு முக்கியப் பிரச்சனைகளைத் தீர்க்கிறது:
- ஒன்றுக்கும் மேற்பட்ட ஏஜென்ட்கள் ஒரே வேலையைச் செய்வதைத் இது தடுக்கிறது.
- இது ஏஜென்ட்களுக்கு ஒரு பகிரப்பட்ட நினைவகத்தை வழங்குகிறது, இதனால் அவர்கள் முக்கிய இலக்கை மறப்பதில்லை.
பெரும்பாலான ஏஜென்ட் பணிப்பாய்வுகள் காலப்போக்கில் சூழலை (context) இழப்பதன் காரணமாகத் தோல்வியடைகின்றன. ஒரு நீண்ட அரட்டைச் சாளரத்திற்குப் பதிலாக, ஒரு பகிரப்பட்ட, வெளிப்புற வரைபடத்தைப் பயன்படுத்துவது பணியைத் திட்டமிட்டபடி வைத்திருக்க உதவுகிறது.
நீங்கள் ஏஜென்ட் பணிப்பாய்வுகளை உருவாக்குகிறீர்கள் என்றால், Prove2Me கட்டமைப்பைப் படிக்க வேண்டும். நீங்கள் Anthropic-இன் ஆராய்ச்சி மாதிரிகளைப் பயன்படுத்தாவிட்டாலும், அவை பணிகளை ஒருங்கிணைக்கும் விதம் நீண்ட காலப் பணிகளுக்கான (long horizon work) ஒரு முன்மாதிரியாகும்.
Source: https://dev.to/raxxostudios/claude-just-formalized-fermats-last-theorem-in-lean-3p36
Optional learning community: https://t.me/GyaanSetuAi