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

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

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

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

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

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

דוגמה לא פורמלית

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

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

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

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

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

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

NP כמערכת הוכחה

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

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

המחלקה IP

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

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

המחלקה IP (ראשי תיבות של Interactive Proof – הוכחה אינטראקטיבית) היא אוסף השפות שניתן לקבל, כאשר מתירים בפרוטוקול ההוכחה לשני הצדדים לשלוח זה לזה הודעות מספר פעמים שהוא פולינומי ביחס לאורך הקלט. מתברר כי כוחה של מערכת ההוכחה הזו גדול יחסית: עדי שמיר הוכיח בשנת 1990 כי 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 וכן הלאה (באופן כללי ${\textstyle {\frac {1}{2^{n}}}}$, כאשר $n$ הוא מספר הסבבים).

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

הוכחות באפס ידע

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

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

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

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

• המחלקה PZK (ראשי תיבות של Perfect Zero-Knowledge) – אוסף השפות, שקיים להן פרוטוקול אפס ידע מושלם; כלומר, שהסימולטור מייצר התפלגות תעתיקים הזהה לחלוטין לזו של הפרוטוקול האמיתי.
• המחלקה SZK (ראשי תיבות של Statistical Zero-Knowledge) – מתירה מרחק קבוע כלשהו (למשל, 1/10) בין ההתפלגויות.
• המחלקה CZK (ראשי תיבות של Computational Zero-Knowledge) – מתירה כל הבדל בין ההתפלגויות, שלא ניתן לגילוי על ידי מכונה שכוחה ככוחו של המוודא (כלומר, מכונת BPP). תחת ההנחה, לפיה קיימות פונקציות חד-כיווניות, ניתן להראות כי CZK שווה למחלקה IP.

המחלקה MIP

ישנן שתי דרכים בסיסיות להרחיב את IP:

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

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

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

פרוטוקול ארתור-מרלין

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

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

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

PCP

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

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

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

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

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

קישורים חיצוניים

• המחלקות שהוצגו בערך, מתוך Complexity Zoo:
  • NP, IP, PZK, SZK, CZK, MIP, AM, MA, PCP.

הערות שוליים

הערך באדיבות ויקיפדיה העברית, קרדיט,
רשימת התורמים
רישיון cc-by-sa 3.0

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