این ویدئو رو دیدید ؟
قطعاً، دیدید.
با این داستان پخش شده که ای وای دوتا AI تصمیم گرفتند یک زبان جدید و بهینه برای خودشون استفاده کنند.

اولین باری که دیدم خندیدم و گفتم، چه فکر مریضی (اونی که درست کرده)

بعد دیدم کلی آدم خیلی جدی دارند ازش تعریف می‌کنند، بخصوص مثلاً متخصص‌های هوش مصنوعی.
خیلی ازین آدما، سنیور هستند مثلاً ولی اگر این سوال مصاحبه بود من درجا طرف رو حذف می‌کردم چون قطعاً چیزی از AI نفهمیده.


اخطار:
اگر پستی در مورد این ویدیو گذاشتید سریعاً پاک کنید، آبروتون نره.

حالا استدلال این داستان چیه ؟
پست بعدی رو بخونید.

فقط کافیه ۱ ساعت راجب LLM ها خونده باشید تا با منطق ثابت کنید این ویدئو کاملاً تقلب هست ولی خب خیلی‌ها نفهمیدن.
با اینکه ML Researcher / Engineer هستند مثلاً.
من خیلی ساده میگم، که اینا هم بفهمند :

۱- همه‌ی ما می‌دونیم LLM چیزی نیست جز یک مدل احتمالاتی که یاد میگیره بر اساس آنچه در اینترنت از متن‌ها دیده به ترکیب کنار هم قرار گرفتن کلمات عددی بین 0-1 بده، و بر اساس این اعداد کلمه بعدی رو پیش‌بینی کنه.

یعنی اگر یک مدل مطالب زیادی در مور‌د "کامپیوتر صنعتی" دیده باشه، وقتی شما کلمه "کامپیوتر" رو بهش بدید احتمال زیادی (عددی نزدیک به ۱) می‌ده که کلمه بعدی "صنعتی" باشه.

خب حالا با این وضعیت، چنین مدلی می‌تونه beep رو ایجاد کنه و بفهمه ؟

۲- این مدل‌ها برای درک زبان در طول زمان آموزش، شروع به ساخت یک فضای برداری می‌کنند که هر کلمه رو به یک بردار عددی تبدیل می‌کنه اصطلاحاً بهش می‌گیم Embedding و این یعنی فرض کنید یک دیکشنری به شما داده بشه و بگم همه کلمات دنیا توی این دیکشنری هست (مدل‌ها خلاقیت ندارند، پس این فرض رو داشته باشید) چطور شما می‌تونید از کلمات داخل دیکشنری محدود به beep برسید ؟!

۳- فرض کنید یک مدل اتفاقاً beep رو هم آموزش دیده، یعنی شما علاوه بر اون دیکشنری کلمات دنیا یک دیکشنری خاص هم بهتون داده شده برای تبدیل آوا و صدای beep به متن (مثل کد مورس)
شما می‌تونید کد مورس بزنید ولی وقتی دیکشنری رو کس دیگری نداره چطور می‌تونه با شما ارتباط برقرار کنه ؟

پس حتماً باید هر ۲ مدل روی صدای beep علاوه بر متن‌های اینترنت آموزش دیده باشند.
پس اینکه خودشون به این زبان رسیده باشه، دروغ محض هست و از فیلم‌های دهه ۸۰-۹۰ میلادی هالیوود میاد.

ولی حتی مورد آموزش دیدن روی beep هم در کار نیست و این رو فقط باید برنامه‌نویس باشید تا بفهمید (نیازی به سواد هوش مصنوعی هم ندارد حتی فهمیدنش)

ابتدای ویدئو هر ۲ مدل، به انگلیسی صحبت می‌کنند که طبیعی هست و هیچ ایرادی ندارد؛ اما بعد مدل دوم پیشنهاد استفاده از زبان مشترک و بهینه رو میده و ادعا شده این زبان ساخت خودشون هست.

۱- پس آدمی که فیلم گرفته نمی‌توانسته بفهمه صحبت بین اینها چی هست.
همون‌طور که شما اگر فرانسه ٫ آلمانی تمرین نکرده باشی نخواهی فهمید گفتگو بین دو نفر چه معنایی داره

۲- کدهای فرانت ٫ اپلیکیشن هر ۲ مدل تا قبل از سوییچ شدن زبان هیچ متنی رو چاپ نمی‌کردند، چرا یک دفعه سورس کد آپدیت شد و شروع به چاپ متن‌ها توی زبان جدید کرد ؟!

۳- اگر beep بهینه‌تر هست، که از نظر محاسبات یک مدل همچین چیزی رو می‌گه، چرا مدل باید زحمت تولید متن به انگلیسی رو هم همزمان بکشه ؟

۴- چرا مدل تبدیل متن به گفتار یکباره، علاوه بر خروجی باید ورودیش رو هم توی خروجی ارسال کنه و چرا خروجی‌ مدل تبدیل به گفتار و متن شد به یکباره ؟

آقا٫خانم مثلاً متخصص، یکم نحوه عملکرد مدل‌هایی که زدی توش تخصص داری رو بخون حداقل.
من این پست رو تو صفحه کسی دیدم که توی پست‌های مختلف؛ خودش رو متخصص LLM ها و البته جزو سازنده های برترین LLM های فارسی معرفی کرده بود، از بد روزگار کلی اسکل تر از خودشم ازش بابت پست خوبش تشکر کرده بودن.

واقعاً چی می‌کشیم از دست این جماعت

اینو دیدم برام جالب بود گفتم شما هم ببینید...

پرامپتی که نوشته بودن:
"یک برنامه‌ی پایتون بنویسید که یک توپ را نشان دهد که درون یک شش‌ضلعی در حال چرخش می‌جهد. توپ باید تحت تأثیر گرانش و اصطکاک باشد و هنگام برخورد با دیوارهای در حال چرخش به‌طور واقع‌گرایانه‌ای بازتاب کند."

@DevTwitter | <Sam92/>

نسخه اندروید Grok هم به صورت بتا منتشر شد.
با عضو شدن به لیست تسترها می‌تونید این برنامه رو روی گوشی اندرویدی‌تون دانلود و استفاده کنید. فعلا فقط قابلیت سرچ اون دردسترس هست در برنامه.

🔗

فقط برنامه نویسا درکش میکنن :)

https://youtu.be/EFmxPMdBqmU?si=dkT-Ry9K_-5m8DxY

#️⃣ #video

➖➖➖➖➖➖➖➖➖

🥷 CHANNEL | GROUP

اکثر سطح هایی که گفته شده مثلا E6 و L6 و ICT5 نیاز به سابقه حدودا 8 تا 15 ساله داره معمولا افرادی که توی این سطح ها هستن 30 تا 40 ساله هستن که تجربه مدیریتی بالایی دارن و تیم های فنی رو هدایت می‌کنن، یعنی علاوه بر دانش فنی عمیق می‌تونن پروژه های پیچیده هم هدایت کنن.


@Linuxor

مایکروسافت یه دوره ی رایگان گذاشته برای یادگیری AI Agentها...
تمرکزش روی استفاده از تکنولوژی های مایکروسافته، مثال های متعددی داره و فریم ورکهای مختلفی رو برای ساخت ایجنت معرفی کردن...

https://github.com/microsoft/ai-agents-for-beginners


@Linuxor ~ Saeedam92

انتشار نسخه 15.2 از Next.js

که امکانات جذابی برای بهبود تجربه توسعه‌دهندگان به همراه دارد. در اینجا به خلاصه‌ای از ویژگی‌های جدید می پردازیم:

رابط کاربری جدید برای خطاها و بهبود استک‌ترِیس‌ها: یک رابط کاربری بهتر و طراحی‌شده برای نمایش خطاها که با دقت بیشتر به شما کمک می‌کند تا سریع‌تر مشکلات را شناسایی و رفع کنید.

استفاده از Streaming Metadata: حالا متادیتاهای async مانع از رندرینگ صفحات نمی‌شوند و بهبود زمان بارگذاری صفحات را به همراه دارد.

بهبود عملکرد Turbopack: زمان کامپایل تا 57.6% سریع‌تر و کاهش 30 درصدی مصرف حافظه در توسعه محلی.

تغییرات ویوها با استفاده از API جدید React View Transitions (آزمایشی): امکان انیمیت کردن بین ویوها و کامپوننت‌های مختلف در برنامه شما.

پشتیبانی آزمایشی از Node.js در Middleware(آزمایشی): قابلیت استفاده از Node.js در Middleware قبلا از این نمی شد از ویژگی های node مثلا package هاش در داخل middleware استفاده کرد .

https://nextjs.org/blog/next-15-2

@DevTwitter | <Alireza soltanian/>

🔶 استفاده دانشجویان از هوش مصنوعی، ناقوس مرگ برای تفکر انتقادی است.

به گزارش گاردین، دانشگاه‌های انگلستان اخیرا هشدار دادند که ۹۲ درصد دانشجویان از هوش مصنوعی استفاده می‌کنند و این برای دانشگاه‌ها که قرن‌ها خود را مخزن دانش و حقیقت می‌دانستند، ناگوار است. فروپاشی زمانی آغاز شد که دیگر کسی برای کارشناسان ارزش قائل نشد، تفکر انتقادی تضعیف شد و گفتمان عمومی به حالت دوقطبی درآمد.

منابع سنتی دانش به طور فزاینده‌ای در حال رد شدن هستند. کتاب‌ها، مقالات، مجلات و رسانه‌های قدیمی با پیشرفت‌های صورت‌گرفته در ارائه و بازیابی اطلاعات، به ویژه از طریق اپلیکیشن‌ها و رسانه‌های اجتماعی به چالش کشیده می‌شوند. این امر منجر به "Tinderfication" دانش شده است.

به عنوان مثال، فهرست‌های مطالعه تنظیم‌شده برای استفاده دانشگاهیان در پژوهش اغلب توسط دانشجویان نادیده گرفته می‌شوند و جست‌وجو در «گوگل» جای آنها را می‌گیرد. اگر دانشجو از آنچه می‌خواند خوشش نیاید، می‌تواند به سادگی به گوگل روی بیاورد. الگوریتم‌ها می‌توانند دانشجویان را به جهت‌های غیرمنتظره بفرستند و اغلب آنها را از سختگیری تحصیلی به سمت منابع غیر دانشگاهی منحرف می‌کنند.

#خبر

@TheRaymondDev

نونگاه اول؛
🔰 «سودای منطق»
درآمدی بر دست‌یارهای اثبات

همراه با ارائه نسخه ایرانی
توسط توسعه‌دهندگان:
حمیدرضا کلباسی؛
دانشجوی رشته هوش مصنوعی دانشگاه شریف
ارشیا معینی؛
دانشجوی رشته ریاضی دانشگاه شریف

📆 سه‌شنبه ۱۴ اسفند ۱۴۰۳ | ساعت ۱۳:۳۰
📍 دانشگاه صنعتی شریف، کلاس ۱ معاونت فرهنگی
🌐 پخش مجازی در اتاق مجازی ژرفا

🔸 چنانچه دانشجوی دانشگاه شریف نیستید اما مایل به حضور در برنامه هستید، لطفاً تا ساعت ۹ روز سه‌شنبه ۱۴ اسفند این فرم را تکمیل فرمایید.

🔻 توضیحات بیشتر

🆔 @Zharfa90

من خیلی این دوستان رو نمی‌شناسم منتهی با یک سرچی که کردم فکر کنم دارن روی این پروژه کار میکنن. اول از همه باید بگم که خیلی دمشون گرم. توسعه‌ی theorem prover کار بسیار سختیه. منتهی به نظرم سخت تر از اون رقابت کردنه. البته شاید کلمه‌ی رقابت خیلی درست نباشه ولی خب هست.
قبل از اینکه ادامه بدیم، اگر با مفهوم Theorem prover آشنا نیستید و نمی‌دونید که چه نقش مهمی می‌تونن توی علم software بازی کنند توصیه می‌کنم این پست‌های کانال رو بخونید :

"Most Successful Program Based on a Wrong Idea - بخش اول"
"Most Successful Program Based on a Wrong Idea - بخش دوم"
"برنامه‌نویسی با طعم شیرین اثبات"
"You Want Poof? I'll give you proof!"
"باگ نه تنها در سافتور، بلکه در ریاضیات"
"اِوِرِست"
"معرفی منابع برای یادگیری Program به همراه Proof"

و اما بعد،‌ من تا جایی که متوجه شدم اسم پروژه‌ی این دوستان بَبَعی هستش(البته شایدم حکیم). این نام‌گذاری احتمالا بخاطر coq، تئورم پرور معروفه. خب coq یا همون خروس نماد کشور فرانسه‌است. جایی که این تئورم پرور ساخته شده. منتهی ببعی بعید می‌دونم نماد ما باشه. کاش اسم بهتری انتخاب بشه. مهم تر از اسم، رقابته. ببینید وقتی صحبت از Theorem prover می‌کنیم، باید حواسمون باشه که در مقابل ما یک کوهی از Theorem prover ها وجود دارند مثل coq و Agda و Isabelle/HOL و Lean و ACL2 که هر کدومشون یک غول بلا رقیبن. مثلا coq سی و پنج ساله که داره دولوپ میشه. یا Agda بیست و شش ساله که داره دولوپ میشه و پشت هر کدوم از این‌ها یک community چند صد نفره وجود داره. خب اگر ما قراره یک Theorem prover دیگه بسازیم، نقطه‌ی اتکا مون رو اگر فقط بذاریم روی بومی بودنش، سرنوشتش به لینوکس بومی، اندروید بومی، و کلی چیز بومی که دیگه اثری ازشون نیست می‌پیونده. ببعی یا هر حیوون دیگه‌ای :)) باید چیزی داشته باشه که کامیونیتی رو مجاب به استفاده ازش کنه. اینکه حقیقتا چه نقطه‌ی برتری‌ای نسبت به دیگر prover ها داره برای من روشن نیست و امیدوارم که توی ارائه‌شون این قضیه رو روشن کنن. یا حتی توی readme و wiki پروژه‌شون بهش اشاره کنن.

اما یک توصیه برای اونایی که کله‌شون باد داره و میخوان دست‌شون رو به نوشتن یک Theorem Prover آلوده کنند. تمرکزتون رو بذارید روی توسعه‌ی یک prover خاص منظوره. به‌طور خاص هدف رو روی program verification بذارید. و به طور خاص برنامه‌های concurrent و distributed. الان F* و Iris و KeY رو در نظر بگیرید که مسیری شبیه رو طی می‌کنند. مثلا KeY برای وریفیکیشن برنامه‌های جاوایی که spec شون با JML نوشته شده توسعه یافته. یعنی ورودیش یک برنامه‌ی جاوا با annotation های JML هستش و اینو ترنسلیت می‌کنه به dynamic logic. زیر بناش هم یک first order theorem prover مبتنی بر sequent calculus داره. منتهی با همه‌ی این حرفا، کار خاصی روی برنامه‌های multi-thread جاوا نمی‌تونه انجام بده. اینجا یک گپی وجود داره که باید یکی پرش کنه. شاید اون یک نفر تو باشی.