DistOptimize:分散プロトコルの自動最適化
arXiv:2610.39017v1 発表タイプ:新規 要旨:分散型コンセンサスおよび一貫性プロトコルは、その解析が極めて困難でありながらクラウドの基盤を成すものであるため、通常は本番環境への導入前に厳密な証明と形式検証を経る。一方で、運用中に頻繁に発生するプロトコルの変更には、同程度の厳密さがほとんど適用されておらず、安全性を損なうリスクが高まっている。本論文では、手動による変更に伴う安全性違反のリスクを排除するため、分散プロトコル向けの自動最適化ツール「DistOptimize」を提案する。DistOptimizeは、学術分野で用いられる言語から実運用で使用されるフレームワークへとスループット向上の最適化手法を移行し、Rocqにおいて書き換えの正当性を検証するとともに、キャリブレーションとILPベースの探索を組み合わせてその適用を自動化する。