論文の概要: TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science

• arxiv url: http://arxiv.org/abs/2609.35606v1
• Date: Mon, 28 Sep 2026 16:52:40 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-01 20:29:42.162876
• Title: TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science
• Title（参考訳）: TCSAlgBench: 研究レベルの理論的コンピュータ科学のためのベンチマーク自動証明
• Abstract要約: 大規模言語モデルは競争数学に強く依存するが、研究レベルの推論は体系的に評価することは困難である。 自然言語による証明発見のためのベンチマークおよび再利用可能なパイプラインであるTCSAlgBenchを紹介する。 128のSTOCとCOLT 2026の論文からの398の定理レベルの挑戦を含んでいる。
• 参考スコア（独自算出の注目度）: 21.20090277386839
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models perform strongly on competition mathematics, but their research-level reasoning remains difficult to evaluate systematically. Theoretical computer science (TCS) connects algorithm design to explicit guarantees and fundamental limits, providing a setting for evaluating whether models can justify computational improvements with arguments humans can inspect. We introduce TCSAlgBench, a benchmark and reusable pipeline for natural-language proof discovery, comprising 398 theorem-level challenges from 138 STOC and COLT 2026 papers. Expert-designed rules complete paper-specific context, preserve computational assumptions and quantitative guarantees, and withhold constructions when discovering an algorithm is part of the task. For each task, prover systems receive theorem statements and access to cited prior work. The pipeline supports fresh, versioned challenge batches from newly released papers. We evaluate ten model configurations from four families under direct inference and prover-verifier discussion, and compare four agent workflows under matched model-call opportunities. All evaluations use the full benchmark. In the model comparison, GPT-5.6 Sol max achieves the highest five-run verifier-accepted coverage at 23.6% after 10-round discussion. Discussion and repeated sampling improve coverage. In the separate agent comparison using GPT-5.5 xhigh, decomposition improves coverage over discussion, and agentic planning achieves the highest five-run verifier-accepted coverage at 25.4%. TCSAlgBench provides a refreshable testbed for measuring progress in model reasoning and studying how agent workflows support research-level proof discovery.
• Abstract（参考訳）: 大規模言語モデルは競争数学に強く依存するが、研究レベルの推論は体系的に評価することは困難である。 理論計算機科学(TCS)は、アルゴリズム設計を明示的な保証と基本的な限界に結び付け、モデルが人間が検査できる引数で計算改善を正当化できるかどうかを評価するための設定を提供する。 我々は,128 STOC と COLT 2026 の論文から 398 の定理レベルの課題を含む,自然言語による証明発見のためのベンチマークおよび再利用可能なパイプライン TCSAlgBench を紹介する。 専門家が設計したルールは、論文固有のコンテキストを完備し、計算仮定と量的保証を保持し、アルゴリズムを発見するときの構造を保留する。 それぞれのタスクに対して、証明システムは定理文を受け取り、引用された先行作業にアクセスすることができる。 パイプラインは、新しくリリースされた論文から新しくバージョン管理されたチャレンジバッチをサポートする。 そこで本研究では,直接推論と検証を行う4家族のモデル構成を10種類評価し,一致したモデルコール機会下での4つのエージェントワークフローを比較した。 すべての評価は完全なベンチマークを使用する。 モデル比較では、GPT-5.6 Sol maxは10ラウンドの議論の後、23.6%で最高5ランの検証対象範囲を達成している。 議論と繰り返しサンプリングによりカバレッジが向上する。 GPT-5.5 xhighを用いた別のエージェント比較では、分解により議論のカバレッジが向上し、エージェント計画では最も高い5ラン検証対象のカバレッジが25.4%に達する。 TCSAlgBenchは、モデル推論の進捗を計測し、エージェントワークフローが研究レベルの証明発見をどのようにサポートするかを研究するために、リフレッシュ可能なテストベッドを提供する。

関連論文リスト

• FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models [53.68149869349268]
  大規模言語モデル(LLM)は、自動理論計算機科学(TCS)研究の可能性を増大させている。 我々は、最前線のエンドツーエンドのTCS研究でLSMを評価するための専門家検証ベンチマークである ourbenchmarkを紹介した。
  論文  参考訳（メタデータ） (2026-08-20T15:13:41Z)
• Deep Academic Survey: Stateful Agentic Closed-Loop Paradigm for Academic Survey Automation [60.151050016855834]
  DASは出版指向の学術調査を作成するためのステートフルなエージェント・フレームワークである。 その鍵となる考え方は、再利用可能な紙分析とトピック固有の原稿構築を分離することである。 DASは4つの次元で最高点に達し、総合スコアは4.34であり、最強の競争相手は4.03である。
  論文  参考訳（メタデータ） (2026-08-18T17:29:00Z)
• TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability [59.079078796751496]
  我々は,研究レベルの理論計算機科学(TCS)証明生成において,Large Language Models(LLMs)を評価するためのベンチマークであるTCS-Benchを紹介する。 TCS-Benchは、理論計算機科学の会場で発表された論文の定理証明タスクで構成されている。
  論文  参考訳（メタデータ） (2026-08-10T12:36:16Z)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T は形式定理の意味的正しさを評価する枠組みである。 5つの実世界のLean 4リポジトリからベンチマークを構築します。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
  論文  参考訳（メタデータ） (2026-04-26T13:24:20Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• RPC-Bench: A Fine-grained Benchmark for Research Paper Comprehension [65.81339691942757]
  RPC-Bench(RPC-Bench)は、高品質なコンピュータサイエンス論文のレビュー・リビューの交換から構築された大規模質問応答ベンチマークである。 我々は、科学研究の流れに沿ったきめ細かい分類を設計し、モデルがなぜ、何、どのように学術的な文脈で質問するかを理解し、答える能力を評価する。
  論文  参考訳（メタデータ） (2026-01-14T11:37:00Z)
• Evaluating Frontier LLMs on PhD-Level Mathematical Reasoning: A Benchmark on a Textbook in Theoretical Computer Science about Randomized Algorithms [14.853721511192736]
  大規模言語モデル(LLM)は、自動数学的推論と科学的発見の突破口となった。 GP-5-Thinking、Gemini-3-Pro、Claude-Sonnet-4.5-Thinking、Grok-4の4つのフロンティアモデルのベンチマークを示す。 上位モデルの精度は高いが,他のモデルでは一貫性が著しく低下していることがわかった。
  論文  参考訳（メタデータ） (2025-12-16T00:34:55Z)
• Proving the Coding Interview: A Benchmark for Formally Verified Code Generation [3.5319285228327417]
  FVAPPS (Formally Verified Automated Programming Progress Standards, FVAPPS) は,プログラムの記述と正確性を証明するための4715サンプルのベンチマークである。 我々は,機械学習とプログラム合成コミュニティに対して,汎用プログラミング問題とその関連した正当性仕様の解決に挑戦する。
  論文  参考訳（メタデータ） (2025-02-08T22:54:58Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。