論文の概要: Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
- arxiv url: http://arxiv.org/abs/2504.17017v1
- Date: Wed, 23 Apr 2025 18:04:38 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-05-02 19:15:53.129144
- Title: Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
- Title（参考訳）: 神経理論の証明:形式的検証のための証明の生成と構造化
- Authors: Balaji Rao, William Eiers, Carlo Lipizzi,
- Abstract要約: 組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。
LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。
我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
- 参考スコア（独自算出の注目度）: 0.4779196219827508
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Formally verifying properties of software code has been a highly desirable task, especially with the emergence of LLM-generated code. In the same vein, they provide an interesting avenue for the exploration of formal verification and mechanistic interpretability. Since the introduction of code-specific models, despite their successes in generating code in Lean4 and Isabelle, the task of generalized theorem proving still remains far from being fully solved and will be a benchmark for reasoning capability in LLMs. In this work, we introduce a framework that generates whole proofs in a formal language to be used within systems that utilize the power of built-in tactics and off-the-shelf automated theorem provers. Our framework includes 3 components: generating natural language statements of the code to be verified, an LLM that generates formal proofs for the given statement, and a module employing heuristics for building the final proof. To train the LLM, we employ a 2-stage fine-tuning process, where we first use SFT-based training to enable the model to generate syntactically correct Isabelle code and then RL-based training that encourages the model to generate proofs verified by a theorem prover. We validate our framework using the miniF2F-test benchmark and the Isabelle proof assistant and design a use case to verify the correctness of the AWS S3 bucket access policy code. We also curate a dataset based on the FVEL\textsubscript{\textnormal{ER}} dataset for future training tasks.
- Abstract（参考訳）: ソフトウェアコードの形式的検証は、特にLLM生成コードの出現において、非常に望ましい課題である。
同じ静脈において、彼らは形式的検証と機械的解釈可能性の探索の興味深い道を提供する。
コード固有モデルの導入以来、Lean4とIsabelleでのコード生成の成功にもかかわらず、一般化された定理証明のタスクは、まだ完全に解決されるには程遠いままであり、LLMの推論能力のベンチマークとなるでしょう。
本研究では,組込み戦術と既製の自動定理証明器の力を利用するシステム内で使用する形式言語における証明全体を生成するフレームワークを提案する。
私たちのフレームワークには,検証対象コードの自然言語文の生成,与えられた文の形式的証明を生成するLLM,最終的な証明を構築するためのヒューリスティックスを利用するモジュールという,3つのコンポーネントが含まれています。
LLMのトレーニングには、2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成し、次にRLベースのトレーニングによりモデルが定理証明器によって検証された証明を生成することを奨励する。
我々は、miniF2F-testベンチマークとIsabelle証明アシスタントを使用してフレームワークを検証し、AWS S3バケットアクセスポリシーコードの正確性を検証するユースケースを設計する。
また、将来のトレーニングタスクのために、FVEL\textsubscript{\textnormal{ER}}データセットに基づいてデータセットをキュレートする。
関連論文リスト
- Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。
訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。
トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
論文 参考訳（メタデータ） (2025-04-28T19:25:29Z) - APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
APE-Bench Iは、Mathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークである。
Eleansticはスケーラブルな並列検証インフラストラクチャで、Mathlibの複数バージョンにわたる検証に最適化されている。
論文 参考訳（メタデータ） (2025-04-27T05:04:02Z) - Insights from Verification: Training a Verilog Generation LLM with Reinforcement Learning with Testbench Feedback [36.69082579950107]
大規模言語モデル(LLM)は、自然言語記述からVerilog生成において強力な性能を示している。
本稿では,テストベンチからの検証洞察をVerilog 生成 LLM のトレーニングに統合する手法を提案する。
論文 参考訳（メタデータ） (2025-04-22T11:38:14Z) - Post-Incorporating Code Structural Knowledge into LLMs via In-Context Learning for Code Translation [10.77747590700758]
大規模言語モデル(LLM)はソフトウェアマイニングにおいて大きな進歩を遂げた。
ソースコードの構文構造を扱うことは 依然として課題です
本稿では、コード構造知識を事前学習したLLMに組み込むために、インコンテキスト学習(ICL)を用いる。
論文 参考訳（メタデータ） (2025-03-28T10:59:42Z) - Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。
本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software [0.4369550829556578]
本稿では,LLMによるコード生成と形式検証を組み合わせ,重要な組込みソフトウェアを作成する方法について検討する。
目標は、仕様のみから産業品質のコードを自動的に生成することだ。
論文 参考訳（メタデータ） (2024-11-20T12:38:17Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。
我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
論文 参考訳（メタデータ） (2024-07-03T15:36:18Z) - FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving [53.43068330741449]
大規模言語モデル(LLM)を用いた対話型形式検証環境FVELを提案する。
FVELは、検証対象のコードをIsabelleに変換し、LLMで証明された神経自動定理を用いて検証を行う。
FVELERデータセットには、Isabelleで定式化されたコード依存関係と検証プロセスが含まれており、758の理論、29,125のレムマ、200,646の証明ステップが含まれている。
論文 参考訳（メタデータ） (2024-06-20T15:31:05Z) - Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。
証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。
人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。
定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
論文 参考訳（メタデータ） (2024-04-18T22:54:08Z) - 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) - Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
Self-Checkerはファクトチェックを容易にするプラグインとプレイモジュールからなるフレームワークである。
このフレームワークは、低リソース環境でファクトチェックシステムを構築するための、高速で効率的な方法を提供する。
論文 参考訳（メタデータ） (2023-05-24T01:46:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。