論文の概要: SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?

• arxiv url: http://arxiv.org/abs/2609.21190v2
• Date: Tue, 22 Sep 2026 21:43:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-25 00:05:17.642677
• Title: SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
• Title（参考訳）: SWE-Proof: 言語モデルは実世界の問題を解決することができるか?
• Abstract要約: Benchprooferは、既知の正しいパッチでコーディングタスクを正式に認証されたパイプラインに変換するパイプラインです。 SWE-bench Verified に適用すると SWE-Proof が得られる。
• 参考スコア（独自算出の注目度）: 39.004582663385364
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Ensuring the correctness of LLM-generated code is a core challenge for modern software engineering. Benchmarks for agentic code generation check correctness with held-out test suites, which are inherently incomplete and increasingly susceptible to memorization. Formal verification avoids both problems, but existing work covers only standalone tasks whose specifications are given as input, not real issues, which touch large repositories and state intent in vague natural language. We present Benchproofer, a pipeline that turns a coding task with a known correct patch into a formally verified one: it writes a specification for the new code, summarizes the existing functions that code calls with axioms, and admits an instance only after mechanical and adversarial gates agree. Applying it to SWE-bench Verified yields SWE-Proof, 500 real issues whose correctness is formally verified rather than tested, and it extends to SWE-bench Pro. Evaluating Claude Opus 4.8, we find that verification catches what tests miss: a quarter of test-passing patches admit counterexamples, which a structured natural-language specification does not fix, while a correct formal one lifts resolution from 85% to 95%. Writing that specification is the hard part: an agent that must write its own gains nothing over an unaided baseline, and only 56% of those specifications pass our audit. The usual failure is faithfulness, a specification that constrains part of the required behavior and leaves the rest free. Specification quality still tracks the outcome, failing on 92% of unresolved instances against 51% of resolved ones, making faithful specification synthesis a concrete open problem.
• Abstract（参考訳）: LLM生成コードの正確性を保証することは、現代のソフトウェア工学における中核的な課題である。 エージェントコード生成のベンチマークは、保持されたテストスイートによる正当性をチェックする。 形式的検証はどちらの問題も避けるが、既存の作業はインプットとして仕様が与えられ、実際の問題ではなく、曖昧な自然言語で大きなリポジトリや状態意図に触れる独立したタスクのみをカバーする。 これは、既知の正しいパッチでコーディングタスクを正式に認証したパイプラインで、新しいコードの仕様を書き、公理でコードを呼び出す既存の関数を要約し、機械的および敵対的なゲートが同意した後のみインスタンスを許可する。 SWE-bench Verified に適用すると、SWE-bench Pro に拡張され、SWE-bench Pro に拡張される。 テストパスパッチの4分の1は、構造化された自然言語仕様が修正しない反例を認めており、正しい形式は、解像度を85%から95%に引き上げている。 その仕様を書かなければならないエージェントは、未確認のベースラインに何の利益も与えず、それらの仕様の56%だけが監査に合格します。 通常の失敗は忠実さであり、必要な振る舞いの一部を制約し、残りを自由にしておく仕様です。 仕様の品質は依然として結果を追跡しており、未解決インスタンスの92%が解決インスタンスの51%に対して失敗し、忠実な仕様合成が具体的なオープンな問題となっている。

関連論文リスト

• Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning [7.228124845671868]
  ニューロフォーマル検証(NFV)は、主流プログラミング言語の開発者の自動化を活用する。 AI符号化エージェントが翻訳し、確立された検証者が決定し、機械チェックされた証明により、音質よりも経験的精度で、主流言語で提起された質問にプッシュボタンで回答する。 正誤のPython問題のデータセットの結果は、llm-as-judgeベースラインと比較して推奨されている。
  論文  参考訳（メタデータ） (2026-08-21T18:00:02Z)
• Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
  SpecCoderは、検証済みの参照プログラム、振る舞いを変えるミュータント、マルチターン仕様修正トレースから学ぶトレーニングフレームワークである。 SpecCoderは、欠陥のある実行を拒否しながら正しい実行を保持する仕様を選択し、受動的アノテーションから実行可能なエビデンスに変換する。
  論文  参考訳（メタデータ） (2026-07-05T11:09:30Z)
• Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization [26.123396123145415]
  LLMエージェントが非公式なプログラミング問題を忠実な形式仕様に変換することができるかどうか、仕様自動書式化について検討する。 Codeforces問題から派生した581の仕様記述タスクのベンチマークであるVerus-SpecBenchを紹介する。 フェールモードの解析は、モデル生成仕様が重要な入力仮定を受け入れ、誤った出力を受け入れ、有効な仕様を拒否できることを示している。
  論文  参考訳（メタデータ） (2026-05-26T02:12:48Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。 RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。 Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
  論文  参考訳（メタデータ） (2026-04-29T09:57:07Z)
• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。 NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。 7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。 以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
  論文  参考訳（メタデータ） (2026-04-24T14:28:10Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。 プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。 また, GPT-4o miniが74.18%と高い修理成功率を示した。
  論文  参考訳（メタデータ） (2025-07-04T15:36:12Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)

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

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