論文の概要: Dissect-and-Restore: AI-based Code Verification with Transient Refactoring
- arxiv url: http://arxiv.org/abs/2510.25406v2
- Date: Thu, 30 Oct 2025 10:03:34 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-31 13:50:54.753821
- Title: Dissect-and-Restore: AI-based Code Verification with Transient Refactoring
- Title（参考訳）: Dissect-and-Restore: 過渡リファクタリングによるAIベースのコード検証
- Authors: Changjie Wang, Mariano Scazzariello, Anoud Alshnakat, Roberto Guanciale, Dejan Kostić, Marco Chiesa,
- Abstract要約: 提案するPrometheusは,現在のAI機能を備えた自動コード検証を容易にする,AI支援システムである。
プロメテウスは、複素補題の構造的分解を通じてより小さく検証可能な部分補題への証明探索を導く。
このアプローチは、ベースラインの68%に比べて、キュレートされたデータセットの86%のタスクをうまく検証します。
- 参考スコア（独自算出の注目度）: 1.2883590530210827
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal verification is increasingly recognized as a critical foundation for building reliable software systems. However, the need for specialized expertise to write precise specifications, navigate complex proof obligations, and learn annotations often makes verification an order of magnitude more expensive than implementation. While modern AI systems can recognize patterns in mathematical proofs and interpret natural language, effectively integrating them into the formal verification process remains an open challenge. We present Prometheus, a novel AI-assisted system that facilitates automated code verification with current AI capabilities in conjunction with modular software engineering principles (e.g., modular refactoring). Our approach begins by decomposing complex program logic, such as nested loops, into smaller, verifiable components. Once verified, these components are recomposed to construct a proof of the original program. This decomposition-recomposition workflow is non-trivial. Prometheus addresses this by guiding the proof search through structured decomposition of complex lemmas into smaller, verifiable sub-lemmas. When automated tools are insufficient, users can provide lightweight natural language guidance to steer the proof process effectively. Our evaluation demonstrates that transiently applying modular restructuring to the code substantially improves the AI's effectiveness in verifying individual components. This approach successfully verifies 86% of tasks in our curated dataset, compared to 68% for the baseline. Gains are more pronounced with increasing specification complexity, improving from 30% to 69%, and when integrating proof outlines for complex programs, from 25% to 87%.
- Abstract（参考訳）: 形式的検証は、信頼性のあるソフトウェアシステムを構築するための重要な基盤として、ますます認識されている。
しかしながら、正確な仕様を書き、複雑な証明義務をナビゲートし、アノテーションを学ぶための専門知識の必要性は、しばしば、検証を実装よりも桁違いに高価にする。
現代のAIシステムは、数学的証明のパターンを認識し、自然言語を解釈できるが、それらを形式的検証プロセスに効果的に統合することは、依然としてオープンな課題である。
Prometheusは、モジュール化されたソフトウェアエンジニアリングの原則(例えば、モジュール化されたリファクタリング)と合わせて、現在のAI機能による自動コード検証を容易にする、新しいAI支援システムである。
私たちのアプローチは、ネストループのような複雑なプログラムロジックを、より小さく検証可能なコンポーネントに分解することから始まります。
検証後、これらのコンポーネントは元のプログラムの証明を構築するために再コンパイルされる。
この分解分解ワークフローは非自明である。
プロメテウスは複素補題の構造的分解を通じて証明探索をより小さく検証可能な部分補題に導くことでこの問題に対処する。
自動化ツールが不十分な場合、ユーザは、証明プロセスを効果的に操るために、軽量な自然言語ガイダンスを提供することができる。
我々の評価は、コードに過渡的にモジュラー再構成を適用することにより、個々のコンポーネントを検証するAIの有効性が大幅に向上することを示した。
このアプローチは、ベースラインの68%に比べて、キュレートされたデータセットの86%のタスクをうまく検証します。
利得はより顕著で、仕様の複雑さが増し、30%から69%に改善され、複雑なプログラムの証明概要を統合すると25%から87%に向上した。
関連論文リスト
- Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
投機的復号化は、複数のドラフトトークンを並列に検証することにより、自動回帰言語モデル推論を加速する。
既存のスペーシフィケーション方式は主にトークン・バイ・トーケンの自己回帰復号化のために設計されている。
そこで本研究では,注目度,FFN,MoEを両立させるスパース検証フレームワークを提案する。
論文 参考訳（メタデータ） (2025-12-26T07:53:41Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Agentic Program Verification [14.684859166069012]
本稿では,プログラム検証を行うための最初の大規模言語モデルエージェントであるAutoRocqを提案する。
LLMの広範な訓練を実証例に頼っている過去の研究とは異なり、我々のエージェントはオンザフライで学習し、反復的な改善ループを通じて証明を改善する。
このようにして、我々の証明構成は証明エージェントと定理証明器との間の自律的な協調を含む。
論文 参考訳（メタデータ） (2025-11-21T15:51:48Z) - Detecting the Root Cause Code Lines in Bug-Fixing Commits by Heterogeneous Graph Learning [1.5213722322518697]
自動欠陥予測ツールは、ソフトウェアプロジェクト内の欠陥に起因するソフトウェア変更を積極的に識別することができる。
異質で複雑なソフトウェアプロジェクトにおける既存の作業は、異質なコミット構造に苦労したり、コード変更におけるクロスライン依存関係を無視したりといった課題に直面し続けている。
本稿では,バグフィックスグラフ構築コンポーネント,コードセマンティックアグリゲーションコンポーネント,クロスラインセマンティック保持コンポーネントの3つの主要コンポーネントからなるRC_Detectorというアプローチを提案する。
論文 参考訳（メタデータ） (2025-05-02T05:39:50Z) - 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) - From Scientific Texts to Verifiable Code: Automating the Process with Transformers [2.536225150399618]
トランスフォーマーは 研究論文を読めます 正式な証明を持つアルゴリズムを 提案し これらの証明を 検証可能なコードに翻訳します
このアプローチは形式的検証の障壁を大幅に減らすことができると我々は主張する。
論文 参考訳（メタデータ） (2025-01-09T14:03:35Z) - Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。
LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。
本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文 参考訳（メタデータ） (2024-10-05T05:21:48Z) - Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
多くの言語モデル推論コールからなる複合AIシステムは、ますます採用されている。
本研究では,提案した回答の生成と正当性検証の区別を中心に,ネットワークネットワーク(NoN)と呼ばれるシステムを構築した。
我々は,Kジェネレータを備えた検証器ベースの判定器NoNを導入し,"Best-of-K"あるいは"judge-based"複合AIシステムのインスタンス化を行う。
論文 参考訳（メタデータ） (2024-07-23T20:40:37Z) - Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
カリキュラムベースの論理認識型チューニングフレームワークであるLACTを提案する。
具体的には、任意の一階論理クエリをバイナリツリー分解によって拡張する。
広く使われているデータセットに対する実験では、LATは高度な手法よりも大幅に改善(平均+5.5% MRRスコア)し、新しい最先端技術を実現している。
論文 参考訳（メタデータ） (2024-05-02T18:12:08Z) - When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
本稿では,コードと推論能力の相関性を測定するために,複雑性に富んだ推論スコア(CIRS)を提案する。
具体的には、抽象構文木を用いて構造情報をエンコードし、論理的複雑性を計算する。
コードはhttps://github.com/zjunlp/EasyInstructのEasyInstructフレームワークに統合される。
論文 参考訳（メタデータ） (2023-08-29T17:22:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。