論文の概要: How Stable Are LLM-Generated Proofs Under Program Refactoring? A Stress Test for Verifiable Code Generation

• arxiv url: http://arxiv.org/abs/2610.36328v1
• Date: Mon, 26 Oct 2026 21:56:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-28 21:04:31.439058
• Title: How Stable Are LLM-Generated Proofs Under Program Refactoring? A Stress Test for Verifiable Code Generation
• Title（参考訳）: プログラムリファクタリングにおけるLLM生成証明の安定性 : 検証可能なコード生成のためのストレステスト
• Abstract要約: RefactorProofは、ピン付き環境でコンパイルされる185のVERINAタスクから458のLean-certified variantを導出します。 VERINAは46のタスクに対する参照証明を提供しており、いずれも基本的な分割からである。 特殊な証明器は、供給された参照アーティファクトよりも総合的に無防備な生存率が高い。
• 参考スコア（独自算出の注目度）: 2.2903728931592395
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Benchmarks for verifiable code generation usually test a proof against one fixed implementation. We ask whether the same proof remains valid after a program refactoring that preserves behavior. We introduce RefactorProof, which derives 458 Lean-certified variants from the 185 VERINA tasks that compile in our pinned environment while holding the specification and evaluated proof fixed byte-for-byte. VERINA supplies reference proofs for 46 tasks, all from its basic split; the primary model-versus-reference comparisons further match on 21-25 short, non-recursive tasks. Structural refactorings expose substantial brittleness across proof sources: task-normalized structural PSR is 4.3% for the supplied references and 13.3-26.8% for the specialized provers. On the matched tasks, specialized prover proofs nevertheless have higher overall unchanged-proof survival than the supplied reference artifacts: +15.6 points for DeepSeek-Prover-V2-7B, +18.8 for Goedel-Prover-V2-32B, and +20.3 for Goedel-Prover-V2-8B; all three 95% CIs exclude zero. The ordering persists after excluding universally survived T1 variants, under family-balanced aggregation, and under alternative deployable valid-proof selection rules. However, unchanged-proof failure is not the same as high repair cost: predefined one-identifier edits repair 51/54 eligible reference structural failures and 58/85 eligible prover failures. RefactorProof therefore measures unchanged-proof stability under program refactoring, not the cost of maintaining a proof after it breaks.
• Abstract（参考訳）: 検証可能なコード生成のベンチマークは通常、1つの固定実装に対する証明をテストする。 動作を保存するプログラムリファクタリング後に、同じ証明が有効であるかどうかを問う。 RefactorProofを紹介します。これは185のVERINAタスクから458のLean-certified variantを導き出します。 VERINAは46のタスクに対する参照証明を提供しており、いずれも基本的な分割からである。 タスク正規化された構造PSRは、供給された参照に対して4.3%、特別なプローバーに対して13.3-26.8%である。 一致したタスクでは、特別な証明は供給された参照アーティファクトよりも総合的に変化しない生存率が高く、+15.6ポイントはDeepSeek-Prover-V2-7B、+18.8ポイントはGoedel-Prover-V2-32B、+20.3ポイントはGoedel-Prover-V2-8Bである。 順序付けは、普遍的に生き残ったT1変種を除外し、ファミリーバランスの取れたアグリゲーションの下で、また、代替のデプロイ可能な有効防御選択ルールの下で継続する。 事前定義された1識別器は、51/54の基準構造的故障と58/85の許容する証明的故障を補正する。 したがってRefactorProofは、プログラムのリファクタリングにおいて、不確実な安定性を計測する。

関連論文リスト

• EviRepair: Evidence-Driven Agents for Reliable Vulnerability Repair [55.22600943144124]
  リポジトリレベルの脆弱性修復のためのエビデンス駆動型マルチエージェントフレームワークであるEviRepairを提案する。 EviRepairは、エージェントが協力して証拠を収集できるようにすることによって、修復プロセスにエビデンスレビューを導入する。 PatchEvalとSecBenchベンチマークの実験は、EviRepairが既存のエージェントベースのベースラインを一貫して上回ることを示した。
  論文  参考訳（メタデータ） (2026-10-09T12:22:43Z)
• MemToC: Benchmarking Memory-Tool Conflict Resolution in Large Language Models [49.47300047353726]
  MemToCは、実行時ツールによるポストツール-リターン仲裁のベンチマークである。 MemToCは、542の質制御された事実質問から構築された6,504回の評価エピソードで構成されている。 オープンウェイトな7-9Bモデルでは、ツールが強く支配的なクローズドブックの回答を返す。
  論文  参考訳（メタデータ） (2026-08-26T18:22:03Z)
• Does Fixing Break Security? An Empirical Study of Security Degradation in Iterative LLM-Driven Infrastructure-as-Code Repair [2.4063592468412276]
  イテレーティブなIaC修復はセキュリティのレグレッションを導入するが、保守的で防御可能なレートはおよそ3.3%のシナリオである。 本研究は,セキュリティに配慮したフィードバックループ設計と,実行可能な反復予算指導の動機付けである。
  論文  参考訳（メタデータ） (2026-08-13T16:01:32Z)
• Security Tests as Executable Specifications for LLM Code Generation: Benefits, Trade-offs, and Coverage Limits [14.44743150931186]
  テストが事前に表示されるか、失敗した実行がリビジョンを引き起こすか、失敗が選択され、どのように表現されるかの3つの要素を分離する、制御されたテストフィードバックの足場を開発する。 2,705の軌道、31のタスクインスタンス、3つのセキュアコードベンチマーク、16のCWEカテゴリ、2つのモデルファミリがあり、すべての目に見えるテストが前もって隠れた機能とセキュリティのジョイントの成功を平均19.3%増加させている。 共有候補比較では、構造化されたフィードバック修復は、当初、共同回帰のない80の候補が失敗し、固定された生フィードバック修復83は3つの回帰を引き起こす。
  論文  参考訳（メタデータ） (2026-08-10T15:37:09Z)
• Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair [36.56438114281786]
  正しいパッチの発見と保持、検証、提出のギャップについて検討する。 我々はエビデンスバウンド型ループ契約を導出し、その機械的に強制可能なサブセットを参照実装でインスタンス化する。
  論文  参考訳（メタデータ） (2026-07-27T16:05:23Z)
• Beyond Fail-to-Pass: Iterative Hardening of Co-Generated Bug Reproduction Tests and Fixes [55.114939648705395]
  大規模言語モデル(LLM)は、現実のバグに対して、プログラムの自動修正をますます実用的にしている。 バグ再現テスト(BRT)は、バグレポートを実行可能なバグ固有の信号に変換することで、このギャップを埋めるのに役立つ。 本稿では,ループ内収束基準としてLax信号を用いるコジェネレーションフレームワークであるCoHardenを提案する。
  論文  参考訳（メタデータ） (2026-07-22T07:30:07Z)
• Are Benchmark Tests Strong Enough? Mutation-Guided Diagnosis and Augmentation of Regression Suites [49.16055123488827]
  十分に強力なテストスイートは、報告された成功率を膨らませながら、妥当だが意味的に正しくないパッチを認めることができる。 STINGは、意味的に変化するプログラムの変種を診断ストレス要因として利用する、ターゲットテスト拡張のためのフレームワークである。 STINGは211インスタンスにまたがる1014の検証テストを生成し、パッチリージョンラインとブランチカバレッジを10.8%、9.5%向上させた。
  論文  参考訳（メタデータ） (2026-04-02T01:13:40Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)

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

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