論文の概要: Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
- arxiv url: http://arxiv.org/abs/2405.01787v2
- Date: Tue, 3 Sep 2024 17:11:31 GMT
- ステータス: 処理完了
- システム内更新日: 2024-09-04 21:52:48.801073
- Title: Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
- Title（参考訳）: SMT支援プロオブオリエントプログラミングのためのニューラル合成に向けて
- Authors: Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, Nikhil Swamy,
- Abstract要約: 我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。
我々のデータセットには、約32KのトップレベルF*定義が含まれており、それぞれが型指向プログラムと証明合成の問題を表している。
我々は、AIを用いてプログラムと証明をF*で合成し、有望な結果を得る。
- 参考スコア（独自算出の注目度）: 8.34623776815378
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite the use of Satisfiability Modulo Theories (SMT) solvers to automate proofs in languages such as F*. Seeking to spur research on using AI to automate the construction of proof-oriented programs, we curate a dataset of 600K lines of open-source F* programs and proofs, including software used in production systems ranging from Windows and Linux, to Python and Firefox. Our dataset includes around 32K top-level F* definitions, each representing a type-directed program and proof synthesis problem -- producing a definition given a formal specification expressed as an F* type. We provide a program-fragment checker that queries F* to check the correctness of candidate solutions. We believe this is the largest corpus of SMT-assisted program proofs coupled with a reproducible program-fragment checker. Grounded in this dataset, we investigate the use of AI to synthesize programs and their proofs in F*, with promising results. Our main finding in that the performance of fine-tuned smaller language models (such as Phi-2 or StarCoder) compare favorably with large language models (such as GPT-4), at a much lower computational cost. We also identify various type-based retrieval augmentation techniques and find that they boost performance significantly. With detailed error analysis and case studies, we identify potential strengths and weaknesses of models and techniques and suggest directions for future improvements.
- Abstract（参考訳）: 証明指向プログラムは、計算内容とプログラムの正しさの証明を混合する。
しかし、Satifiability Modulo Theories (SMT) を用いて F* などの言語での証明を自動化するにもかかわらず、プログラミングと証明に関わる人間の努力は依然として重要なものである。
証明指向プログラムの構築を自動化するためにAIを使用する研究を促進するために,WindowsやLinux,Python,Firefoxなど,実運用システムで使用されているソフトウェアを含む,600万行のオープンソースF*プログラムと証明のデータセットをキュレートする。
我々のデータセットには、約32KのトップレベルF*定義が含まれており、それぞれが型指向プログラムと証明合成問題を表す。
候補解の正しさを確認するためにF*を問うプログラムフラグメントチェッカーを提供する。
再現性のあるプログラムフラグメントチェッカーと組み合わさったSMT支援プログラム証明の最大コーパスである。
このデータセットに基づいて,AIを用いてプログラムとその証明をF*で合成し,有望な結果を得る。
我々の主な発見は、微調整された小さな言語モデル(Phi-2やStarCoderなど)の性能が、より低い計算コストで大きな言語モデル(GPT-4など)と良好に比較できることである。
また,多種多様な検索手法を同定し,性能を著しく向上させた。
詳細なエラー解析とケーススタディにより、モデルと技術の潜在的な長所と短所を特定し、今後の改善に向けた方向性を提案する。
関連論文リスト
- Learning to Reason via Program Generation, Emulation, and Search [33.11955431589091]
言語モデル(LM)によるプログラム合成は、多くの推論能力を解放した。
すべての推論タスクは、コードとして容易に表現できるわけではない。例えば、常識的推論、道徳的意思決定、皮肉な理解を含むタスクである。
我々は,プログラム合成スキルをこのようなタスクに拡張するために,コード生成とエミュレートされた実行(CoGEX)を提案する。
論文 参考訳（メタデータ） (2024-05-25T19:40:50Z) - 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) - Do Neutral Prompts Produce Insecure Code? FormAI-v2 Dataset: Labelling Vulnerabilities in Code Generated by Large Language Models [3.4887856546295333]
この研究は、最先端の大規模言語モデル(LLM)の比較分析を提供する。
中立なゼロショットプロンプトを使って単純なCプログラムを書く際に、脆弱性が発生する可能性を分析する。
論文 参考訳（メタデータ） (2024-04-29T01:24:14Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - Towards AI-Assisted Synthesis of Verified Dafny Methods [1.0187122752343796]
既存の大規模言語モデルでは、検証プログラムの習熟度が著しく低下している。
Dafny検証対応言語における2つの事前学習モデルの習熟度を改善する方法を示す。
論文 参考訳（メタデータ） (2024-02-01T00:07:23Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳（メタデータ） (2023-09-25T15:42:18Z) - Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。
まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。
我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
論文 参考訳（メタデータ） (2023-05-22T06:11:15Z) - NAPG: Non-Autoregressive Program Generation for Hybrid Tabular-Textual
Question Answering [52.10214317661547]
現在の数値推論法はプログラムシーケンスを自己回帰的にデコードする。
プログラム生成の精度は、デコードステップがエラー伝搬によって展開されるにつれて急激に低下する。
本稿では,非自己回帰型プログラム生成フレームワークを提案する。
論文 参考訳（メタデータ） (2022-11-07T11:25:21Z) - Fault-Aware Neural Code Rankers [64.41888054066861]
サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。
我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
論文 参考訳（メタデータ） (2022-06-04T22:01:05Z) - Self-Supervised Learning to Prove Equivalence Between Straight-Line
Programs via Rewrite Rules [9.1570563482476]
2つのプログラムは、1つのプログラムをもう1つのプログラムに書き換える、書き換え規則の一連の適用が存在する場合と同値である。
本稿では,プログラムペア間の等価性の証明を生成するために,トランスフォーマーモデルに基づくニューラルネットワークアーキテクチャを提案する。
我々のシステムであるS4Eqは、1万対の等価プログラムをキュレートしたデータセット上で97%の証明成功を達成した。
論文 参考訳（メタデータ） (2021-09-22T01:37:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。