論文の概要: Extraction and Search in Rocq: Theorems, Definitions and Their dependencies

• arxiv url: http://arxiv.org/abs/2606.04704v1
• Date: Wed, 03 Jun 2026 10:33:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-05 07:07:40.486779
• Title: Extraction and Search in Rocq: Theorems, Definitions and Their dependencies
• Title（参考訳）: Rocqにおける抽出と検索:理論と定義とその依存関係
• Authors: Jian Fang, Yingfei Xiong,
• Abstract要約: Rocq (Coq) は、ソフトウェア検証や数学的証明など、様々な分野で広く使われている。 本稿では、定理合成を解析し、定理、依存関係、定義を抽出できるRocq定理抽出解析ツールTheoremExtrを紹介する。 我々はまた、定理と定義のクロスプロジェクト類似性検索をサポートするウェブサイトを開発した。
• 参考スコア（独自算出の注目度）: 2.6146136791093104
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Rocq (Coq) are now widely used in various fields, including software verification and mathematical proofs. When proving a new theorem, users often need to search and apply proven theorems to assist the current proof process. However, the current search command is limited to the environment of imported modules and cannot search for theorems outside of this scope. Furthermore, tool developers and researchers may want to obtain detailed information about theorems, such as theorem's names, statements, and dependencies. But there are currently no user-friendly and efficient tools available for extracting comprehensive information from Rocq projects. We introduce a Rocq theorem extraction and analysis tool, TheoremExtr, which is capable of analyzing theorem composition and extracting theorems, dependencies, and definitions from both parsing phase and runtime. We extracted 71,795 theorems and their dependencies from 32 open-source projects from the Rocq community. In addition, we extracted 27,481 definitions and their types among these projects. We also developed a website that supports cross-project similarity search for theorems and definitions. The tool is available at https://github.com/Rw1nd/TheoremExtr, and the search website is available at https://lemmasearch.com.
• Abstract（参考訳）: Rocq (Coq) は現在、ソフトウェア検証や数学的証明など、様々な分野で広く使われている。 新しい定理を証明する場合、ユーザーは現在の証明プロセスを支援するために証明済みの定理を探索して適用する必要があることが多い。 しかし、現在の検索コマンドは輸入されたモジュールの環境に限られており、この範囲外の定理を探索することはできない。 さらに、ツール開発者や研究者は、定理の名前、ステートメント、依存関係など、定理に関する詳細な情報を得たいかもしれない。 しかし現時点では,Rocqプロジェクトから包括的な情報を抽出するための,ユーザフレンドリで効率的なツールが存在しない。 本稿では,定理合成を解析し,解析フェーズと実行時の両方から定理,依存関係,定義を抽出する,Rocq定理抽出解析ツールTheoremExtrを紹介する。 我々はRocqコミュニティの32のオープンソースプロジェクトから71,795の定理とその依存関係を抽出した。 さらに,これらのプロジェクトの中から27,481個の定義とそのタイプを抽出した。 我々はまた、定理と定義のクロスプロジェクト類似性検索をサポートするウェブサイトを開発した。 このツールはhttps://github.com/Rw1nd/TheoremExtrで入手できる。

関連論文リスト

• Semantic Search over 9 Million Mathematical Theorems [0.31229177276953496]
  我々は、arXivと他の7つの情報源から抽出された9.2億ドルの定理文の統一コーパス上で、意味定理の検索を大規模に導入、研究する。 それぞれの定理を,検索表現として短い自然言語記述で表現し,表現コンテキスト,言語モデルの選択,埋め込みモデル,探索戦略が検索品質にどのように影響するかを体系的に分析する。
  論文  参考訳（メタデータ） (2026-02-05T02:16:20Z)
• miniCTX: Neural Theorem Proving with (Long-)Contexts [19.51651334079961]
  miniCTXは、トレーニング中に見えない新しい文脈に依存する形式的な数学的定理を証明するモデルの能力をテストする。 miniCTXには、実際のリーンプロジェクトと教科書に由来する定理が含まれており、それぞれに数万のトークンにまたがるコンテキストが関連付けられています。
  論文  参考訳（メタデータ） (2024-08-05T20:19:18Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
  我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。 新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。 また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
  論文  参考訳（メタデータ） (2024-02-26T21:21:30Z)
• Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry [0.0]
  我々は、幾何定理(と性質)の自動発見のための異なるアプローチを提示し、議論する。 定理証明者が興味深い定理を生成できるかどうかを判断することは、決定論的でない課題である。
  論文  参考訳（メタデータ） (2024-01-22T12:51:19Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
  GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。 TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
  論文  参考訳（メタデータ） (2023-05-21T17:51:35Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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