論文の概要: Dissect-and-Restore: AI-based Code Verification with Transient Refactoring

• arxiv url: http://arxiv.org/abs/2510.25406v1
• Date: Wed, 29 Oct 2025 11:23:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-30 15:50:45.477245
• Title: Dissect-and-Restore: AI-based Code Verification with Transient Refactoring
• Title（参考訳）: Dissect-and-Restore: 過渡リファクタリングによるAIベースのコード検証
• Authors: Changjie Wang, Mariano Scazzariello, Anoud Alshnaka, 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%に向上した。

関連論文リスト

• When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
  本稿では,コードと推論能力の相関性を測定するために,複雑性に富んだ推論スコア(CIRS)を提案する。 具体的には、抽象構文木を用いて構造情報をエンコードし、論理的複雑性を計算する。 コードはhttps://github.com/zjunlp/EasyInstructのEasyInstructフレームワークに統合される。
  論文  参考訳（メタデータ） (2023-08-29T17:22:39Z)

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

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