論文の概要: SorryDB: Can AI Provers Complete Real-World Lean Theorems?
- arxiv url: http://arxiv.org/abs/2603.02668v1
- Date: Tue, 03 Mar 2026 06:55:15 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-04 21:38:10.677909
- Title: SorryDB: Can AI Provers Complete Real-World Lean Theorems?
- Title（参考訳）: SorryDB: AIプロデューサは現実のリーン理論を完全化できるか?
- Authors: Austin Letson, Leopoldo Sarra, Auguste Poiroux, Oliver Dressler, Paul Lezeau, Dhyan Aranha, Frederick Pu, Aaron Hill, Miguel Corredera Hidalgo, Julian Berman, George Tsoukalas, Lenny Taelman,
- Abstract要約: SorryDBは、GitHub上の78の現実世界のフォーマル化プロジェクトから引き出されたオープンなリーンタスクのベンチマークである。
我々は,汎用的な大規模言語モデル,エージェント的アプローチ,特殊記号型プロバーなど,一連のアプローチを評価する。
- 参考スコア（独自算出の注目度）: 0.5578094397833855
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition problems, hillclimbing the SorryDB benchmark will yield tools that are aligned to the community needs, more usable by mathematicians, and more capable of understanding complex dependencies. Moreover, by providing a continuously updated stream of tasks, SorryDB mitigates test-set contamination and offers a robust metric for an agent's ability to contribute to novel formal mathematics projects. We evaluate a collection of approaches, including generalist large language models, agentic approaches, and specialized symbolic provers, over a selected snapshot of 1000 tasks from SorryDB. We show that current approaches are complementary: even though an agentic approach based on Gemini Flash is the most performant, it is not strictly better than other off-the-shelf large-language models, specialized provers, or even a curated list of Lean tactics.
- Abstract（参考訳）: 私たちはSorryDBを紹介します。GitHubの78のリアルワールドフォーマル化プロジェクトから引き出されたオープンリーンタスクの動的更新ベンチマークです。
競合問題で構成される既存の静的ベンチマークとは異なり、SorryDBベンチマークをヒルクライミングすると、コミュニティのニーズに合わせて、数学者がより使いやすく、複雑な依存関係を理解することができるツールが得られる。
さらに、連続的に更新されたタスクストリームを提供することで、SorryDBはテストセットの汚染を軽減し、エージェントが新しい形式的な数学プロジェクトに貢献できるための堅牢な指標を提供する。
我々は、SorryDBから選択された1000タスクのスナップショットに対して、汎用的な大規模言語モデル、エージェントアプローチ、特殊記号プロデューサを含むアプローチの集合を評価した。
Gemini Flashをベースとしたエージェント的アプローチが最もパフォーマンスが高いとはいえ、市販の大規模言語モデルや専門のプロバー、さらにはリーン戦略のキュレートされたリストよりも厳密には優れていません。
関連論文リスト
- ISO-Bench: Can Coding Agents Optimize Real-World Inference Workloads? [0.8749675983608171]
実世界の推論タスクでその能力をテストするためのコーディングエージェントのベンチマークであるISO-Benchを紹介する。
統合プルリクエストから54のタスクをキュレートし、測定可能なパフォーマンスを改善しました。
論文 参考訳（メタデータ） (2026-02-23T08:37:53Z) - Terminal-Bench: Benchmarking Agents on Hard, Realistic Tasks in Command Line Interfaces [126.23612941699565]
Terminal-Bench 2.0は、現実世界の問題に触発されたコンピュータ端末環境における89のタスクからなるベンチマークである。
ベンチマークでは、フロンティアモデルとエージェントのスコアが65%未満であることが示されています。
将来的にはhttps://www.tbench.ai/で開発者や研究者を支援するために、データセットと評価ハーネスを公開しています。
論文 参考訳（メタデータ） (2026-01-17T01:29:30Z) - ABC-Bench: Benchmarking Agentic Backend Coding in Real-World Development [72.4729759618632]
本稿では,現実的かつ実行可能なワークフロー内でエージェントバックエンドコーディングを評価するベンチマークであるABC-Benchを紹介する。
オープンソースリポジトリから8つの言語と19のフレームワークにまたがる224の実践的なタスクをキュレートしました。
我々の評価は、最先端モデルでさえ、これらの総合的なタスクに対して信頼性の高いパフォーマンスを提供するのに苦労していることを示している。
論文 参考訳（メタデータ） (2026-01-16T08:23:52Z) - What Limits Virtual Agent Application? OmniBench: A Scalable Multi-Dimensional Benchmark for Essential Virtual Agent Capabilities [56.646832992178105]
我々は、制御可能な複雑性のタスクを合成するための自動パイプラインを備えたクロスプラットフォームグラフベースのベンチマークであるOmniBenchを紹介した。
OmniEvalは、サブタスクレベルの評価、グラフベースのメトリクス、および10機能にわたる包括的なテストを含む多次元評価フレームワークである。
我々のデータセットには、20のシナリオにわたる36万のグラフ構造化タスクが含まれており、人間の受け入れ率は91%に達する。
論文 参考訳（メタデータ） (2025-06-10T15:59:38Z) - IDA-Bench: Evaluating LLMs on Interactive Guided Data Analysis [60.32962597618861]
IDA-Benchは、多ラウンドの対話シナリオで大規模言語モデルを評価する新しいベンチマークである。
エージェント性能は、最終的な数値出力と人間由来のベースラインを比較して判断する。
最先端のコーディングエージェント(Claude-3.7-thinkingなど)でさえ50%のタスクを成功させ、シングルターンテストでは明らかでない制限を強調している。
論文 参考訳（メタデータ） (2025-05-23T09:37:52Z) - MergeBench: A Benchmark for Merging Domain-Specialized LLMs [25.333088749417414]
MergeBenchは、スケールでのモデルマージを評価するために設計された評価スイートである。
2Bから9BスケールのLlamaやGemmaファミリなど、最先端のオープンソース言語モデルの上に構築されている。
マルチタスク性能, 忘れられたこと, 実行効率にまたがる8つの代表的なマージ手法を評価した。
論文 参考訳（メタデータ） (2025-05-16T04:02:55Z) - Program Semantic Inequivalence Game with Large Language Models [20.43560028315856]
大きな言語モデル(LLM)は、日々のコーディングタスクにおいて強力なパフォーマンスを達成することができるが、プログラムのセマンティクスに関する非自明な推論を必要とする複雑なタスクでは失敗する可能性がある。
本研究では,意味的不等価ゲームSInQに基づいて,コード推論学習データを合成的に生成する手法について検討する。
この設定により、無限の計算資源の限界における自己再生による理論的に無制限な改善が可能であることを証明した。
論文 参考訳（メタデータ） (2025-05-02T20:03:35Z) - DiscoveryBench: Towards Data-Driven Discovery with Large Language Models [50.36636396660163]
我々は、データ駆動探索の多段階プロセスを形式化する最初の包括的なベンチマークであるDiscoveryBenchを紹介する。
我々のベンチマークには、社会学や工学などの6つの分野にまたがる264のタスクが含まれている。
私たちのベンチマークでは、自律的なデータ駆動型発見の課題を説明し、コミュニティが前進するための貴重なリソースとして役立ちます。
論文 参考訳（メタデータ） (2024-07-01T18:58:22Z) - AgentQuest: A Modular Benchmark Framework to Measure Progress and Improve LLM Agents [19.439775106707344]
AgentQuestは、ベンチマークとメトリクスがモジュール化され、十分にドキュメント化され使いやすいAPIを通じて容易に利用できるフレームワークである。
課題を解決しながら LLM エージェントの進捗を確実に追跡できる2つの新しい評価指標を提供する。
一般的な障害点を特定し,エージェントアーキテクチャを洗練し,大幅な性能向上を実現する2つのユースケースにおけるメトリクスの有用性を実証する。
論文 参考訳（メタデータ） (2024-04-09T16:01:24Z) - KILT: a Benchmark for Knowledge Intensive Language Tasks [102.33046195554886]
知識集約型言語タスク(KILT)のベンチマークを示す。
KILTのすべてのタスクはウィキペディアのスナップショットと同じだ。
共有密度ベクトル指数とSeq2seqモデルとの結合が強いベースラインであることが分かる。
論文 参考訳（メタデータ） (2020-09-04T15:32:19Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。