অনুভব করা যাচ্ছে যে কৃত্রিম বুদ্ধিমত্তা প্রায় প্রতি সপ্তাহে একটি নতুন গাণিতিক সমস্যা সমাধান করছে। গত মাসে, শুধুমাত্র OpenAI-এর একটি প্রতিষ্ঠানই 719টি হস্তলিখিত প্রবন্ধ প্রকাশ করেছে, যেগুলি এই ক্ষেত্রের কিছু সবচেয়ে কঠিন সমস্যা সমাধান করেছে বলে দাবি করে। এমনকি কম্পিউটার পরীক্ষাও ভুল করতে পারে। বছরের পর বছর ধরে AI-এর অপ্রয়োজনীয় কনটেন্টের পর, মানুষ প্রশ্ন করছে যে, গণিত কি পরবর্তী প্রভাবিত ক্ষেত্র হয়ে উঠবে।
অক্সিয়মম্যাথ এই ভাগ্য এড়াতে পারে, গতি কমানোর পরিবর্তে একটি দৃঢ় ভিত্তি গড়ে তোলার মাধ্যমে। এই 16 বিলিয়ন ডলার মূল্যায়নযুক্ত স্টার্টআপটি একটি যাচাইকৃত ভিত্তি তৈরির লক্ষ্যে কাজ করছে, যার উপর AI এজেন্টগুলি সফটওয়্যার লেখার জন্য নির্ভর করতে পারবে এবং শেষপর্যন্ত বৈজ্ঞানিক গবেষণা করতে পারবে।
বুধবার, কোম্পানিটি ঘোষণা করেছে যে এটি স্ট্যাকস প্রকল্পকে অফিসিয়ালভাবে যাচাই করেছে, যা মানুষ দ্বারা লিখিত সবচেয়ে বড় গণিতের অর্জনগুলির মধ্যে একটি। গণিতবিদরা সাধারণত স্ট্যাকসকে অত্যন্ত উচ্চ মূল্যায়ন করেন। কলম্বিয়া বিশ্ববিদ্যালয়ের গণিতবিদ পিটার ওয়িট এটিকে “অন্য কিছুর সঙ্গে তুলনা করার মতো কিছুই নেই” বলেছিলেন এবং এই প্রকল্পটিকে “প্রখ্যাত বুরবাকি সিরিজ”-এর সঙ্গে তুলনা করেছিলেন—যে সিরিজটি ২০শ শতাব্দীতে গণিতকে মৌলিকভাবে পুনর্গঠন করেছিল।
২০০৫ সালে ওয়াইটের কলম্বিয়ার সহকর্মী জোহান ডি জং স্ট্যাকস প্রজেক্টটি একটি ওপেন-সোর্স রেফারেন্স হিসেবে শুরু করেন। তারপর থেকে গণিতবিদরা এটিতে অবদান রাখছেন, বিশ্ববিদ্যালয় স্তরের বীজগণিত থেকে শুরু করে বীজগণিত, জ্যামিতি এবং সংখ্যাতত্ত্বের সবচেয়ে অগ্রগামী ধারণাগুলি পর্যন্ত।
কোম্পানির এআই এজেন্ট গুচ্ছ এই প্রায় 7,654 পৃষ্ঠার ডেটাবেসকে প্রায় 1.6 কোটি লাইনে কম্পিউটার-পরীক্ষণযোগ্য কোডে অনুবাদ করেছে।
ফর্মাল গণিতের উদ্দেশ্য হল এটির নীচের কাঠামোকে নির্ভরযোগ্য করে তোলা। গণিতবিদরা প্রমাণগুলিকে একটি লিন নামক প্রোগ্রামিং ভাষায় কোডে পুনর্লিখন করেন, এবং একটি প্রুফ অ্যাসিসট্যান্ট নামক প্রোগ্রাম দ্বারা এই কোডগুলির প্রতিটি লাইন যাচাই করা হয়। যদি প্রমাণটি পাস করে, তবে গণিতবিদরা এটির যৌক্তিকভাবে সত্যতা বিশ্বাস করতে পারেন।
ইঞ্জিনিয়াররা চিপ ডিজাইনের সম্ভাব্যতা নিশ্চিত করতে একই ধারণা, অর্থাৎ ফর্মাল ভেরিফিকেশন, ব্যবহার করেন; ফ্রান্সের গবেষকরা এটি ব্যবহার করে পরিবারের জন্য সুবিধা গণনা করার সফটওয়্যারের ভুল আবিষ্কার করেন।
স্ট্যাকস প্রজেক্টের মতো একটি সংগ্রহের জন্য, উপপাদ্যগুলি একে একে পরীক্ষা করা কাজের একটি অংশ। স্ট্যাকসের উপপাদ্য এবং সংজ্ঞাগুলি পরস্পরের সাথে সংযুক্ত, প্রতিটি আগেরটির উপর ভিত্তি করে তৈরি। একটি পরিবারগত বৃক্ষের মতো, স্ট্যাকসের অনেক ফলাফলই আগের ফলাফলগুলির দিকে ফিরে যায়।
এই পরস্পর সংযোগের কারণে অ্যাক্সিয়ম প্রথমে নিশ্চিত ছিল না যে এই প্রকল্পটি সম্ভব কিনা। টিমটিকে প্রায় 16 মিলিয়ন লাইন লিয়ান কোডের মধ্যে প্রতিটি সংযোগকে অখণ্ড রাখতে হবে।
অক্সিয়মের সিইও কারিনা হং টেকক্রাঞ্চকে বলেন: “বড় আকার এবং সূক্ষ্মতা বাস্তবে সাধারণত সামঞ্জস্যপূর্ণ নয়। [Stacks] হল গাণিতিক ভিত্তি গঠন করে এমন গাণিতিক ফলাফলের একটি সেট। আপনি চান যে [প্রমেয়]গুলি পরস্পরের সাথে সঙ্গতিপূর্ণ হোক, প্যারাডক্সের মতো নয়। আপনি চান যে এই সংজ্ঞাগুলির মধ্যে কোনো সংঘাত না থাকে।”
এই ২৫ বছর বয়সী সিইও স্ট্যানফোর্ড বিশ্ববিদ্যালয়ের গণিতের ডক্টরেট প্রোগ্রাম থেকে প্রত্যাহার করেন এবং ২০২৫ সালের মার্চে এই কোম্পানি প্রতিষ্ঠা করেন। এই বছরের মার্চে, এক্সিওম Menlo Ventures-এর নেতৃত্বে ২ বিলিয়ন ডলারের A রাউন্ড ফান্ডিং সম্পন্ন করে।
হং বলেছেন: “আমরা তখন অনিশ্চিত ছিলাম যে vibe coding কি Stacks-এর সৌন্দর্য বজায় রাখতে পারবে।”
এই প্রকল্পটি সম্পন্ন করার জন্য, টিমটি এজেন্টগুলিকে একটি ঢিলে কাঠামো দিয়েছে এবং তাদের সমান্তরালভাবে চালানোর অনুমতি দিয়েছে। এক্সিওম টেকনোলজি টিমের সদস্য অশ্বিন স্বামিনাথন বলেছেন, “স্ট্যাকসের জন্য, আমরা একটি স্তরবদ্ধ কাঠামো তৈরি করেছি… কিন্তু সেটি এমন কোনো স্তরবদ্ধ কাঠামো নয় যা প্রতিটি এজেন্টকে কী করতে হবে তা সম্পূর্ণভাবে নির্দিষ্ট করে দেয়। এজেন্টগুলি নিজেদেরই কাজগুলি খুঁজে বের করবে এবং যেসব কাজগুলি সমান্তরালভাবে প্রক্রিয়াকরণযোগ্য, সেগুলি চিহ্নিত করবে।”
অক্সিয়াম নিজেদের মডেলগুলিকে গণিতে দক্ষ করার জন্য প্রশিক্ষণ দিয়েছে। হং বলেন, এই পদ্ধতিটি অন্যান্য বেশিরভাগ যাচাইকারী স্টার্টআপ গ্রহণ করেনি। প্রাথমিকভাবে, দলটি একজন অভ্যন্তরীণ লিয়ান বিশেষজ্ঞের উপর নির্ভর করেছিল যিনি এজেন্টগুলিকে মানুষের মতো বিচারক্ষমতা বিকাশের জন্য শেখানোর দায়িত্ব পালন করেছিলেন। সময়ের সাথে সাথে, হং বলেন, এজেন্টগুলি নিজেদেরই এই বিচারক্ষমতা শিখেছে।
এই অর্জনটি ফর্মাল গণিতের সবচেয়ে বড় ফাঁকগুলির একটিকে পূরণ করে। স্বামিনাথন বলেন: “যখন আপনি ইতিমধ্যে ফর্মালাইজড গণিতের বিষয়বস্তু দেখেন, তখন আপনি একটি বিশাল ব্ল্যাকহোল দেখতে পান। এবং সেই ব্ল্যাকহোলটি বীজগণিতীয় জ্যামিতিকে কভার করে।”
স্বামিনাথন বলেছেন, এখন পর্যন্ত লিয়ান ব্যবহার করে বীজগণিতীয় জ্যামিতির নতুন কাজ পরীক্ষা করতে চাইছিলেন এমন গবেষকদের কাছে প্রায় কোনও প্রস্তুত ভিত্তি ছিল না। "এখন তাদের আছে।"
অক্সিয়ম মনে করে, প্রতিটি যাচাইকৃত ফলাফল একটি ব্লক হয়ে ওঠে, যার উপর ভবিষ্যতের প্রমাণগুলি ইতিমধ্যে যাচাইকৃত গণিতের উপর ভিত্তি করে গড়ে উঠতে পারে, শূন্য থেকে শুরু করার প্রয়োজন ছাড়াই। UCLA-এর গণিতবিদ এবং ফিল্ডস পুরস্কার বিজয়ী টেরেন্স টাও এটিকে আরও সংক্ষেপে বলেছেন: "আপনার যতবেশি ফর্মালাইজড প্রমাণ থাকবে, আপনি ততবেশি ফর্মালাইজড প্রমাণ তৈরি করতে পারবেন।"
অক্সিয়মের লক্ষ্য শুধু গণিতবিদদের নয়। ডেভেলপাররা দীর্ঘদিন ধরে নিশ্চিত করার চেষ্টা করে আসছে যে তাদের কোডে কোনো ত্রুটি বা নিরাপত্তা ঝুঁকি নেই। যতই AI এজেন্টগুলি বেশি সফটওয়্যার লিখছে, এই সমস্যাটি আরও বড় হয়ে উঠছে।
অক্সিয়ম বেটিং, ভবিষ্যতের সফটওয়্যার এখনকার স্ট্যাকসের মতো প্রমাণিত ভিত্তির উপর গড়ে উঠবে।
স্বামিনাথন বলেন: “আমরা মনে করি, গণিত হল আপনি এই জিনিসগুলি তৈরি শুরু করার ক্ষেত্র, এবং এটি একটি স্থানান্তরযোগ্য দক্ষতা। এজেন্টগুলি আমাদের কোড পড়তে পারে, এটি বুঝতে পারে এবং এর উপরে নতুন ইনফ্রাস্ট্রাকচার তৈরি করতে পারে। আমরা লিয়ানের সাহায্যে যা ফর্মালাইজ করেছি, সেটিই এখন এজেন্টগুলির জন্য নীচের ভিত্তি।”
অক্সিয়মের এজেন্টগুলি যেভাবে স্ট্যাকস তৈরি করে—একসাথে কাজ করে এবং নিজেদের কাজ বাছাই করে—তা হোং ভবিষ্যতের অনেক AI কাজের জন্য প্রত্যাশা করেন। তিনি মনে করেন, AI এজেন্টগুলিকে অপ্রয়োজনীয় কনটেন্ট এড়ানোর জন্য একটি ভালভাবে গঠিত, পুনঃব্যবহারযোগ্য জ্ঞানভাণ্ডারের প্রয়োজন।
হং বলেন: “আপনি চান যে [এজেন্ট] একটি পুনর্ব্যবহারযোগ্য ডেটাবেস নিয়ে কাজ করুক, যাতে তারা সেখানে ভবিষ্যতের সীমানা বাড়াতে পারে। যদি শুরুতেই খারাপ ইঞ্জিনিয়ারিং বাছাইয়ের মাধ্যমে কুৎসিত জিনিস ঢুকিয়ে দেওয়া হয়, তাহলে তাদের সেই সীমানা বাড়ানো কঠিন হয়ে যাবে।”
হং এই পদ্ধতির প্রতি খুব আত্মবিশ্বাসী এবং প্রকাশ্যে চ্যালেঞ্জ জানিয়েছেন। তিনি বলেছেন: “আমি সমস্ত প্রোগ্রামিং কোম্পানিকে প্রকাশ্যে চ্যালেঞ্জ করছি, এই স্কেলে ফরমাল কাজ করতে।”