論文の概要: TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability
- arxiv url: http://arxiv.org/abs/2608.09538v2
- Date: Thu, 13 Aug 2026 16:11:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-14 14:00:09.562871
- Title: TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability
- Title（参考訳）: TCS-BENCH: 最先端のAI理論コンピュータサイエンス研究能力のベンチマーク
- Authors: Vincent Cohen-Addad, Dimitris Paparas, Ernest van Wijland, Max Springer, Julien Canitrot-Paradis, Honghao Lin, David Woodruff, Adarsh Kumarappan, Rajesh Jayaram, Rudrajit Das, Lalit Jain, Ola Svensson, Silvio Lattanzi, Mislav Balunovic, Theophane Weber, Vahab Mirrokni,
- Abstract要約: 我々は,研究レベルの理論計算機科学(TCS)証明生成において,Large Language Models(LLMs)を評価するためのベンチマークであるTCS-Benchを紹介する。
TCS-Benchは、理論計算機科学の会場で発表された論文の定理証明タスクで構成されている。
- 参考スコア（独自算出の注目度）: 59.079078796751496
- License: http://creativecommons.org/publicdomain/zero/1.0/
- Abstract: We introduce TCS-Bench, a benchmark for evaluating Large Language Models (LLMs) on research-level Theoretical Computer Science (TCS) proof generation. TCS-Bench consists of theorem-proving tasks from papers published at top theoretical computer science venues (STOC, FOCS, and SODA). Each task provides the necessary context to derive a self-contained proof for a target result. We evaluate state-of-the-art models on this benchmark. We verify the correctness of generated proofs via a verification agent, and further benchmark the verifier against human-expert proof judgements on a set of target statements and generated proofs pairs. Our reference verifier achieves over 90% accuracy on the expert labeled set.
- Abstract（参考訳）: 我々は,研究レベルの理論計算機科学(TCS)証明生成において,Large Language Models(LLMs)を評価するためのベンチマークであるTCS-Benchを紹介する。
TCS-Benchは、理論計算機科学の上位会場(STOC、FOCS、SODA)で発表された論文の定理証明タスクで構成されている。
各タスクは、目標とする結果に対する自己完結した証明を導き出すために必要なコンテキストを提供する。
このベンチマークで最先端のモデルを評価する。
検証エージェントを用いて生成した証明の正当性を検証し、さらに、目標文と生成した証明ペアのセット上で、人間-専門家による証明判定に対する検証結果をベンチマークする。
我々の参照検証器は、専門家ラベル付き集合に対して90%以上の精度を達成している。
関連論文リスト
- Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
T は形式定理の意味的正しさを評価する枠組みである。
5つの実世界のLean 4リポジトリからベンチマークを構築します。
実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
論文 参考訳（メタデータ） (2026-04-26T13:24:20Z) - Neural Theorem Proving for Verification Conditions: A Real-World Benchmark [9.350519191460018]
この研究は、NTP4VC(Neural Theorem Proving for Verification Conditions)を導入し、このタスクのための最初の実世界のマルチ言語ベンチマークを示す。
NTP4VC を用いて,大言語モデル (LLM) の評価を行った。
論文 参考訳（メタデータ） (2026-01-26T20:37:11Z) - Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics [1.2978846076301875]
Ax-Proverは、リーンにおける自動定理証明のためのマルチエージェントシステムである。
様々な科学的領域にまたがる問題を解決し、自律的または協調的に人間の専門家と操作することができる。
我々は,2つの公的な数学ベンチマークと,抽象代数学と量子論の分野において導入される2つのリーンベンチマークにおいて,フロンティア LLM と特殊証明モデルに対するアプローチをベンチマークする。
論文 参考訳（メタデータ） (2025-10-14T17:57:04Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - INT: An Inequality Benchmark for Evaluating Generalization in Theorem
Proving [36.194330645092634]
本稿では,エージェントの一般化能力をテストするために,INequality Theorem Proving benchmarkを提案する。
Int は定理と証明を生成する手順に基づいており、この手順のノブは6つの異なる種類の一般化を測ることができる。
次に,モンテカルロ木探索(MCTS)で拡張したエージェントを試験時に評価し,MCTSが新たな定理を証明できることを示す。
論文 参考訳（メタデータ） (2020-07-06T17:55:33Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。