論文の概要: BRIDGE: Building Representations In Domain Guided Program Verification

• arxiv url: http://arxiv.org/abs/2511.21104v1
• Date: Wed, 26 Nov 2025 06:39:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-27 18:37:58.99414
• Title: BRIDGE: Building Representations In Domain Guided Program Verification
• Title（参考訳）: BRIDGE: ドメインガイドによるプログラム検証における表現の構築
• Authors: Robert Joseph George, Carson Eisenach, Udaya Ghai, Dominique Perrault-Joncas, Anima Anandkumar, Dean Foster,
• Abstract要約: BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
• 参考スコア（独自算出の注目度）: 67.36686119518441
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) have achieved impressive results in code generation, yet struggle with program verification, especially in interactive proof frameworks such as Lean4. A central challenge is scalability: verified synthesis requires not just code, but also precise specifications and correctness proofs, and existing approaches rarely span all three domains. We present BRIDGE, the first systematic study of structured prompting for scalable verified program generation. BRIDGE decomposes verification into three interconnected domains: Code (executable implementations), Specifications (formal intent statements), and Proofs (constructive correctness arguments). Our key idea is to elicit distinct reasoning behaviors functional, specification-driven, and proof-oriented as intermediate representations that preserve semantic structure and connect these domains. Through systematic ablations, we show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods. For example, functional reasoning improves correctness of code in formal languages (Lean4) by nearly 1.5x (pass@5) over direct baselines. In inference-time compute, functional reasoning is also 2x more efficient, achieving higher pass rates with fewer generations and lower total sampling budgets. Similarly, we find that specification-driven prompting boosts Python coding pass rates by up to 17.5%. These findings suggest that structured domain alignment is a promising direction for advancing verified synthesis. BRIDGE establishes a foundation for training via expert iteration or RLVR, enabling models to internalize these reasoning strategies across code, specifications, and proofs.
• Abstract（参考訳）: 大規模言語モデル(LLM)はコード生成において印象的な成果を上げていますが、特にLean4のようなインタラクティブな実証フレームワークでは、プログラム検証に苦戦しています。 検証された合成にはコードだけでなく、正確な仕様と正当性証明が必要です。 BRIDGEは、スケーラブルな検証プログラム生成のための構造化プロンプトの最初の体系的な研究である。 BRIDGEは、検証をコード(実行可能実装)、仕様(形式的インテントステートメント)、証明(構成的正当性引数)の3つの相互接続ドメインに分解する。 我々のキーとなる考え方は、セマンティック構造を保持し、これらのドメインを接続する中間表現として機能的、仕様駆動的、そして証明指向の異なる推論行動を引き出すことである。 体系的な改善を通じて、本手法は標準誤差フィードバック法よりも精度と効率を著しく改善することを示す。 例えば、関数推論は形式言語(Lean4)におけるコードの正しさを、直接ベースラインよりも1.5倍(pass@5)近く向上させる。 推論時間計算では、関数的推論も2倍効率が高く、より少ない世代でより高い通過率を達成でき、総サンプリング予算も小さくなる。 同様に、仕様駆動のプロンプトはPythonのコーディングパス率を最大17.5%向上させる。 これらの結果から, 構造ドメインアライメントは, 精度の高い合成を推し進める上で有望な方向であることが示唆された。 BRIDGEはエキスパートイテレーションまたはRLVRによるトレーニングの基礎を確立し、モデルがコード、仕様、証明を越えてこれらの推論戦略を内部化できるようにする。

関連論文リスト

• TeaRAG: A Token-Efficient Agentic Retrieval-Augmented Generation Framework [62.66056331998838]
  TeaRAGは、検索内容と推論ステップの両方を圧縮できるトークン効率のエージェントRAGフレームワークである。 報奨関数は,過剰な推論ステップをペナルティ化しながら,知識マッチング機構によって知識満足度を評価する。
  論文  参考訳（メタデータ） (2025-11-07T16:08:34Z)
• Chain of Execution Supervision Promotes General Reasoning in Large Language Models [48.100128916029064]
  TracePileは260万のサンプルからなる大規模なコーパスで、コード実行を明示的でステップバイステップのチェーン・オブ・シンクスタイルの論理に変換する。 我々は,継続事前訓練,事前訓練後の指導訓練,2段階微調整という3つのトレーニング設定を用いてTracePileを評価する。 特にTracePileは、9つの数学データセットでLLaMA3.1-8Bを平均7.1%向上させ、LiveCodeBench、CRUX、MMLUで明確なゲインを提供する。
  論文  参考訳（メタデータ） (2025-10-24T02:21:11Z)
• CodeRL+: Improving Code Generation via Reinforcement with Execution Semantics Alignment [98.87395842351627]
  大きな言語モデル(LLM)は、巨大なコードコーパスから学習することで、コード生成において優れています。 テキストパターンのトレーニングと機能的正しさの目標の間には、基本的な意味的ギャップが残っている。 我々は、コード生成のためのRLVRトレーニングパイプラインに実行セマンティクスアライメントを統合する新しいアプローチであるCodeRL+を提案する。
  論文  参考訳（メタデータ） (2025-10-21T09:48:06Z)
• ConciseHint: Boosting Efficient Reasoning via Continuous Concise Hints during Generation [74.37307916314407]
  提案するフレームワークはConciseHintと呼ばれ,推論モデルが簡潔に話すことを継続的に奨励する。 DeepSeek-R1 および Qwen-3 シリーズを含む最先端の LRM 実験により,本手法が簡潔な推論を効果的に生成できることが実証された。
  論文  参考訳（メタデータ） (2025-06-23T16:20:44Z)
• ProtoReasoning: Prototypes as the Foundation for Generalizable Reasoning in LLMs [54.154593699263074]
  ProtoReasoningは、大規模推論モデルの推論能力を高めるフレームワークである。 ProtoReasoningは問題を対応するプロトタイプ表現に変換する。 ProtoReasoningは論理的推論に基づくベースラインモデルよりも4.7%改善されている。
  論文  参考訳（メタデータ） (2025-06-18T07:44:09Z)
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
  組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。 我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
  論文  参考訳（メタデータ） (2025-04-23T18:04:38Z)
• VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
  VEL はマシンチェック可能な正当性証明を備えた公式な EL++ 推論器である。 本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。
  論文  参考訳（メタデータ） (2024-12-11T19:17:28Z)
• Think Beyond Size: Adaptive Prompting for More Effective Reasoning [0.0]
  本稿では,動的かつ反復的なフレームワークであるAdaptive Promptingを紹介する。 その結果、Adaptive Promptingは、算術的推論(GSM8K、MultiArithm)、論理的推論、コモンセンスタスクなど、様々な推論ベンチマークのパフォーマンスを著しく向上させることを示した。 提案手法は,計算効率を維持しつつ,GPT-4などの大規模モデルと競合する性能を実現する。
  論文  参考訳（メタデータ） (2024-10-10T17:14:36Z)

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

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