論文の概要: Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing
- arxiv url: http://arxiv.org/abs/2607.09072v1
- Date: Fri, 10 Jul 2026 03:33:47 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-13 14:47:12.773497
- Title: Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing
- Title（参考訳）: データ集約型コンピューティングにおけるエージェント証明とプロパティベースのプロパティテンプレートによるテスト
- Abstract要約: 本稿では,Apache Spark計算における繰り返し特性パターンについて検討する。
我々は、プロパティテンプレートを使用して、Lean 4定理証明器の正確性を正式に検証するエージェント型デュアルトラック検証フレームワークを設計する。
評価の結果, 特性テンプレートは薬剤的証明工学的成功率を2.6倍(平均1.6倍)に向上し, 実証幻覚を59%減少させることがわかった。
- 参考スコア（独自算出の注目度）: 6.28395649374318
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: As the cost of code generation becomes cheaper with AI, the new bottleneck in software engineering has shifted to intent specification and validation. Overcoming this durability crisis of AI-driven coding requires more than traditional fuzzing: each candidate property must be proven correct over a model and shown to hold on the real implementation, making formal proof and systematic property-based testing (PBT) complementary. However, validating properties this way at scale requires solving two subproblems: verifying candidate properties and operationalizing PBT without AI hallucination. We hypothesize that recurring property patterns, cast as property templates--abstract, parameterized forms with holes--address both at once. This paper investigates recurring property patterns in Apache Spark. In data-intensive scalable computing systems, correctness properties arise from the principles of data partition, computation decomposition, and dataflow computation. For instance, aggregation decomposition relates a global function executed on the entire dataset to a local function followed by a recombiner. We design an agentic, dual-track validation framework that uses property templates to formally verify correctness in the Lean 4 theorem prover and instantiate PBT templates as executable PySpark tests. Our evaluation shows that property templates increase agentic proof engineering success by up to 2.6x (1.6x on average) and reduce proof hallucinations by 59%. Template-guided PBT synthesis reduces intent misalignments from 22 to 1 and cuts synthesis cost by up to 5.7x (3.8x on average). Template-guided synthesis further exceeds a state-of-the-art Spark fuzzer and approaches unguided LLM-based PBT on code coverage. Finally, comparing the two tracks is informative: when a proof succeeds yet a PBT finds a counterexample, the mismatch identifies a gap between the formal model and implementation.
- Abstract（参考訳）: AIによってコード生成コストが安くなるにつれて、ソフトウェアエンジニアリングにおける新たなボトルネックは、意図的な仕様とバリデーションへとシフトしている。
AI駆動コーディングのこの耐久性危機を克服するには、従来のファズリング以上のものが必要となる。各候補プロパティはモデル上で正しく証明され、実際の実装を保留することを示し、正式な証明と体系的プロパティベーステスト(PBT)を補完する。
しかし、これを大規模に検証するには、候補プロパティの検証と、AI幻覚を伴わないPBTの運用という、2つのサブプロブレムの解決が必要である。
プロパティテンプレートとしてキャストされる反復的なプロパティパターン - 穴のあるパラメータ化されたフォーム - は、両方を同時に配置する、という仮説を立てる。
本稿では,Apache Sparkの繰り返し特性パターンについて検討する。
データ集約型スケーラブルコンピューティングシステムでは、データ分割、計算分解、データフロー計算の原理から正当性特性が生じる。
例えば、集約分解はデータセット全体で実行されるグローバル関数をローカル関数に関連付け、その後にリコンビネータが続く。
我々は、プロパティテンプレートを使用して、Lean 4定理証明器の正当性を正式に検証し、PBTテンプレートを実行可能なPySparkテストとしてインスタンス化するエージェント的デュアルトラック検証フレームワークを設計する。
評価の結果, 特性テンプレートは薬剤的証明工学的成功率を2.6倍(平均1.6倍)に向上し, 実証幻覚を59%減少させることがわかった。
テンプレート誘導PBT合成は意図的不一致を22から1に減らし、合成コストを平均5.7倍(3.8倍)に削減する。
テンプレート誘導合成は、最先端のSparkファズーを超え、コードカバレッジにおいて無誘導のLCMベースのPBTにアプローチする。
証明がまだ成功しても PBT が反例を見つけると、ミスマッチは形式モデルと実装の間のギャップを識別する。
関連論文リスト
- Should I Use This Synthetic Dataset for Training? How to Test with Minimal Real Data [73.19814469893088]
デジタルツインと学習された世界モデルは、エンジニアリングシステムにおける人工知能(AI)モデルのトレーニングに利用可能な、少ない実際のデータセットを増大させる合成データを生成するために、ますます使われています。
本稿では,拡張データセットのトレーニングが真の,人口レベルのパフォーマンスを向上する一方で,実際のテストデータポイントを可能な限り少なく消費するかどうかを論じる。
合成データ分類タスク、DT支援無線パケットスケジューリングタスク、および無線マップ予測タスクにおいて、aeSFTは平均ベースのシーケンシャルテストよりもはるかに少ない実検サンプルを用いて有用な合成データを識別することを示す。
論文 参考訳（メタデータ） (2026-08-28T07:05:38Z) - VeriEvol: Scaling Multimodal Mathematical Reasoning via Verifiable Evol-Instruct [71.22358682581215]
ビジュアルな数学的推論のための強化学習のスケーリングは、難しい質問を生成すること以上のものを必要とします。
これは2つのコンポーネントからなる反復的なフレームワークであるVeriEvolとしてインスタンス化します。
5ベンチマークのビジュアル・マス・スイートでは、10Kから250KサンプルまでのSFTデータのスケーリングが平均精度を35.42から54.73に引き上げている。
論文 参考訳（メタデータ） (2026-06-22T16:17:30Z) - Tensor Algebraic Property Skeletons: Amplifying Property-Based Testing for AI Compilers [7.684444178725619]
Propilotは、GPT 5.5を使ったディープラーニング(DL)コンパイラのためのエージェントプロパティベースのテストフレームワークである。
テンソル代数の知識を再利用可能なプロパティスケルトンとして表現し、それぞれが演算子制約、形状と値規則、およびオラクルテンプレートと結合する。
212のオペレーターと20のプロパティスケルトンでTVM上でPropilotを評価し,4,579のPBTを生成した。
論文 参考訳（メタデータ） (2026-06-04T22:01:30Z) - PBT-Bench: Benchmarking AI Agents on Property-Based Testing [29.035258104995204]
PBT-Benchは、40の実際のPythonライブラリにまたがる100のプロパティベースのテスト問題のベンチマークである。
各問題は1つ以上のセマンティックなバグ(総数365、平均3.65)を注入し、デフォルトのストラテジーなランダムな入力がほとんど起こらないように設計する。
PBT指導によるバグリコールは42.1%から83.4%の範囲で、オープンエンドベースラインでは31.4%から76.7%である。
論文 参考訳（メタデータ） (2026-05-13T18:01:05Z) - Template-as-Ontology: Configurable Synthetic Data Infrastructure for Cross-Domain Manufacturing AI Validation [0.0]
1つのPython構成モジュールは、タイムステップ製造シミュレータの仕様として機能する。
5層パイプライン-シミュレート、CDC/Icebergレイクハウス、スタースキーマ、12のパラメータ化されたAIツール-は、因果的に一貫性のあるMES型のデータを生成します。
このフレームワークは、個別の製造AIバリデーションのための再利用可能なデータ層を提供する。
論文 参考訳（メタデータ） (2026-05-11T21:36:05Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳（メタデータ） (2026-04-20T22:02:57Z) - Dynamic analysis enhances issue resolution [53.50448142467294]
DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。
テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。
Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
論文 参考訳（メタデータ） (2026-03-23T14:48:54Z) - Synthesizing File-Level Data for Unit Test Generation with Chain-of-Thoughts via Self-Debugging [40.29934051200609]
本稿では,高品質なUTトレーニングを実現するための新しいデータ蒸留手法を提案する。
このパイプラインをオープンソースプロジェクトの大規模なコーパスに適用します。
実験により, 微調整モデルにより, UT生成効率が高いことを示す。
論文 参考訳（メタデータ） (2026-02-03T06:52:54Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。
本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
論文 参考訳（メタデータ） (2025-10-02T06:25:10Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。