論文の概要: Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq

• arxiv url: http://arxiv.org/abs/2202.13823v2
• Date: Mon, 10 Mar 2025 18:58:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-12 15:40:19.668582
• Title: Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
• Title（参考訳）: 証明アシスタントにおける自動テストケースの削減:Coqを事例として
• Authors: Jason Gross, Théo Zimmermann, Rajashree Agrawal, Adam Chlipala,
• Abstract要約: 我々は、最小限のファイルとスタンドアロンのファイルでバグの振る舞いを再現するツールであるCoq Bug Minimizerを紹介する。 私たちのツールは、CoqのリバースCI障害を自動的にトリガーするために、Coqbotと統合されています。
• 参考スコア（独自算出の注目度）: 3.355947151753714
• License:
• Abstract: As the adoption of proof assistants increases, there is a need for efficiency in identifying, documenting, and fixing compatibility issues that arise from proof assistant evolution. We present the Coq Bug Minimizer, a tool for reproducing buggy behavior with minimal and standalone files, integrated with coqbot to trigger automatically on Coq reverse CI failures. Our tool eliminates the overhead of having to download, set up, compile, and then explore and understand large developments: enabling Coq developers to easily obtain modular test-case files for fast experimentation. In this paper, we describe insights about how test-case reduction is different in Coq than in traditional compilers. We expect that our insights will generalize to other proof assistants. We evaluate the Coq Bug Minimizer on over 150 CI failures. Our tool succeeds in reducing failures to smaller test cases in roughly 75% of the time. The minimizer produces a fully standalone test case 89% of the time, and it is on average about one-third the size of the original test. The average reduced test case compiles in 1.25 seconds, with 75% taking under half a second.
• Abstract（参考訳）: 証明アシスタントの採用が進むにつれて、証明アシスタントの進化から生じる互換性の問題を特定し、文書化し、修正する効率性が必要である。 Coq Bug Minimizerは、最小限のスタンドアロンファイルでバグの振る舞いを再現するツールで、Coqbotと統合して、Coqの逆CI障害を自動的にトリガする。 私たちのツールは、ダウンロード、セットアップ、コンパイル、そして大規模な開発を探索し、理解する必要のあるオーバーヘッドを取り除く。 本稿では,従来のコンパイラとCoqではテストケース削減の違いについて考察する。 私たちは私たちの洞察が他の証明アシスタントに一般化されることを期待しています。 我々は150以上のCI障害に対するCoq Bug Minimizerの評価を行った。 私たちのツールは、およそ75%の時間で、失敗を小さなテストケースに還元することに成功しています。 最小化器は、完全にスタンドアロンのテストケースを89%生成し、最初のテストの3分の1ほどの大きさである。 平均縮小テストケースは1.25秒でコンパイルされ、75%は半秒以下である。

関連論文リスト

• s1: Simple test-time scaling [148.4204982041058]
  テスト時間スケーリングは、パフォーマンスを改善するために余分なテスト時間計算を使用する言語モデリングに対する、有望な新しいアプローチである。 テストタイムのスケーリングと強力な推論性能を実現するための最もシンプルなアプローチを探します。
  論文  参考訳（メタデータ） (2025-01-31T18:48:08Z)
• CoqPilot, a plugin for LLM-based generation of proofs [0.0]
  CoqPilotは、Coq証明の記述を自動化するために設計されたVS Codeエクステンションである。 プラグインは、Coqファイルの許容戦術でマークされた証明の一部を収集する。 LLMと非機械学習法を組み合わせて、ホールの証明候補を生成する。
  論文  参考訳（メタデータ） (2024-10-25T14:57:29Z)
• CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
  本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。
  論文  参考訳（メタデータ） (2024-05-07T12:50:28Z)
• GPT-HateCheck: Can LLMs Write Better Functional Tests for Hate Speech Detection? [50.53312866647302]
  HateCheckは、合成データに対してきめ細かいモデル機能をテストするスイートである。 GPT-HateCheckは,スクラッチからより多彩で現実的な機能テストを生成するフレームワークである。 クラウドソースのアノテーションは、生成されたテストケースが高品質であることを示しています。
  論文  参考訳（メタデータ） (2024-02-23T10:02:01Z)
• Automatic Generation of Test Cases based on Bug Reports: a Feasibility Study with Large Language Models [4.318319522015101]
  既存のアプローチは、単純なテスト(例えば単体テスト)や正確な仕様を必要とするテストケースを生成する。 ほとんどのテスト手順は、テストスイートを形成するために人間が書いたテストケースに依存しています。 大規模言語モデル(LLM)を活用し,バグレポートを入力として利用することにより,この生成の実現可能性を検討する。
  論文  参考訳（メタデータ） (2023-10-10T05:30:12Z)
• Reducing Variance in Temporal-Difference Value Estimation via Ensemble of Deep Networks [109.59988683444986]
  MeanQは単純なアンサンブル法であり、ターゲット値をアンサンブル平均として推定する。 本稿では,Atari Learning Environmentベンチマークを用いた実験において,MeanQが顕著なサンプル効率を示すことを示す。
  論文  参考訳（メタデータ） (2022-09-16T01:47:36Z)
• AdaTest:Reinforcement Learning and Adaptive Sampling for On-chip Hardware Trojan Detection [25.593824693347113]
  AdaTestは、HT(Hardware Trojan)検出のための新しい適応型テストパターン生成フレームワークである。 高いトリガーカバレッジを達成するために、AdaTestはReinforcement Learning(RL)を活用して、さまざまなテストインプットを生成する。 AdaTestは、テスト生成のスピードアップを最大2つ、テストセットサイズを前回よりも2つまで削減する。
  論文  参考訳（メタデータ） (2022-04-12T23:56:59Z)
• Mobile App Crowdsourced Test Report Consistency Detection via Deep Image-and-Text Fusion Understanding [13.180855645914928]
  画像とテキストの融合理解によるクラウドソーシングテストレポートの一貫性を検出するためにReCoDeを提案する。 我々は、ReCoDeを評価するために、22k以上のテストレポートを持つデータセットで実験を行う。
  論文  参考訳（メタデータ） (2021-08-17T02:02:56Z)
• Detecting Rewards Deterioration in Episodic Reinforcement Learning [63.49923393311052]
  多くのRLアプリケーションでは、トレーニングが終了すると、エージェント性能の劣化をできるだけ早く検出することが不可欠である。 我々は,各エピソードにおける報酬が独立でもなく,同一に分散した,マルコフでもない,エピソード的枠組みを考察する。 平均シフトは、時間信号の劣化(報酬など)に対応する方法で定義し、最適な統計的パワーでこの問題の試行を導出する。
  論文  参考訳（メタデータ） (2020-10-22T12:45:55Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)
• Noisy Adaptive Group Testing using Bayesian Sequential Experimental Design [63.48989885374238]
  病気の感染頻度が低い場合、Dorfman氏は80年前に、人のテストグループは個人でテストするよりも効率が良いことを示した。 本研究の目的は,ノイズの多い環境で動作可能な新しいグループテストアルゴリズムを提案することである。
  論文  参考訳（メタデータ） (2020-04-26T23:41:33Z)

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

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