Sinir ağları, güvenlik ve görev açısından kritik sistemlerde giderek daha fazla kullanılmasına rağmen, doğrulama ve analiz sonuçları genellikle modelin tanımlandığı ve çalıştığı programlama ortamının dışında üretilir. Bu ayrım, yürütülen ağ ile analiz edilen yapı arasında anlamsal bir boşluk oluşturur. Bu durum, operatör anlambilimi, tensör düzenleri, ön işleme ve kayan nokta köşe durumları gibi örtük kurallara dayanan garantilere yol açabilir ve potansiyel güvenlik açıklarını beraberinde getirebilir.
Bu sorunu çözmek için, Lean 4 teorem ispatlayıcısında geliştirilen TorchLean adlı bir framework tanıtılıyor. TorchLean, öğrenilmiş modelleri hem yürütme hem de doğrulama için tek, kesin bir anlambilimi paylaşan birinci sınıf matematiksel nesneler olarak ele alır. Framework, PyTorch tarzı doğrulanmış bir API'yi (istekli ve derlenmiş modlarla) paylaşılan bir op-etiketli SSA/DAG hesaplama grafiği IR'sine indirger. Ayrıca, yürütülebilir bir IEEE-754 binary32 çekirdeği ve ispatla ilgili yuvarlama modelleri aracılığıyla açık Float32 anlambilimi sunar. Doğrulama ise IBP ve CROWN/LiRPA tarzı sınır yayılımı ve sertifika kontrolü ile gerçekleştirilir.
TorchLean, sertifikalı sağlamlık, PINN'ler için fizik tabanlı kalıntı sınırları ve Lyapunov tarzı nöral denetleyici doğrulaması gibi alanlarda uçtan uca doğrulamayı başarıyla göstermiştir. Ayrıca, evrensel yaklaşıklık teoremi de dahil olmak üzere mekanize edilmiş teorik sonuçlar sunar. Bu sonuçlar, öğrenme özellikli sistemlerin tamamen resmi, uçtan uca doğrulaması için anlambilim odaklı bir altyapının mümkün olduğunu kanıtlamaktadır.
TorchLean, yapay zeka modellerinin hem çalıştırılması hem de doğrulanması için tek, kesin bir anlambilim sağlayarak, kritik sistemlerdeki sinir ağlarının güvenilirliğini ve şeffaflığını artırıyor.