מערכת הוכחה אינטראקטיבית

מתוך ויקיפדיה, האנציקלופדיה החופשית

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

כל מערכות ההוכחה האינטראקטיביות נדרשות לקיים שתי תכונות בסיסיות:

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

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

תוכן עניינים

[עריכה] סוגים של מערכות הוכחה אינטראקטיביות

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

[עריכה] NP כמערכת הוכחה

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

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

[עריכה] המחלקה IP

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

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

המחלקה IP (ראשי תיבות של Interactive Proof - הוכחה אינטראקטיבית) היא אוסף השפות שניתן לקבל כאשר מתירים בפרוטוקול ההוכחה לשני הצדדים לשלוח זה לזה הודעות מספר פעמים שהוא פולינומי באורך הקלט. מתברר כי כוחה של מערכת ההוכחה הזו גדול יחסית: עדי שמיר הוכיח בשנת 1992 כי IP זהה למחלקה PSPACE - אוסף השפות שניתן להכריע באמצעות שימוש בזיכרון פולינומי, מחלקה גדולה יחסית. תוצאה זו קושרת בין מערכת הוכחה אינטראקטיבית הסתברותית ובין מחלקת סיבוכיות דטרמיניסטית "קלאסית".

[עריכה] דוגמה לשפה ב-IP

בעיית איזומורפיזם הגרפים היא זו: בהינתן שני גרפים בעלי אותו מספר צמתים, הם איזומורפיים אם הם זהים עד כדי שינוי שמות הצמתים. בצורה פורמלית, הם איזומורפיים אם קיימת פונקציה חד-חד ערכית ועל שמשמרת את יחסי הקשתות של הגרפים: \ \left(v,u\right) היא קשת בגרף הראשון אם ורק אם \ \left(\sigma (v),\sigma (u)\right) היא קשת בגרף השני (כאשר \ \sigma היא הפונקציה).

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

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

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

לעומת זאת, אם שני הגרפים איזומורפיים ואם המוודא בחר בהתפלגות אחידה את התמורה שלו על הצמתים, אין למוכיח שום דרך לדעת מה הגרף שבחר המוודא, והוא יכול רק לנחש, כשהוא צודק בהסתברות 1/2. על כן, קיימת למוודא הסתברות 1/2 לטעות ולקבל זוג גרפים איזומורפיים. עם זאת, על ידי חזרה על הפרוטוקול פעם נוספת ההסתברות יורדת ל-1/4 (ההסתברות שבשני סיבובים רצופים יתמזל מזלו של המוכיח והוא ינחש נכון מה בחר המוודא), אחרי שלושה סיבובים היא יורדת ל-1/8 וכן הלאה.

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

[עריכה] המחלקה MIP

ישנן שתי דרכים בסיסיות להרחיב את IP. האחת, על ידי הוספת כוח חישוב למוודא. דרך זו בעייתית מכיוון שעיקר העניין במערכות הוכחה אינטראקטיביות הוא בכך שלמוודא כוח "סביר". הדרך השנייה להרחיב את IP היא על ידי הוספת מוכיחים נוספים, שאינם מסוגלים לתקשר ביניהם ואינם מודעים לתקשורת של המוודא עם מוכיחים אחרים מלבדם. התוצאה של הרחבה זו היא המחלקה MIP (ראשי תיבות של Multi-Prover Interactive Proof - הוכחה אינטראקטיבית מרובת מוכיחים).

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

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

[עריכה] פרוטוקול ארתור-מרלין

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

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

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

[עריכה] PCP

מערכת הוכחה מסוג PCP (ראשי תיבות של "Probabilistically checkable proof") דומה למערכת MA, בה המוודא מקבל מהמוכיח הוכחה ובודק אותה באופן הסתברותי, אך בנוסף מושתתת מגבלה נוספת על המוודא: הוא אינו מסוגל בהכרח לגשת לכל ההוכחה, אלא רק לחלקים ממנה. המחלקה \ PCP(f(n),g(n)) היא מחלקת כל השפות שניתן לקבל במערכת הוכחה שכזו בה המוודא משתמש לכל היותר ב-\ f(n) הטלות מטבע אקראיות, וקורא לכל היותר \ g(n) ביטים מההוכחה.

שתי דוגמאות טריוויאליות למחלקות PCP הן:

  • המחלקה \ PCP(0,poly) שבה המוודא יכול לקרוא כמות פולינומית של ביטים מההוכחה אך אינו יכול להשתמש כלל באקראיות. מחלקה זו שווה למחלקה NP, שבה מוודא דטרמיניסטי הפועל בזמן ריצה פולינומי בודק הוכחה.
  • המחלקה \ PCP(poly,0) שבה המוודא יכול להטיל מטבע מספר פולינומי של פעמים אך אינו קורא כלל את ההוכחה. מחלקה זו שווה למחלקה co-RP, מכיוון שככל מערכת הוכחה אינטראקטיבית, גם כאן נדרשת ממנה שלמות מלאה ונאותות גבוהה.

החשיבות של מערכות PCP היא בכך שהן מראות כי כוח רב יחסית נשמר גם כאשר המוודא אינו קורא את כל ההוכחה. התוצאה המרכזית הראשונה שהושגה בתחום הראתה כי \ PCP(\log(n),\log(n))=NP - כלומר, די בכמות לוגריתמית של הטלות מטבע וקריאת רק כמות לוגריתמית מההוכחה על מנת לקבל כל שפה השייכת ל-NP. תוצאה זו הורחבה אף יותר במשפט ה-PCP, מהמשפטים הבולטים בתורת הסיבוכיות, אשר מראה כי \ PCP(\log(n),O(1))=NP - כלומר, בהינתן שפה כלשהי מ-NP, די לקרוא כמות קבועה של מידע מתוך ההוכחה (כלומר, כמות שאינה תלויה בגודל המילה הנבדקת) ולהשתמש במספר לוגריתמי של הטלות מטבע, כדי להיות מסוגלים לקבוע בהסתברות גבוהה האם מילה שייכת לשפה או לא.

[עריכה] קישורים חיצוניים

שפות אחרות