Fugu-MT 論文翻訳(概要): FVSpec: Real-World Property-Based Tests as Lean Challenges

論文の概要: FVSpec: Real-World Property-Based Tests as Lean Challenges

arxiv url: http://arxiv.org/abs/2606.01008v1
Date: Sun, 31 May 2026 04:51:27 GMT
ステータス: 翻訳完了
システム内更新日: 2026-06-02 21:34:29.067415
Title: FVSpec: Real-World Property-Based Tests as Lean Challenges
Title（参考訳）: FVSpec: リーンの課題としての現実世界のプロパティベースのテスト
Abstract要約: 本稿では,実世界のソフトウェア検証タスクにおいて,AIモデルとエージェントを評価するためのベンチマークを示す。まず、現実世界のPythonリポジトリから11,039のプロパティベースのテスト(PBT)を取り除き、それから自動的に2,772を9,415のLean 4仕様に翻訳します。
参考スコア（独自算出の注目度）: 3.2338802435415794
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically translate 2,772 of them (25%) into 9,415 Lean 4 specifications with sorry placeholders (about 3 formalizations/PBT; we retain multiple attempts when none dominates on quality metrics). Translating PBTs into Lean specifications is challenging: it requires modeling Python semantics in Lean, inferring the logical property encoded in an imperative PBT, and handling the inherent difficulties of dependently-typed programming in a seldom-used language. We describe a three-agent LLM pipeline for transpiling PBTs into Lean specifications, evaluate coverage and quality metrics, and provide baselines for proof generation using several automated and model based approaches. All code (scraper and agents) and data (PBTs and Lean specifications) are open source. Our benchmark aims to drive progress on the underexplored problem of AI-assisted formal verification of real-world software, which is of increasing interest as AI produces more and more of the world's code.
Abstract（参考訳）: 本稿では,実世界のソフトウェア検証タスクにおいて,AIモデルとエージェントを評価するためのベンチマークを示す。 11,039件のプロパティベースのテスト(PBT)を現実のPythonリポジトリから取り除き、それから2,772件(25%)を自動的に9,415件のLean 4仕様に翻訳しました。 PBTをリーン仕様に翻訳するには、Pythonのセマンティクスをリーンでモデル化し、命令型PBTでエンコードされた論理的プロパティを推論し、ほとんど使われていない言語で依存型プログラミングの固有の困難に対処する必要がある。 PBTをLean仕様にトランスパイルし、カバレッジと品質のメトリクスを評価し、いくつかの自動化されたモデルベースのアプローチを使用して、証明生成のベースラインを提供する。すべてのコード(スクラッパとエージェント)とデータ(PBTとリーンの仕様)はオープンソースです。我々のベンチマークは、AIが世界のコードのより多くを生成するため、現実のソフトウェアに対するAI支援の正式な検証という未解決の問題の進展を促進することを目的としています。

関連論文リスト

Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning [7.228124845671868]
ニューロフォーマル検証(NFV)は、主流プログラミング言語の開発者の自動化を活用する。 AI符号化エージェントが翻訳し、確立された検証者が決定し、機械チェックされた証明により、音質よりも経験的精度で、主流言語で提起された質問にプッシュボタンで回答する。正誤のPython問題のデータセットの結果は、llm-as-judgeベースラインと比較して推奨されている。
論文参考訳（メタデータ） (2026-08-21T18:00:02Z)
Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing [6.28395649374318]
本稿では,Apache Spark計算における繰り返し特性パターンについて検討する。我々は、プロパティテンプレートを使用して、Lean 4定理証明器の正確性を正式に検証するエージェント型デュアルトラック検証フレームワークを設計する。評価の結果, 特性テンプレートは薬剤的証明工学的成功率を2.6倍(平均1.6倍)に向上し, 実証幻覚を59%減少させることがわかった。
論文参考訳（メタデータ） (2026-07-10T03:33:47Z)
LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文参考訳（メタデータ） (2026-05-02T11:31:33Z)
Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents [7.228124845671868]
エージェントAIシステムは、驚くほどの頻度でコードを生成することができる。生成されたコードが実際にユーザが意図した通りに動作するようにします。
論文参考訳（メタデータ） (2026-03-17T21:28:59Z)
Toward Training Superintelligent Software Agents through Self-Play SWE-RL [66.11447353341926]
セルフプレイSWE-RLは、超知能ソフトウェアエージェントのトレーニングパラダイムに向けた第一歩である。当社のアプローチでは,ソースコードとインストール済みの依存関係を備えたサンドボックスリポジトリへのアクセスのみを必要としています。我々の成果は、早い段階で、エージェントが現実世界のソフトウェアリポジトリから広範囲にわたる学習経験を自律的に収集する道のりを示唆している。
論文参考訳（メタデータ） (2025-12-21T00:49:40Z)
Propose, Solve, Verify: Self-Play Through Formal Verification [75.44204610186587]
形式的検証が信頼性の高い正当性信号を提供する検証コード生成設定における自己再生について検討する。本稿では,PSV(Propose, Solve, Verify)という,難易度の高い合成問題を生成可能なプロジェクタと,専門家の反復によって訓練された解決器を作成するための,形式的検証信号を用いた簡単なセルフプレイフレームワークを紹介する。そこで本研究では,生成した質問数とトレーニングの繰り返し数によるパフォーマンスの尺度を示し,形式的検証と難易度を考慮した提案を,自己再生を成功させる上で不可欠な要素として同定する。
論文参考訳（メタデータ） (2025-12-20T00:56:35Z)
FeatBench: Evaluating Coding Agents on Feature Implementation for Vibe Coding [11.846768103642583]
FeatBenchは、機能実装に焦点を当てた、バイブコーディングのための新しいベンチマークである。 FeatBenchは、ベンチマークを進化させるための品質と完全に自動化されたパイプラインを保証するために、マルチレベルのフィルタリングパイプライン上に構築されている。我々の評価によると、ビブ符号化パラダイムにおける機能実装は重要な課題であり、最高成功率は29.94%である。
論文参考訳（メタデータ） (2025-09-26T11:47:50Z)
Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文参考訳（メタデータ） (2025-07-22T08:13:01Z)
Automated Repair of Ambiguous Problem Descriptions for LLM-Based Code Generation [9.943472604121425]
自然言語(NL)の曖昧さは、ソフトウェアの品質を損なう可能性がある。あいまいなNL記述の自動修復を導入する。このアプローチをSpecFixというツールで実装しています。
論文参考訳（メタデータ） (2025-05-12T06:47:53Z)
Towards Automated Formal Verification of Backend Systems with LLMs [9.66648456498893]
バックエンドのコードを形式的なリーン表現に変換するために,関数型プログラミングと型システムを活用する新しいフレームワークを提案する。我々のパイプラインは、APIやデータベース操作の意図した振る舞いを規定する定理を自動生成し、LSMベースのプロバーを用いて検証する。本手法を現実的なバックエンドシステム上で評価した結果,テスト要件の50%以上を正式に検証できることがわかった。
論文参考訳（メタデータ） (2025-04-13T16:49:37Z)
SOPBench: Evaluating Language Agents at Following Standard Operating Procedures and Constraints [59.645885492637845]
SOPBenchは、各サービス固有のSOPコードプログラムを実行可能な関数の有向グラフに変換する評価パイプラインである。提案手法では,各サービス固有のSOPコードプログラムを実行可能関数の有向グラフに変換し,自然言語SOP記述に基づいてこれらの関数を呼び出しなければならない。我々は18の先行モデルを評価し、上位モデルでさえタスクが困難であることを示す。
論文参考訳（メタデータ） (2025-03-11T17:53:02Z)
Can Large Language Models Write Good Property-Based Tests? [5.671039991090038]
プロパティベースのテスト(PBT)は、現実世界のソフトウェアではいまだにあまり使われていない。 2つのプロンプト手法を用いて,近代言語モデルを用いてPSTを自動的に合成する。最適なモデルとプロンプトアプローチにより,有効かつ健全なPBTを平均2.4サンプルで合成できることが判明した。
論文参考訳（メタデータ） (2023-07-10T05:09:33Z)
LeTI: Learning to Generate from Textual Interactions [60.425769582343506]
本稿では,テキストインタラクション(LETI)から学習するLMの可能性を,バイナリラベルによる正当性をチェックするだけでなく,テキストフィードバックを通じて出力中のエラーをピンポイントし,説明する。私たちの焦点はコード生成タスクであり、そこではモデルが自然言語命令に基づいてコードを生成する。 LETIは、目的のLMを用いて、自然言語命令、LM生成プログラム、テキストフィードバックの結合に基づいて、モデルを反復的に微調整する。
論文参考訳（メタデータ） (2023-05-17T15:53:31Z)

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

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