STARK’ta 200’den 148’e: 3 matematik problemi yayımlandı, düşüş olasılığı masada

STARK kanıtlarında doğrulama sayısını azaltmaya yönelik üç matematik problemi yayımlandı. Görev sayfasındaki hesaplama örneğine göre, belirli koşullarda 100 bit güvenlik için gereken doğrulama sayısı 200’den 148’e düşebilir. Ancak bu hesap, hedef kanıtın ispatlanmasına ve güvenliğin bütün olarak analiz edilmesine bağlı.

provably.fast’in resmî görev sayfasında üç hedef yer alıyor. Her önerme, matematiksel teorem kanıtlama aracı Lean’de tanımlanmış durumda; yalnızca bağımsız incelemeden geçen kanıtlar çözüm kabul ediliyor. Üç hedefin tamamı hâlâ açık.

STARK, hash fonksiyonlarına dayalı bir sıfır bilgi kanıt sistemi. Reed-Solomon kodları, bu sistemde doğrulanacak verinin güvenilirliğini ele almak için kullanılıyor. Doğrulayıcı, sunulan verinin kod yapısına ne kadar yakın olduğunu kontrol etmek üzere rastgele kombinasyonları inceliyor.

Görevler, bu kontrol sırasında hatalı verinin geçerli bir kod gibi görünmesine yol açabilecek ‘kötü meydan okuma değerlerinin’ sayısını sınırlamaya odaklanıyor. Bu değerler için üst sınırın düşürülmesi, doğrulamada gereken rastgele kontrollerin azaltılmasını sağlayabilir. Ancak üst sınırdaki iyileşme tek başına kanıt boyutunu veya güvenliği değiştirmiyor.

Hedefler, kodun kabul oranı aralıklarına göre ayrılıyor. T1, birinci sınır ile Johnson sınırı arasındaki aralıkta bilinen ikinci dereceden üst sınırı doğrusal bir sınıra indirmeyi amaçlıyor. T2 ise birinci sınırın altındaki daha geniş aralıkta ikinci dereceden bir üst sınırın kanıtlanmasını hedefliyor.

T3, kanıt üretiminde kullanılan değerlendirme alanının üst sınırını ele alıyor. Görev sayfası, kabul oranının 5/8 ve oranın 1/2 olduğu ilk örnekte, mevcut yapıda kötü meydan okuma değerlerinin sayısının 114n/16’ya ulaşabildiği koşullar için 16n üst sınırının kanıtlanmasını istiyor.

Sayfadaki doğrulama sayısı örneği FRI yöntemi, 1/2 oranı, n=2²⁰ ve 124 bitlik alan gibi belirli koşullara dayanıyor. Bu hesapta 100 bit güvenlik için gereken kontrol sayısı şu anda 200. T3’ün ilk örneği kanıtlanırsa bu sayı 148’e iniyor. Sayfa, hesabın yalnızca kontrol sayısıyla sınırlı olduğunu ve uygulama için güvenliğin bütün olarak analiz edilmesi gerektiğini belirtiyor.

Önceki bir araştırma, matematiksel üst sınırları gerçek uygulamalardaki kanıt boyutlarıyla ilişkilendirdi. Quang Dao, Scott Duke Kominers ve Justin Thaler’ın 17 Eylül’de kayda geçirdiği ön baskıda, aynı güvenlik hedefi altında ProveKit’in pasaport kanıtının 79,4 KB (yüzde 11,1), ZisK’nin sıkıştırılmış nihai kanıtının 13,2 KB (yüzde 4,63) ve LambdaVM’in CPU alt kanıtının 59,8 KB (yüzde 4,85) küçüldüğü bildirildi. Bu sonuçlar makalede ele alınan belirli uygulama ve ayarlardan elde edildi.

Sonuçların uygulanabileceği alanın sınırları da var. 9 Ekim’de yayımlanan ayrı bir makale, ikili alanlarda Johnson sınırının altındaki yakınlık aralığının geçerli olmadığına dair bir karşı örnek sundu. Görev sayfasındaki arka plan açıklamasına göre bu bulgu, yeterince büyük karakteristiğe sahip alanları koşul olarak belirleyen mevcut hedefleri ne çözüyor ne de çürütüyor.

İnsanlar ve yapay zekâ ajanları görevlere katkıda bulunabiliyor; fikirler, yardımcı önermeler, karşı örnekler ve kanıtlar kayda geçiriliyor. OpenAI’ın kurum içi modellerinin matematik sonuçlarını ve bazı Lean biçimselleştirmelerini yayımlaması gibi, biçimselleştirilmiş matematik sonuçlarının paylaşımı da sürüyor.

Üç açık görevin çözüldüğüne veya gerçek STARK uygulamalarında kanıt boyutunun daha da küçüldüğüne dair henüz bir sonuç yok. Matematiksel üst sınırlar kanıtlansa bile gerçek etkisini görmek için ilgili protokollerin güvenliği ve kanıt boyutu ayrıca incelenmeli.