論文の概要: StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
- arxiv url: http://arxiv.org/abs/2609.09264v1
- Date: Tue, 08 Sep 2026 17:59:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-10 19:44:08.749073
- Title: StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
- Title（参考訳）: StochBench: リーンの確率的プロセスのためのドメイン特有ベンチマーク
- Abstract要約: オプス語エージェントは、プロブレム当たり15分の制限で34.9%の証明レート(15/450)を達成する。
StochBenchはドメイン固有の応用数学をより良く表現する一方で、高度な証明者には挑戦的である。
- 参考スコア（独自算出の注目度）: 5.381817018558283
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Leading benchmarks for formal theorem proving with large language models are small collections drawn from competition math, such as the IMO and Putnam, that poorly represent field-specific applications. We introduce StochBench, a Lean 4 benchmark of 450 graduate stochastic-processes problems at varying abstraction levels, each paired with its natural-language source. Addressing a field underrepresented in Mathlib, it covers finite and countable Markov chains, renewal processes, random walks, martingales, stopping times, queues, Brownian motion, stochastic calculus, weak convergence, and Poisson and continuous-time Markov processes. Our Opus 4.8-based agent achieves a 34.9% proof rate (157/450) under a 15-minute per-problem limit. StochBench better represents domain-specific applied mathematics while remaining challenging for advanced provers.
- Abstract（参考訳）: 大きな言語モデルで証明された形式定理のベンチマークは、IMOやパットナムのような競合数学から引き出された小さなコレクションであり、フィールド固有の応用は不十分である。
StochBenchは450の卒業確率過程問題を、さまざまな抽象化レベルで、それぞれが自然言語ソースとペアリングするリーン4ベンチマークである。
マドリブで表現されていない分野に対処すると、有限および可算マルコフ連鎖、更新過程、ランダムウォーク、マーチンガル、停止時間、キュー、ブラウン運動、確率計算、弱収束、ポアソンおよび連続時間マルコフ過程を含む。
我々のOpus 4.8ベースのエージェントは、プロブレム当たり15分の制限で34.9%の証明率(157/450)を達成する。
StochBenchはドメイン固有の応用数学をより良く表現し、高度な証明者にとって挑戦的である。
関連論文リスト
- LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean [10.684401671916158]
CAM-Benchは、計算および応用数学における1000のリーン証明目標のLean 4定理証明ベンチマークである。
これらの問題は教科書の演習に適応しており、しばしばローカルに導入された定義、表記法、アルゴリズム、基礎的な結果に依存している。
リーンコンパイルとセマンティックレビューを通じて、結果のフォーマルな問題を検証し、フォーマルな正当性とセマンティックなアライメントの両方を元のエクササイズで確認します。
論文 参考訳（メタデータ） (2026-05-17T04:53:47Z) - Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs [4.559742899048613]
我々は、その範囲を大幅に広げることで、オリジナルのMathArenaベンチマークを構築します。
MathArenaは現在、証明ベースの競争、研究レベルのarXiv問題、Leanでの正式な証明生成など、より広範なタスクをカバーしています。
最強のモデルであるGPT-5.5は、2026年のアメリカ数学オリンピックで98%、研究レベルの質問で74%に達した。
論文 参考訳（メタデータ） (2026-05-01T13:56:34Z) - LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
新たな定義枠組みに適用した場合の現在のATPシステムの堅牢性を評価する。
本稿では,terence Tao氏のAnalytic Iから派生した,学部レベルのベンチマークであるTaoBenchを紹介する。
公平な評価のために,各問題に対してコンパイル可能な自己完結型ローカル環境を自動的に抽出するエージェントパイプラインを構築した。
論文 参考訳（メタデータ） (2026-03-13T07:39:47Z) - BayesSum: Bayesian Quadrature in Discrete Spaces [8.571182593542565]
モンテカルロやロシアのルーレット推定器を含む既存のアプローチは一貫性があるが、正確な結果を得るためには大量のサンプルを必要とすることが多い。
ベイズ二次の離散領域への拡張である新しい推定器 emphBayesSum を提案する。
論文 参考訳（メタデータ） (2025-12-18T02:43:30Z) - IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch [8.80477323574638]
IndiMathBenchは、数学的定理の証明を評価するために設計された人間検証ベンチマークである。
IndiMathBenchは312の形式的Lean 4定理とそれに対応する非公式な問題文を組み合わせて構成されている。
論文 参考訳（メタデータ） (2025-11-30T17:40:13Z) - CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics [45.32204834230928]
100の問題をまとめた総合的なベンチマークであるCombiBenchを紹介します。
CombiBenchは2000年以降の問題解決に適している(画像を含むIMO 2004 P3を除く)。
また、フォーマル数学のための包括的で標準化された評価フレームワーク「ファイン・エバル」も提供する。
論文 参考訳（メタデータ） (2025-05-06T04:32:17Z) - Sample, Don't Search: Rethinking Test-Time Alignment for Language Models [55.2480439325792]
新しいテストタイムアライメントアプローチであるQAlignを紹介します。
テスト時間計算をスケールする際、QAlignは各プロンプトの最適配向分布からのサンプリングに収束する。
マルコフ連鎖モンテカルロのテキスト生成における最近の進歩を取り入れることで、基礎となるモデルを変更したり、ロジットアクセスを必要とせずに、より良い整合出力を可能にする。
論文 参考訳（メタデータ） (2025-04-04T00:41:40Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - Efficiently Sampling Functions from Gaussian Process Posteriors [76.94808614373609]
高速後部サンプリングのための簡易かつ汎用的なアプローチを提案する。
分離されたサンプルパスがガウス過程の後部を通常のコストのごく一部で正確に表現する方法を実証する。
論文 参考訳（メタデータ） (2020-02-21T14:03:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。