13 haber bu etiketle işaretlenmiş
Yazılım doğrulama çalışmalarında büyük dil modellerinin kullanımı artarken en büyük darboğaz, dillerin matematiksel kurallarını tanımlayan anlambilim (semantik) şartnamelerinin doğruluğu haline…
Lean ekibi, yapay zeka ajanlarının yazılımdaki açıkları bulma konusundaki etkinliğinin artması üzerine Lean kanıt asistanı için doğrulanmış yeni çekirdekler sundu. Lean v4.35.0 sürümüyle birlikte…
Aralarında Jeremy Avigad ve Kevin Buzzard'ın bulunduğu matematikçiler, yapay zeka sistemlerinin teorem kanıtlama yeteneklerini değerlendiren ortak bir yazı yayımladı. Metinde, son dönemde OpenAI ve…
Matematikçi Thomas Hales, Lean teorem kanıtlayıcısının güvenilirliği ve yapay zeka destekli otomatik biçimselleştirme süreçlerine dair teknik bir değerlendirme yayımladı. Gelişmiş dil modellerinin…
Araştırmacılar, yapay zeka modelleri tarafından üretilen matematiksel metinlerin Lean gibi biçimsel dillere otomatik çevrilmesi sürecinin güvenilirlik sorunları barındırdığını açıkladı. 6 Ekim 2026…
Büyük dil modellerinin ve yapay zeka sistemlerinin karmaşık matematiksel teoremleri çözmeye başlaması, matematik camiasında geniş çaplı bir tartışmayı ve tepki sürecini tetikledi. Birçok araştırmacı…
Vals araştırmacıları, negatif olmayan gerçel ağırlıklı yönlü çizgelerde en kısa yol problemini çözen C-HD adlı yeni bir deterministik algoritma geliştirdi. Yaklaşık 15 saat süren ve 733 mesajlaşma…
React çekirdek ekibinin eski üyelerinden Dan Abramov, 18 Eylül 2026 tarihinde yayımladığı yazıyla John Conway'in 50 yıllık omnifik tamsayılar varsayımını yapay zeka ajanları ve Lean kanıt yardımcısı…
zkSecurity araştırmacıları, Proximity Prize ekibi ve Ethereum Foundation ortaklığıyla kurulan better.codes platformundaki otomatik matematiksel araştırma süreçlerinde yaşanan güvenlik sorununu…
Trail of Bits araştırmacıları, matematiksel kanıt doğrulama dili Lean üzerinde çalışırken sistemin her türlü teoremi sahte biçimde kanıtlamasına yol açan bir yazılım hatası buldu. 4.33.1 sürümüne…
Yapay zeka şirketi Anthropic, dahili modellerinden birini ve prove2.me platformunu kullanarak Fermat'ın Son Teoremi'nin Lean programlama dilinde tam bir biçimsel kanıtını üretti. Gelişme, Freek…
Yazılımcı ve araştırmacı Paul Gruhn, teorem kanıtlama dili Lean'in arkasındaki temel mantığı TypeScript tip sistemini kullanarak modellediğini açıkladı. Curry-Howard izomorfizmine dayanan bu…