論文の概要: APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries

• arxiv url: http://arxiv.org/abs/2504.19110v2
• Date: Thu, 22 May 2025 15:53:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-23 17:12:47.769741
• Title: APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries
• Title（参考訳）: APE-Bench I:形式数学ライブラリのファイルレベル自動証明工学を目指して
• Authors: Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, Wenda Li,
• Abstract要約: APE-Bench Iは、Mathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークである。 Eleansticはスケーラブルな並列検証インフラストラクチャで、Mathlibの複数バージョンにわたる検証に最適化されている。
• 参考スコア（独自算出の注目度）: 5.227446378450704
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent progress in large language models (LLMs) has shown promise in formal theorem proving, yet existing benchmarks remain limited to isolated, static proof tasks, failing to capture the iterative, engineering-intensive workflows of real-world formal mathematics libraries. Motivated by analogous advances in software engineering, we introduce the paradigm of Automated Proof Engineering (APE), which aims to automate proof engineering tasks such as feature addition, proof refactoring, and bug fixing using LLMs. To facilitate research in this direction, we present APE-Bench I, the first realistic benchmark built from real-world commit histories of Mathlib4, featuring diverse file-level tasks described in natural language and verified via a hybrid approach combining the Lean compiler and LLM-as-a-Judge. We further develop Eleanstic, a scalable parallel verification infrastructure optimized for proof checking across multiple versions of Mathlib. Empirical results on state-of-the-art LLMs demonstrate strong performance on localized edits but substantial degradation on handling complex proof engineering. This work lays the foundation for developing agentic workflows in proof engineering, with future benchmarks targeting multi-file coordination, project-scale verification, and autonomous agents capable of planning, editing, and repairing formal libraries.
• Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩は形式定理の証明において有望であることを示しているが、既存のベンチマークは孤立した静的な証明タスクに限られており、実世界の形式数学ライブラリの反復的な工学的なワークフローを捉えていない。 ソフトウェア工学の類似的な進歩に触発され,機能追加や証明リファクタリング,LLMを用いたバグ修正などの証明工学タスクを自動化することを目的とした,自動証明工学(APE)のパラダイムを紹介した。 APE-Bench IはMathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークであり、自然言語で記述された多様なファイルレベルのタスクを特徴とし、LeanコンパイラとLLM-as-a-Judgeを組み合わせたハイブリッドアプローチによって検証されている。 さらに,複数のバージョンのMathlibの検証に最適化された,スケーラブルな並列検証インフラストラクチャであるEleansticを開発した。 最先端LLMの実証実験の結果は、局所的な編集では高い性能を示すが、複雑な証明工学の処理では著しく劣化する。 この研究は、証明工学におけるエージェントワークフローの開発の基礎を築き、将来のベンチマークは、複数ファイルの調整、プロジェクト規模の検証、そして正式なライブラリの計画、編集、修復が可能な自律エージェントをターゲットにしている。

関連論文リスト

• On LLM-Assisted Generation of Smart Contracts from Business Processes [0.08192907805418582]
  大規模言語モデル(LLM)は、ソフトウェアの生成方法の現実を変えました。 本稿では、ビジネスプロセス記述からスマートコントラクトコードを生成するためのLCMの使用について探索的研究を行う。 以上の結果から,LLMの性能はスマートコントラクト開発に必要な信頼性に劣ることがわかった。
  論文  参考訳（メタデータ） (2025-07-30T20:39:45Z)
• Discrete Tokenization for Multimodal LLMs: A Comprehensive Survey [69.45421620616486]
  本研究は、大規模言語モデル(LLM)用に設計された離散トークン化手法の最初の構造的分類と解析である。 古典的および近代的なパラダイムにまたがる8つの代表的なVQ変種を分類し、アルゴリズムの原理を分析し、力学を訓練し、LLMパイプラインとの統合に挑戦する。 コードブックの崩壊、不安定な勾配推定、モダリティ固有の符号化制約など、重要な課題を特定する。
  論文  参考訳（メタデータ） (2025-07-21T10:52:14Z)
• MLE-Dojo: Interactive Environments for Empowering LLM Agents in Machine Learning Engineering [57.156093929365255]
  自律型大規模言語モデル(LLM)エージェントを体系的に強化し、評価し、改善するためのガイムスタイルのフレームワーク。 MLE-Dojoは、現実的なエンジニアリングシナリオを反映した、多様でオープンなMLEタスクを慎重にキュレートする。 完全に実行可能な環境は、教師付き微調整と強化学習の両方を通して包括的なエージェントトレーニングをサポートする。
  論文  参考訳（メタデータ） (2025-05-12T17:35:43Z)
• Evaluating Large Language Models for Real-World Engineering Tasks [75.97299249823972]
  本稿では,実運用指向のエンジニアリングシナリオから得られた100以上の質問をキュレートしたデータベースを提案する。 このデータセットを用いて、4つの最先端の大規模言語モデル(LLM)を評価する。 以上の結果から,LLMは時間的および構造的推論において強みを示すが,抽象的推論や形式的モデリング,文脈に敏感な工学的論理にはかなり苦労することがわかった。
  論文  参考訳（メタデータ） (2025-05-12T14:05:23Z)
• Paper2Code: Automating Code Generation from Scientific Papers in Machine Learning [57.09163579304332]
  機械学習論文を機能コードリポジトリに変換するフレームワークであるPaperCoderを紹介した。 PaperCoderは3つの段階で動作する。計画、図によるシステムアーキテクチャの設計、ファイル依存の特定、構成ファイルの生成である。 次に、モデルベースおよび人的評価の両方に基づいて、機械学習論文からコード実装を生成するPaperCoderを評価する。
  論文  参考訳（メタデータ） (2025-04-24T01:57:01Z)
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.4779196219827508]
  組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。 我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
  論文  参考訳（メタデータ） (2025-04-23T18:04:38Z)
• Towards Automated Formal Verification of Backend Systems with LLMs [9.66648456498893]
  バックエンドのコードを形式的なリーン表現に変換するために,関数型プログラミングと型システムを活用する新しいフレームワークを提案する。 我々のパイプラインは、APIやデータベース操作の意図した振る舞いを規定する定理を自動生成し、LSMベースのプロバーを用いて検証する。 本手法を現実的なバックエンドシステム上で評価した結果,テスト要件の50%以上を正式に検証できることがわかった。
  論文  参考訳（メタデータ） (2025-04-13T16:49:37Z)
• TuRTLe: A Unified Evaluation of LLMs for RTL Generation [0.6010802600885173]
  本研究では,主要なRTL生成タスク間でLLMを評価するための統合評価フレームワークTuRTLeを提案する。 オープンLLMの多様なセットをベンチマークし、EDA固有のタスクの長所と短所を分析します。 以上の結果から,DeepSeek R1のような推論モデルの方が,複数の評価基準で常に優れていたことが示唆された。
  論文  参考訳（メタデータ） (2025-03-31T07:43:12Z)
• VeriMind: Agentic LLM for Automated Verilog Generation with a Novel Evaluation Metric [4.590930025882158]
  We propose VeriMind, a agentic LLM framework for Verilog code generation。 本稿では,従来のpass@k測度とARC(Average Refinement Cycles)を組み合わせた新しい評価手法を提案する。 様々なハードウェア設計タスクの実験結果によると、我々のアプローチはpass@kメトリックで最大8.3%、pass@ARCメトリックで最大8.1%向上した。
  論文  参考訳（メタデータ） (2025-03-15T23:43:06Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Commit0: Library Generation from Scratch [77.38414688148006]
  Commit0は、AIエージェントにスクラッチからライブラリを書くよう促すベンチマークである。 エージェントには、ライブラリのAPIを概説する仕様文書と、インタラクティブなユニットテストスイートが提供されている。 Commit0はまた、モデルが生成したコードに対して静的解析と実行フィードバックを受け取る、インタラクティブな環境も提供する。
  論文  参考訳（メタデータ） (2024-12-02T18:11:30Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Reference Trustable Decoding: A Training-Free Augmentation Paradigm for Large Language Models [79.41139393080736]
  大規模言語モデル(LLM)は急速に進歩し、印象的な機能を示している。 In-Context Learning (ICL) など。 効率的なファインチューニング(PEFT)は、現在2つの主要な拡張方法である。 下流タスクへのLLM。 我々は、モデルが微調整なしで新しいタスクに迅速に適応できるパラダイムである参照信頼復号(RTD)を提案する。
  論文  参考訳（メタデータ） (2024-09-30T10:48:20Z)
• AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
  本稿では,アサーション生成におけるLarge-Language Modelsの有効性を評価するための新しいベンチマークを提案する。 AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
  論文  参考訳（メタデータ） (2024-06-26T14:47:28Z)
• Enhancing LLM-based Test Generation for Hard-to-Cover Branches via Program Analysis [8.31978033489419]
  難解な分岐に到達可能なテストを生成する新しい技術である TELPA を提案する。 27のオープンソースPythonプロジェクトに対する実験結果から,TELPAは最先端のSBSTやLLMベースの技術よりも優れていたことが判明した。
  論文  参考訳（メタデータ） (2024-04-07T14:08:28Z)
• LLM Inference Unveiled: Survey and Roofline Model Insights [62.92811060490876]
  大規模言語モデル(LLM)推論は急速に進化しており、機会と課題のユニークなブレンドを提示している。 本調査は, 研究状況を要約するだけでなく, 屋上モデルに基づく枠組みを導入することによって, 従来の文献レビューから際立っている。 このフレームワークは、ハードウェアデバイスにLSMをデプロイする際のボトルネックを特定し、実用上の問題を明確に理解する。
  論文  参考訳（メタデータ） (2024-02-26T07:33:05Z)
• ML-Bench: Evaluating Large Language Models and Agents for Machine Learning Tasks on Repository-Level Code [76.84199699772903]
  ML-Benchは、既存のコードリポジトリを利用してタスクを実行する現実世界のプログラミングアプリケーションに根ざしたベンチマークである。 LLM(Large Language Model)とAIエージェントの両方を評価するために、事前に定義されたデプロイメント環境でLLMのテキスト-コード変換を評価するML-LLM-Benchと、Linuxサンドボックス環境でエンドツーエンドのタスク実行で自律エージェントをテストするML-Agent-Benchの2つの設定が採用されている。
  論文  参考訳（メタデータ） (2023-11-16T12:03:21Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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