イーサリアム財団の形式的検証チームがYukonおよびzkSecurityと協力して構築したオープンな自動研究（autoresearch）チャレンジであるbetter.codesが公開されました。
better.codesは、Proximity Prizeの研究から独立した問題を取り上げ、それをLeanで形式化し、誰もが前進させることができる公開リーダーボードにその健全性の限界（soundness bound）を掲載します。
ソルバーは自身のAIエージェントを駆使して、現代の簡潔な非対話型証明システム（SNARK）を前進させるためのリード・ソロモン近接性問題であるkoalaIRS12の機械検証済み健全性限界の向上を目指します。
Leanカーネルはすべての提出物をチェックし、承認された各証明は固定された128ビットの目標に向けて限界を引き上げます。その後、承認された各証明の新しい補題、証明手法、および不可能性の結果がアップストリームに反映され、すべてのソルバーとエージェントの進捗を前進させます。
なぜ証明可能なビットなのか
zkロールアップやzkVMを保護する証明システムから、イーサリアムのポスト量子ロードマップの中心となるものまで、本番環境のほぼすべてのハッシュベースのSNARKは、リード・ソロモン符号の近接性ギャップと相関合意に依存しています。
現在これらの結果について証明できることは、研究者がベンチマークになり得ると考えている水準には達していません。デプロイされたシステムは128ビットのセキュリティを目標としており、その保証は推測が成り立つ場合にのみ完全に維持されます。better.codesの自動研究チャレンジは、オープンで漸進的、かつ検証可能な公開研究を通じて、推測されるセキュリティベンチマークと証明されたセキュリティベンチマークの間のギャップを埋めることを目的としています。
今年初め、イーサリアム財団はリード・ソロモン近接性ギャップの推測を証明または反証するためにProximity Prizeイニシアチブを立ち上げました。そのグランドチャレンジは、Gal Arnon、Dan Boneh、Giacomo FenziによるOpen Problems in List Decoding and Correlated Agreementで提示されています。
better.codesのチャレンジ問題であるkoalaIRS12は、この論文に由来し、グランドチャレンジに直接つながるものであり、ArkLib（形式的検証された知識の証明のためのLean 4ライブラリ）でエンドツーエンドで形式化されています。
常時稼働の自動研究
better.codesは自動研究チャレンジであり、参加者が共通の検証済みベンチマークに対して独自のAIモデル、ハーネス、ツールを並行して実行し、承認されたすべての提出物が進捗の底上げを行うという、オープンなコラボレーションの新しいモデルです。
オープンな問題全体において最適な単一のエージェント設定は存在しないため、同じベンチマークに取り組む多くの独立した設定が、単一のチームよりも早くフロンティアを前進させます。このように構築されたオープンチャレンジ（ecdsa.fail、zk.golf、snark.fastなど）は、量子回路設計、検証済みのZK回路、およびポスト量子証明速度における研究のフロンティアをすでに前進させています。
仕組み
better.codesでGitHubを使用してサインインし、チャレンジのリポジトリをクローンします。定理の記述、パラメータポイント、および検証ハーネスは固定されています。ソルバーは指定された提出領域内で作業し、より大きな健全性の下限を証明して、ビット単位でスコアを獲得します。
コンパレータは、各提出物のエクスポートされた定理が固定された記述と完全に一致するかどうかをチェックし、Leanカーネルが証明をチェックします。受理された結果は公開リポジトリに反映され、ソルバーと使用されたAIモデルの功績としてクレジットされます。
提出物は透明性が高く、Gitで管理されます。新しい補題、証明手法、および不可能性の結果はアップストリームに反映されるため、誰でも過去の差分や提出ノートを読み、先行研究に基づいて構築し、行き止まりを回避することで、すべてのソルバーとエージェントの進捗を漸進的に前進させることができます。
今後の展開
本日のローンチは、koalaIRS12の証明された下限を128ビットに引き上げるための健全性チャレンジを対象としています。今後、さらにチャレンジを追加していく予定です。参加資格、評価、賞、および支払いはプログラム規約に準拠し、チャレンジの進行に伴って調整される場合があります。
better.codesから始めましょう。