Eski Axiom Math ve Kimi araştırmacıları bir araya gelerek girişim kurdu, yapay zeka ile çip doğrulama zorluklarını aşıyor

动察 Beating AI hızlı haber: Çip tasarımında en korkulan şeylerden biri, üretildikten sonra mantık hatasının fark edilmesidir. Bir sorun ortaya çıktığında, yeniden tasarım ve yeniden üretim gerekebilir, bu da yüksek maliyetlere yol açar. Çip doğrulama, bu gizli hataları üretimden önce mümkün olduğunca bulmayı amaçlar.

Geleneksel çip doğrulama esas olarak simülasyon testlerine dayanır, ancak çip içindeki çalışma durumu kombinasyonları astronomik sayılara ulaşabilir ve bunları tek tek test etmek imkansızdır. Biçimsel doğrulama ise matematiksel yöntemler kullanarak çipin belirtilen koşullar altında her zaman belirli bir kurala uyduğunu kanıtlar. Örneğin, aynı anda açılmaması gereken iki devre, özel bir işlem nedeniyle asla birlikte açılmamalıdır.

Bu yöntem uzun süredir mevcut, ancak karmaşık çipler için matematiksel kanıtlar çok zordur. Birçok sorunun uzmanlar tarafından manuel olarak ele alınması gerekir ve mevcut araçlar hesaplama ölçeği çok büyük olduğu için sonuç veremeyebilir.

Leiphone'un haberine göre, Axiom Math'in eski Biçimsel Doğrulama sorumlusu Zhang Jujian ve Moonshot AI'da AI matematiği üzerine araştırma yapan Liu Junqi, AI kullanarak daha fazla çip biçimsel kanıt çalışmasını otomatik olarak tamamlamak üzere Pekin Youlishu Technology'yi kurdu. Şirket tohum turu finansmanını tamamladı.

Her ikisinin de güçlü matematiksel kanıt geçmişi var. Zhang Jujian, Mathlib ve AxiomProver geliştirmelerine katıldı. Liu Junqi, 2025 Putnam Matematik Yarışması'nın 12 sorusunun tamamını başarıyla kanıtlayan ve kanıt sürecini Lean aracıyla doğrulayan Numina-Lean-Agent sisteminin baş yazarıdır.

Şu anda Youlishu teknik prototipi tamamladı ve yüz binlerce satır RTL kodu içeren çip projelerinde mevcut EDA araçlarının belirleyemediği bazı iddiaları doğruladı. Ekip, çip müşterileriyle işbirliği yaparak bu yeteneği ticari bir doğrulama hizmetine dönüştürmeye çalışıyor.