אז מה זה IP=PSPACE?

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

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

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

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

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

בואו נביט שניה בהוכחה מתמטית “אמיתית” - הוכחת אוקלידס לקיום אינסוף ראשוניים. נניח שיש רק מספר סופי של ראשוניים, \( p_{1},\dots,p_{n} \). נתבונן במספר \( p_{1}\cdot p_{2}\cdots p_{n}+1 \). הוא אינו מתחלק על ידי אף אחד מהראשוניים \( p_{1},\dots,p_{n} \) ולכן מתחלק על ידי ראשוני שונה מהם. זו כל ההוכחה, ועבור המתמטיקאים בקהל אני בטוח שהיא מספיקה, אבל האם זו הייתה “סדרה סופית של טענות הנובעות זו מזו בעזרת כללי היסק תוך שימוש באקסיומות”? היכן האקסיומות? מיהם כללי ההיסק? גרוע מכך - ההוכחה הזו מבצעת הרבה קפיצות לוגיות שעבור מתמטיקאי הן טריוויאליות אבל עבור מי שמעולם לא ראה אותן הן אסון. למה ש-\( p_{1}\cdots p_{n}+1 \) לא יתחלק על ידי אף אחד מהראשוניים \( p_{1},\dots,p_{n} \)? ולמה שהוא כן יתחלק על ידי ראשוני שונה מהם? אלו דברים שדורשים הסבר - למעשה, הוכחה - בפני עצמם. ויקיפדיה העברית מכסה זאת בעזרת “ידע קודם שהוכח קודם לכן”, אבל כשקוראים הוכחות אמיתיות לא תמיד ברור בכלל לאיזה ידע קודם ההוכחה מתייחסת. בהוכחות אמיתיות (כאלו שנמצאות בספרי לימוד מתקדמים; בספרי מבוא לרוב ההוכחות יותר ידידותיות) יש המון קפיצות מעל פרטים שרק קורא שבקיא בחומר מסוגל להשלים; קוראים אחרים נאלצים לפנות לעזרה לאתרים כמו MathOverflow ו-MathStackExchange.

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

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

בואו נעבור לדבר באופן טהור על גישתם של מדעי המחשב לכל העסק הזה. עבור מדעני המחשב, “טענה” היא בסך הכל סדרה סופית של תווים מעל א”ב כלשהו (למשל, כזה שבו יש רק שתי אותיות - 0 ו-1; שני אלו מספיקים כדי לקודד כל דבר וזה בדיוק מה שקורה במחשבים). לסדרה סופית כזו של תווים קוראים “מילה”, ולקבוצה כלשהי של מילים קוראים “שפה” ומסמנים אותה ב-\( L \) לרוב. היעד של מערכות ההוכחה שלנו הוא להראות עבור מילה \( w \) כלשהי כי \( w\in L \). אם \( L \) היא אוסף כל המחרוזות אשר מקודדות טענות נכונות במתמטיקה ו-\( w \) היא המחרוזת “יש אינסוף זוגות ראשוניים שההפרש בין אברי הזוג הוא 2”, הרי שלהראות \( w\in L \) במקרה הזה זה בעצם “להוכיח את השערת הראשוניים התאומים”, כך שכל הדיבורים הללו על מילים ושפות לא באמת מגבילות את מה שאנחנו מסוגלים לדבר עליו, אלא רק נותנות לו פורמליזם שנוח עבורנו. לכל שפה תהיה מערכת הוכחה משל עצמה.

את המושג של “תהליך הבדיקה” ממדלים בצורה פורמלית בעזרת אלגוריתם, \( V \) - “המוודא” (מלשון Verifier). למי שהמושג אלגוריתם מעורפל מדי בשבילו, בדרך כלל דורשים ש-\( V \) הוא מודל חישוב קונקרטי מסויים, דוגמת מכונת טיורינג; אלו לא פרטים שיש צורך להיכנס אליהם כאן. \( V \) מקבל כקלט זוג \( \left(w,\pi\right) \), כש-\( w \) היא מילה כלשהי ו-\( \pi \) היא מחרוזת שמטרתה להוות הוכחה לכך ש-\( w \) שייך ל-\( L \). מ-\( V \) אנחנו דורשים שבהינתן קלט \( \left(w,\pi\right) \), \( V \) יסיים מתישהו את ריצתו על הזוג (אם הוא לא עוצר לעולם, כל העסק חסר ערך מבחינתנו), ויגיד “כן” או “לא”. כדי שנוכל לומר שהאלגוריתם \( V \) פועל נכון, נצטרך שיקרו שני דברים:

1. שלמות: אם \( w\in L \) אז קיימת הוכחה \( \pi \) כלשהי כך ש-\( V \) מסיים את ריצתו על \( \left(w,\pi\right) \) ואומר "כן".
2. נאותות: אם \( w\notin L \) אז לכל \( \pi \) מתקיים ש-\( V \) מסיים את ריצתו על \( \left(w,\pi\right) \) ואומר "לא".

כלומר, אם \( V \) אומר “כן” הוא בעצם אומר “כן, \( w\in L \) וההוכחה \( \pi \) שכנעה אותי בכך”, ואילו אם הוא אומר “לא”, הוא בעצם אומר “\( \pi \) לא שכנעה אותי ש-\( w\in L \)” (שימו לב להבדל המהותי בין זה ובין לומר “\( w\notin L \), נקודה”).

ההגדרה הזו נותנת המון חופש פעולה ל-\( V \); הוא רק צריך לעצור ולקיים את תנאי השלמות והנאותות, אבל אף אחד לא אומר לו איך בדיוק הוא צריך לבדוק ש-\( w \) נכון, איך הוא אמור להשתמש ב-\( \pi \), וכדומה. למעשה, הוא יכול גם להתעלם מ-\( \pi \) לחלוטין ולבצע בדיקה על \( w \) באופן בלתי תלוי. אם למשל \( L \) היא שפת המספרים הראשוניים, אז \( V \) יכול פשוט לבדוק את כל המחלקים האפשריים של \( w \) ואם לא התגלו מחלקים לא טריוויאליים - לעצור ולהגיד “כן”, ואחרת לעצור ולהגיד “לא”. בלי שהוא השתמש בכלל ב-\( \pi \) לשום מטרה שהיא.

אם כן, עולה השאלה הטבעית - האם השימוש ב-\( \pi \) - האם המעבר מ”\( V \) בודק דברים לבד” ל-“\( V \) מקבל הוכחה מהעולם החיצון ונעזר בה” - מוסיפה למערכת כוח חישובי? התשובה היא - בהחלט כן.

הבה וניקח כדוגמה את הבעיה העשירית של הילברט. בבעיה הזו נתונה משוואה דיופנטית (משוואה פולינומית במקדמים שלמים), והשאלה היא אם קיים לה פתרון במקדמים שלמים. הילברט ביקש למצוא אלגוריתם לפתרון הבעיה כבר ב-1900, אך רק בשנות השבעים של המאה ה-20 הוכח סופית כי אלגוריתם שכזה אינו קיים. הבה ונקבל כנתון את הטענה הזו (שתזכה יום אחד לפוסט - או סדרת פוסטים - משל עצמה) - זה אומר ש-\( V \) המסכן, אם קיבל \( w \) שמקודדת משוואה דיופנטית, לא יכול לבצע אף חישוב שגם יעצור תמיד וגם יחזיר תמיד את התשובה הנכונה. פורמלית אומרים על כך שהבעיה איננה במחלקה \( \mbox{R} \). מה הוא כן יכול לעשות? ובכן, אם קיים פתרון, אפשר בעזרת חיפוש ממצה למצוא אותו לבסוף, לעצור ולהחזיר אותו. רק מה? אם לא קיים פתרון, החישוב לא יסתיים לעולם (וזה, כזכור, מנוגד באופן חזק לדרישה הבסיסית שלנו מ-\( V \) שיעצור תמיד). על בעיות שניתנות ל”חצי פתרון” שכזה אומרים שהן במחלקה \( \mbox{RE} \).

כעת, לבעיה העשירית של הילברט יש מערכת הוכחה פשוטה למדי: אם \( w \) משוואה דיופנטית בעלת פתרון, אז \( \pi \) יקודד את הפתרון הזה - ההצבה הנדרשת למשתנים. אם \( V \) מקבל \( \left(w,\pi\right) \), הוא פשוט מציב את \( \pi \) לתוך המשוואה ובודק אם המשוואה מתקיימת או לא. אם כן - האח, \( V \) עוצר ומקבל; אחרת, \( V \) עוצר ודוחה. בכל מקרה \( V \) יעצור, ובכל מקרה הוא לא יטעה - אם ל-\( w \) יש פתרון, אז יש \( \pi \) שעבורו \( V \) יקבל (ההצבה ה”נכונה” למשוואה) ואם ל-\( w \) אין פתרון, ברור שלכל \( \pi \) הוא ידחה.

לא קשה להוכיח טענה כללית על מערכות הוכחה שכאלו - השפות שקיימת להן מערכת הוכחה שכזו הן בדיוק השפות שב-\( \mbox{RE} \). מכיוון ש-\( \mbox{RE} \) גדולה יותר מ-\( \mbox{R} \), זה מראה שמערכת ההוכחה שתיארנו מוסיפה כוח חישובי רב.

המחלקות \( \mbox{R} \) ו-\( \mbox{RE} \) שייכות לעולם המופלא של תורת החישוביות - לשאלה מה ניתן לחשב בכלל. העניינים נהיים סבוכים ומעניינים בהרבה כאשר עוברים לעולם המפלא של תורת הסיבוכיות - שבו השאלה היא מה ניתן לחשב ביעילות, כשכאן “יעילות” מזוהה עם “ריצה בזמן שהוא פולינומי בגודל הקלט”. לכן אנחנו מדברים פה על מערכת הוכחה שזהה למה שתיארנו קודם פרט לדרישה ש-\( V \) ירוץ בזמן שהוא פולינומי בגודל של \( w \) (וכפועל יוצא מכך נובע ש-\( \pi \) אף הוא צריך להיות פולינומי בגודל \( w \) אחרת \( V \) לא יספיק לקרוא את כולו).

בעולם החדש הזה המחלקה \( \mbox{P} \) היא המקבילה של \( \mbox{R} \), ולמחלקת השפות שיש להן מערכת הוכחה מהסוג שתיארתי קוראים \( \mbox{NP} \). זו, אם כן, המקבילה של \( \mbox{RE} \) בעולם הסיבוכיותי, וכמו שאפשר להוכיח ש-\( \mbox{R}\ne\mbox{RE} \) ולכן הוכחות מוסיפות כוח באופן כללי, עולה השאלה האם \( \mbox{P}\ne\mbox{NP} \) ולכן הוכחות מוסיפות כוח בהקשר של חישובים יעילים. זו, אולי כבר שמעתם, הבעיה הפתוחה המרכזית במדעי המחשב, ואחת מהבעיות הפתוחות החשובות ביותר במתמטיקה באופן כללי. ההשערה היא שאכן \( \mbox{P}\ne\mbox{NP} \), אבל לכו תוכיחו - העולם הסיבוכיותי מאתגר הרבה יותר מהעולם החישוביותי וכבר נתתי דוגמה לכך בעבר.

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

אינטראקציה אומרת כך - הבה ונניח שלמשחק שלנו מצטרף מתמודד נוסף, \( P \), “המוכיח” (מלשון Prover). בהינתן \( w \) \( P \) ו-\( V \) מנהלים ביניהם דיאלוג כלשהו - \( P \) שולח ל-\( V \) הודעה, ו-\( V \) יכול לענות לו, ו-\( P \) יכול לענות לתשובה, וכן הלאה. בסופו של דבר (ואחרי זמן פולינומי) \( V \) צריך לעצור ולקבל או לדחות את \( w \), ואותם תנאים של קודם תקפים: אם \( w\in L \) אז יש דרך התנהגות של \( P \) שגורמת ל-\( V \) לקבל, ואילו אם \( w\notin L \) אז לא משנה איך \( P \) יתנהג, \( V \) ידחה. בדרך כלל במערכות כאלו אנחנו לא מניחים ש-\( P \) מוגבל חישובית בכלל - כמו שקודם ההוכחה \( \pi \) הגיעה באורח קסום מהשמיים, כך גם כאן \( P \) הוא יצור שמיימי בעל כוח לא מוגבל (בעולם האמיתי הכוח של \( P \) ינבע לרוב מכך שיש לו כבר ידע קודם שאין ל-\( V \); למשל, \( P \) יכיר פירוק לגורמים של מספר \( n=pq \) מסויים בגלל שהוא עצמו הגריל מלכתחילה את \( p,q \) והכפיל אותם לקבלת \( n \)) .

טוב, אז מה נשתנה אם מרשים אינטראקציה? באופן מאכזב למדי, כלום. \( \mbox{NP} \) היא עדיין מחלקת הבעיות שקיימת להן הוכחה, גם עם מוכיח אינטראקטיבי שכזה. הסיבה לכך היא שאת כל מה ש-\( P \) עושה “אינטראקטיבית” אפשר היה לכתוב ב-\( \pi \) מראש, שכן ברור למוכיח בדיוק איך \( V \) הולך להגיב לכל דבר ש-\( P \) יאמר, כי \( V \) הוא דטרמיניסטי. אז ההוכחה תהיה בערך כך: “התשובה לשאלה הראשונה שלך היא: 42. התשובה לשאלה השניה שלך היא: 0. נכון שזה קריפי שאני יודע מה אתה הולך לשאול? נכון? נכון? נכון? טוב, בוא נמשיך, התשובה לשאלה השלישית היא: 42. וואו, השאלות שלך לא מקוריות. טוב, בוא נמשיך…”.

איך אפשר להתקדם מכאן? בכמה דרכים. אחת מהדרכים היפות היא מערכת בוררות. במערכת שכזו אין מוכיח אחד אלא שני מוכיחים, שכל אחד מהם רוצה להוכיח משהו שונה. המטרה של אחד מהם היא להוכיח ש-\( w\in L \) והמטרה של השני - ש-\( w\notin L \). ברור שאחד מהם משקר, ולכן הם מנהלים מאבק כלשהו. בינתיים \( V \) יושב בצד ומאזין לויכוח שלהם (הוא לא צריך לשאול שאלות בעצמו כי, כמו קודם, המוכיחים יודעים בדיוק מה הוא הולך לשאול שכן הוא דטרמיניסטי). בסוף הויכוח (שצריך להימשך זמן פולינומי), \( V \) חורץ דין ומחליט האם \( w\in L \) או לא. כרגיל, ל-\( V \) אסור לטעות, בכלל.

האם המערכת הזו מוסיפה כוח? ככל הנראה כן. אפשר להוכיח שמחלקת השפות שיש להן מערכת בוררות שכזו היא \( \mbox{PSPACE} \) - מחלקת כל השפות שניתן להכריע בזכרון פולינומי. \( \mbox{PSPACE} \) היא מחלקה ענקית, שכוללת את \( \mbox{NP} \) וגם הרבה מעבר לכך; אתאר אותה בפוסט הבא יותר בפירוט. מצד שני, אין לנו מושג כיום אם \( \mbox{P}\ne\mbox{PSPACE} \).

הדרך השניה להתקדם מכאן היא להרשות אקראיות. נניח שאנחנו מרשים למוודא לעשות הגרלות שמכתיבות אילו שאלות הוא ישאל את המוכיח. האם שינינו משהו? ובכן, אם כל מה שעשינו הוא להרשות למוודא להגריל שאלות, לא ממש. כי איך תיראה כעת הוכחה \( \pi \) לנכונות טענה? היא תהיה מהצורה “אם היית מגריל 0, אז היית שואל כך וכך, והייתי עונה לך: 42! ואז, אם היית מגריל 1, היית שואל כך וכך והייתי עונה לך: 17! ואחר כך…”. כלומר, ההוכחה מתארת מה קורה בסדרת בחירות אקראיות אחת של המוודא ומתעלמת מכל שאר האפשרויות. למה זה עובד? כי בסוף הדיאלוג הזה, התשובה של המוודא חייבת להיות התשובה הנכונה. אם \( w\in L \), כל מה שאנחנו רוצים הוא לראות סדרת בחירות אקראיות אחת שגורמת למוודא להשיב “כן”. לא אכפת לנו מכך שיש אולי עוד המון דרכים לגרום לו להשיב כך.

אז כדי לפרוץ את גבולות \( \mbox{NP} \), אנחנו מכניסים לתמונה משהו שנראה כמו חילול הקודש כאשר מדובר על הוכחות - משהו שבאמת משנה לגמרי את התמונה: אנחנו מרשים למוודא לטעות. אנחנו עדיין דורשים שאם \( w\in L \) אז המוכיח יהיה מסוגל לשכנע אותו, ולא משנה מה המוודא שואל; אבל אם \( w\notin L \) אנחנו מרשים למוודא לענות בטעות “כן” בסוף הפרוטוקול. אנחנו רק דורשים שההסתברות לכך תהיה נמוכה. כמה נמוכה? ובכן, כמה שתרצו! אני ארחיב על כך בהמשך. הנקודה היא שלמוודא חייבת להיות הסתברות כלשהי, זניחה ככל שתהיה, לטעות.

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

כמה כוח הוסיפה לנו האפשרות הן לבצע אינטראקיציה והן האקראיות? כלומר, מהי המחלקה \( \mbox{IP} \) של כל השפות שיש להן הוכחה אינטראקטיבית הסתברותית? זו הייתה שאלה פתוחה במשך זמן מה מאז שהוצע המודל. היה ברור לכולם ש-\( \mbox{IP}\subseteq\mbox{PSPACE} \), אבל מה פרט לכך? כשהסתכלו על המחלקות \( \mbox{IP}\left[k\right] \) של מערכות הוכחה שבהן האינטראקציה היא של \( k \) סיבובים בדיוק, התגלה שלא משנה כמה \( k \) גדול - כל עוד הוא קבוע בגודלו ביחס לגודל הקלט, מתקבלת המחלקה \( \mbox{IP}\left[2\right] \). רק כשמרשים למספר הסיבובים בפרוטוקול להיות פולינומי בגודלו ביחס לגודל הקלט יש סיכוי לקבל משהו גדול יותר. מצד שני, אף אחד לא הכיר בעיות שדרשו זאת - כל מה שמצאו לו פרוטוקול הוכחה אינטראקטיבית (ונראה לכך דוגמאות בפוסט הבא) יכל להסתפק במספר קבוע של סיבובים. בנוסף, לא נראה היה שהסתברות אמורה להוסיף הרבה כוח למערכת ההוכחה; הסתברות לא מוסיפה הרבה כוח גם לחישוב רגיל (המחלקה \( \mbox{BPP} \), שהיא המקבילה ההסתברותית של \( \mbox{P} \), איננה גדולה מ-\( \mbox{P} \) בהרבה ויש החושדים ש-\( \mbox{P=BPP} \), ובניגוד ל-\( \mbox{P=NP} \) זה גם לא מופרך).

אם כן, האמונה הרווחת בקרב מדעני המחשב הייתה ש-\( \mbox{IP} \) היא מחלקה חלשה יחסית. ואז ב-1990 הוכיחו ש-\( \mbox{IP=PSPACE} \) (הוכיח את זה עדי שמיר, ה-S שב-RSA, ובאופן בלתי תלוי הוכיחה את זה עוד חבורה שלא אכתוב את כולה). זו באמת הייתה פצצה, בדיוק בגלל ש-PSPACE היא מחלקה כל כך גדולה ו”חזקה”. זה היה גילוי מאוד מפתיע גם מבחינה רעיונית - האופן שבו הוכחה אינטראקטיבית היא הרבה, הרבה יותר מאשר הוכחה “קלאסית”. וכמובן, ההוכחה של \( \mbox{IP=PSPACE} \) הייתה גם מבריקה בפני עצמה והשתמשה בטכניקות חדשות ביחס למה שהיה קיים אז.

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