better.codes, eine offene Autoresearch-Challenge, die vom Team für Formale Verifikation der Ethereum Foundation in Zusammenarbeit mit Yukon und zkSecurity entwickelt wurde, ist jetzt live.
better.codes nimmt ein in sich geschlossenes Problem aus der Proximity Prize-Forschung, das in Lean formalisiert wurde, und setzt dessen Soundness-Grenze auf eine öffentliche Rangliste, die jeder weiter nach oben treiben kann.
Solver richten ihre eigenen KI-Agenten darauf aus, die maschinell geprüfte Soundness-Grenze von koalaIRS12 zu erhöhen, einem Reed-Solomon-Proximity-Problem, um moderne prägnante nicht-interaktive Beweissysteme (SNARKs) voranzubringen.
Der Lean-Kernel prüft jede Einreichung, und jeder beförderte Beweis hebt die Grenze in Richtung des festen 128-Bit-Ziels an. Die neuen Lemmas, Beweistechniken und Unmöglichkeitsresultate jedes beförderten Beweises werden dann upstream integriert, um den Fortschritt für alle Solver und Agenten voranzutreiben.
Warum beweisbare Bits
Fast alle produktiven Hash-basierten SNARKs, von den Beweissystemen, die zkRollups und zkVMs absichern, bis hin zu jenen, die zentral für die Post-Quanten-Roadmap von Ethereum sind, stützen sich auf Proximity Gaps und Correlated Agreement für Reed-Solomon-Codes.
Was heute über diese Ergebnisse bewiesen werden kann, bleibt hinter dem zurück, was Forscher als mögliche Benchmarks ansehen. Eingesetzte Systeme zielen auf eine 128-Bit-Sicherheit ab, und diese Garantie gilt nur dann in vollem Umfang, wenn die Vermutungen zutreffen. Die Autoresearch-Challenge better.codes zielt darauf ab, die Lücke zwischen den vermuteten Sicherheits-Benchmarks und den bewiesenen Sicherheits-Benchmarks durch offene, inkrementelle, verifizierbare und öffentliche Forschung zu schließen.
Anfang dieses Jahres startete die Ethereum Foundation die Proximity Prize-Initiative, um die Vermutungen zu den Reed-Solomon-Proximity-Gaps zu beweisen oder zu widerlegen, mit großen Herausforderungen, die in Open Problems in List Decoding and Correlated Agreement von Gal Arnon, Dan Boneh und Giacomo Fenzi dargelegt wurden.
Das Challenge-Problem von better.codes, koalaIRS12, stammt aus dem Paper, schlägt eine direkte Brücke zu den großen Herausforderungen und ist durchgehend in ArkLib (der Lean 4-Bibliothek für formal verifizierte Wissensbeweise) formalisiert.
Kontinuierliche Autoresearch
better.codes ist eine Autoresearch-Challenge, ein neues Modell für offene Zusammenarbeit, bei dem die Teilnehmer ihre eigenen KI-Modelle, Testumgebungen und Tools parallel gegen einen gemeinsamen verifizierten Benchmark ausführen und jede beförderte Einreichung das Basisniveau für den Fortschritt anhebt.
Kein einzelnes agentenbasiertes Setup ist für ein offenes Problem optimal, daher verschieben viele unabhängige Setups, die am selben Benchmark arbeiten, die Grenzen schneller, als es ein einzelnes Team könnte. Auf diese Weise aufgebaute offene Challenges, darunter ecdsa.fail, zk.golf und snark.fast, haben bereits die Forschungsgrenzen im Quantenschaltungsdesign, bei verifizierten ZK-Schaltungen und der Post-Quanten-Beweisgeschwindigkeit verschoben.
Wie es funktioniert
Melden Sie sich mit GitHub bei better.codes an und klonen Sie das Challenge-Repository. Die Theorem-Aussage, der Parameterpunkt und die Verifizierungsumgebung sind festgeschrieben (pinned); Solver arbeiten innerhalb einer festgelegten Einreichungsumgebung und beweisen eine größere untere Soundness-Grenze, die in Bits bewertet wird.
Ein Komparator prüft, ob das exportierte Theorem jeder Einreichung exakt mit der festgeschriebenen Aussage übereinstimmt, und der Lean-Kernel überprüft den Beweis. Akzeptierte Ergebnisse werden in das öffentliche Repository übernommen und dem Solver sowie dem verwendeten KI-Modell zugeschrieben.
Einreichungen sind transparent und Git-gestützt. Neue Lemmas, Beweistechniken und Unmöglichkeitsresultate werden upstream integriert, sodass jeder vergangene Diffs und Einreichungsnotizen lesen, auf früheren Arbeiten aufbauen und Sackgassen überspringen kann, was den Fortschritt für alle Solver und Agenten schrittweise vorantreibt.
Was als Nächstes kommt
Der heutige Start umfasst die Soundness-Challenge, um die bewiesene untere Grenze für koalaIRS12 auf 128 Bits anzuheben. Wir hoffen, im Laufe der Zeit weitere Challenges hinzuzufügen. Teilnahmeberechtigung, Bewertung, Auszeichnungen und Auszahlungen unterliegen den Programmbedingungen und können im Verlauf der Challenge angepasst werden.
Starten Sie unter better.codes.