論文の概要: LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

• arxiv url: http://arxiv.org/abs/2512.24796v1
• Date: Wed, 31 Dec 2025 11:33:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-01 23:27:28.640277
• Title: LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
• Title（参考訳）: LeanCat: リーンの形式的カテゴリ理論のためのベンチマークスイート(第1部:1カテゴリ)
• Authors: Rongge Xu, Hui Dai, Yiming Fu, Jiedong Jiang, Tianjiao Nie, Hongwei Wang, Junkai Wang, Holiverse Yang, Jiatong Yang, Zhi-Hao Zhang,
• Abstract要約: LeanCatは、カテゴリ理論の形式化のためのリーンベンチマークである。 パート I: 1-カテゴリには、完全に形式化されたステートメントレベルのタスクが100個含まれています。 Part II: LeanBridgeはLeanExploreを使ってMathlibを検索し、単一モデルベースラインに対する一貫した利得を観察します。
• 参考スコア（独自算出の注目度）: 7.871706113805829
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) have made rapid progress in formal theorem proving, yet current benchmarks under-measure the kind of abstraction and library-mediated reasoning that organizes modern mathematics. In parallel with FATE's emphasis on frontier algebra, we introduce LeanCat, a Lean benchmark for category-theoretic formalization -- a unifying language for mathematical structure and a core layer of modern proof engineering -- serving as a stress test of structural, interface-level reasoning. Part I: 1-Categories contains 100 fully formalized statement-level tasks, curated into topic families and three difficulty tiers via an LLM-assisted + human grading process. The best model solves 8.25% of tasks at pass@1 (32.50%/4.17%/0.00% by Easy/Medium/High) and 12.00% at pass@4 (50.00%/4.76%/0.00%). We also evaluate LeanBridge which use LeanExplore to search Mathlib, and observe consistent gains over single-model baselines. LeanCat is intended as a compact, reusable checkpoint for tracking both AI and human progress toward reliable, research-level formalization in Lean.
• Abstract（参考訳）: 大規模言語モデル (LLMs) は形式定理の証明において急速に進歩しているが、現在のベンチマークでは、現代の数学を組織する抽象論やライブラリによる推論を下敷きにしている。 FATEがフロンティア代数に重点を置いているのと並行して、LeanCatを紹介します。LeanCatは、カテゴリ理論の形式化のためのリーンベンチマークです。これは、数学構造のための統一言語で、現代の証明工学のコアレイヤで、構造的、インターフェースレベルの推論のストレステストとして機能します。 パートI: 1カテゴリは100の完全形式化されたステートメントレベルタスクを含み、トピックファミリにキュレーションされ、LLMアシスト+ヒューマングレーティングプロセスを介して3つの難易度レベルに分類される。 最良のモデルはpass@1(32.50%/4.17%/0.00%、Easy/Medium/High)で8.25%、pass@4(50.00%/4.76%/0.00%)で12.00%である。 また、LeanExploreを使ってMathlibを検索するLeanBridgeを評価し、単一モデルベースラインに対する一貫した利得を観察します。 LeanCatは、AIと人間の進歩の両方を追跡するためのコンパクトで再利用可能なチェックポイントとして、リーンの信頼性の高い研究レベルの形式化を目指している。

関連論文リスト

• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。 これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。 我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
  論文  参考訳（メタデータ） (2025-10-12T21:42:04Z)
• FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory [44.64175433092553]
  大規模言語モデル (LLM) は、最近、形式定理の証明において顕著な進歩を見せている。 しかし、数学者の実践的なアシスタントとして機能する能力は、複雑な証明の中で欠落したステップを埋めるものであり、まだ解明されていない。 機械学習の基礎理論に基づいて構築された、リーン4ベンチマークであるFormalMLを紹介します。
  論文  参考訳（メタデータ） (2025-09-26T14:40:14Z)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
  LLMは難解な解答作業に対処できるが、幻覚や不可解なステップの誤りを生じやすい。 創造性と数学的厳密性の両方を保ちながら、どのように解答-構成問題を解決するか? 本稿では,パターン駆動型推論と形式的定理証明を統合したニューロシンボリックな手法であるLLM-Conjecture-Prove(ECP)フレームワークを紹介する。 ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、公式な数学的推論を前進させる可能性を示している。
  論文  参考訳（メタデータ） (2025-05-24T03:52:25Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Lila: A Unified Benchmark for Mathematical Reasoning [59.97570380432861]
  LILAは、23の多様なタスクと4次元からなる統一的な数学的推論ベンチマークである。 我々は,Pythonプログラムの形式でタスク命令とソリューションを収集することにより,20のデータセットベンチマークを拡張してベンチマークを構築した。 LILAで訓練された汎用数学的推論モデルであるBHASKARAを紹介する。
  論文  参考訳（メタデータ） (2022-10-31T17:41:26Z)

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

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