מוכיח בשער

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

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

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

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

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

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

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

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

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

המערכת הפשוטה הזו כבר מצויידת בשתי התכונות ההכרחיות בכל מערכת הוכחה: שלמות ונאותות.

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

נאותות פירושה שלא מסוגלים “לעבוד” עלינו - שאי אפשר יהיה להוכיח דברים שאינם נכונים. ברמה המחמירה ביותר הדרישה הזו היא מוחלטת, אבל מתברר שהחלשתה (כלומר, התרת האפשרות שיעבדו עלינו, אף אם בהסתברות אפסית שאנו מסוגלים לשלוט על גודלה) היא זו שמביאה אותנו לחלקים המעניינים באמת של מערכות ההוכחה, וארחיב על כך בהמשך. במקרה שלנו הנאותות של המערכת היא מוחלטת: אם יש לנו מספר ראשוני \( b \), אז לא משנה איזה מספר נשלח למוודא, הוא יסרב להשתכנע בנכונות ההוכחה שלנו - כי לא משנה איזה מספר נשלח למוודא, כל עוד הוא אינו \( b \) או 1, הוא לא יחלק את \( b \) בלי שארית ולכן דעתו של המוודא לא תפוייס.

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

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

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

בפעם הבאה - איך האינטראקטיביות נכנסת לסיפור.