論文の概要: Automated Formalization via Conceptual Retrieval-Augmented LLMs

• arxiv url: http://arxiv.org/abs/2508.06931v1
• Date: Sat, 09 Aug 2025 10:54:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-12 21:23:28.617424
• Title: Automated Formalization via Conceptual Retrieval-Augmented LLMs
• Title（参考訳）: 概念検索型LLMによる自動形式化
• Authors: Wangyue Lu, Lun Du, Sirui Li, Ke Weng, Haozhe Sun, Hengyu Liu, Minghe Yu, Tiancheng Zhang, Ge Yu,
• Abstract要約: CRAMFは概念駆動のRetrieval-Augmented Mathematical Formalizationフレームワークである。 概念定義知識ベースをMathlib4から自動構築するフレームワークを提案する。 miniF2F, ProofNet, そして新たに提案したAdvancedMathベンチマークでは, CRAMF を LLM ベースのオートフォーマライザにシームレスに統合できることが示されている。
• 参考スコア（独自算出の注目度）: 19.328918823576153
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Interactive theorem provers (ITPs) require manual formalization, which is labor-intensive and demands expert knowledge. While automated formalization offers a potential solution, it faces two major challenges: model hallucination (e.g., undefined predicates, symbol misuse, and version incompatibility) and the semantic gap caused by ambiguous or missing premises in natural language descriptions. To address these issues, we propose CRAMF, a Concept-driven Retrieval-Augmented Mathematical Formalization framework. CRAMF enhances LLM-based autoformalization by retrieving formal definitions of core mathematical concepts, providing contextual grounding during code generation. However, applying retrieval-augmented generation (RAG) in this setting is non-trivial due to the lack of structured knowledge bases, the polymorphic nature of mathematical concepts, and the high precision required in formal retrieval. We introduce a framework for automatically constructing a concept-definition knowledge base from Mathlib4, the standard mathematical library for the Lean 4 theorem prover, indexing over 26,000 formal definitions and 1,000+ core mathematical concepts. To address conceptual polymorphism, we propose contextual query augmentation with domain- and application-level signals. In addition, we design a dual-channel hybrid retrieval strategy with reranking to ensure accurate and relevant definition retrieval. Experiments on miniF2F, ProofNet, and our newly proposed AdvancedMath benchmark show that CRAMF can be seamlessly integrated into LLM-based autoformalizers, yielding consistent improvements in translation accuracy, achieving up to 62.1% and an average of 29.9% relative improvement.
• Abstract（参考訳）: 対話的定理証明者(ITP)は、労働集約的で専門家の知識を必要とする手作業の形式化を必要とする。 自動形式化は潜在的な解決策を提供するが、モデル幻覚(例えば、未定義の述語、シンボル誤用、バージョン非互換性)と、自然言語記述における曖昧さや欠落による意味的ギャップという2つの大きな課題に直面している。 これらの問題に対処するため、我々はCRAMF(Concept-driven Retrieval-Augmented Mathematical Formalization framework)を提案する。 CRAMFは、コア数学的概念の形式的定義を取得することにより、LLMベースのオートフォーマル化を強化し、コード生成時のコンテキスト基底を提供する。 しかし、この環境での検索強化生成(RAG)の適用は、構造化知識基盤の欠如、数学的概念の多型性、形式的検索に必要な高精度さなどにより、簡単ではない。 我々は、Lean 4定理証明器の標準的な数学的ライブラリであるMathlib4から概念定義知識ベースを自動的に構築するフレームワークを導入し、26,000以上の形式定義と1000以上のコア数学的概念をインデックス化する。 概念的多型に対処するため,ドメインレベルおよびアプリケーションレベルの信号を用いたコンテキストクエリ拡張を提案する。 さらに, 高精度かつ関連性の高い定義検索を実現するために, 再ランク付けされた2チャネルハイブリッド検索戦略を設計する。 miniF2F, ProofNet, そして新たに提案したAdvancedMathベンチマークでは, CRAMF を LLM ベースのオートフォーマライザにシームレスに統合し,翻訳精度を一貫した改善を実現し,62.1%, 平均29.9% の相対的改善を実現した。

関連論文リスト

• Computational Thinking Reasoning in Large Language Models [69.28428524878885]
  計算思考モデル(CTM)は、計算思考パラダイムを大規模言語モデル(LLM)に組み込んだ新しいフレームワークである。 ライブコード実行は推論プロセスにシームレスに統合され、CTMが計算によって考えることができる。 CTMは、精度、解釈可能性、一般化可能性の観点から、従来の推論モデルとツール拡張ベースラインを上回っている。
  論文  参考訳（メタデータ） (2025-06-03T09:11:15Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
  本稿では,高品質なオリンピアードレベルの数学問題を自動生成する新しい手法であるPromptCoTを紹介する。 提案手法は,問題構築の背景にある数学的概念と理論的根拠に基づいて複雑な問題を合成する。 提案手法は, GSM8K, MATH-500, AIME2024などの標準ベンチマークで評価され, 既存の問題生成手法を一貫して上回っている。
  論文  参考訳（メタデータ） (2025-03-04T06:32:30Z)
• Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions [8.135142928659546]
  我々は、ウィキペディア(Def_Wiki)とarXiv論文(Def_ArXiv)から定義を収集する、自動形式化のための2つの新しいリソースを紹介する。 我々は、Isabelle/HOLに定義を形式化する能力を解析し、LLMの範囲を評価した。 以上の結果から, miniF2Fのような既存のベンチマークと比較して, 定義がより困難であることが判明した。
  論文  参考訳（メタデータ） (2025-02-17T17:34:48Z)
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。 MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
  論文  参考訳（メタデータ） (2024-10-28T11:37:39Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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