DeepSeek ஆனது DeepSeek-Prover-V2 ஐ அறிமுகப்படுத்தியுள்ளது, இது லீன் 4 கட்டமைப்பிற்குள் ஃபார்மல் தேற்றம் நிரூபிக்கும் சிக்கலான களத்திற்காக வடிவமைக்கப்பட்ட ஒரு அற்புதமான திறந்த-மூல பெரிய மொழி மாதிரி (LLM). இந்த புதிய மாதிரி, டீப் சீக்கின் அதிநவீன டீப் சீக்-வி3 அடித்தள மாதிரியின் ஆற்றலைப் பயன்படுத்தி, ஒரு சுழல் தேற்றம் நிரூபண பைப்லைனை பயன்படுத்துகிறது. லீன் 4, லீன் தேற்றம் நிரூபணத்தின் சமீபத்திய மறு செய்கை, மைக்ரோசாஃப்ட் ரிசர்ச் மூலம் உருவாக்கப்பட்ட ஒரு ஊடாடும் நிரூபண உதவியாளராக உள்ளது. இந்த அதிநவீன செயல்பாட்டு நிரலாக்க மொழி மற்றும் ஊடாடும் தேற்றம் நிரூபிக்கும் அமைப்பு, கணிதவியலாளர்கள் மற்றும் கணினி விஞ்ஞானிகளுக்கு இணையற்ற இயந்திர-சோதனை சரிபார்ப்புடன் ஃபார்மல் நிரூபணங்களை உருவாக்க அதிகாரம் அளிக்கிறது.
இந்த திட்டம், ஃபார்மல் மற்றும் முறைசாரா கணித பகுத்தறிவுக்கு இடையே உள்ள இடைவெளியைக் குறைக்கும் நோக்கில் ஒரு முக்கியமான படியாகும். பொது நோக்கங்களுக்காக உருவாக்கப்பட்ட எல்எல்எம்-களின் உள்ளார்ந்த திறன்களைப் பயன்படுத்தி, ஃபார்மல் தேற்றம் நிரூபிக்கும் அதிக கட்டமைப்பு களத்தை திறம்பட தீர்க்க முற்படுகிறது. சிக்கலான தேற்றங்களை நிர்வகிக்கக்கூடிய மற்றும் புரிந்துகொள்ளக்கூடிய கூறுகளாக உன்னிப்பாகப் பிரிக்கும்போது, மனித கணிதவியலாளர்கள் நிரூபணங்களை உருவாக்கும்போது பயன்படுத்தும் அறிவாற்றல் செயல்முறைகளை அவர்களின் புதுமையான அணுகுமுறை பிரதிபலிக்கிறது என்று டீப் சீக் ஆராய்ச்சி குழு கூறுகிறது.
மதிப்பீட்டு கட்டமைப்பு விரிவாக்கம்: ProverBench அறிமுகம்
தங்கள் ஆராய்ச்சியின் துல்லியத்தை மேம்படுத்தும் ஒரு முக்கியமான நடவடிக்கையில், டீப் சீக் குழுவினர், ஃபார்மல் தேற்றம் நிரூபிக்கும் திறன்களை விரிவாக மதிப்பிடுவதற்காக வடிவமைக்கப்பட்ட புத்தம் புதிய Benchmark சேகரிப்பான ProverBench ஐ அறிமுகப்படுத்தி தங்கள் மதிப்பீட்டு கட்டமைப்பை விரிவாக்கியுள்ளனர். இந்தக் விரிவான சேகரிப்பு ஃபார்மல் கணிதத்தின் சூழலில் எல்எல்எம்-களின் செயல்திறனை மதிப்பிடுவதற்கு ஒரு மதிப்புமிக்க ஆதாரமாக செயல்படுகிறது.
"சாதாரண Benchmarkகளுக்கு அப்பாற்பட்டு, எங்கள் மதிப்பீட்டு செயல்முறையை வளப்படுத்த கவனமாகத் தொகுக்கப்பட்ட 325 ஃபார்மல் பிரச்சனைகளின் ProverBench ஐ பெருமையுடன் அறிமுகப்படுத்துகிறோம். இந்தத் தொகுப்பில், சமீபத்திய அமெரிக்கன் இன்விடேஷனல் கணிதத் தேர்வு (AIME) போட்டிகளில் இருந்து குறிப்பாக 24-25 ஆண்டுகளில் இருந்து நேரடியாக எடுக்கப்பட்ட 15 கவனமாகத் தேர்ந்தெடுக்கப்பட்ட பிரச்சனைகள் அடங்கும்," என்று ஆராய்ச்சியாளர்கள் விளக்கினர்.
ProverBench தரவுத்தொகுப்பில் AIME சிக்கல்களைச் சேர்ப்பது குறிப்பாகக் குறிப்பிடத்தக்கது, ஏனெனில் இது கணித சமூகத்தில் பரவலாக அங்கீகரிக்கப்பட்ட சவாலான மற்றும் நன்கு நிறுவப்பட்ட கணித சிக்கல்களை அறிமுகப்படுத்துகிறது. இது டீப் சீக்-ப்ரூவர்-வி2 இன் செயல்திறனை மதிப்பிடுவதற்கும் பிற அணுகுமுறைகளுடன் ஒப்பிடுவதற்கும் ஒரு தரப்படுத்தப்பட்ட மற்றும் கடுமையான அடிப்படையை வழங்குகிறது.
வாக்குறுதியளிக்கும் ஆரம்ப முடிவுகள்: AIME பிரச்சனைகளை கையாளுதல்
இந்த சவாலான AIME பிரச்சனைகள் குறித்த கடுமையான சோதனையிலிருந்து கிடைக்கப்பெற்ற ஆரம்ப முடிவுகள், அவர்களின் கூர்ந்துபார்க்கக்கூடிய வடிவமைக்கப்பட்ட சிறப்பு தேற்றம் நிரூபண மாடலால் விதிவிலக்காக உறுதியளிக்கும் செயல்திறனை வெளிப்படுத்தியுள்ளது. டீப் சீக் குழுவினர், டீப் சீக்-ப்ரூவர்-வி2 தனக்கு வழங்கப்பட்ட 15 AIME பிரச்சனைகளில் 6 ஐ வெற்றிகரமாக தீர்த்து வைத்துள்ளது என்று பெருமையுடன் தெரிவிக்கிறது. ஒப்பிடுகையில், பொது நோக்கங்களுக்காக உருவாக்கப்பட்ட டீப் சீக்-வி3 மாதிரி, பெரும்பான்மை வாக்களிப்பு முறைகளைப் பயன்படுத்தும்போது, 8 சிக்கல்களை வெற்றிகரமாக தீர்த்தது.
சிக்கலான கணித சிக்கல்களைத் தீர்ப்பதில் சிறப்பு மற்றும் பொது நோக்கங்களுக்காக உருவாக்கப்பட்ட எல்எல்எம்களின் திறனை இந்த கண்டுபிடிப்புகள் எடுத்துக்காட்டுகின்றன. இந்த குறிப்பிட்ட Benchmarkகில் பொது நோக்கங்களுக்காக உருவாக்கப்பட்ட மாடல் சற்று அதிக வெற்றி விகிதத்தைக் காட்டியிருந்தாலும், சிறப்பு தேற்றம் நிரூபண மாதிரி ஃபார்மல் கணித பகுத்தறிவில் திறமையைக் காட்டியது.
மனித நிரூபண கட்டுமானத்தை பின்பற்றுதல்: ஒரு எண்ணச் சங்கிலி அணுகுமுறை
"பொதுவாக உருவாக்கப்பட்டுள்ள மாதிரிகள் முழுமையான லீன் நிரூபணங்களை உருவாக்க முயற்சிக்கும்போது அடிக்கடி எதிர்கொள்ளும் நன்கு ஆவணப்படுத்தப்பட்ட சவால்களைக் கருத்தில் கொண்டு, சிக்கலான விவரங்களைத் தவிர்த்துவிட்டு, உயர்ந்த அளவிலான நிரூபண வரைவு ஒன்றை மட்டுமே உருவாக்க டீப் சீக்-வி3க்கு நாங்கள் அறிவுறுத்தினோம். இதன் விளைவாக சிந்தனைச் சங்கிலி ஒரு லீன் தேற்றத்தில் முடிவடைகிறது, இது தொடர்ச்சியான ஹேவ் அறிக்கைகளைக் கொண்டது, ஒவ்வொன்றும் ஒரு மன்னிக்கவும் ஒதுக்கிடத்துடன் கவனமாக முடிக்கப்பட்டுள்ளது, இது தீர்க்கப்பட வேண்டிய ஒரு துணை இலக்கை திறம்படக் குறிக்கிறது. சிக்கலான தேற்றம் படிப்படியாக நிர்வகிக்கக்கூடிய லெம்மாக்களின் வரிசையாகக் குறைக்கப்படும் மனித வகை நிரூபண கட்டுமானத்தை இந்த புதுமையான அணுகுமுறை நேர்த்தியாக பிரதிபலிக்கிறது," என்று டீப் சீக் குழுவினர் விளக்கினர்.
உயர்ந்த அளவிலான நிரூபண வரைபடங்களை உருவாக்குவதற்கான இந்த புதுமையான அணுகுமுறை, கணிதவியலாளர்கள் சிக்கலான நிரூபணங்களை எவ்வாறு அணுகுகிறார்கள் என்பதை ஒத்துள்ளது. ஒட்டுமொத்த அமைப்பு மற்றும் முக்கிய படிகளில் கவனம் செலுத்துவதன் மூலம், மாதிரி நிரூபணத்தின் அடுத்தடுத்த சுத்திகரிப்பு மற்றும் நிறைவுக்கு திறம்பட வழிகாட்ட முடியும்.
முறையான உத்தி: நிரூபணத்தின் ஒவ்வொரு கூறுபாட்டையும் தனித்தனியாக கையாளுதல்
பின்னர் இந்த அமைப்பு நிரூபணத்தின் ஒவ்வொரு தனிப்பட்ட கூறுபாடையும் கையாள ஒரு முறையான மற்றும் கட்டமைக்கப்பட்ட உத்தியை உன்னிப்பாகப் பயன்படுத்துகிறது. இந்த முறையான அணுகுமுறை நிரூபணத்தின் ஒவ்வொரு அம்சமும் கவனமாக கருதப்பட்டு தர்க்கரீதியான மற்றும் ஒத்திசைவான வழியில் கையாளப்படுவதை உறுதி செய்கிறது. முன்னதாக நிறுவப்பட்ட முடிவுகளை அடிப்படையாகக் கொண்டு தேற்றம் நிரூபணத்திற்கான உயர் கட்டமைக்கப்பட்ட அணுகுமுறையை இந்த அமைப்பு உருவாக்குகிறது, ஒவ்வொரு அடுத்தடுத்த படிக்கும் ஒரு உறுதியான அடித்தளத்தை உறுதி செய்கிறது.
"டீப் சீக்-வி3 ஆல் உருவாக்கப்பட்ட துணை இலக்குகளைப் பயன்படுத்தி, ஒவ்வொரு இடைநிலை நிரூபணப் படியையும் முறையாகத் தீர்க்க ஒரு சுழல் தீர்க்கும் உத்தியை நாங்கள் பின்பற்றுகிறோம். கொடுக்கப்பட்ட பிரச்சனைகளில் அசல் இலக்குகளுக்குப் பதிலாக ஹேவ் அறிக்கைகளிலிருந்து துணை இலக்கு வெளிப்பாடுகளைப் பிரித்து, முந்தைய துணை இலக்குகளை வளாகங்களாக இணைக்கிறோம். இந்த கட்டுமானம் முந்தைய படிகளின் இடைநிலை முடிவுகளைப் பயன்படுத்தி அடுத்தடுத்த துணை இலக்குகளைத் தீர்க்க உதவுகிறது, இதன் மூலம் மேலும் உள்ளூர்மயமாக்கப்பட்ட சார்பு கட்டமைப்பை மேம்படுத்துகிறது மற்றும் எளிமையான லெம்மாக்களின் வளர்ச்சியை எளிதாக்குகிறது," என்று ஆராய்ச்சியாளர்கள் விவரித்தனர்.
சிக்கலான நிரூபணங்களைக் கையாளும் அமைப்பின் திறனின் ஒரு முக்கிய அம்சம் சுழல் தீர்க்கும் உத்தி ஆகும். சிக்கலை சிறிய, நிர்வகிக்கக்கூடிய துணை இலக்குகளாகப் பிரிப்பதன் மூலம், ஒவ்வொரு தனிப்பட்ட கூறுபாட்டிற்கும் அதன் பகுத்தறிவு திறன்களை திறம்பட பயன்படுத்த முடியும்.
கணக்கீட்டு வளங்களை மேம்படுத்துதல்: ஒரு சிறப்பு 7பி அளவுரு மாதிரி
கணக்கீட்டு வளங்களை திறம்பட மேம்படுத்துவதற்கும், திறமையான செயலாக்கத்தை உறுதி செய்வதற்கும், சிதைந்த லெம்மாக்களை செயலாக்க ஒரு சிறிய, மிகவும் சிறப்பு வாய்ந்த 7பி அளவுரு மாதிரியை அமைப்பு வியூகமாக பயன்படுத்துகிறது. விரிவான நிரூபண தேடல்களுடன் தொடர்புடைய கணக்கீட்டு தேவைகளை திறம்பட நிர்வகிப்பதற்கு இந்த அணுகுமுறை முக்கியமானது, தேடல் இடத்தின் சிக்கலால் பாதிக்கப்படாமல் அமைப்பு திறமையாக செயல்பட முடியும் என்பதை உறுதி செய்கிறது. அனைத்து சிதைந்த படிகளும் வெற்றிகரமாக தீர்க்கப்படும் போது இந்த அணுகுமுறை தானாகவே பெறப்பட்ட முழுமையான நிரூபணத்தில் விளைகிறது.
"அல்горитமிக் கட்டமைப்பு இரண்டு தனித்துவமான கட்டங்களில் செயல்படுகிறது, இரண்டு நிரப்பு மாதிரிகளைப் பயன்படுத்துகிறது: லெம்மா சிதைவுக்கு டீப் சீக்-வி3 மற்றும்தொடர்புடைய ஃபார்மல் நிரூபண விவரங்களை முடிக்க ஒரு 7பி நிரூபண மாதிரி," என்று ஆராய்ச்சியாளர்கள் விவரித்தனர்.
இந்த இரண்டு-நிலை அணுகுமுறை ஒரு பெரிய பொது நோக்கங்களுக்காக உருவாக்கப்பட்ட மாதிரி மற்றும் சிறிய சிறப்பு மாதிரி இரண்டின் பலத்தையும் பயன்படுத்த அமைப்பு அனுமதிக்கிறது. பெரிய மாதிரி உயர்ந்த அளவிலான நிரூபண வரைபடங்களை உருவாக்க பயன்படுகிறது, அதே நேரத்தில் சிறிய மாதிரி விவரங்களை நிரப்பவும் ஃபார்மல் நிரூபணத்தை முடிக்கவும் பயன்படுத்தப்படுகிறது.
ஃபார்மல் பகுத்தறிவு தரவை ஒருங்கிணைத்தல்: ஒரு இயற்கையான பாதை
இந்த கவனமாக வடிவமைக்கப்பட்ட கட்டமைப்பு, உயர்ந்த அளவிலான கணித பகுத்தறிவை, ஃபார்மல் சரிபார்ப்பின் கடுமையான மற்றும் கடுமையான தேவைகளுடன் தடையின்றி ஒன்றிணைத்து, ஃபார்மல் பகுத்தறிவு தரவை ஒருங்கிணைப்பதற்கான ஒரு இயற்கையான மற்றும் உள்ளுணர்வு பாதையை திறம்பட நிறுவுகிறது. அமைப்பின் முடிவுகளின் நம்பகத்தன்மை மற்றும் நம்பகத்தன்மையை உறுதி செய்வதற்கு இந்த ஒருங்கிணைப்பு அவசியம்.
"இறுதி முதல் இறுதி வரை 7பி நிரூபண மாதிரியால் தீர்க்கப்படாமல் இருக்கும் சவாலான பிரச்சனைகளின் துணைக்குழுவை நாங்கள் தொகுக்கிறோம், ஆனால் அனைத்து சிதைந்த துணை இலக்குகளும் வெற்றிகரமாக தீர்க்கப்பட்டுள்ளன, அனைத்து துணை இலக்குகளின் நிரூபணங்களையும் தொகுப்பதன் மூலம், அசல் பிரச்சனைக்கான முழுமையான-ஃபார்மல் நிரூபணத்தை உருவாக்குகிறோம்," என்று ஆராய்ச்சியாளர்கள் விளக்கினர்.
சிக்கலான சிக்கல்களைத் தீர்க்கும் திறனை மேம்படுத்தவும், அதன் தவறுகளிலிருந்து கற்றுக் கொள்ளவும் இந்த அணுகுமுறை அமைப்பு உதவுகிறது. சிரமத்தை ஏற்படுத்தும் குறிப்பிட்ட துணை இலக்குகளை அடையாளம் காண்பதன் மூலம், அந்த பகுதிகளில் அதன் செயல்திறனை மேம்படுத்துவதில் அமைப்பு அதன் முயற்சிகளை மையப்படுத்த முடியும்.
கவலைகள் மற்றும் சவால்கள்: அமலாக்க விவரங்கள் ஆய்வு
டீப் சீக்-ப்ரூவர்-வி2 ஆல் நிரூபிக்கப்பட்ட மறுக்கமுடியாத தொழில்நுட்ப சாதனைகள் இருந்தபோதிலும், துறையில் உள்ள சில வல்லுநர்கள் சில அமலாக்க விவரங்கள் குறித்து பொருத்தமான கவலைகளை எழுப்பியுள்ளனர். epoch AI யில் ஒரு தலைமை கணிதவியலாளரான எல்லியட் கிளேசர், மேலும் விசாரணைக்கு உத்தரவாதம் அளிக்கும் சாத்தியமான சிக்கல்களை சுட்டிக்காட்டியுள்ளார்.
டீப் சீக்-ப்ரூவர்-வி2 காகிதம் பற்றிய சில கவலைகள். தவறாக உருவாக்கப்பட்ட எடுத்துக்காட்டுகள் மற்றும் லீன் ஜூலிப்பில் நடந்த விவாதம், புட்னம்பெஞ்ச் நிரூபணங்கள் அபத்தமானது மற்றும் அவர்களின் ரீட்-மதிப்பீடு-அச்சிட்டு-சுழற்சியில் தெரிவிக்கப்படாத ஒரு மறைமுகமாக மன்னிக்கவும் (ஒருவேளை apply? தந்திரத்தில் மறைக்கப்பட்டுள்ளது) பயன்படுத்துகிறது என்று கூறுகிறது.
ஃபார்மல் சரிபார்ப்பு இடத்தில் இருக்கும் தொடர்ச்சியான சவால்களை இந்த கவலைகள் தெளிவாக எடுத்துக்காட்டுகின்றன, அங்கு சிறிய மற்றும் முக்கியமற்ற அமலாக்க விவரங்கள் கூட முடிவுகளின் ஒட்டுமொத்த செல்லுபடியாகும் மற்றும் நம்பகத்தன்மையில் விகிதாசாரமற்ற பெரிய தாக்கத்தை ஏற்படுத்தும். ஃபார்மல் சரிபார்ப்பு செயல்முறை விவரங்களுக்கு அசைக்க முடியாத கவனம் மற்றும் நிறுவப்பட்ட தரங்களுக்கு உன்னிப்பாக இணங்குதல் தேவைப்படுகிறது.
தவறாக உருவாக்கப்பட்ட எடுத்துக்காட்டுகளுக்கான சாத்தியம் மற்றும் புட்னம்பெஞ்ச் நிரூபணங்களில் மறைக்கப்பட்ட "மன்னிக்கவும்" தந்திரோபாயங்களின் சாத்தியக்கூறு சரிபார்ப்பு செயல்முறையின் துல்லியம் மற்றும் முழுமை பற்றிய முக்கியமான கேள்விகளை எழுப்புகின்றன. இந்த கவலைகள் முடிவுகளின் தொடர்ச்சியான ஆய்வு மற்றும் சுயாதீனமான சரிபார்ப்பின் தேவையை அடிக்கோடிட்டுக் காட்டுகின்றன.
கிடைக்கக்கூடிய தன்மை மற்றும் வளங்கள்: ஃபார்மல் தேற்றம் நிரூபிப்பதற்கான ஜனநாயக அணுகலை அளித்தல்
டீப் சீக் அதன் Prover-V2 ஐ இரண்டு தனித்துவமான மாதிரி அளவுகளில் கிடைக்கச் செய்துள்ளது, இது பல்வேறு கணக்கீட்டு வளங்கள் மற்றும் ஆராய்ச்சி நோக்கங்களுக்காக உதவுகிறது. முதல் பதிப்பு ஒரு 7பி அளவுரு மாதிரி, இது அவர்களின் முந்தைய Prover-V1.5-Base ஐ அடிப்படையாகக் கொண்டது, இது 32K டோக்கன்கள் வரை நீட்டிக்கப்பட்ட சூழல் நீளத்தைக் கொண்டுள்ளது. இரண்டாவது பதிப்பு டீப் சீக்-வி3-Base இல் பயிற்சி செய்யப்பட்ட 671பி அளவுரு மாதிரியாகும். இரண்டு மாதிரிகளும் இப்போது ஹக்கிங்ஃபேஸில் உடனடியாக அணுகக்கூடிய வகையில் உள்ளன, இது இயந்திர கற்றல் மாதிரியில் பகிர்தல் மற்றும் ஒத்துழைப்பதற்கான ஒரு முன்னணி தளமாகும்.
மாடல்களுக்கு கூடுதலாக, மதிப்பீட்டு நோக்கங்களுக்காக 325 உன்னிப்பாக வடிவமைக்கப்பட்ட சிக்கல்களைக் கொண்ட முழு ProverBench தரவுத்தொகுப்பையும் டீப் சீக் ஹக்கிங்ஃபேஸில் கிடைக்கச் செய்துள்ளது. இந்த விரிவான தரவுத்தொகுப்பு ஆராய்ச்சியாளர்கள் மற்றும் டெவலப்பர்களுக்கு அவர்களின் மாடல்களின் செயல்திறனை மதிப்பிடுவதற்கும் டீப் சீக்-ப்ரூவர்-வி2 உடன் ஒப்பிடுவதற்கும் ஒரு மதிப்புமிக்க ஆதாரத்தை வழங்குகிறது.
இந்த வளங்களை இலவசமாக கிடைக்கச் செய்வதன் மூலம், ஃபார்மல் தேற்றம் நிரூபிக்கும் தொழில்நுட்பத்திற்கான ஜனநாயக அணுகலை டீப் சீக் வழங்குகிறது மற்றும் ஆராய்ச்சி சமூகத்திற்குள் ஒத்துழைப்பை ஊக்குவிக்கிறது. இந்த திறந்த-திறன் அணுகுமுறை துறையில் முன்னேற்றத்தை துரிதப்படுத்தவும் தானியங்கி பகுத்தறிவு மற்றும் சரிபார்ப்பில் புதிய முன்னேற்றங்களுக்கு வழிவகுக்கும்.
இந்த வெளியீடு இந்த தொழில்நுட்பத்தின் திறன்கள் மற்றும் வரம்புகளை ஆராய்வதற்கு தேவையான ஆதாரங்களைக் கொண்டு ஆராய்ச்சியாளர்கள் மற்றும் டெவலப்பர்களுக்கு அதிகாரம் அளிக்கிறது. மாதிரிகள் மற்றும் ProverBench தரவுத்தொகுப்பிற்கு திறந்த அணுகலை வழங்குவதன் மூலம், துறையில் உள்ள நிபுணர்களால் எழுப்பப்பட்ட கவலைகளை நிவர்த்தி செய்ய மேலும் ஆய்வு மற்றும் கூட்டு முயற்சிகளை டீப் சீக் ஊக்குவிக்கிறது. ஃபார்மல் தேற்றம் நிரூபிப்பதில் உள்ள சிக்கல்களை அவிழ்த்து விடுவதற்கும், இந்த அற்புதமான முன்னேற்றங்களின் நம்பகத்தன்மையை உறுதிப்படுத்துவதற்கும் இந்த கூட்டு அணுகுமுறை முக்கியமாகும்.