Axiom Math sê sy KI-agente het die Stacks Project, ’n belangrike wiskundige naslaanwerk, formeel geverifieer. Die resultaat is sowat 16 miljoen reëls rekenaargekontroleerde kode, gegrond op ongeveer 7,654 bladsye wiskunde.
Axiom Math het KI-agente wat parallel werk, gebruik om die wiskundige biblioteek in Lean-kode om te skakel. Die agente het binne ’n los hiërargie self take geïdentifiseer, eerder as om gedetailleerde instruksies vir elke stap te ontvang.
Die Stacks Project het in 2005 begin as ’n oopbron-naslaanwerk oor algebra, meetkunde en getalteorie. Lean stel wiskundiges in staat om bewyse as kode uit te druk wat ’n bewysassistent reël vir reël nagaan. Axiom moes ook die verbande tussen definisies en stellings deur die hele biblioteek behou.
Vir maatskappye wat KI-agente bou, is die breër doel ’n herbruikbare grondslag van gekontroleerde kennis om sagteware te skryf en uiteindelik wetenskaplike werk te doen. Formele verifikasie help ingenieurs reeds om skyfieontwerpe na te gaan, maar Axiom se strewe om sy wiskundige vermoëns na sagteware oor te dra, bly ’n waagstuk eerder as ’n bewese uitkoms.
’n Groot versameling gekontroleerde wiskunde kan toekomstige KI-bewyse op geverifieerde resultate laat voortbou, eerder as om van voor af te begin.
Die projek demonstreer hoe KI-agente wat parallel werk, komplekse, onderling gekoppelde tegniese werk kan verdeel.
Ontwikkelaars moet onderskei tussen die voltooide wiskundige formalisering en die steeds onbewese belofte van betroubaarder sagteware wat deur KI geskryf word.
Outomaties geskryf deur die Made in 10-nuuskamer uit die bron hierbo.
Isomorphic Labs is in gesprek om sowat $5 miljard teen ’n waardasie van sowat $50 miljard in te samel, berig Bloomberg. Die finansiering is nog nie afgehandel nie, en die maatskappy se werk aan KI-geneesmiddelontdekking is steeds in die prekliniese fase.
