論文の概要: 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: リーンの課題としての現実世界のプロパティベースのテスト
- Authors: Quinn Dougherty, Max von Hippel, Hazel Shackleton, Mike Dodds,
- 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支援の正式な検証という未解決の問題の進展を促進することを目的としています。
関連論文リスト
- 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。