論文の概要: Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
- arxiv url: http://arxiv.org/abs/2502.05714v1
- Date: Sat, 08 Feb 2025 22:54:58 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-02-11 14:36:28.654143
- Title: Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
- Title（参考訳）: コーディングインタビューを証明する - 形式的に検証されたコード生成のためのベンチマーク
- Authors: Quinn Dougherty, Ronak Mehta,
- Abstract要約: FVAPPS (Formally Verified Automated Programming Progress Standards, FVAPPS) は,プログラムの記述と正確性を証明するための4715サンプルのベンチマークである。
我々は,機械学習とプログラム合成コミュニティに対して,汎用プログラミング問題とその関連した正当性仕様の解決に挑戦する。
- 参考スコア（独自算出の注目度）: 3.5319285228327417
- License:
- Abstract: We introduce the Formally Verified Automated Programming Progress Standards, or FVAPPS, a benchmark of 4715 samples for writing programs and proving their correctness, the largest formal verification benchmark, including 1083 curated and quality controlled samples. Previously, APPS provided a benchmark and dataset for programming puzzles to be completed in Python and checked against unit tests, of the kind seen in technical assessments in the software engineering industry. Building upon recent approaches for benchmarks in interactive theorem proving, we generalize the unit tests to Lean 4 theorems given without proof (i.e., using Lean's "sorry" keyword). On the 406 theorems of 100 randomly selected samples, Sonnet correctly proves 30% and Gemini correctly proves 18%. We challenge the machine learning and program synthesis communities to solve both each general purpose programming problem and its associated correctness specifications. The benchmark is available at https://huggingface.co/datasets/quinn-dougherty/fvapps.
- Abstract（参考訳）: FVAPPS (Formally Verified Automated Programming Progress Standards, FVAPPS) は,プログラムを記述し,その正確性を証明する4715個のサンプルのベンチマークである。
以前は、APPSはPythonで完了し、ユニットテストに対してチェックすべきパズルのベンチマークとデータセットを提供していた。
インタラクティブな定理証明における最近のベンチマークのアプローチに基づいて、ユニットテストを証明なしで与えられるLean 4の定理に一般化する(つまり、Leanの"sorry"キーワードを使って)。
100個のランダムに選択された標本の406の定理では、ソンネットは30%を正しく証明し、ジェミニは18%を正しく証明している。
我々は,機械学習とプログラム合成コミュニティに対して,汎用プログラミング問題とその関連した正当性仕様の解決に挑戦する。
ベンチマークはhttps://huggingface.co/datasets/quinn-dougherty/fvappsで公開されている。
関連論文リスト
- EquiBench: Benchmarking Code Reasoning Capabilities of Large Language Models via Equivalence Checking [54.354203142828084]
本稿では,大規模言語モデルのコード推論能力を評価する新しい手法として等価チェックの課題を提案する。
EquiBenchは、4つのプログラミング言語と6つの等価カテゴリにまたがる2400のプログラムペアのデータセットである。
その結果,OpenAI o3-miniの精度は78.0%と高いことがわかった。
論文 参考訳（メタデータ） (2025-02-18T02:54:25Z) - CLOVER: A Test Case Generation Benchmark with Coverage, Long-Context, and Verification [71.34070740261072]
本稿では,テストケースの生成と完成におけるモデルの能力を評価するためのベンチマークCLOVERを提案する。
ベンチマークはタスク間でのコード実行のためにコンテナ化されています。
論文 参考訳（メタデータ） (2025-02-12T21:42:56Z) - How Should We Build A Benchmark? Revisiting 274 Code-Related Benchmarks For LLMs [60.25940747590386]
本稿では,コード関連ベンチマークの開発を包括的に管理するためのガイドラインとして,55の基準チェックリストからなるHow2Benchを提案する。
私たちは過去10年以内にリリースされた274のベンチマークをプロファイルし、問題を見つけました。
ベンチマークの70%近くはデータ品質保証の措置を取らず、10%以上がオープンソースでも、部分的にはオープンソースでもなかった。
論文 参考訳（メタデータ） (2025-01-18T09:51:57Z) - Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification [11.115201117143929]
本稿では,Coq用の完全自動合成証明ツールであるRangoを紹介する。
Rangoは関連する前提と、それに類似した証明を現在のプロジェクトから特定し、合成時にそれらを使用する。
評価の結果, Rangoが文脈に関連付けると, 証明された定理の数が47%増加することがわかった。
論文 参考訳（メタデータ） (2024-12-18T17:08:42Z) - TestGenEval: A Real World Unit Test Generation and Test Completion Benchmark [24.14654309612826]
TestGenEvalは、1,210のコードから68,647のテストと、11の保守されたPythonリポジトリにまたがるテストファイルペアで構成されている。
初期テストのオーサリング、テストスイートの補完、コードカバレッジの改善をカバーしている。
パラメータは7Bから405Bまで様々である。
論文 参考訳（メタデータ） (2024-10-01T14:47:05Z) - Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。
このデータセットには、Windows、Linux、Python、Firefoxなど、プロダクションシステムで使用されるソフトウェアが含まれている。
我々は,AIを用いてプログラムとその証明をF*で合成し,有望な結果を得る。
論文 参考訳（メタデータ） (2024-05-03T00:14:33Z) - Can Language Models Solve Olympiad Programming? [40.54366634332231]
本稿ではUSACOベンチマークについて,USA Computing Olympiadの307の問題点について紹介する。
競争型プログラミングのための様々なLM推論手法を初めて構築・テストする。
GPT-4 は 8.7% パス@1 の精度しか達成していない。
論文 参考訳（メタデータ） (2024-04-16T23:27:38Z) - CodeT: Code Generation with Generated Tests [49.622590050797236]
テストケースを自動的に生成するための事前学習言語モデルについて検討する。
CodeTは生成されたテストケースを使ってコードソリューションを実行し、次に最良のソリューションを選択します。
我々は,HumanEvalとMBPPのベンチマークを用いて,5種類の事前学習モデル上でCodeTを評価する。
論文 参考訳（メタデータ） (2022-07-21T10:18:37Z) - Measuring Coding Challenge Competence With APPS [54.22600767666257]
コード生成のベンチマークであるAPPSを紹介する。
私たちのベンチマークには1万の問題が含まれています。
GPT-Neoのような最近のモデルでは、導入問題のテストケースの約15%をパスできる。
論文 参考訳（メタデータ） (2021-05-20T17:58:42Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z) - Unit Test Case Generation with Transformers and Focal Context [10.220204860586582]
AthenaTestは、現実世界の焦点メソッドと開発者が記述したテストケースから学習することで、単体テストケースを生成することを目的としている。
我々は,Javaにおける単体テストケースメソッドとそれに対応する焦点メソッドの並列コーパスとして最大規模で公開されているMethods2Testを紹介する。
AthenaTestを5つの欠陥4jプロジェクトで評価し、30回の試行で焦点メソッドの43.7%をカバーする25Kパステストケースを生成した。
論文 参考訳（メタデータ） (2020-09-11T18:57:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。