論文の概要: FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models
- arxiv url: http://arxiv.org/abs/2608.20153v1
- Date: Thu, 20 Aug 2026 15:13:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-21 20:28:51.621657
- Title: FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models
- Title（参考訳）: FormalTCS: 大規模言語モデルにおけるエッジ・ツー・エンドの形式的コンピュータ科学研究のベンチマーク
- Abstract要約: 大規模言語モデル(LLM)は、自動理論計算機科学(TCS)研究の可能性を増大させている。
我々は、最前線のエンドツーエンドのTCS研究でLSMを評価するための専門家検証ベンチマークである ourbenchmarkを紹介した。
- 参考スコア（独自算出の注目度）: 53.68149869349268
- License: http://creativecommons.org/publicdomain/zero/1.0/
- Abstract: Large language models (LLMs) have shown growing potential for automated theoretical computer science (TCS) research, yet existing benchmarks remain far from realistic research settings. We introduce \ourbenchmark, an expert-validated benchmark for evaluating LLMs on frontier, end-to-end TCS research. \ourbenchmark contains $175$ instances drawn from papers accepted to STOC, FOCS, SODA, and COLT in 2025-2026, preserving paper-specific definitions, assumptions, and proof dependencies, with expert-verified Lean formalizations and proofs. Evaluations of leading LLMs reveal that current models remain far from reliably completing the full research pipeline. In particular, autoformalization is the sharpest bottleneck: the best model achieves only $11.5$ on translating natural-language claims into formal theorem statements, compared with $28.6$ Pass@8 when proving human-provided formal statements. Building on \ourbenchmark, we further develop an automated TCS research framework that generates, formalizes, filters, and proves new claims. Of $64$ generated claims, only $6$ ultimately pass expert evaluation and proof verification, indicating that beyond formalization, limited research taste remains another major barrier to autonomous TCS research.
- Abstract（参考訳）: 大規模言語モデル(LLM)は、自動理論計算機科学(TCS)研究の可能性を増大させているが、既存のベンチマークは現実的な研究環境からは程遠いままである。
我々は、フェデラルなエンドツーエンドのTCS研究でLLMを評価するためのエキスパート検証ベンチマークである \ourbenchmarkを紹介した。
\ourbenchmarkには、2025-2026年にSTOC、FOCS、SODA、COLTに受け入れられた論文から175ドルのインスタンスが含まれており、専門家が検証したリーンの形式化と証明とともに、論文固有の定義、仮定、証明の依存関係を保存する。
LLMをリードする評価は、現在のモデルが完全な研究パイプラインを確実に完成させるには程遠いことを示している。
特に、自己形式化(autoformalization)は、最も急激なボトルネックである: 最良のモデルは、自然言語のクレームを形式的な定理ステートメントに変換することでわずか11.5ドルしか達成しない。
さらに、‘ourbenchmark’に基づいて、新たなクレームを生成し、形式化し、フィルタし、証明する自動TCS研究フレームワークを開発します。
640ドル(約6万3000円)のクレームのうち、専門家による評価と検証を最終的にパスしたのは6ドル(約6万3000円)に過ぎません。
関連論文リスト
- 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) - CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference [17.447741518678374]
CausalForgeは因果推論における自動理論研究のためのフレームワークである。
因果推論のためのリーンライブラリであるCausaleanと、自己改善型のエージェントパイプラインであるCausalSmithを組み合わせたものだ。
論文 参考訳（メタデータ） (2026-07-24T17:32:35Z) - Theory-Scale Auto-Formalization of Logics for Computer Science [36.45195518081978]
LCS-Bench は Logics for Computer Science に基づく理論スケールのベンチマークである。
アーティファクトには327の教科書項目,4,076以上のリーン宣言,85万行以上のリーンコードが含まれています。
LCS-Benchは高品質で一貫性があり、忠実であることを示す。
論文 参考訳（メタデータ） (2026-06-25T01:59:53Z) - Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
T は形式定理の意味的正しさを評価する枠組みである。
5つの実世界のLean 4リポジトリからベンチマークを構築します。
実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
論文 参考訳（メタデータ） (2026-04-26T13:24:20Z) - Learning to Predict Future-Aligned Research Proposals with Language Models [59.79457676644722]
我々は目標から得られた17,771の論文とそれらの事前カットオフ引用の時間一貫性のあるデータセットを構築した。
モデルをトレーニングするために、ターゲットとそれらのカットオフ前の引用から17,771枚のタイム一貫性のあるデータセットを構築します。
Llama-3.1 と Qwen2.5 のモデル全体で、将来のアライメントチューニングは、非アライメントベースラインに対する将来のアライメントを改善する。
論文 参考訳（メタデータ） (2026-03-28T05:41:15Z) - RPC-Bench: A Fine-grained Benchmark for Research Paper Comprehension [65.81339691942757]
RPC-Bench(RPC-Bench)は、高品質なコンピュータサイエンス論文のレビュー・リビューの交換から構築された大規模質問応答ベンチマークである。
我々は、科学研究の流れに沿ったきめ細かい分類を設計し、モデルがなぜ、何、どのように学術的な文脈で質問するかを理解し、答える能力を評価する。
論文 参考訳（メタデータ） (2026-01-14T11:37:00Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。