លេខកូដ AlphaProof និងសញ្ញា: ភស្តុតាងសុវត្ថិភាពលេខកូដម៉ាស៊ីនដែលបានត្រួតពិនិត្យ និងការសន្មត់ដែលគួរឱ្យទុកចិត្ត

អ្វីដែលវីដេអូនេះគ្របដណ្ដប់

• ភ្នាក់ងារ AI បង្កើតភស្តុតាងបេក្ខជន។ ឧបករណ៍ Lean's kernel ពិនិត្យមើលថាតើពួកគេបង្កើតការទាមទារផ្លូវការដែលមនុស្សបានអនុម័តឬអត់។
• គោលដៅដែលបានផ្ទៀងផ្ទាត់គឺជាខ្សែប្រយុទ្ធពាក្យបញ្ជា libsignal CLI ដែលបានចងក្រងជាក់លាក់មួយ ជាមួយនឹងអត្ថន័យដែលគួរឱ្យទុកចិត្ត និងកិច្ចសន្យាគ្រីបតូក្រាហ្វិក។
• ការបញ្ជាក់ពីគោលពីរដែលបានចងក្រងយកកម្មវិធីចងក្រង Rust ចេញពីមូលដ្ឋានដែលគួរឱ្យទុកចិត្តសម្រាប់លក្ខណៈសម្បត្តិដែលបានបញ្ជាក់របស់គោលពីរនោះ។
• អ្នកស្រាវជ្រាវរាយការណ៍ពីការណែនាំឡើងវិញដោយឯកោចំនួនពីរនៃកំហុសដែលបានជួសជុលពីមុនដែលបំពានលើទ្រឹស្តីបទសុវត្ថិភាពនិមិត្តសញ្ញារបស់ពួកគេ។
• ឧបករណ៍ប្រៀបធៀបពិនិត្យមើលទ្រឹស្តីបទ និងនិយមន័យដែលពាក់ព័ន្ធនីមួយៗប្រឆាំងនឹងការបញ្ជាក់ដែលបានការពារ និងអនុម័ត។ វិសោធនកម្មឆ្លងកាត់ដំណើរការត្រួតពិនិត្យដាច់ដោយឡែកមួយ។

កំណត់ត្រាដែលបានបកប្រែ

បកប្រែចេញពីការនិទានដើមជាភាសាអង់គ្លេស។ សំឡេង និងចំណងជើងរងដែលមានគឺស្ថិតនៅក្រោមការគ្រប់គ្រងរបស់ YouTube។

តើអ្នកណាពិនិត្យភស្តុតាងសុវត្ថិភាព AI?

0:00 ការសវនកម្មសុវត្ថិភាព AI នៅតែស្តាប់ទៅដូចជាការជឿទុកចិត្តលើឆាតបូត។ លទ្ធផល Signal ថ្មីរបស់ Google ភ្ជាប់មកជាមួយភស្តុតាងគណិតវិទ្យាដែលជា kernel ដាច់ដោយឡែកមួយ ពិនិត្យមើល។ នៅក្នុងវីដេអូនេះ តើ Google បានបញ្ជាក់អ្វីខ្លះ? ហើយតើពួកគេបញ្ឈប់ភ្នាក់ងារពីការផ្លាស់ប្តូរគោលដៅដោយរបៀបណា? នេះគឺជាចម្លើយដ៏មានប្រយោជន៍។ គំរូសរសេរភស្តុតាងបេក្ខជន ហើយ Lean ពិនិត្យភស្តុតាងប្រឆាំងនឹងការទាមទារដែល មនុស្សបានអនុម័តអំពីលេខកូដដែលបានចងក្រងដែលបានជ្រើសរើស។ មនុស្សនៅតែជាម្ចាស់ការទាមទារ និងការសន្មត់។

0:21 អ្នកអាចពិនិត្យមើលលទ្ធផលដោយមិនជឿលើសុន្ទរកថាជ័យជម្នះរបស់គំរូ។ ការត្រួតពិនិត្យដាច់ដោយឡែកមួយចាប់បានការផ្លាស់ប្តូរសំណួរដោយស្ងៀមស្ងាត់។ យើងនឹងតាមដានវាចុះទៅនិយមន័យ។ វាជាថ្ងៃអង្គារ ទីដប់ ខែវិច្ឆិកា ហើយនេះគឺជា The Daily Diff។ លេខកូដ AlphaProof គឺជាក្របខ័ណ្ឌរបស់ Google សម្រាប់ការសរសេរការបញ្ជាក់កម្មវិធីដោយមាន ការណែនាំពីមនុស្ស និងការបង្កើតភស្តុតាងដែលបានពិនិត្យដោយភ្នាក់ងារ AI ។ ការសិក្សានេះកំណត់គោលដៅ libsignal ដែលជាបណ្ណាល័យ Rust ដែលអនុវត្តពិធីការផ្ញើសាររបស់ Signal នៅក្នុងកម្មវិធីពាក្យបញ្ជាជាក់លាក់មួយ។

0:45 Google បានប្រកាសពីការងារនេះនៅថ្ងៃនេះ។ ឯកសាររបស់វាបាននិយាយថាអ្នកស្រាវជ្រាវ ៥ នាក់បានធ្វើការអស់រយៈពេល ៤ សប្តាហ៍។ ភ្នាក់ងារបានសរសេរភស្តុតាង ខណៈដែលមនុស្សបានចំណាយការខិតខំប្រឹងប្រែងភាគច្រើនរបស់ពួកគេលើ ការបញ្ជាក់។ តម្រូវការបានរកឃើញវិធីដើម្បីក្លាយជាការប្រជុំដែលមានតម្លៃថ្លៃជាងមុន ។ ការបញ្ជាក់បាននិយាយថាអ្វីដែលកម្មវិធីត្រូវធ្វើ

តើការទាមទារក្លាយជាគោលដៅភស្តុតាងដោយរបៀបណា?

0:59 អ្វីដែលអ្នកវាយប្រហារគ្រប់គ្រង និងការសន្មត់ណាដែលអំណះអំណាងត្រូវការ។ អ្នកត្រួតពិនិត្យសួរថាតើវាចាប់យកសុវត្ថិភាពដែលមនុស្សខ្វល់ខ្វាយឬអត់។ ចម្លើយដែលបានពិនិត្យយ៉ាងស្រស់ស្អាតចំពោះសំណួរខ្សោយទុកសំណួរនោះនៅដដែល។ ក្រុមនេះបង្កើតឡើងលើការស្រាវជ្រាវពីមុនទៅក្នុងការចាប់ដៃរបស់ Signal និង ratchet គន្លឹះសាររបស់វា។ ការវិភាគផ្លូវការបានសិក្សារួចហើយនូវការរចនាទាំងនោះ។ ការទាមទាររបស់ Google ភ្ជាប់អំណះអំណាងសុវត្ថិភាពរបស់ពួកគេទៅនឹងការអនុវត្តដែលបានចងក្រងបណ្ណាល័យ ផលិតកម្មដែលមិនបានកែប្រែ ដែលការរចនាត្រូវតែរួចជីវិតពីការទំនាក់ទំនងជាមួយលេខកូដ ពិតប្រាកដ។ ប្រធានផ្នែកបច្ចេកវិទ្យារបស់ Signal លោក Ehren Kret

1:27 ពិពណ៌នាអំពីការពង្រីកលើសពីវិសាលភាពតូចៗនៃការផ្ទៀងផ្ទាត់ពីមុន។ ព័ត៌មានលម្អិតនៃការអនុវត្តរួមមានសារដែលមិនមានលំដាប់ និងវគ្គដែលបានទុកក្នុងប័ណ្ណសារសម្រាប់សារដែល ពន្យារពេល។ កម្មវិធីពិតរក្សាទុកបង្កាន់ដៃដែលគំនូរដ្យាក្រាមដ៏ឆើតឆាយរបស់អ្នកបានបោះចោល។ អ្នកស្រាវជ្រាវចងក្រងបណ្ណាល័យ Rust ដែលមិនបានកែប្រែជាមួយនឹងកម្មវិធីចងក្រងស្តង់ដារ

ហេតុអ្វីបានជាត្រូវបញ្ជាក់គោលពីរដែលបានចងក្រង?

1:41 ទៅជា Arm 64 Linux executable ។ ទ្រឹស្តីបទរបស់ពួកគេពិពណ៌នាអំពីគោលពីរនោះដោយប្រើគំរូការណែនាំផ្លូវការ ឈានដល់គម្លាតរវាងប្រភព និងលេខកូដម៉ាស៊ីនដែលបានបង្កើនប្រសិទ្ធភាព។ កំហុសកម្មវិធីចងក្រងដែលបំពានលក្ខណសម្បត្តិដែលបានបញ្ជាក់នឹងធ្វើឱ្យទ្រឹស្តីបទរបស់វាខុស។ ដូច្នេះ កម្មវិធីចងក្រងទុកមូលដ្ឋានដែលគួរឱ្យទុកចិត្តសម្រាប់គោលពីរនេះ។ អ្នកនៅតែជឿទុកចិត្តលើគំរូការណែនាំ និងកម្មវិធីត្រួតពិនិត្យរបស់ Lean ។ ព្រំដែនទំនុកចិត្តបានផ្លាស់ប្តូរ ហើយវាមានអាសយដ្ឋាន។ ភស្តុតាងដែលបានពិនិត្យប្រហែលប្រាំមួយលានកន្លះបន្ទាត់គឺផ្អែកលើប្រហែលម្ភៃប្រាំមួយ

2:06 ពាន់បន្ទាត់នៃការបញ្ជាក់ដែលគួរឱ្យទុកចិត្ត និងអត្ថន័យការណែនាំ។ ទាំងនេះគឺជាចំនួនវត្ថុបុរាណ។ ការចាត់ទុកពួកវាជាពិន្ទុភាពវៃឆ្លាតគឺដូចជាការចាត់ថ្នាក់អ្នកអភិវឌ្ឍន៍តាមទំហំនៃ ថតម៉ូឌុលថ្នាំងរបស់ពួកគេ។

តើលក្ខណៈសម្បត្តិសុវត្ថិភាពអ្វីខ្លះដែលបានរួចជីវិតពីគម្លាតនៃការអនុវត្ត?

2:16 អំណះអំណាងគ្របដណ្តប់លើការសម្ងាត់សារ និងការផ្ទៀងផ្ទាត់ភាពត្រឹមត្រូវ ជាមួយនឹងការសម្ងាត់ទៅមុខ និងសុវត្ថិភាពក្រោយការសម្របសម្រួលក្រោមគំរូដែលបានបញ្ជាក់។ ពីរចុងក្រោយពិពណ៌នាអំពីដែនកំណត់លើការខូចខាតគន្លឹះដែលត្រូវបានលួច និងការងើបឡើងវិញបន្ទាប់ពីការផ្លាស់ប្តូរ ថ្មីៗ។ ការធានានីមួយៗមានលក្ខខណ្ឌលើអ្នកវាយប្រហារ និងវគ្គ។ វត្ថុបុរាណគ្រីបតូក្រាហ្វិកស្ថិតនៅពីក្រោយកិច្ចសន្យាដែលគួរឱ្យទុកចិត្ត។ ភស្តុតាងសន្មត់ថារបៀបទាំងនោះមានឥរិយាបថដូចដែលបានបញ្ជាក់ ហើយពឹងផ្អែកលើការសន្មត់ សុវត្ថិភាពគ្រីបតូក្រាហ្វិក។ ភស្តុតាងមួយធ្វើឱ្យគ្រីបតូក្រាហ្វិកល្អឥតខ្ចោះ។ មួយទៀតពិភាក្សាអំពី ប្រូបាប៊ីលីតេជោគជ័យរបស់អ្នកវាយប្រហារ។

2:42 ទាំងពីរមានការរឹតបន្តឹងលើសេណារីយ៉ូដែលពួកគេគ្របដណ្តប់។ សួរថាការបង្កើតណា លក្ខណសម្បត្តិណា និងការសន្មត់ណា។ លទ្ធផលនេះទាក់ទងនឹងខ្សែប្រយុទ្ធពាក្យបញ្ជារបស់អ្នកស្រាវជ្រាវ។ ការផ្ញើសារជាក្រុមគឺជាការងារនាពេលអនាគត ហើយគំរូគណនាបដិសេធ ស្ថានភាពពហុឧបករណ៍។ ការហៅការដំឡើង Signal ទាំងអស់ថាមិនមានកំហុសគឺនៅក្រៅ ទ្រឹស្តីបទ។ អ្នកស្រាវជ្រាវបានណែនាំឡើងវិញនូវកំហុស Signal ដែលបានជួសជុលពីមុនចំនួនពីរទៅក្នុង

តើការបញ្ជាក់អាចបដិសេធលេខកូដខូចបានទេ?

3:02 ចម្លងដោយឯកោហើយចងក្រងពួកវា។ ភស្តុតាងដែលបានពិនិត្យបានបង្ហាញថាគោលពីរទាំងនោះបំពានទ្រឹស្តីបទសុវត្ថិភាពនិមិត្តសញ្ញា។ នោះបានសាកល្បងថាតើការបញ្ជាក់អាចបដិសេធការអនុវត្តដែលខូចពិតប្រាកដឬអត់។ សញ្ញាធីកពណ៌បៃតងរបស់អ្នកត្រូវការការធ្វើតេស្តពណ៌ក្រហម។ Google បោះពុម្ពផ្សាយការបញ្ជាក់ និងភស្តុតាងជាមួយនឹងការណែនាំត្រួតពិនិត្យ។ ឃ្លាំងទិន្នន័យបាននិយាយថាការបង្កើតថ្មីមួយចំណាយពេលរាប់ម៉ោង និងការចងចាំច្រើន។ ការអានសេចក្តីប្រកាសគឺងាយស្រួលជាងនៅលើកុំព្យូទ័រយួរដៃ។ គំរូផ្នែករឹង និងកិច្ចសន្យាដែលគួរឱ្យទុកចិត្តនៅតែត្រូវការការពិនិត្យឡើងវិញ។

3:26 ខ្ញុំមិនទាន់បានបង្កើតឡើងវិញនូវវត្ថុបុរាណដ៏ធំសម្បើមសម្រាប់វគ្គនេះទេ។ យើងកំពុងរាយការណ៍ពីលទ្ធផលដែលបានបោះពុម្ពផ្សាយ និងដែនកំណត់របស់វា។ អ្នកខាងក្រៅមានផ្លូវដើម្បីត្រួតពិនិត្យវា ដែលសំខាន់ជាងសម្រាប់ខ្ញុំជាងជ័យជម្នះ AI មួយទៀត។ ឥឡូវនេះអន្ទាក់។

តើភស្តុតាងត្រឹមត្រូវអាចឆ្លើយសំណួរខុសបានទេ?

3:36 Lean អាចទទួលយកភស្តុតាងត្រឹមត្រូវនៃសេចក្តីថ្លែងការណ៍ដែលស្ទើរតែមិនទាមទារអ្វីទាំងអស់។ ការសន្មត់មិនអាចទៅរួចអាចធ្វើឱ្យទ្រឹស្តីបទគ្មានន័យ។ ការផ្លាស់ប្តូរនិយមន័យដែលកប់នៅក្រោមទ្រឹស្តីបទចំណងជើងអាចធ្វើឱ្យគោលដៅ ចុះខ្សោយ។ ឯកសារនេះរចនាការត្រួតពិនិត្យប្រឆាំងនឹងបញ្ហានេះ។ អ្នកយាមទ្វាររក្សាការបញ្ជាក់ដែលបានអនុម័តដែលភ្នាក់ងារភស្តុតាងមិនអាច សរសេរបាន។ ពួកគេអាចស្នើការកែតម្រូវតាមរយៈដំណើរការវិសោធនកម្មដាច់ដោយឡែកមួយ។ ការចុះខ្សោយសុវត្ថិភាពត្រូវបានបង្កើនជាកំហុសដែលអាចកើតមាន។ ការប្រកាសជោគជ័យរបស់អ្នកបញ្ជាក់មិនមានសិទ្ធិអំណាចនៅទីនេះទេ។

4:00 មនុស្សសម្រេចចិត្តលើការផ្លាស់ប្តូរការសន្មត់ដែលគួរឱ្យទុកចិត្ត ដោយផ្ទាល់ ឬតាមរយៈគោលការណ៍របស់ពួកគេ និងពិនិត្យវិសោធនកម្មបន្ទាប់ពីយុទ្ធនាការនីមួយៗ។ ការវិនិច្ឆ័យរបស់អ្នកជំនាញនៅតែស្ថិតក្នុងទំនួលខុសត្រូវ។ ភ្នាក់ងារអាចស្នើសុំការចាត់តាំងផ្សេងគ្នា។ វាមិនអាចផ្តល់ឱ្យខ្លួនឯងនូវពិន្ទុឆ្លងកាត់បានទេ។

តើអ្វីដែលចាប់បានគោលដៅដែលកំពុងផ្លាស់ប្តូរ?

4:13 នេះគឺជាការត្រួតពិនិត្យដែលបានសន្យា។ ឧបករណ៍ប្រៀបធៀបរបស់ Lean ប្រៀបធៀបទ្រឹស្តីបទ និងនិយមន័យនីមួយៗដែលវាពឹងផ្អែកលើជាមួយ ចម្លងដែលបានការពារ និងអនុម័តនោះ។ វាក៏ពិនិត្យមើល axiom ដែលអនុញ្ញាត និងចាក់ឡើងវិញនូវភស្តុតាងនៅក្នុង kernel ថ្មី។ ការចុះខ្សោយដោយស្ងៀមស្ងាត់នូវនិយមន័យជំនួយ ដូច្នេះផ្លាស់ប្តូរអ្វីដែលកំពុងត្រូវបាន ប្រៀបធៀប។ ភស្តុតាងដែលទទួលយកត្រូវតែបង្កើតគោលដៅដែលបានអនុម័ត។ នោះនៅតែទុកឱ្យមនុស្សទទួលខុសត្រូវក្នុងការជ្រើសរើសគោលដៅដ៏រឹងមាំ និងការសន្មត់ ស្មោះត្រង់។ សម្រាប់លំហូរការងារ AI ផ្ទាល់ខ្លួនរបស់អ្នក រក្សាទុកលក្ខណៈវិនិច្ឆ័យទទួលយកនៅខាងក្រៅ

4:37 សិទ្ធិកែសម្រួលរបស់កម្មករ និងពិនិត្យការផ្លាស់ប្តូរដែលបានស្នើឡើងដោយឡែកពីគ្នា។ លទ្ធផលរបស់ Google ធ្វើឱ្យការបំបែកនោះជាក់ស្តែង។ អ្នកសរសេរភស្តុតាងធ្វើការងារ ព្រំដែនត្រួតពិនិត្យសម្រេចចិត្តថាតើវាត្រូវបានរាប់បញ្ចូលឬអត់។ ប្រសិនបើអ្នកចង់អាននេះជាងស្តាប់ខ្ញុំនិយាយ វាបានធ្លាក់ចូលក្នុងប្រអប់សំបុត្ររបស់អ្នក រៀងរាល់ព្រឹក ឥតគិតថ្លៃនៅ daily diff dot dev តំណភ្ជាប់ខាងក្រោម។ ដូច្នេះសាលក្រមថ្ងៃនេះគឺ SHIP IT ។

តើខ្ញុំនឹងអនុវត្តលំហូរការងារភស្តុតាងនេះទេ?

4:54 ខ្ញុំនឹងអនុវត្តលំហូរការងារភស្តុតាងដែលបានត្រួតពិនិត្យនេះ ពីព្រោះការទាមទារដែលបានអនុម័តនៅតែដាច់ដោយឡែក ពីភ្នាក់ងារដែលផលិតចម្លើយ។ ខ្ញុំនឹងរក្សាលក្ខណៈវិសាលភាព និងការសន្មត់ដែលភ្ជាប់ទៅនឹងលទ្ធផលនីមួយៗ។ ជាវ ចុចកណ្ដឹង ហើយប្រាប់ខ្ញុំនៅក្នុងមតិយោបល់ ប្រសិនបើអ្នកបានបោះត្រាវា ខុសគ្នា។ ហើយនោះគឺជាភាពខុសគ្នាសម្រាប់ថ្ងៃនេះ។ ខ្ញុំឈ្មោះ Niko មកពី Axrisi។ បញ្ចូលដោយការទទួលខុសត្រូវ។

ប្រភព

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub