הסקה אוטומטית (Automated Reasoning)

הוכחה במקום טקסט משכנע

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

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

ההתחלה: זוגי ועוד זוגי

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

שאפתני יותר היה התיאורטיקן הלוגי (Logic Theorist) של אלן ניואל, הרברט סיימון וקליף שו, מ-1956. התוכנית בנתה הוכחות לוגיות מתוך Principia Mathematica של וייטהד וראסל, והצליחה להוכיח 38 מתוך 52 המשפטים הראשונים שנבדקו. היא השתמשה בכללי-אצבע (היוריסטיקות) שחיקו מתמטיקאים, ולכן לא הבטיחה למצוא הוכחה לכל משפט נכון. במקביל פותחו שיטות שיטתיות יותר, שלפחות בתאוריה כן מבטיחות זאת ללוגיקה מסדר ראשון. גם התחום הזה עבר "חורף" בשנות ה-80 ובתחילת שנות ה-90, ואחר כך התאושש.

איך מכונה מוכיחה, ואיפה היא נעצרת

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

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

משפטים שאנשים לא הצליחו להוכיח

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

במאי 2016 פתרו מריין הויל, אוליבר קולמן וויקטור מארק את "בעיית השלשות הפיתגוריות הבוליאנית" — האם אפשר לצבוע כל מספר שלם חיובי באדום או בכחול כך שאף שלשה פיתגורית לא תהיה כולה בצבע אחד. התשובה: אפשר רק עד המספר 7824. את המקרים בדק פותר SAT, תוכנה שמכריעה אם אפשר לקיים נוסחה לוגית, וההוכחה שנוצרה שקלה 200 טרה-בייט ודוחסה ל-68 גיגה-בייט. כבר קודם לכן עורר משפט ארבעת הצבעים ויכוח, כי ההוכחה שלו נשענה על חישוב ממוחשב שבני אדם אינם יכולים לבדוק בעצמם.

בשבבים ובענן

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

קוק המחיש את ההיגיון בדוגמה פשוטה: פונקציה שבודקת אם x+y שווה ל-y+x. לפי קוק, בדיקה של כל זוגות הערכים מסוג המספרים שבדוגמה (מספרים שלמים בלי סימן בשפת C) הייתה אורכת "יותר מ-1,360 שנה" בקצב שמדד במחשב שלו; הוא עצמו הפסיק אחרי יותר מ-48 שעות. כלי שמבצע היסק לוגי, לעומת זאת, משתמש באלגברה ומסיק שהתשובה תמיד "אמת". באמזון, לדבריו, כלים כאלה עומדים מאחורי שירותים כמו IAM Access Analyzer, שבודק הרשאות גישה בענן. קוק גם הסתייג: בדרך כלל מאמתים שכבה אחת בכל פעם — קוד המקור, או לפעמים המהדר או המעבד — תוך הנחות על שאר השכבות, ולכן היא מצמצמת את הצורך בבדיקות רגילות אבל לא מבטלת אותו. חיבור דומה בין כלים כאלה למודלי שפה מתואר בערך על בינה נוירו-סימבולית.

כשמודלי שפה פוגשים הוכחות פורמליות

בשנים האחרונות התחום חזר למרכז הבמה, דווקא בגלל מודלי השפה. ב-25 ביולי 2024 הציגה גוגל דיפמיינד את AlphaProof, מערכת שמתאמנת להוכיח טענות מתמטיות בשפה הפורמלית Lean. יחד עם מערכת גיאומטריה נוספת היא פתרה ארבע מתוך שש בעיות באולימפיאדה הבינלאומית למתמטיקה של אותה שנה, וקיבלה 28 מתוך 42 נקודות — רמה של מדליית כסף. הבעיות תורגמו לשפה הפורמלית בידי אדם, וחלקן דרשו עד שלושה ימי חישוב. המאמר המלא פורסם ב-Nature בנובמבר 2025.

שפת Lean עצמה פותחה בעיקר בידי לאונרדו דה מורה, בתחילה במיקרוסופט ריסרץ', והושקה ב-2013. ספריית המתמטיקה הקהילתית שלה, mathlib, כללה נכון למאי 2025 יותר מ-210,000 משפטים מוכחים. ב-4 בספטמבר 2026 דיווחה Anthropic שסוכני Claude פירמלו ב-Lean את המשפט האחרון של פרמה — כלומר תרגמו הוכחה קיימת, גרסה מפושטת של הוכחת ויילס, לצורה שהמחשב בודק עד הסוף. לפי החברה, העבודה נמשכה 11 ימים, נעשתה "ברובה באופן אוטונומי" עם הנחיות אנושיות מזדמנות, והניבה 13 מיליון שורות קוד עם 29,500 משפטי ביניים. זה דיווח של החברה עצמה; המתמטיקאי קווין באזארד, שמוביל מאז 2024 פרויקט קהילתי לאותה מטרה, אמר לחברה שההוכחה מוכיחה את המשפט "בלי הנחות מלבד האקסיומות של המתמטיקה". הדפוס בשני המקרים דומה: מודל שפה מציע, ומוכיח פורמלי בודק.