Forwarded from دستاوردهای یادگیری عمیق(InTec)
فقط کافیه ۱ ساعت راجب
با اینکه
من خیلی ساده میگم، که اینا هم بفهمند :
۱- همهی ما میدونیم
یعنی اگر یک مدل مطالب زیادی در مورد "کامپیوتر صنعتی" دیده باشه، وقتی شما کلمه "کامپیوتر" رو بهش بدید احتمال زیادی (عددی نزدیک به ۱) میده که کلمه بعدی "صنعتی" باشه.
خب حالا با این وضعیت، چنین مدلی میتونه beep رو ایجاد کنه و بفهمه ؟
۲- این مدلها برای درک زبان در طول زمان آموزش، شروع به ساخت یک فضای برداری میکنند که هر کلمه رو به یک بردار عددی تبدیل میکنه اصطلاحاً بهش میگیم
۳- فرض کنید یک مدل اتفاقاً beep رو هم آموزش دیده، یعنی شما علاوه بر اون دیکشنری کلمات دنیا یک دیکشنری خاص هم بهتون داده شده برای تبدیل آوا و صدای beep به متن (مثل کد مورس)
شما میتونید کد مورس بزنید ولی وقتی دیکشنری رو کس دیگری نداره چطور میتونه با شما ارتباط برقرار کنه ؟
پس حتماً باید هر ۲ مدل روی صدای beep علاوه بر متنهای اینترنت آموزش دیده باشند.
پس اینکه خودشون به این زبان رسیده باشه، دروغ محض هست و از فیلمهای دهه ۸۰-۹۰ میلادی هالیوود میاد.
ولی حتی مورد آموزش دیدن روی beep هم در کار نیست و این رو فقط باید برنامهنویس باشید تا بفهمید (نیازی به سواد هوش مصنوعی هم ندارد حتی فهمیدنش)
ابتدای ویدئو هر ۲ مدل، به انگلیسی صحبت میکنند که طبیعی هست و هیچ ایرادی ندارد؛ اما بعد مدل دوم پیشنهاد استفاده از زبان مشترک و بهینه رو میده و ادعا شده این زبان ساخت خودشون هست.
۱- پس آدمی که فیلم گرفته نمیتوانسته بفهمه صحبت بین اینها چی هست.
همونطور که شما اگر فرانسه ٫ آلمانی تمرین نکرده باشی نخواهی فهمید گفتگو بین دو نفر چه معنایی داره
۲- کدهای فرانت ٫ اپلیکیشن هر ۲ مدل تا قبل از سوییچ شدن زبان هیچ متنی رو چاپ نمیکردند، چرا یک دفعه سورس کد آپدیت شد و شروع به چاپ متنها توی زبان جدید کرد ؟!
۳- اگر beep بهینهتر هست، که از نظر محاسبات یک مدل همچین چیزی رو میگه، چرا مدل باید زحمت تولید متن به انگلیسی رو هم همزمان بکشه ؟
۴- چرا مدل تبدیل متن به گفتار یکباره، علاوه بر خروجی باید ورودیش رو هم توی خروجی ارسال کنه و چرا خروجی مدل تبدیل به گفتار و متن شد به یکباره ؟
آقا٫خانم مثلاً متخصص، یکم نحوه عملکرد مدلهایی که زدی توش تخصص داری رو بخون حداقل.
من این پست رو تو صفحه کسی دیدم که توی پستهای مختلف؛ خودش رو متخصص
واقعاً چی میکشیم از دست این جماعت
LLM ها خونده باشید تا با منطق ثابت کنید این ویدئو کاملاً تقلب هست ولی خب خیلیها نفهمیدن.با اینکه
ML Researcher / Engineer هستند مثلاً.من خیلی ساده میگم، که اینا هم بفهمند :
۱- همهی ما میدونیم
LLM چیزی نیست جز یک مدل احتمالاتی که یاد میگیره بر اساس آنچه در اینترنت از متنها دیده به ترکیب کنار هم قرار گرفتن کلمات عددی بین 0-1 بده، و بر اساس این اعداد کلمه بعدی رو پیشبینی کنه.یعنی اگر یک مدل مطالب زیادی در مورد "کامپیوتر صنعتی" دیده باشه، وقتی شما کلمه "کامپیوتر" رو بهش بدید احتمال زیادی (عددی نزدیک به ۱) میده که کلمه بعدی "صنعتی" باشه.
خب حالا با این وضعیت، چنین مدلی میتونه beep رو ایجاد کنه و بفهمه ؟
۲- این مدلها برای درک زبان در طول زمان آموزش، شروع به ساخت یک فضای برداری میکنند که هر کلمه رو به یک بردار عددی تبدیل میکنه اصطلاحاً بهش میگیم
Embedding و این یعنی فرض کنید یک دیکشنری به شما داده بشه و بگم همه کلمات دنیا توی این دیکشنری هست (مدلها خلاقیت ندارند، پس این فرض رو داشته باشید) چطور شما میتونید از کلمات داخل دیکشنری محدود به beep برسید ؟! ۳- فرض کنید یک مدل اتفاقاً beep رو هم آموزش دیده، یعنی شما علاوه بر اون دیکشنری کلمات دنیا یک دیکشنری خاص هم بهتون داده شده برای تبدیل آوا و صدای beep به متن (مثل کد مورس)
شما میتونید کد مورس بزنید ولی وقتی دیکشنری رو کس دیگری نداره چطور میتونه با شما ارتباط برقرار کنه ؟
پس حتماً باید هر ۲ مدل روی صدای beep علاوه بر متنهای اینترنت آموزش دیده باشند.
پس اینکه خودشون به این زبان رسیده باشه، دروغ محض هست و از فیلمهای دهه ۸۰-۹۰ میلادی هالیوود میاد.
ولی حتی مورد آموزش دیدن روی beep هم در کار نیست و این رو فقط باید برنامهنویس باشید تا بفهمید (نیازی به سواد هوش مصنوعی هم ندارد حتی فهمیدنش)
ابتدای ویدئو هر ۲ مدل، به انگلیسی صحبت میکنند که طبیعی هست و هیچ ایرادی ندارد؛ اما بعد مدل دوم پیشنهاد استفاده از زبان مشترک و بهینه رو میده و ادعا شده این زبان ساخت خودشون هست.
۱- پس آدمی که فیلم گرفته نمیتوانسته بفهمه صحبت بین اینها چی هست.
همونطور که شما اگر فرانسه ٫ آلمانی تمرین نکرده باشی نخواهی فهمید گفتگو بین دو نفر چه معنایی داره
۲- کدهای فرانت ٫ اپلیکیشن هر ۲ مدل تا قبل از سوییچ شدن زبان هیچ متنی رو چاپ نمیکردند، چرا یک دفعه سورس کد آپدیت شد و شروع به چاپ متنها توی زبان جدید کرد ؟!
۳- اگر beep بهینهتر هست، که از نظر محاسبات یک مدل همچین چیزی رو میگه، چرا مدل باید زحمت تولید متن به انگلیسی رو هم همزمان بکشه ؟
۴- چرا مدل تبدیل متن به گفتار یکباره، علاوه بر خروجی باید ورودیش رو هم توی خروجی ارسال کنه و چرا خروجی مدل تبدیل به گفتار و متن شد به یکباره ؟
آقا٫خانم مثلاً متخصص، یکم نحوه عملکرد مدلهایی که زدی توش تخصص داری رو بخون حداقل.
من این پست رو تو صفحه کسی دیدم که توی پستهای مختلف؛ خودش رو متخصص
LLM ها و البته جزو سازنده های برترین LLM های فارسی معرفی کرده بود، از بد روزگار کلی اسکل تر از خودشم ازش بابت پست خوبش تشکر کرده بودن.واقعاً چی میکشیم از دست این جماعت
Forwarded from Geek Alerts
تاکسی Uber یه حسابکاربری ویژه نوجوونهارو داره، اینجوری که خانوادهها میتونن برای نوجوونهاشون (۱۳ تا ۱۷ سال) حساب کاربری بسازن.
بعد تمام سفرهایی که اون نوجوون میگیره رو پدر و مادر به صورت زنده روی نقشه میتونن ببینن و حتی امکان ضبط صدارو هم میده، میتونن محدودیتهای سفر بذارن و رانندگان با رتبه بالا انتخاب میشن.
این سرویس الان توی آمریکا و کانادا فعال هست و قراره که به کشور هند هم بیاد.
🔗 techcrunch
🤓 @geekalerts
بعد تمام سفرهایی که اون نوجوون میگیره رو پدر و مادر به صورت زنده روی نقشه میتونن ببینن و حتی امکان ضبط صدارو هم میده، میتونن محدودیتهای سفر بذارن و رانندگان با رتبه بالا انتخاب میشن.
این سرویس الان توی آمریکا و کانادا فعال هست و قراره که به کشور هند هم بیاد.
Please open Telegram to view this post
VIEW IN TELEGRAM
Forwarded from Geek Alerts
هفتهی پیش، موزیلا قوانین استفاده از فایرفاکس رو آپدیت کرد. بعد یه جایی از قوانین نوشته بود اطلاعاتی که داخل فایرفاکس وارد میکنید ما ازشون برای تجربه و تعامل بهتر استفاده میکنیم.
کاربرها هم اینجوری بودن که این جمله خیلی کلی هست و احتمالا فایرفاکس میخواد از اطلاعات ما برای AI یا فروششون استفاده کنه، حتی بخش زیادی از کاربرها هم فایرفاکس رو کنار گذاشتن.
موزیلا هم اومد گفت جمعآوری دیتاش هنوز محدود و مثل قدیم بر اساس اعلامیه حریم خصوصی Firefox’s Privacy Notice هست. بعد اومدن جمله رو اصلاح کردن و نوشتن موزیلا مالک محتوا و اطلاعات شما نیست و پردازش اطلاعات بر اساس اعلامیه حریمخصوصی هست.
در واقع موزیلا خیلی واضحتر الان میگه این اطلاعات رو فقط برای کار کردن خود فایرفاکس و کارایی که کاربر انجام میده استفاده میکنه.
🔗 techcrunch
🤓 @geekalerts
کاربرها هم اینجوری بودن که این جمله خیلی کلی هست و احتمالا فایرفاکس میخواد از اطلاعات ما برای AI یا فروششون استفاده کنه، حتی بخش زیادی از کاربرها هم فایرفاکس رو کنار گذاشتن.
موزیلا هم اومد گفت جمعآوری دیتاش هنوز محدود و مثل قدیم بر اساس اعلامیه حریم خصوصی Firefox’s Privacy Notice هست. بعد اومدن جمله رو اصلاح کردن و نوشتن موزیلا مالک محتوا و اطلاعات شما نیست و پردازش اطلاعات بر اساس اعلامیه حریمخصوصی هست.
در واقع موزیلا خیلی واضحتر الان میگه این اطلاعات رو فقط برای کار کردن خود فایرفاکس و کارایی که کاربر انجام میده استفاده میکنه.
Please open Telegram to view this post
VIEW IN TELEGRAM
Forwarded from DevTwitter | توییت برنامه نویسی
This media is not supported in your browser
VIEW IN TELEGRAM
اینو دیدم برام جالب بود گفتم شما هم ببینید...
پرامپتی که نوشته بودن:
"یک برنامهی پایتون بنویسید که یک توپ را نشان دهد که درون یک ششضلعی در حال چرخش میجهد. توپ باید تحت تأثیر گرانش و اصطکاک باشد و هنگام برخورد با دیوارهای در حال چرخش بهطور واقعگرایانهای بازتاب کند."
@DevTwitter | <Sam92/>
پرامپتی که نوشته بودن:
"یک برنامهی پایتون بنویسید که یک توپ را نشان دهد که درون یک ششضلعی در حال چرخش میجهد. توپ باید تحت تأثیر گرانش و اصطکاک باشد و هنگام برخورد با دیوارهای در حال چرخش بهطور واقعگرایانهای بازتاب کند."
@DevTwitter | <Sam92/>
Forwarded from Geek Alerts
جیمز هریسون استرالیایی در سن ۸۸ سالگی درگذشت
ایشون یه آنتیبادی نادر به اسم anti-D توی پلاسمای خونش داشت که با اهدای خون از یه عارضه خطرناک توی بارداری جلوگیری میکرد.
ماجرای anti-D اینه که گلبولهای قرمز خون ما میتونن یه پروتئین خاص روی سطحشون داشته باشن به اسم رزوس (RhD). اگه این پروتئین رو داشته باشیم، میگیم گروه خونیمون Rh مثبت (+RhD) هست، اگه نداشته باشیم میگیم Rh منفی (-RhD).
وقتی یه خانم باردار که Rh منفی داره، بدنش به خون Rh مثبت حساس بشه (معمولاً توی بارداری قبلی این اتفاق میفته)، بدنش ممکنه آنتیبادیهایی بسازه که به جنین Rh مثبت خودش حمله کنن. به این بیماری میگن «بیماری رزوس» (Rhesus disease).
اما اگه به مادرانی که در معرض خطر بیماری رزوس هستن، یه دوز anti-D تزریق بشه، میشه از همون اول جلوی این بیماری رو گرفت.
وقتی جیمز هریسون متوجه این موضوع میشه از سن ۱۸ سالگی شروع میکنه به اهدای خون و بیش از ۶۰ سال هر ۳ هفته یک بار خون اهدا کرد. تخمین زدن جون بیش از دو میلیون بچه رو توی استرالیا نجات داده.
🔗 gizmodo
🤓 @geekalerts
ایشون یه آنتیبادی نادر به اسم anti-D توی پلاسمای خونش داشت که با اهدای خون از یه عارضه خطرناک توی بارداری جلوگیری میکرد.
ماجرای anti-D اینه که گلبولهای قرمز خون ما میتونن یه پروتئین خاص روی سطحشون داشته باشن به اسم رزوس (RhD). اگه این پروتئین رو داشته باشیم، میگیم گروه خونیمون Rh مثبت (+RhD) هست، اگه نداشته باشیم میگیم Rh منفی (-RhD).
وقتی یه خانم باردار که Rh منفی داره، بدنش به خون Rh مثبت حساس بشه (معمولاً توی بارداری قبلی این اتفاق میفته)، بدنش ممکنه آنتیبادیهایی بسازه که به جنین Rh مثبت خودش حمله کنن. به این بیماری میگن «بیماری رزوس» (Rhesus disease).
اما اگه به مادرانی که در معرض خطر بیماری رزوس هستن، یه دوز anti-D تزریق بشه، میشه از همون اول جلوی این بیماری رو گرفت.
وقتی جیمز هریسون متوجه این موضوع میشه از سن ۱۸ سالگی شروع میکنه به اهدای خون و بیش از ۶۰ سال هر ۳ هفته یک بار خون اهدا کرد. تخمین زدن جون بیش از دو میلیون بچه رو توی استرالیا نجات داده.
Please open Telegram to view this post
VIEW IN TELEGRAM
Forwarded from Geek Alerts
نسخه اندروید Grok هم به صورت بتا منتشر شد.
با عضو شدن به لیست تسترها میتونید این برنامه رو روی گوشی اندرویدیتون دانلود و استفاده کنید. فعلا فقط قابلیت سرچ اون دردسترس هست در برنامه.
🔗 join | playstore
🤓 hadi @geekalerts
با عضو شدن به لیست تسترها میتونید این برنامه رو روی گوشی اندرویدیتون دانلود و استفاده کنید. فعلا فقط قابلیت سرچ اون دردسترس هست در برنامه.
Please open Telegram to view this post
VIEW IN TELEGRAM
Forwarded from Geek Alerts
نسخه اندروید Grok هم به صورت بتا منتشر شد.
با عضو شدن به لیست تسترها میتونید این برنامه رو روی گوشی اندرویدیتون دانلود و استفاده کنید. فعلا فقط قابلیت سرچ اون دردسترس هست در برنامه.
🔗
با عضو شدن به لیست تسترها میتونید این برنامه رو روی گوشی اندرویدیتون دانلود و استفاده کنید. فعلا فقط قابلیت سرچ اون دردسترس هست در برنامه.
🔗
Forwarded from Geek Alerts
نسخه اندروید Grok هم به صورت بتا منتشر شد.
با عضو شدن به لیست تسترها میتونید این برنامه رو روی گوشی اندرویدیتون دانلود و استفاده کنید. فعلا فقط قابلیت سرچ اون دردسترس هست در برنامه.
🔗 join | playstore
🤓 hadi @geekalerts
با عضو شدن به لیست تسترها میتونید این برنامه رو روی گوشی اندرویدیتون دانلود و استفاده کنید. فعلا فقط قابلیت سرچ اون دردسترس هست در برنامه.
Please open Telegram to view this post
VIEW IN TELEGRAM
Forwarded from Geek Alerts
نسخه اندروید Grok هم به صورت بتا منتشر شد.
با عضو شدن به لیست تسترها میتونید این برنامه رو روی گوشی اندرویدیتون دانلود و استفاده کنید و البته فعلاً دو قابلیت Deep Research و Reasoning در دسترس نیست اما به اینترنت و وب دسترسی لحظهای داره.
🔗 join | playstore
🤓 hadi @geekalerts
با عضو شدن به لیست تسترها میتونید این برنامه رو روی گوشی اندرویدیتون دانلود و استفاده کنید و البته فعلاً دو قابلیت Deep Research و Reasoning در دسترس نیست اما به اینترنت و وب دسترسی لحظهای داره.
Please open Telegram to view this post
VIEW IN TELEGRAM
Forwarded from Ninja Learn | نینجا لرن
فقط برنامه نویسا درکش میکنن :)
https://youtu.be/EFmxPMdBqmU?si=dkT-Ry9K_-5m8DxY
➖➖➖➖➖➖➖➖➖
https://youtu.be/EFmxPMdBqmU?si=dkT-Ry9K_-5m8DxY
#️⃣ #video
➖➖➖➖➖➖➖➖➖
🥷 CHANNEL | GROUP
Forwarded from Linuxor ?
مایکروسافت یه دوره ی رایگان گذاشته برای یادگیری AI Agentها...
تمرکزش روی استفاده از تکنولوژی های مایکروسافته، مثال های متعددی داره و فریم ورکهای مختلفی رو برای ساخت ایجنت معرفی کردن...
https://github.com/microsoft/ai-agents-for-beginners
@Linuxor ~ Saeedam92
تمرکزش روی استفاده از تکنولوژی های مایکروسافته، مثال های متعددی داره و فریم ورکهای مختلفی رو برای ساخت ایجنت معرفی کردن...
https://github.com/microsoft/ai-agents-for-beginners
@Linuxor ~ Saeedam92
Forwarded from DevTwitter | توییت برنامه نویسی
انتشار نسخه 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/>
که امکانات جذابی برای بهبود تجربه توسعهدهندگان به همراه دارد. در اینجا به خلاصهای از ویژگیهای جدید می پردازیم:
رابط کاربری جدید برای خطاها و بهبود استکترِیسها: یک رابط کاربری بهتر و طراحیشده برای نمایش خطاها که با دقت بیشتر به شما کمک میکند تا سریعتر مشکلات را شناسایی و رفع کنید.
استفاده از 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/>
Forwarded from 🎄 یک برنامه نویس تنبل (The Lazy 🌱 Raymond)
🔶 استفاده دانشجویان از هوش مصنوعی، ناقوس مرگ برای تفکر انتقادی است.
به گزارش گاردین، دانشگاههای انگلستان اخیرا هشدار دادند که ۹۲ درصد دانشجویان از هوش مصنوعی استفاده میکنند و این برای دانشگاهها که قرنها خود را مخزن دانش و حقیقت میدانستند، ناگوار است. فروپاشی زمانی آغاز شد که دیگر کسی برای کارشناسان ارزش قائل نشد، تفکر انتقادی تضعیف شد و گفتمان عمومی به حالت دوقطبی درآمد.
منابع سنتی دانش به طور فزایندهای در حال رد شدن هستند. کتابها، مقالات، مجلات و رسانههای قدیمی با پیشرفتهای صورتگرفته در ارائه و بازیابی اطلاعات، به ویژه از طریق اپلیکیشنها و رسانههای اجتماعی به چالش کشیده میشوند. این امر منجر به "Tinderfication" دانش شده است.
به عنوان مثال، فهرستهای مطالعه تنظیمشده برای استفاده دانشگاهیان در پژوهش اغلب توسط دانشجویان نادیده گرفته میشوند و جستوجو در «گوگل» جای آنها را میگیرد. اگر دانشجو از آنچه میخواند خوشش نیاید، میتواند به سادگی به گوگل روی بیاورد. الگوریتمها میتوانند دانشجویان را به جهتهای غیرمنتظره بفرستند و اغلب آنها را از سختگیری تحصیلی به سمت منابع غیر دانشگاهی منحرف میکنند.
#خبر
@TheRaymondDev
به گزارش گاردین، دانشگاههای انگلستان اخیرا هشدار دادند که ۹۲ درصد دانشجویان از هوش مصنوعی استفاده میکنند و این برای دانشگاهها که قرنها خود را مخزن دانش و حقیقت میدانستند، ناگوار است. فروپاشی زمانی آغاز شد که دیگر کسی برای کارشناسان ارزش قائل نشد، تفکر انتقادی تضعیف شد و گفتمان عمومی به حالت دوقطبی درآمد.
منابع سنتی دانش به طور فزایندهای در حال رد شدن هستند. کتابها، مقالات، مجلات و رسانههای قدیمی با پیشرفتهای صورتگرفته در ارائه و بازیابی اطلاعات، به ویژه از طریق اپلیکیشنها و رسانههای اجتماعی به چالش کشیده میشوند. این امر منجر به "Tinderfication" دانش شده است.
به عنوان مثال، فهرستهای مطالعه تنظیمشده برای استفاده دانشگاهیان در پژوهش اغلب توسط دانشجویان نادیده گرفته میشوند و جستوجو در «گوگل» جای آنها را میگیرد. اگر دانشجو از آنچه میخواند خوشش نیاید، میتواند به سادگی به گوگل روی بیاورد. الگوریتمها میتوانند دانشجویان را به جهتهای غیرمنتظره بفرستند و اغلب آنها را از سختگیری تحصیلی به سمت منابع غیر دانشگاهی منحرف میکنند.
#خبر
@TheRaymondDev
the Guardian
Students’ use of AI spells death knell for critical thinking | Letters
Letters: Prof Andrew Moran and Dr Ben Wilkinson on the ramifications of the explosion in university essays being written with artificial intelligence
Forwarded from انجمن علمی ژرفا
نونگاه اول؛
🔰 «سودای منطق»
درآمدی بر دستیارهای اثبات
همراه با ارائه نسخه ایرانی
توسط توسعهدهندگان:
حمیدرضا کلباسی؛
دانشجوی رشته هوش مصنوعی دانشگاه شریف
ارشیا معینی؛
دانشجوی رشته ریاضی دانشگاه شریف
📆 سهشنبه ۱۴ اسفند ۱۴۰۳ | ساعت ۱۳:۳۰
📍 دانشگاه صنعتی شریف، کلاس ۱ معاونت فرهنگی
🌐 پخش مجازی در اتاق مجازی ژرفا
🔸 چنانچه دانشجوی دانشگاه شریف نیستید اما مایل به حضور در برنامه هستید، لطفاً تا ساعت ۹ روز سهشنبه ۱۴ اسفند این فرم را تکمیل فرمایید.
🔻 توضیحات بیشتر
🆔 @Zharfa90
🔰 «سودای منطق»
درآمدی بر دستیارهای اثبات
همراه با ارائه نسخه ایرانی
توسط توسعهدهندگان:
حمیدرضا کلباسی؛
دانشجوی رشته هوش مصنوعی دانشگاه شریف
ارشیا معینی؛
دانشجوی رشته ریاضی دانشگاه شریف
📆 سهشنبه ۱۴ اسفند ۱۴۰۳ | ساعت ۱۳:۳۰
📍 دانشگاه صنعتی شریف، کلاس ۱ معاونت فرهنگی
🌐 پخش مجازی در اتاق مجازی ژرفا
🔸 چنانچه دانشجوی دانشگاه شریف نیستید اما مایل به حضور در برنامه هستید، لطفاً تا ساعت ۹ روز سهشنبه ۱۴ اسفند این فرم را تکمیل فرمایید.
🔻 توضیحات بیشتر
🆔 @Zharfa90
Forwarded from a pessimistic researcher (Kc)
من خیلی این دوستان رو نمیشناسم منتهی با یک سرچی که کردم فکر کنم دارن روی این پروژه کار میکنن. اول از همه باید بگم که خیلی دمشون گرم. توسعهی 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 جاوا نمیتونه انجام بده. اینجا یک گپی وجود داره که باید یکی پرش کنه. شاید اون یک نفر تو باشی.
قبل از اینکه ادامه بدیم، اگر با مفهوم 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 جاوا نمیتونه انجام بده. اینجا یک گپی وجود داره که باید یکی پرش کنه. شاید اون یک نفر تو باشی.
GitHub
GitHub - babaeee/hakim: A hacky interactive theorem prover
A hacky interactive theorem prover. Contribute to babaeee/hakim development by creating an account on GitHub.
Forwarded from a pessimistic researcher (Kc)
Simply Typed Existence
والا تو کل دنیا دوتا اثباتیار معروف (نه دست!یار! اثبات، ای نادانهای خوشخیال) - coq و lean - داریم که با بودجه کلان و تیمهای بزرگ از مهندسین محقق (نه هر مهندسی! از هوش مصنوعی بپره تو علوم کامپیوتر نظری و برعکس) و ریاضیدانها و دانشمندان علوم کامپیوتر…
البته که رئیس زبان تندی داره و یکمی باید چیل داون کنه :))) ولی نکات مهمی رو لابهلای دق و دلی هاش اشاره کرد
Forwarded from a pessimistic researcher (Kc)
آقا من این رو هم بگم،
قبول دارم که بعضی وقتا ادایی میشم و مثلا توی متنام به جای سخنرانی میگم talk یا مثلا به جای رویداد میگم event، ولی بیاید و در پویش حفظ و نشر لغات فنی و آکادمیک کوشا باشم. همونطور که غرب وقتی با جبر و خوارزمی آشنا شد، ترجمهاش نکرد، بیاید ما هم چیزایی که غرب ابداع کرده و توسعه داده رو دست نزنیم.
قبول دارم که بعضی وقتا ادایی میشم و مثلا توی متنام به جای سخنرانی میگم talk یا مثلا به جای رویداد میگم event، ولی بیاید و در پویش حفظ و نشر لغات فنی و آکادمیک کوشا باشم. همونطور که غرب وقتی با جبر و خوارزمی آشنا شد، ترجمهاش نکرد، بیاید ما هم چیزایی که غرب ابداع کرده و توسعه داده رو دست نزنیم.