הבאג של $10 מיליון שה-AI כתב — ולמה הקמתי חברה כדי לחסל אותו
אני זוכר את הרגע המדויק שבו החלטתי להקים את Veriprajna.
זה לא היה הבזק של השראה. זו הייתה שיחת טלפון. מהסוג שבו אף אחד לא מדבר בחמש השניות הראשונות כי האדם בצד השני מנסה להבין איך לומר את מה שהוא צריך לומר. צוות עיצוב — אנשים שכיבדתי, אנשים שהיו טובים באמת בעבודתם — בדיוק קיבל בחזרה סיליקון ראשון מבית היציקה על מאיץ RISC-V מותאם אישית. השבב היה מת. לא מת ברמת "צריך פתרון עוקף". לא מת ברמת "אפשר לתקן את זה בקושחה". הפך ללבנה. תחת יישור ספציפי ונדיר של ויסות תרמי (thermal throttling) ותעבורת זיכרון ברוחב-פס גבוה, מודול הבוררות נכנס למצב לא-מוגדר וכל העניין נכנס לקיפאון.
סיבת השורש הייתה מצב מרוץ (race condition). אי-התאמה בודדת ועדינה בין השמות חוסמות ולא-חוסמות ב-RTL — מהסוג שמסמלץ באופן מושלם, עובר lint ללא לחישה, עובר כל בדיקת רגרסיה שתטילו עליו, ואז בוגד בכם בסיליקון שבו אין הזדמנויות שניות.
סט המסכות לשבב ה-5nm ההוא עלה בערך $10 מיליון. אבד. אבל הנזק האמיתי לא היה המסכות. הוא היה ששת החודשים שנדרשו כדי לאבחן, לתקן, לאמת מחדש, ולייצר מחדש. בשוק מאיצי ה-AI, שבו דורות של מוצרים נמשכים כ-18 חודשים, החלקה של שישה חודשים יכולה לשחוק 50% מכלל הרווח הגולמי של מוצר לאורך חייו. עבור חברה המכוונת ל-$100 מיליון בהכנסות, מצב המרוץ הזה לא עלה $10 מיליון. הוא עלה $50 מיליון.
והנה החלק ששמר עליי ער בלילות: הקוד שגרם לזה נוצר על ידי LLM.
בהלת הזהב שאיש אינו מטיל בה ספק
כרגע, תעשיית המוליכים למחצה נמצאת באמצע בהלת זהב. כולם — ואני מתכוון לכולם — מתחרים לחבר מודלי שפה גדולים (Large Language Models) אל תוך זרימת העבודה של Electronic Design Automation (EDA). ההצעה בלתי-ניתנת לעמידה: לקחת מחזורי עיצוב שנהגו להימשך שנים ולכווץ אותם לחודשים. לדמוקרטיזציה של עיצוב שבבים. לתת ל-AI לטפל בקידוד המייגע ברמת register-transfer כדי שמהנדסים יוכלו להתמקד בארכיטקטורה.
אני מבין את המשיכה. הרגשתי אותה בעצמי. בפעם הראשונה שצפיתי ב-LLM מייצר מודול Verilog תקין תחבירית מפרומפט בשפה טבעית, חשבתי: זה משנה הכול.
אבל אז התחלתי להסתכל בזהירות רבה יותר על מה ש"תקין תחבירית" באמת אומר כשכותבים חומרה במקום תוכנה. והבנתי שהתעשייה בונה על יסוד של חול.
הכלים שמציפים את השוק כרגע הם מה שאני מכנה "Wrappers" (עוטפים). הם לוקחים LLM כללי — GPT-4, Claude, Llama — עוטפים אותו בממשק צ'אט עם כמה פרומפטי מערכת בטעם Verilog, ומוכרים אותו כ"Copilot לעיצוב שבבים". חלקם הם דמואים מרשימים באמת. הקוד נראה נקי. הוא עובר קומפילציה. הוא אפילו מסמלץ.
אבל הנה מה שהכלים האלה הם ביסודם: חזאי טוקנים סטוכסטיים עם מעטה חומרה. הם לא מבינים טופולוגיית מעגלים. הם לא מבינים סגירת תזמון (timing closure). הם לא מבינים מטא-יציבות (metastability). הם חוזים את הטוקן הסביר הבא על סמך דפוסים סטטיסטיים בנתוני האימון שלהם.
כש-LLM מהזה בתוכנה, מקבלים שגיאת זמן-ריצה שאפשר לתקן מרחוק (over the air). כש-LLM מהזה בחומרה, מקבלים משקולת-נייר של $10 מיליון.
האסימטריה הזו היא כל הסיבה ש-Veriprajna קיימת.
למה AI כותב קוד חומרה גרוע?
זו השאלה שאני נשאל הכי הרבה, בדרך כלל על ידי מהנדסי תוכנה שראו LLM-ים כותבים Python פונקציונלי לחלוטין ואינם מבינים למה Verilog שונה. התשובה עמוקה יותר מ"חומרה קשה יותר". זו אי-התאמה יסודית בין האופן שבו LLM-ים חושבים לבין האופן שבו חומרה עובדת.
LLM-ים מאומנים באופן מכריע על תוכנה — Python, Java, C++, JavaScript. אלה שפות ציווייות, סדרתיות. שורה A מתבצעת, ואז שורה B. מצב המערכת מוגדר על ידי סדר הפעולות. LLM-ים הפנימו את הפרדיגמה הזו כה עמוק עד שהיא בעצם שפת האם שלהם.
Verilog ו-VHDL הן דקלרטיביות ומקביליות. במודול חומרה, כל always בלוק, כל assign ביטוי, כל יצירת מופע של מודול מתבצעים בו-זמנית וברציפות. סדר השורות בקוד המקור לרוב אין לו כל השפעה על סדר הביצוע בסיליקון.
צפיתי בזה מתרחש בזמן אמת באחד הניסויים המוקדמים שלנו. ביקשנו משלושה LLM-ים חזיתיים שונים לממש רגיסטר צנרת פשוט בן שלושה שלבים. כל השלושה השתמשו בהשמות חוסמות (=) במקום השמות לא-חוסמות (<=). הקוד נראה סביר לחלוטין אם מציצים בו כאילו היה קוד C. אבל בחומרה, השמות חוסמות בבלוק מתוזמן פירושן שstage2 מתעדכן עם הערך של stage1 מיד, ואז stage3 מקבל את הערך החדש של stage2 — וכך למעשה מכווץ צנרת דו-מחזורית למחזור יחיד.
אחת המהנדסות שלי, פריה, בהתה בפלט למשך דקה ואמרה: "הוא כותב C עם נקודות-פסיק במקומות הלא נכונים." היא צדקה בדיוק. ל-LLM הייתה הטיה סדרתית — הוא התייחס ל-Verilog כאל שפת תכנות בעוד שלמעשה מדובר בשפת תיאור. ההבחנה עדינה מבחינה תחבירית והרסנית מבחינה פיזית.
וזה נעשה גרוע יותר. עיצוב חומרה מסתמך על פרוטוקולי ממשק נוקשים — AXI, AHB, PCIe, TileLink — עם כללים טמפורליים מורכבים. "Ready אסור שימתין ל-Valid." "Grant חייב להיות מופעל בתוך 5 מחזורים." LLM-ים יכולים לייצר קוד שמכבד את הכללים האלה 90% מהזמן, מה שנשמע נהדר עד שמבינים ש-10% שהם טועים בהם הם בדיוק מקרי הקצה שהורגים שבבים. מנהל AXI שמפעיל את WVALID לפני AWREADY תוך הפרה של סעיף-משנה מסוים לא יזרוק שגיאת תחביר. הוא יעבור קומפילציה, יסמלץ, ואז ייתקע כשיחובר לבקר זיכרון תואם בסיליקון.
בעיית נתוני האימון מחמירה את הכול. נפח ה-Verilog האיכותי, ברמת ייצור, הזמין לאימון הוא קטן בסדרי גודל מ-Python או JavaScript. חלק ניכר מקוד ה-Verilog בקוד פתוח ב-GitHub הוא פרויקטים של סטודנטים, אבות-טיפוס נטושים, ומימושי צעצוע שלעולם לא היו שורדים סקירת tape-out. כשמאמנים על נתונים בינוניים, מקבלים תוצרים בינוניים — תוצרים שנראים מקצועיים אך מכילים את ה-DNA של טעויות חובבניות.
הכלל שרודף כל מעצב שבבים
יש היוריסטיקה בעיצוב מוליכים למחצה הנקראת "כלל העשר", וברגע שמבינים אותה, מבינים למה אני כה אובססיבי לתפיסת באגים מוקדם.
העלות לתיקון פגם גדלה ב-10x בכל שלב עוקב במחזור חיי העיצוב. באג שנתפס במהלך עיצוב RTL עולה כ-$100 לתיקון — מישהו עורך קובץ ומריץ מחדש בדיקה. אותו באג שנתפס במהלך אימות בלוק עולה $1,000. באימות מערכת, $10,000. אם הוא נמלט לאימות פוסט-סיליקון — כשמנפים שבבים אמיתיים במעבדה — מדובר ב-$10 מיליון או יותר עבור ריספין. ואם הוא מגיע ללקוחות בשטח? זו כבר טריטוריה של $100 מיליון. ריקולים, תביעות, הרס מותג. שאלו את Intel על באג ה-FDIV של ה-Pentium.
כלי ה-AI מסוג Wrapper פועלים כמעט אך ורק בשלב עיצוב ה-RTL. הם עוזרים למהנדסים לכתוב קוד מהר יותר. אבל מכיוון שחסרה להם כל יכולת אימות מעבר ל"האם זה עובר קומפילציה", הם מזריקים באגים שחולפים בקלות דרך אימות בלוק ומערכת, רק כדי להתפוצץ בסיליקון.
והנה האירוניה האכזרית: על ידי הגברת מהירות יצירת הקוד מבלי להגביר את קפדנות האימות, כלים אלה מאיצים את הזרקת הפגמים יקרי-העלות אל תוך הצנרת. אתם לא רק נעים מהר ושוברים דברים. אתם נעים מהר ואופים באגים לתוך סטי מסכות של $10 מיליון.
נתוני התעשייה מאששים זאת. רק 32% מהעיצובים משיגים הצלחה בסיליקון הראשון. 68% הנותרים דורשים לפחות ריספין אחד, והסיבה העיקרית היא פגמים לוגיים ופונקציונליים — בדיוק סוג השגיאות ש-LLM-ים מייצרים כשהם מהזים פרוטוקולים או מבינים מקביליות באופן שגוי.
הסברתי זאת למשקיע פעם אחת, בתחילת גיוס ההון שלנו. הוא הקשיב בסבלנות, ואז אמר: "אתם לא יכולים פשוט להשתמש ב-GPT-4 עם פרומפטים טובים יותר?"
שלפתי את דוגמת רגיסטר הצנרת. הראיתי לו את באג ההשמה החוסמת. הראיתי לו שהוא עבר lint, עבר סימולציה, עבר כל בדיקה אוטומטית שכלי ה-Wrapper הציעו. ואז הראיתי לו מה הוא היה עושה בסיליקון.
הוא לא שאל שוב על פרומפטים טובים יותר.
מה אם יכולתם להוכיח שקוד נכון במקום רק לבדוק אותו?
כאן הסיפור מתהפך. כי התשובה לבעיית ההזיות של LLM אינה פרומפטים טובים יותר, מודלים גדולים יותר, או יותר נתוני אימון. זו גישה שונה מהיסוד לאימות.
אימות מסורתי מסתמך על סימולציה — כותבים testbenches, מריצים מיליוני מחזורים, ובודקים אם העיצוב עושה את מה שאתם מצפים לו. זה כמו לבדוק את הבלמים של מכונית על ידי נסיעה סביב הבלוק אלף פעמים. אם הבלמים לא כושלים, מניחים שהם בטוחים. אבל מה אם הם כושלים רק כשיורד גשם, אתם נוסעים בדיוק 62 מייל לשעה, והרדיו מכוונן לתדר מסוים? סימולציה יכולה לאמת רק את התרחישים שהיא בודקת במפורש. כל השאר הוא תפילה.
אימות פורמלי אינו מריץ את העיצוב כלל. הוא ממיר את העיצוב כולו לנוסחה מתמטית ומשתמש בפותרני Satisfiability Modulo Theories (SMT) — כלים כמו Z3 של Microsoft — כדי להוכיח באופן ממצה שתכונה מתקיימת תחת כל צירוף קלט ומצב פנימי אפשריים. כל אחד ואחד. לא מדגם. לא קירוב סטטיסטי. הוכחה מתמטית.
סימולציה שואלת: "האם זה עובד במקרים שבדקתי?" אימות פורמלי שואל: "האם קיים מקרה אפשרי כלשהו שבו זה נכשל?" ההבדל הוא ההבדל בין תקווה להוכחה.
כשהפותרן מחזיר "UNSAT" — בלתי-ספיק — משמעות הדבר שאין דוגמה נגדית. התכונה מובטחת מתמטית. כשהוא מחזיר "SAT", הוא מוסר לך רצף ספציפי של קלטים ששובר את העיצוב שלך, עד למחזור השעון המדויק.
אימות פורמלי קיים כבר עשרות שנים. הסיבה שהוא לא השתלט על התעשייה היא שכתיבת התכונות הפורמליות — SystemVerilog Assertions, או SVA — קשה לשמצה. היא דורשת מערך מיומנויות מתמחה שאין לרוב צוותי העיצוב. ה-assertions הם ה"חוזה" של החומרה: "אם request עולה, grant חייב לבוא בתוך N מחזורים." "נתונים שנקראו מכתובת X חייבים להתאים לנתונים האחרונים שנכתבו לכתובת X." "הצנרת לעולם לא תיכנס לקיפאון." כתיבתן כראוי היא צורת אמנות, ואין מספיק מתרגלים בנמצא.
וכאן בדיוק ה-AI הופך לשימושי — לא לכתיבת קוד החומרה, אלא לכתיבת ההוכחה.
"הסנדוויץ' הפורמלי" — איך באמת בנינו את זה
ביליתי חודשים בוויכוח עם הצוות שלי על הארכיטקטורה הנכונה. הדיון היה עז, ובדיעבד, מבהיר. מחנה אחד רצה לכוונן LLM עד שייצר Verilog נכון כברירת מחדל. המחנה השני — זה שבסופו של דבר הצטרפתי אליו — טען שנכונות-על-ידי-אימון היא פנטזיה. אי אפשר לאמן החוצה את ההזיות. אפשר רק לתפוס אותן.
התכנסנו למה שאנחנו מכנים "הסנדוויץ' הפורמלי" — ארכיטקטורה נוירו-סימבולית שבה ה-LLM הוא המנוע היצירתי ופותרן אימות פורמלי הוא המבקר הבלתי-מתפשר. אף אחד מהם לא עובד לבד. יחד, הם עושים משהו שאף אחד מהם לא יכול לעשות באופן עצמאי.
הנה איך זה עובד בפועל. מעצב מספק מפרט — "עצבו גשר APB-to-AXI" או אפילו צילום מסך של תרשים תזמון. סוכן ה-Spec Analyzer שלנו מפרק זאת לדרישות פונקציונליות. ואז מגיע החידוש המרכזי: במקום לייצר רק קוד, ה-LLM מייצר שני ארטיפקטים בו-זמנית.
ארטיפקט A הוא מימוש ה-RTL — קוד ה-Verilog עצמו. ארטיפקט B הוא המפרט הפורמלי — קבוצה של תכונות SVA הנגזרות מאותן דרישות. אם המפרט אומר "Grant חייב לבוא אחרי Request", ה-LLM מייצר את מכונת המצבים וגם את ה-assertion שמוכיח שמכונת המצבים עושה את מה שהיא מצהירה.
ואז אנחנו משחררים את הפותרן. הוא לוקח את ארטיפקט A ומנסה לשבור אותו באמצעות ארטיפקט B. ראשית, בדיקת ריקנות (vacuity) — לוודא שה-assertions אינם נכונים באופן טריוויאלי (יצירה "עצלה" שבה תנאי ההדק לעולם אינו נורה). ואז בדיקת מודל חסומה, החוקרת מרחבי מצבים עמוקים — 50, 100 מחזורים לעומק — צדה קיפאונים, מצבי מרוץ, הפרות פרוטוקול.
אם הפותרן מוצא באג, הוא לא רק מסמן אותו. הוא מייצר עקבת דוגמה-נגדית — צורת גל מדויקת המראה בדיוק כיצד הבאג מתבטא. וכאן הלולאה נסגרת: אנחנו מזינים את העקבה הזו בחזרה ל-LLM כפרומפט. "העיצוב שלך נכשל. הנה העקבה: מחזור 1, Reset משתחרר. מחזור 2, Request עולה. מחזור 10, Grant עדיין נמוך. ה-grant מעולם לא הגיע. תקן את מכונת המצבים."
ה-LLM מנתח את העקבה, מזהה את מעבר המצב החסר, כותב מחדש את הקוד. הפותרן בודק שוב. הלולאה הזו חוזרת על עצמה אוטומטית עד שהעיצוב מוכח כנכון.
כתבתי על הארכיטקטורה הזו בהרבה יותר עומק בגרסה האינטראקטיבית של המחקר שלנו, אבל התובנה המרכזית פשוטה: אנחנו משתמשים ב-AI כדי לכתוב את ההוכחה, ובמתמטיקה כדי לבדוק את ה-AI. אף אחד לא בוטח בשני. שניהם הופכים זה את זה לטובים יותר.
הבאגים שהפכו אותי למאמין
הפכתי למאמין אמיתי בגישה הזו לא דרך תיאוריה אלא דרך באגים ספציפיים שתפסנו, שדבר אחר לא היה מוצא.
קהילת ה-RISC-V בקוד פתוח הפיקה ליבות מעבד מצוינות באמת — Ibex (המשמשת בשבב האבטחה OpenTitan של Google), פלטפורמת PULP מ-ETH ציריך. אלה עיצובים שנבחנים בקפדנות רבה עם כישרון הנדסי אמיתי מאחוריהם. ועדיין הם מכילים באגים שרק אימות פורמלי יכול למצוא.
Axiomise, חברת ייעוץ לאימות פורמלי, מצאה באג בליבת Ibex שבו בקשת ניפוי (debug) המגיעה במחזור מסוים במהלך הוראת הסתעפות עלולה לגרום לליבה להיכנס לקיפאון או לבצע את ההוראה הלא נכונה. חשבו על זה — ליבה קריטית-לאבטחה, שנסקרה על ידי עשרות מהנדסים, וכלי פורמלי מצא באג שהסימולציה החמיצה לחלוטין.
בפלטפורמת PULP, נמצא באג שבו ה-AXI interconnect עלול להרעיב מנהל אפיק (bus master) ללא הגבלת זמן תחת דפוס "עסוק" מסוים של אינטראקציות AWVALID ו-AWREADY. כשל liveness קלאסי — המערכת לא קורסת, היא פשוט מפסיקה להתקדם. לעולם לא הייתם כותבים בדיקה ממוקדת לדפוס האינטראקציה הספציפי הזה. יש יותר מדי דפוסים אפשריים מכדי למנות אותם.
כשאנחנו מכוונים את Veriprajna אל יחידת Load-Store של RISC-V, היא מייצרת אוטומטית assertions לתאימות ממשק ("אם valid מופעל, הוא חייב להישאר גבוה עד ready"), שלמות נתונים ("נתונים שנקראו מכתובת X תואמים לכתיבה האחרונה לכתובת X"), והתקדמות קדימה ("היחידה חייבת בסופו של דבר להחזיר תגובה"). אלה אינם מחשבות שלאחר מעשה שהוברגו על הקוד. הם נוצרים לצד הקוד, מאותו מפרט, ונאכפים לפני ששורה אחת של RTL עוזבת את המערכת שלנו.
לפירוט הטכני המלא של המתודולוגיה שלנו ומנוע האימות הפורמלי, ראו את מאמר המחקר המפורט שלנו.
"אבל אימות פורמלי אינו מתרחב"
אנשים תמיד מתנגדים לנקודה הזו, ואני מבין למה. לאימות פורמלי יש מוניטין של התפוצצות חישובית — מרחב המצבים של SoC מודרני הוא אסטרונומי בגודלו, וגישות פורמליות נאיביות נחנקות מכל דבר גדול יותר מעיצוב צעצוע.
השקענו מאמץ משמעותי בזה. המערכת שלנו משתמשת בטכניקות הפשטה אוטומטיות כדי להפוך את הפורמלי לבר-פתרון בקנה מידה. קופסה-שחורה (Black-boxing) מאפשרת לנו לאמת את לוגיקת הדבק תוך התייחסות לתת-בלוקים גדולים כמו RAM-ים או ALU-ים מורכבים כישויות מופשטות עם ממשקים מוגדרים. נקודות-חיתוך (Cut-points) שוברות מסלולי handshake של valid/ready כך שנוכל לאמת בקרת זרימה באופן בלתי-תלוי בעיבוד הנתונים. הפחתת סימטריה (Symmetry reduction) מאפשרת לנו להוכיח תכונה עבור ערוץ אחד של נתב רב-פורטים ולהסיק אותה מתמטית עבור כל N הערוצים.
האם זה נפתר לחלוטין? לא. פיזיקה אנלוגית תמיד תציב אתגרים ששיטות פורמליות לא יכולות לגעת בהם. אבל הבאגים הלוגיים — מצבי המרוץ, הקיפאונים, הפרות הפרוטוקול — הופכים לבלתי-אפשריים מתמטית בקוד המיוצר. ואלה הבאגים שגורמים לריספינים.
ההתנגדות האחרת שאני שומע נוגעת למהירות. "האם הרצת פותרן פורמלי לא מאטה את תהליך העיצוב?" כן, זה מוסיף עלות חישובית. אבל אני אחליף זמן חישוב בוודאות לוח-זמנים בכל יום ויום. פותרן פורמלי שרץ שעה נוספת זול לאין-שיעור מריספין של שישה חודשים.
האמת הלא-נוחה על "שבבים שעוצבו על ידי AI"
יש נרטיב שצובר תאוצה בתעשייה — שה-AI יעצב בקרוב שבבים מקצה לקצה, שאנחנו עוברים מעיצוב בעזרת מחשב (Computer-Aided Design) לעיצוב אוטומטי במחשב (Computer-Automated Design). אני מאמין שהנרטיב הזה נכון בכיוונו אך חסר באופן מסוכן.
אנחנו בונים לקראת זרימות עבודה אג'נטיות שבהן סוכני AI אוטונומיים משתפים פעולה — סוכן Architect לחלוקה ברמה גבוהה, RTL Coder למימוש, Verification Engineer לכתיבת testbenches ו-assertions, ו-Manager לתזמור הזרימה מול אילוצי הספק, ביצועים ושטח. אנחנו משתמשים ב-Retrieval-Augmented Generation (RAG) לא רק עבור קוד אלא עבור ידע — שולפים כללי פרוטוקול ספציפיים, אילוצי process design kit, ותקני קידוד פנימיים כך שה-LLM מייצר קוד תואם ללא הזיות.
אבל שום דבר מזה לא עובד — שום דבר מזה — ללא עמוד שדרה של אימות פורמלי. ככל שה-AI נעשה אוטונומי יותר, כך קריטי יותר שכל פלט יאומת מתמטית לפני שהוא ממשיך במורד הזרם. סוכן AI שמייצר קוד מהר יותר בעל ערך רק אם הקוד הזה נכון. סוכן AI שמייצר קוד מהר יותר וגם מוכיח שהוא נכון? זה העתיד.
הבעיה של תעשיית המוליכים למחצה אינה שה-AI איטי מדי בכתיבת קוד חומרה. הבעיה היא שה-AI מהיר מדי בכתיבת קוד חומרה שגוי באופן עדין.
אנחנו לא copilot. אנחנו לא צ'אטבוט. אנחנו בית-יציקה לאימות פורמלי שבמקרה משתמש ב-AI גנרטיבי כחזית שלו. ההבחנה חשובה כי היא קובעת למה אתם ממטבים. Copilots ממטבים למהירות. אנחנו ממטבים לנכונות. בעולם שבו באג בודד שנמלט עולה $10 מיליון במסכות ו-$50 מיליון בהכנסות אבודות, אני יודע איזה מיטוב הייתי בוחר.
הבחירה כבר נעשתה
תעשיית המוליכים למחצה כבר לא יכולה להרשות לעצמה את גישת "ייצר והתפלל". כלל העשר אינו הצעה — זו פיזיקה וכלכלה שחוברות יחד כדי להעניש כל מי ששולח סיליקון לא-מאומת. ב-5nm ומטה, עם סטי מסכות המתקרבים ל-$20 מיליון, שולי הטעות התכווצו לאפס.
כל שבוע, אני מדבר עם צוותי עיצוב שנרגשים ממה ש-LLM-ים יכולים לעשות לפרודוקטיביות שלהם ומבועתים ממה ש-LLM-ים עלולים לעשות ללוח הזמנים של ה-tape-out שלהם. הם צודקים כשהם מרגישים את שני הדברים בו-זמנית. הטכנולוגיה באמת מהפכנית. היא גם באמת מסוכנת ללא רשת ביטחון.
Veriprajna היא רשת הביטחון הזו. אנחנו נותנים לכם את מהירות ה-AI עם הוודאות של המתמטיקה. לא "כנראה נכון". לא "עבר רגרסיה". מוכח כנכון, על פני כל קלט אפשרי, כל מצב אפשרי, כל מקרה קצה אפשרי שסימולציה לעולם לא הייתה חושבת לבדוק.
הבחירה העומדת בפני כל מעצב שבבים כיום אינה האם להשתמש ב-AI. הרכבת הזו כבר יצאה מהתחנה. הבחירה היא האם להשתמש ב-AI שיכול להוכיח את עבודתו שלו, או ב-AI שרק מקווה לטוב.
אני יודע על איזה מהם הייתי מהמר $10 מיליון.
