AI

[הסוכן סמית]

AI

עד עכשיו עבדתי על אינטלגנציה למשחקי לוח וכאלה בשיטות שאני פיתחתי. ועניין אותי ללמוד קצת מקצועי מספרים. מה החומר שאני צריך לדעת לפני שאני מתחיל ללמוד אינטלגנציה? והבנתי שלמשחקי לוח זה נמוכה. ויש גבוה של בני אדם אני מתלבט מה אני מעד'ף ללמוד אבל אני רוצה לעבוד על אינטלגנציה במחשב(ברגע שהמחשב שלי יוכל לחשוב אני ירגיש גאה (= )

 

[טיורינג]

אוקי,

רק אל תשכח לספר לנו כשזה קורה, שנדע... סתם, מה אתה כבר יודע? בוא נתחיל מסתם שליפות מהשרוול - השמות הבאים מוכרים לך? אלגוריתם מינמקס, אלפא-בתא, היוריסטיקה, רשתות נוירונים, לוגיקה עמומה. מה זאת אומרת "לעבוד על אינטלגנציה במחשב"? למה אתה מתכוון? מה אתה רוצה שהמחשב שלך ידע לעשות? תנסה להתמקד במשימות יותר קטנות, "לחשוב" זאת מילה קצת גדולה, בטח על המחשב. בקיצור, תמקד אותנו קצת...

 

[operandx]

You think its air you're breathing?

 

[הסוכן סמית]

הכאבתה לי פה, לא אני לא יודע

אבל מה אני אוהב ללמוד ונהנה מזה. ברעיון עד עככשיו עשיתי אינטלגנציה (אם אפשר לקרוא לזה ככה בכלל) למשחקי קופסא (שאם אין לך בכלל ידע קודם זה טיפה מאתגר!!, מנסה לשמור לעצמי קצת כבוד) אבל יותר מזה לא בידיוק יודע מה אני רוצה לעשות אבל אם אני ידע יותר דברים יהיה לי יותר רעיונות מה אני רוצה לעשות. ככה שאני אשמח לשמוע מה יש לך להמליץ (= ?

 

[טיורינג]

../images/Emo52.gif

זה היה בצחוק, אם פגעתי אני מתנצל... מה שהתכוונתי להגיד זה ש"ללמד את המחשב לחשוב" זה עניין שנוי במחלוקת (שלא לדבר על הצדדים הטכנים שכרגע בכלל לא ברורים מספיק), ומשימה קצת גדולה מידי. לדעתי חשוב להתמקד בהיבט מסויים של אינטיליגנציה ולנסות לעבוד עליו. אותי למשל מאוד מושך הנושא של עיבוד שפות טבעיות, ודרך ההתעסקות בזה הבנתי המון על כמה מורכב עניין האינטיליגנציה אצל בני אדם. מקום טוב להתחיל בו זה פה, האתר הרשמי של AAAI, תמצא שם את הנושאים המקובלים בבינה מלאכותית, וים של קישורים (טובים יותר או פחות) להעמקת הידע. תראה מה מושך אותך יותר, למה אתה מתחבר יותר, ולך על זה...

 

[הוליסטי]

ש"ללמד את המחשב לחשוב"

כתב אדם שכינויו 'טיורינג'

 

[yuvalmadar]

כעקרון, אני רוצה שהוא יעשה לי את

השיעורים. אפשר לבנות משהו כזה?

 

[טיורינג]

כשהייתי בן 10

ומחשבים עוד לא היו דבר נפוץ כל כך דמיינתי שאני ממציא מכונה שפותרת לי את שיעורי הבית... מאז לא הצלחתי לעשות זאת...

 

[gil levi]

מבחינה תאורטית, אני חושב שכן.

 

[טיורינג]

נראה לי שזה מחזיר אותנו

שוב לדיון על יצירתיות ממוחשבת. כי באופן עקרוני, ברור שתוכל ליצור מאגר מידע שיכיל את כל החומר לבגרות בתנ"ך, אבל איך תוכל ליצור מערכת שתקבל שאלה ותמצא את התשובה במאגר? זה יעבוד טוב על תשובות שאמורות להיות אינפורמטיביות מיסודן, אבל מה על שאלות בסגנון של "מדוע לדעתך צחקה שרה כששמעה את מלאכי ה'?"?

 

[gil levi]

התכוונתי רק להוכחות.

אני חושב שאפשר לבנות (מבחינה תיאורטית כמובן) מכונת טיורינג שתוכיח טענות, כל עוד הן ניתנות להוכחה (לרוץ על כל הטקסטים האפשריים שאורכם קטן ממליון שורות). אני חושב שגם אפשר לבנות מכונה (שוב, גם מבחינה תיאורטית בלבד) שתעבור את מבחן טיורינג (לבנות תמלילים של כל השיחות האפשריות שאורכן קטן ממליון שורות).

 

[טיורינג]

אבל יש בזה

יותר מיצירה של כל האפשרויות... הרי ברור שתוכנה שנבחנת במבחן טיורינג יכולה לחולל כל משפט חוקי, אבל זה צריך להיות בקונטקסט של שיחה! אותו כנ"ל עבור הוכחת משפטים, ועל זה יש ספרות עניפה. התוכנה אמורה לבנות טיעונים לוגיים שיוכיחו משפט מסויים, לא סתם לזרוק ערימות של טיעונים אפשריים ולקוות שבסוף יצא מ.ש.ל

 

[gil levi]

אני ארחיב, אבל בקצרה.

מה שאני התכוונתי הוא דבר די טיפשי. בשביל לכתוב תכנית שתעבור את מבחן טיורינג כל מה שצריך זה ליצור מסד-נתונים של כל השיחות האפשריות. כדי להוכיח משפטים אפשר לבנות מכונה שתיצור את כל הטקסטים האפשריים ולהעביר אותם למכונה אחרת שתבדוק עבור כל טקסט אם הוא הוכחה של המשפט.

 

[טיורינג]

אני לא בטוח שאתה צודק

ברור שאפשר ליצור את כל האפשרויות, אבל להעביר למכונה אחרת שתבדוק אם זאת הוכחה - זאת הבעיה, לא? ולגבי השיחה, שוב, אין בעיה לייצר את כל השיחות הקיימות (בתיאוריה) אבל לבחור את המשפט הנכון שיהווה תגובה טובה לבן אדם שמשוחח עם התוכנה - איך? זה כל העניין של המבחן הזה.

 

[gil levi]

תגובה.

בקשר להוכחה, המרצה במודלים דיבר על זה. צריך רק לכתוב אותה בשורות, כאשר כל שורה היא טענה. התכנית תבדוק עבור כל שורה אם היא כתובה קודם לכן או שניתן לגזור אותה מהשורות הקודמות על ידי כללי גזירה שנספק לתכנית (דוגמא לכלל גזירה: ( ((B גורר A) וגם B) גורר A). השורות הראשונות יהיו האקסיומות והשורה האחרונה תהיה המשפט שרוצים להוכיח. בקשר למבחן טיורינג: נניח שבן האנוש מתחיל את השיחה. צריך לכתוב את כל המשפטים שבהם הוא יכול להתחיל את השיחה (המספר הזה חסום מלמעלה על ידי כל הטקסטים שאורכם קטן מאלף). לכל דרך שלו להתחיל את השיחה צריך לחשוב על כמה תגובות של המחשב. אח"כ צריך לכתוב את כל התגובות האפשריות של בן האנוש לכל התגובות (הראשונות) של המחשב. אח"כ לכל אפשרות כזו כותבים את כל האפשרויות לענות. וכך ממשיכים. לא המכונה עושה את כל זה. זה מסד-נתונים של "שיחות" שהמתכנת אמור לכתוב. בכל שלב יש לתוכנה 20 אפשרויות לענות שמהן היא תבחר אחת באקראי. אפשר להסתכל על זה כעל עץ ענקי. השיחה היא בעצם טיול על העץ מהשורש.

 

[gil levi]

אני ארחיב קצת על ההוכחות.

אני אתן דוגמא, הוכחה ש5 הוא מספר ראשוני: מספר X מתחלק במספר Y אם X/Y הוא שלם. מספר הוא ראשוני אם הוא לא מתחלק באף מספר שקטן ממנו פרט אולי ל1. 5/2= 2.5. 5/3=1.6 5/4=1.25 2.5 לא שלם. 1.6 לא שלם. 1.25 לא שלם. 5/2 לא שלם. 5/3 לא שלם. 5/4 לא שלם. 5 לא מתחלק ב2. 5 לא מתחלק ב3. 5 לא מתחלק ב4. 5 לא מתחלק באף מספר שקטן ממנו פרט אולי ל1. 5 ראשוני. אני מניח פה שהמחשב יודע מתי מספר הוא שלם. נראה לי שזו הוכחה שמחשב יכול לבדוק (אם מספקים לו כללי גזירה).

 

[gil levi]

שיפצור קטן של הדוגמא:

אם X/Y לא שלם ==> מספר X לא מתחלק במספר Y. X לא מתחלק באף מספר שקטן ממנו פרט אולי ל1 ==> X ראשוני. 5/2= 2.5. 5/3=1.6 5/4=1.25 2.5 לא שלם. 1.6 לא שלם. 1.25 לא שלם. 5/2 לא שלם. 5/3 לא שלם. 5/4 לא שלם. 5 לא מתחלק ב2. 5 לא מתחלק ב3. 5 לא מתחלק ב4. 5 לא מתחלק באף מספר שקטן ממנו פרט אולי ל1. 5 ראשוני. עכשיו אפשר לראות ממש את הבדיקה. כשבודקים את הטענה בשורה ה12 סורקים את ההוכחה מההתחלה. רואים שיש את המחרוזות "אם X/Y לא שלם ==> מספר X לא מתחלק במספר Y" ו "5/2 לא שלם" ומשני אלו נובע, לפי כלל הגזירה שכתבתי בהודעה הקודמת, ש 5 לא מתחלק ב2.

 

[ron369]

חה!

אתה מדבר על הוכחות? אתה יודע עד כמה שקשה למחשב לעשות הוכחות כאלו בצורה פורמלית לחלוטין?

(פותח נושא דיון חדש) (וממליץ לך ללכת לשיעור "הוכחות אוטומטיות" באת"א, הוא נשמע לי די טוב

)

 

[gil levi]

שמע, אני דיברתי באופן תיאורטי

ורק מבחינה של כריעות ולא מבחינת יעילות. ברור שליצור את כל הטקסטים האפשריים זה לא ריאלי. אגב, בהינתן פסוק לוגי שניתן להוכחה (או להפרכה), להוכיח אותו זו בעיה כריעה (נדמה לי), אבל בהינתן פסוק לוגי שלא בהכרח ניתן להוכחה (או להפרכה), להוכיח אותו זו בעיה לא כריעה (נדמה לי). הרצתי חיפוש על "הוכחה אוטומטית" ומצאתי שרק השנה התחילו להעביר את הקורס. כנראה ששינו לו את השם או משהו כזה. בכל אופן, המרצה הספציפי שהיה השנה זו כבר סיבה טובה להימנע. נראה מי יהיו המרצים בשנה הבאה. בכל אופן יש לי רק שני קורסים בחירה במדמ"ח אז קשה לי להאמין שאני אקח את הקורס הזה (אני חושב שאני אקח שני קורסים בתכנות או קורס בתכנות וקורס ברשתות (או משהו פרקטי אחר) או קורס בתכנות וקורס באלגוריתמיקה). אם כבר נושא חדש לדיון, האם לדעתכם מחשב מסוגל לחקור? הסברתי מדוע הוא מסוגל להוכיח, אך האם הוא מסוגל להגדיר הגדרות ואקסיומות, להוכיח משפטים על ההגדרות והאקסיומות ואז להגדיר הגדרות חדשות וכו'? האם ניתן לבנות מחשב שנזין לתוכו את כל מה שיודע סטודנט שסיים תואר שני נניח והמחשב יוכל להמשיך ולפתח את האינפי למשל או אולי "להמציא" תורות מתמטיות חדשות?

 

[ron369]

זה שאלה די טריוויאלית

ההגדרות שלנו, לפחות ממה שראיתי, נועדו לתאר את הממשות הקיימת בצורה מתמטית. כלומר, עבור מחשב תיאור כזה יהיה, כנראה, יחסית קשה - כל עוד הוא אינו אנושי לחלוטין. אבל, לקחת את האקסיומות הקיימות, ואיתן לפתח דברים שונים - זה כבר משהו אחר. לא? מה אתה חושב?