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

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

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

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

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

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

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

המחלקה IP

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

דוגמה לשפה ב-IP

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