論文の概要: Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarsity

• arxiv url: http://arxiv.org/abs/2502.11901v1
• Date: Mon, 17 Feb 2025 15:24:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-18 14:16:29.024181
• Title: Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarsity
• Title（参考訳）: GPT-4oより64%優れたプロ指向型プログラマをデータスカシティで構築する
• Authors: Dylan Zhang, Justin Wang, Tianran Sun,
• Abstract要約: 本稿では,プロジェクトレベルの証明指向プログラミングのための合成データ拡張について,生成と修復の両面について紹介する。 本手法は,その言語の習熟度に関する基礎的証明指向プログラミング問題を合成することにより,データの不足に対処する。 我々は,プロジェクトレベルでの証明指向プログラミングにおいて,GPT-4oよりも優れた性能を示すモデルとして,細調整した14BパラメータモデルPoPilotを提案する。
• 参考スコア（独自算出の注目度）: 0.5370906227996627
• License:
• Abstract: Existing LMs struggle with proof-oriented programming due to data scarcity, which manifest in two key ways: (1) a lack of sufficient corpora for proof-oriented programming languages such as F*, and (2) the absence of large-scale, project-level proof-oriented implementations that can teach the model the intricate reasoning process when performing proof-oriented programming. We present the first on synthetic data augmentation for project level proof oriented programming for both generation and repair. Our method addresses data scarcity by synthesizing basic proof-oriented programming problems for proficiency in that language; incorporating diverse coding data for reasoning capability elicitation and creating new proofs and repair data within existing repositories. This approach enables language models to both synthesize and repair proofs for function- and repository-level code. We show that our fine-tuned 14B parameter model, PoPilot, can exceed the performance of the models that outperforms GPT-4o in project-level proof-oriented programming by 64% relative margin, and can improve GPT-4o's performance by 54% by repairing its outputs over GPT-4o's self-repair.
• Abstract（参考訳）: 1) F*のような証明指向プログラミング言語に十分なコーパスがないこと、2) 証明指向プログラミングを行う際に複雑な推論過程をモデルに教えることができる大規模でプロジェクトレベルの証明指向実装がないこと、である。 本稿では,プロジェクトレベルの証明指向プログラミングのための合成データ拡張について,生成と修復の両面について紹介する。 提案手法は,その言語の習熟度に関する基本的証明指向プログラミング問題を合成し,推論能力向上のための多種多様なコーディングデータを取り入れ,既存のリポジトリ内に新たな証明と修復データを作成することで,データの不足に対処する。 このアプローチにより、関数レベルのコードとリポジトリレベルのコードの証明を合成および修復することが可能になる。 本稿では,プロジェクトレベルの証明指向プログラミングにおいて GPT-4o を 64% で上回り,GPT-4o を 54% で上回り,GPT-4o の自己修復により GPT-4o の性能を 54% 向上させることができることを示す。

関連論文リスト

• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  本稿では,オープンソースの大規模言語モデル(LLM)であるGoedel-Proverを紹介する。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• Phi-4 Technical Report [72.06109095293243]
  本研究では,データ品質に重点を置いた14ビリオンパラメータ言語モデル phi-4 を提案する。 多くの言語モデルとは異なり、事前学習は主にWebコンテンツやコードなどの有機データソースに基づいており、phi-4はトレーニングプロセス全体を通して戦略的に合成データを組み込んでいる。
  論文  参考訳（メタデータ） (2024-12-12T03:37:41Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Improving Retrieval Augmented Language Model with Self-Reasoning [20.715106330314605]
  本稿では,ALMの信頼性とトレーサビリティ向上を目的とした,新たな自己推論フレームワークを提案する。 このフレームワークは、関連性を認識したプロセス、エビデンスを認識した選択プロセス、軌跡解析プロセスの3つのプロセスで自己推論軌道を構築することを含む。 提案手法の優位性を示すため,4つの公開データセットにまたがるフレームワークの評価を行った。
  論文  参考訳（メタデータ） (2024-07-29T09:05:10Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
  我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。 このデータセットには、Windows、Linux、Python、Firefoxなど、プロダクションシステムで使用されるソフトウェアが含まれている。 我々は,AIを用いてプログラムとその証明をF*で合成し,有望な結果を得る。
  論文  参考訳（メタデータ） (2024-05-03T00:14:33Z)
• Towards AI-Assisted Synthesis of Verified Dafny Methods [1.0187122752343796]
  既存の大規模言語モデルでは、検証プログラムの習熟度が著しく低下している。 Dafny検証対応言語における2つの事前学習モデルの習熟度を改善する方法を示す。
  論文  参考訳（メタデータ） (2024-02-01T00:07:23Z)
• DebugBench: Evaluating Debugging Capability of Large Language Models [80.73121177868357]
  DebugBench - LLM(Large Language Models)のベンチマーク。 C++、Java、Pythonの4つの主要なバグカテゴリと18のマイナータイプをカバーする。 ゼロショットシナリオで2つの商用および4つのオープンソースモデルを評価する。
  論文  参考訳（メタデータ） (2024-01-09T15:46:38Z)
• Struc-Bench: Are Large Language Models Really Good at Generating Complex Structured Data? [49.688233418425995]
  Struc-Benchは、大きな言語モデル(LLM)を特徴とする包括的なベンチマークである。 Pスコア(Prompting Score)とHスコア(Heuristical Score)の2つの革新的な指標を提案する。 実験の結果,LLaMA-7Bに構造認識の微調整を適用すると,性能が大幅に向上することがわかった。
  論文  参考訳（メタデータ） (2023-09-16T11:31:58Z)

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

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