論文の概要: SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability
- arxiv url: http://arxiv.org/abs/2610.13461v1
- Date: Fri, 09 Oct 2026 11:59:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-13 04:06:29.559232
- Title: SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability
- Title（参考訳）: SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability
- Abstract要約: 飽和に耐性のあるベンチマークであるSqueezeBenchを紹介します。
各問題は整数関数 $f(n)$ を固定し、その値が小さい$n$でしか知られていない。
Recordは計算可能なLean関数で、マシンチェックされた証明で$f$に制限されている。
- 参考スコア（独自算出の注目度）: 22.15125586581917
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: AI systems are making rapid progress in mathematics, but this progress is hard to measure. Benchmarks of solved problems saturate, and in benchmarks of open problems each problem can be resolved for the first time only once. We present SqueezeBench, a benchmark that is resilient to saturation: a success raises the bar instead of removing the problem. Each problem fixes an integer function $f(n)$ whose values are known only for small $n$, and the benchmark keeps a lower and an upper record on it. A record is a computable Lean function with a machine-checked proof that it bounds $f$. A submission proposes a new function and proves that it bounds $f$, that it is no worse than the current record at any $n$, and that it is strictly better at some $n$. Once accepted, it becomes the record that the next submission has to beat. The system thus chooses the bound as well as its proof, and it may improve the record at a single $n$ or its growth rate. At every $n$, the gap between the two records shows how far the certified bounds are from determining $f(n)$. Every proof is checked by two independent Lean kernels, so no referee needs to check the mathematics. The checks also reject a function that computes $f$ by exhaustive search at small $n$, and a maintainer only reads the submitter's report and looks for such a search at larger $n$. We release ten problems from extremal combinatorics with twenty proved initial records and the admission tools. As a baseline, agents based on a frontier language model, with at most one hour per record, had 82 submissions accepted and improved every record, without going beyond the published literature. Agents based on two newer models then started from these records, had 60 more submissions accepted and improved 19 of the 20 records again. For eight of the ten problems, at least one record is still asymptotically behind the best published bound.
- Abstract（参考訳）: AIシステムは数学で急速に進歩していますが、この進歩を測るのは困難です。
解決された問題のベンチマークは飽和し、オープンな問題のベンチマークでは、各問題が最初に解決できるのは1回だけである。
飽和に耐性のあるベンチマークであるSqueezeBenchを紹介します。
各問題は整数関数$f(n)$の値が小さい$n$でしか知られておらず、ベンチマークは低い値と上位値を保持する。
Recordは計算可能なLean関数で、マシンチェックされた証明で$f$に制限されている。
提案書は、新しい関数を提案し、その値が$f$であること、現在のレコードの任意の$n$よりも悪くないこと、そして、ある$n$で厳密に優れていることを証明している。
一度受け入れられると、次の申請が勝たなければならない記録となる。
したがって、システムは境界と証明を選択でき、記録を1ドルまたはその成長率で改善することができる。
それぞれの$n$で、2つのレコード間のギャップは、認定された境界が$f(n)$の決定からどれくらいの距離にあるかを示す。
すべての証明は2つの独立したリーンカーネルによってチェックされます。
チェックはまた、小さな$n$で徹底的な検索によって$f$を計算する関数を拒否する。
初回成績は20例, 初回成績は20例であった。
ベースラインとして、フロンティア言語モデルに基づくエージェントは、少なくとも1時間ごとに82件の提出を受理し、全ての記録を改善したが、出版された文献には及ばなかった。
2つの新しいモデルに基づくエージェントがこれらのレコードから始まり、60以上の応募が受け入れられ、20レコードのうち19が再び改善された。
10つの問題のうち8つについては、少なくとも1つの記録は、最も公表された境界線の背後で漸近的に残されている。
関連論文リスト
- A Sharp Barrier for Consistent Submodular Maximization: Any Improvement over $2-\sqrt{2}$ Entails Exponential Queries or Linear Recourse [50.69285844345291]
我々は、要素が時間とともに到着する際のソリューションの品質と安定性のトレードオフについて研究する。
我々のアルゴリズムは,有理オラクル$を$O(varepsilon-1)$recourseで実装し,そのアルゴリズムから普遍価格証明書の存在を分離する。
論文 参考訳（メタデータ） (2026-09-09T10:13:43Z) - Robustness-Aware Evaluation and Enhancement of Mutation-Based Fuzzing for Bug Discovery [29.62963078889574]
突然変異ベースのファジィは、ソフトウェアの脆弱性を発見するために広く使われている。
計算処理後のバグトリガー率の変動を計測する。
次に、バグトリガの後にファザのキュー状態をコピーするブラックボックスラッパーであるsplittingを紹介します。
論文 参考訳（メタデータ） (2026-09-06T18:28:47Z) - The Condition-Number Barrier in Sparse Least Squares [77.64108812086542]
AxiotisとSviridenkoは[AS21]において、凸最適化における制限条件数への線形依存はスパース時間アルゴリズムでは改善できないと推測した。
我々は、最小二乗目的に対する予想下界を確立し、ランダム化された完全体積小セット展開仮説に基づく条件付けを行う。
論文 参考訳（メタデータ） (2026-08-03T17:57:01Z) - Exponentially Fewer-Server PIR from Sparser $S$-Decoding Polynomials [2.5782420501870296]
一定の$s$に対して、$s$サーバのプライベート情報検索プロトコルが存在することを示す。
我々の数論予想は既存の予想によって示唆される。
論文 参考訳（メタデータ） (2026-07-24T06:59:30Z) - A Forced-Structure Reduction and Verifiable Bounds for Conway's 99-Graph [0.0]
コンウェイの99グラフ問題はパラメータ $mathrmsrg(99,14,1,2)$ の強い正則グラフが存在するかどうかを問うものである。
我々は,自律型AI研究エージェントによる,体系的で完全に再現可能な攻撃を報告した。
論文 参考訳（メタデータ） (2026-07-13T18:42:21Z) - $k$-server-bench: Automating Potential Discovery for the $k$-Server Conjecture [4.29490433621832]
我々は、$k$-server予想に基づいて、自動でオープンな数学的発見のためのコードベースの挑戦を紹介する。
この課題は、単純な線形不等式からなる大きなグラフ構造系を満たすポテンシャル関数を発見することである。
以上の結果から,現在の手法の範囲内において,課題は困難である可能性が示唆された。
論文 参考訳（メタデータ） (2026-04-08T16:06:43Z) - Fingerprinting Codes Meet Geometry: Improved Lower Bounds for Private Query Release and Adaptive Data Analysis [25.476062424924713]
本稿では,フィンガープリント方式の下位境界の証明のための一般的なフレームワークを提案する。
宇宙上の任意の適応的数え上げクエリにQ$$$mathcalX$ to accuracy $alpha$ needs $Omega(fracsqrt log|mathcalX| log (1/delta) log Qvarepsilonalpha2)$ sample, matching known upper bounds to constants。
論文 参考訳（メタデータ） (2024-12-18T23:11:07Z) - Computational Lower Bounds for Regret Minimization in Normal-Form Games [68.66209476382213]
乗算重み更新などの既存の学習アルゴリズムが最適に近いことを示す。
結果はKothari と Mehta が提案したアルゴリズムの枠組みで得られた。
論文 参考訳（メタデータ） (2024-11-04T00:39:52Z) - Testing the Feasibility of Linear Programs with Bandit Feedback [53.40256244941895]
我々は,低回帰アルゴリズムと反復対数の漸近法則に基づくテストを開発する。
このテストが信頼できることを証明し、信号レベルに適応する'$Gamma,$ of any instance。
信頼性テストのサンプルコストに対して、最小限の$(Omegad/Gamma2)$で補う。
論文 参考訳（メタデータ） (2024-06-21T20:56:35Z) - Fast Rates for Bandit PAC Multiclass Classification [73.17969992976501]
我々は,帯域幅フィードバックを用いたマルチクラスPAC学習について検討し,入力を$K$ラベルの1つに分類し,予測されたラベルが正しいか否かに制限する。
我々の主な貢献は、問題の無知な$(varepsilon,delta)$PACバージョンのための新しい学習アルゴリズムを設計することである。
論文 参考訳（メタデータ） (2024-06-18T08:54:04Z) - Online Learning with Adversaries: A Differential-Inclusion Analysis [52.43460995467893]
我々は,完全に非同期なオンラインフェデレート学習のための観察行列ベースのフレームワークを提案する。
我々の主な結果は、提案アルゴリズムがほぼ確実に所望の平均$mu.$に収束することである。
新たな差分包摂型2時間スケール解析を用いて,この収束を導出する。
論文 参考訳（メタデータ） (2023-04-04T04:32:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。