STARK檢查次數可能從200降至148次　3項數學挑戰公開

三項旨在減少 STARK 證明檢查次數的數學挑戰已公開。挑戰頁列出一項條件式計算：若目標證明成立，在特定條件下，達到100位元安全性所需的檢查次數可能從200次降至148次；這項數字仍以證明目標成立及完成整體安全性分析為前提。

provably.fast 官方挑戰頁提出三項目標。各項命題都固定在數學定理證明工具 Lean 中，只有經獨立審查的證明才會被認定為解答。目前三項目標都尚未解決。

STARK 是一種以雜湊函數為基礎的零知識證明系統。Reed–Solomon 編碼用於處理系統中待驗證資料的可信度；驗證者會檢查隨機組合，確認提交資料是否接近該編碼。

這些挑戰聚焦於限制檢查過程中可能讓錯誤資料看起來像正常編碼的「不良挑戰值」數量。若能降低不良挑戰值的上限，便有理由減少驗證所需的隨機檢查；但單靠改善上限，不會直接改變實際證明大小或安全性。

三項目標依編碼的一致率區間區分。T1 要在一階門檻與 Johnson 界限之間的區間，將目前已知的二次上界降為線性上界。T2 則要在一階門檻以下更廣的範圍內，證明二次上界。

T3 探討生成證明所用評估域的上界。挑戰頁以一致率 5/8、比率 1/2 的第一個案例為例，要求在既有構造的不良挑戰值數量最高可達 114n/16 的條件下，證明其上限為 16n。

挑戰頁列出的檢查次數範例，採用 FRI 類型方法、比率 1/2、n=2²⁰ 及 124 位元有限體等特定條件。依該計算，達到100位元安全性目前需要200次檢查；若 T3 的第一個案例獲得證明，次數可降至148次。頁面說明，這只涉及檢查次數的計算，實際應用仍須完成整體安全性分析。

先前研究曾將數學上界與實際實作的證明大小連結。Quang Dao、Scott Duke Kominers 與 Justin Thaler 於 9 月 17 日登錄的預印本指出，在相同安全目標下，ProveKit 的護照證明減少了 79.4KB（11.1%）、ZisK 的壓縮最終證明減少了 13.2KB（4.63%），LambdaVM 的 CPU 子證明則減少了 59.8KB（4.85%）。這些結果來自論文採用的特定實作與設定。

適用範圍仍有限。10 月 9 日公開的另一篇論文，在二元有限體中提出 Johnson 界限以下近鄰性間隙不成立的反例。挑戰頁的背景說明指出，該結果既未解決也未反駁本次挑戰，因為本次目標以特徵足夠大的有限體為條件。

人類與 AI 代理都能參與挑戰，貢獻的想法、輔助引理、反例與證明都會留下紀錄。OpenAI 公開內部模型的數學成果及部分 Lean 形式化內容，也顯示形式化數學結果的公開仍在持續。

目前尚無三項公開挑戰已獲解決，或實際 STARK 實作的證明大小進一步縮減的結果。即使數學上界獲得證明，仍須另行分析適用協定的安全性與證明大小，才能確認實際效果。