論文の概要: FormalGrad: Integrating Formal Methods with Gradient-Based LLM Refinement

• arxiv url: http://arxiv.org/abs/2508.10059v1
• Date: Tue, 12 Aug 2025 22:03:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-15 22:24:48.059671
• Title: FormalGrad: Integrating Formal Methods with Gradient-Based LLM Refinement
• Title（参考訳）: FormalGrad: グラディエント型LCMリファインメントによる形式的手法の統合
• Authors: Yueke Zhang, Yifan Zhang, Kevin Leach, Yu Huang,
• Abstract要約: FormalGradは、形式的なメソッドを直接反復生成ループに統合する、原則化されたフレームワークを導入している。 コードを微分可能な変数として扱い、構造化されたフィードバックと形式的な制約をテキストの擬似階調に変換する。 我々は,HumanEval,HumanEval+,LiveCodeBenchベンチマーク上でFormalGradを評価する。
• 参考スコア（独自算出の注目度）: 8.574686422653345
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: While Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, they often produce solutions that lack guarantees of correctness, robustness, and efficiency. The limitation is acute in domains requiring strict constraints. FormalGrad introduces a principled framework that integrates formal methods directly into an iterative LLM-based generation loop. It uniquely treats code as a differentiable variable, converting structured feedback and formal constraints into a textual pseudo-gradient. This gradient guides the model to iteratively refine solutions, ensuring they are not only functional but also robust and formally justified. We evaluate FormalGrad on the HumanEval, HumanEval+, and LiveCodeBench benchmarks. Our implementation outperforms strong baselines, achieving an absolute improvement of up to 27% on HumanEval and a 41% relative improvement on the challenging LiveCodeBench V6. FormalGrad generates formally justified code that is robust and efficient, paving the way for reliable AI-assisted software development in high-stakes applications.
• Abstract（参考訳）: 大規模言語モデル(LLM)はコード生成において顕著な能力を示してきたが、正確性、堅牢性、効率性の保証を欠いたソリューションをしばしば生み出す。 この制限は、厳密な制約を必要とする領域において急性である。 FormalGradは、形式的なメソッドを直接反復的なLCMベースの生成ループに統合する、原則化されたフレームワークを導入している。 コードを微分可能な変数として一意に扱い、構造化されたフィードバックと形式的な制約をテキストの擬似階調に変換する。 この勾配は、モデルを反復的に洗練された解へと導き、それらが機能的だけでなく、頑健で正式に正当化されることを保証する。 我々は,HumanEval,HumanEval+,LiveCodeBenchベンチマーク上でFormalGradを評価する。 私たちの実装は、HumanEvalで最大27%の改善を実現し、挑戦的なLiveCodeBench V6で41%の相対的な改善を実現しています。 FormalGradは、堅牢で効率的な、正式に正当化されたコードを生成する。

関連論文リスト

• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
  大規模言語モデル(LLM)の最近の進歩は、コーディングベンチマークのパフォーマンスを改善している。 しかし、手軽に利用できる高品質なデータの枯渇により、改善は停滞している。 本稿では,単一モデルのコードとテスト生成能力を共同で改善するセルフプレイ・ソルバ検証フレームワークであるSol-Verを提案する。
  論文  参考訳（メタデータ） (2025-02-20T18:32:19Z)
• LLM4EFFI: Leveraging Large Language Models to Enhance Code Efficiency and Correctness [38.399282089600284]
  大規模言語モデル(LLM)は、コード生成において素晴らしいパフォーマンスを示している。 ulineLarge ulineLanguage ulineModel for Code ulineEfficiencyは、LLMが効率性と正確性の両方のバランスをとるコードを生成することができる新しいフレームワークである。
  論文  参考訳（メタデータ） (2025-02-17T07:01:18Z)
• CodeDPO: Aligning Code Models with Self Generated and Verified Source Code [52.70310361822519]
  我々は、コード生成に好み学習を統合するフレームワークであるCodeDPOを提案し、コードの正確性と効率性という2つの重要なコード優先要因を改善した。 CodeDPOは、コードとテストケースを同時に生成、評価するセルフジェネレーション・アンド・バリデーションメカニズムを利用して、新しいデータセット構築方法を採用している。
  論文  参考訳（メタデータ） (2024-10-08T01:36:15Z)
• ECCO: Can We Improve Model-Generated Code Efficiency Without Sacrificing Functional Correctness? [12.862825053595934]
  ECCOは、自然言語(NL)ベースのコード生成と履歴ベースのコード編集という、2つのパラダイムを通じてプログラム効率を評価するためのベンチマークである。 実行情報の追加は機能的正確性を維持するのによく役立ち、NLフィードバックは効率を向上する。
  論文  参考訳（メタデータ） (2024-07-19T05:47:40Z)

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

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