Kanıtlanabilir Simülasyon: Doğrulanabilir Karar Altyapısı

1Sorun: karar için güvenilebilir simülasyon

Makul görünen bir sahne çizen fizik motoru çözülmüş bir problemdir. Çıktısına güvenip eyleme geçtiğinizbir simülasyon değildir. Bir simülasyon gerçek bir kararı beslediği an — angaje ol ya da bekle, sevk et ya da durdur, sensöre güven ya da güvenme — üç soru kaçınılmaz olur:

• Tekrar-üretilebilirlik:aynı senaryoyu başka bir makinede tekrar koşarsak aynı cevabı alır mıyız?
• Atıf:simülasyon ile gerçeklik ayrıştığında bu model hatası mı, gerçek arıza mı, müdahale mi?
• Savunulabilirlik:sistemin ne hesapladığını ve neden hesapladığını sonradan kanıtlayabilir miyiz?

Çoğu simülasyon yığını için üçünün de dürüst cevabı "pek sayılmaz"dır. Bu boşluk bir arayüz sorunu değildir; demo ile enstrüman arasındaki farktır.

2Kayan-nokta simülasyonu güven testini neden geçemez

IEEE-754 kayan-nokta sonuçları derleyici bayraklarına, FMA varlığına, komut sırasına ve iş-parçacığı zamanlamasına bağlıdır. Aynı kod farklı bir işlemcide son bitlerde biraz farklı sonuç verebilir; bu minik farklar simülasyon zaman çizgisinde birikir. Üç sonuç doğar:

Determinizm çoğu zaman lockstep çok-oyunculuk için "olsa iyi olur" gibi görülür. Karar-sınıfı simülasyon içinse diğer her şeyin üstünde durduğu temeldir.

3Replay neden gerekli — ama yetersiz

Kayıt-tekrar (record-replay) ciddi bir yığının eklediği ilk şeydir: tohum ve sıralı girdiler alınırsa bir koşum yeniden üretilebilir. Bu "ne oldu?" sorusunu yanıtlar ve hata ayıklama ile denetim için şarttır. Ama iki sınırı vardır. Birincisi, float motorda replay yalnız aynıikili dosyada tekrar-üretilebilir — çapraz-platform bir kanıt değildir. İkincisi ve daha temeli: replay yalnız fiilen gerçekleşen zaman çizgisini anlatır. Karar vericinin asıl sorduğu soruyu yanıtlayamaz:

Bunu yanıtlamak, anı olası geleceklere dallandırmayı gerektirir. Replay bir çizgidir; kararlar bir ağaçta yaşar.

4Çatallama neden eksik katman

Bir simülasyon deterministikse ve tüm durumunu snapshot/restore edebiliyorsa, herhangi bir canlı andan onu çatallayabilirsin: snapshot al, A dalını bir planla koştur, geri yükle, B dalını başka bir planla koştur, ve böyle devam. Her dal, skorlanabilir (bu sonuç ne kadar iyi?) ve hash'le adreslenebilir (bu tam olarak hangi gelecek?) bir durumda biter. Çekirdek deterministik olduğundan, aynı taban + aynı plan her zaman aynı dalı verir — yani ürettiğin seçenekler tekrar-üretilebilir ve savunulabilirdir, tek-seferlik bir Monte-Carlo ürünü değil.

İzleme ile karar desteği arasındaki fark budur:

Danışman, anı eylem-planı (COA) dallarına çatallar ve sıralar; Gölge İkiz, gerçek varlığın yanında aynı girdilerle koşan deterministik bir kopya çalıştırır ve ölçülen durum tahminden ayrıldığı ilk karede alarm verir. İkisi de aynı deterministik çekirdeğin operasyonel yüzüdür.

5Hash: kanıtlanabilirliği bağlayan öğe

Deterministik bir koşum, her adımda 64-bitlik bir state_hashüretir — taşınan tüm durumun parmak izi. Bu tek değer muazzam iş görür:

• Çapraz-platform kanıt:hash'te anlaşan iki makine simülasyonun her bitinde anlaşır. CI bunu her değişiklikte Linux, Windows ve macOS'ta doğrular.
• Kurcalamaya-duyarlılık:bir koşum raporu metadata-tohumlu hash zinciriyle mühürlenebilir; herhangi bir kareyi, parametreyi veya mührün kendisini oynatmak doğrulamayı kırar. Rapor imzayla değil senaryoyu yeniden koşturarakkanıtlanır — noterin yerini fizik alır.
• Adreslenebilir gelecekler:her çatal dalı sonuç hash'iyle tanımlanır; bir eylem planı alıntılanabilir, karşılaştırılabilir ve birebir yeniden üretilebilir.
• Sapma adli analizi:iki kare-başı hash izini karşılaştırmak, iki koşumun (ya da bir koşum ile gerçekliğin) ayrıldığı ilk kareyi tam olarak gösterir.

6Berk DT bu dördünü nasıl sağlar

Tek bir Rust çekirdeği, C-ABI (ve Unity, Unreal, WebAssembly bağlamaları) üzerinden şunları verir:

• Deterministik:tüm simülasyon matematiği sabit-nokta (Q32.32) tamsayıdır; trigonometri CORDIC, karekök deterministik tamsayı yöntemiyle. state_hash'i besleyen duruma hiçbir IEEE float değmez.
• Tekrar-oynatılabilir:tohum + sıralı girdi + periyodik hash bir koşumu birebir üretir ve sapmayı yakalar; tam snapshot/restore taşınan durumu bayta ve geri, bit-aynı serileştirir.
• Çatallanabilir:Danışman (deterministik ne-olur ağacı) ve rollback netcode aynı atomik snapshot yolunu paylaşır — bir dal tabanını asla bozamaz.
• Kanıtlanabilir:çapraz-platform golden-hash CI, kurcalamaya-duyarlı denetim rapor aracı, sapma hata-ayıklayıcısı ve eşzamanlılık/karar mantığının formal (TLA+) modelleri.

7Bunun açtığı alan

Savunma — karar güvenliği

Seçenek uzayının tek-seferlik senaryo yerine kanıtlanabilir olduğu COA analizi; bir saha olayının (deterministik loglanan girdilerle) bit-bit yeniden üretildiği ve alternatif karar dallarının keşfedildiği olay-sonrası analiz; dış bağımlılığı olmayan kapalı-ağ (air-gapped) dağıtım; her kararın epistemik durum, yetki seviyesi ve provenans hash'i taşıdığı denetlenebilir otonomi.

Endüstri — operasyon optimizasyonu

What-if planlama için operasyonel gelecek ağacı (duruş optimizasyonu, tedarik-zinciri çatalları); kullanışlı olacak kadar dar eşikli kestirimci bakım ve anomali/müdahale tespiti için gölge ikiz; her koşumun tekrar-üretilebilir denetimi.

Robotik / AI — sim-to-real doğrulama

Tekrar-üretilebilir eğitim ve değerlendirme; kapalı sensör-döngü replay için deterministik sensör (LiDAR/menzil) simülasyonu; GPU eğitim yığınlarının yanında tamamlayıcı bir "yer-gerçeği yürütme katmanı". Her yerde eğit; kanıtlanabilir yürüt.

8Determinizmin garanti etmediği

Bu konumun tüm güvenilirliği, sınırları konusunda net olmaya bağlıdır. Burada abartmak teknik bir kitleyi kaybetmenin yoludur — o yüzden açıkça söylüyoruz:

Bunlar gizlenecek zayıflıklar değil; içindeki her şeyi güvenilir yapan sınırdır. Bu anlatının en güçlü hali, dürüst halidir.

9Kanıtı kendin üret

Yukarıdaki her iddia, depoda yaşayan ve istendiğinde yeniden koşan artefaktlarla desteklenir:

# Determinizm: golden hash her platformda birebir aynı
cargo test --release --test determinism_dynamics

# Adli rapor: koşumu üret, sonra İMZAYLA değil FİZİKLE yeniden doğrula
cargo run --bin berk-audit -- run
cargo run --bin berk-audit -- verify report.json

# Ölçek: 10.001 gövdede iki farklı broadphase AYNI hash'i üretir
cargo test --release --test scale_10k -- --ignored --nocapture

# ~1050 test, 0 hata
cargo test

Canlı, tarayıcı-içi kanıtlar: Hash Mutabakatı (aynı sim her cihazda aynı parmak izini verir), CPU ≡ GPU ≡ tarayıcıözdeşlik demosu ve Zaman Yolcusu (geleceği mühürle, sonra canlı doğrula).

Sonuç

Berk DT özünde bir fizik motoru, dijital ikiz ya da netcode değildir — bunlar yüzeydir. O, bir deterministik, denetlenebilir, çatallanabilir gerçeklik motorudur: kanıtlayabileceğin kararlar vermek için bir altyapı. Fizik motoru diye anlatılırsa, ihtiyacı olmayan özelliklerde rekabet eder. Doğrulanabilir karar altyapısı diye anlatılırsa, alternatifin kanıtsız güven olduğu bir kategori açar — ve savunmada, endüstride ve güvenlik-kritik robotikte kanıtsız güven yeterli değildir.