論文の概要: dafny-annotator: AI-Assisted Verification of Dafny Programs
- arxiv url: http://arxiv.org/abs/2411.15143v1
- Date: Tue, 05 Nov 2024 19:27:56 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-12-01 05:39:31.000146
- Title: dafny-annotator: AI-Assisted Verification of Dafny Programs
- Title(参考訳): dafny-annotator: AIによるDafnyプログラムの検証
- Authors: Gabriel Poesia, Chloe Loughridge, Nada Amin,
- Abstract要約: 本稿では,大言語モデルと検索を組み合わせたダファニーアノテーションの構築について検討する。
DafnyBench プログラムのコレクションから得られたテストセットでは、LLaMa 3.1 8B でガイドされたgreedy search が15.7%のメソッドに注釈を付けることに成功した。
我々の結果は、大規模な人為的な例がまだない言語のための有能なAIアシスタントへの道のりを示唆している。
- 参考スコア(独自算出の注目度): 4.651620941143133
- License:
- Abstract: Formal verification has the potential to drastically reduce software bugs, but its high additional cost has hindered large-scale adoption. While Dafny presents a promise to significantly reduce the effort to write verified programs, users are often required to provide logical annotations to aid the verifier. Here, we explore using a combination of Large Language Models and search to build dafny-annotator: a tool that adds logical annotations to a Dafny method until the verifier can prove it correct. On a test set from the DafnyBench collection of programs, greedy search guided by LLaMa 3.1 8B successfully annotates only 15.7% of the methods. Since this data-driven approach is hindered by the lack of large-scale training data, we propose a method for open-ended synthesis of new Dafny programs in a flexible pipeline where LLMs formulate high-level ideas, implement them, and incrementally propose changes to existing programs, which Dafny validates. This gives us a synthetic dataset, DafnySynth, which we use to augment DafnyBench for training. Fine-tuning on both datasets boosts LLaMa 8B's success rate to 50.6% -- significantly better than the base model, or training on either dataset alone. Our results suggest a path towards capable AI assistants for languages that don't yet have large-scale human-generated examples. In turn, such assistants might reduce friction for users and ultimately drive adoption.
- Abstract(参考訳): 形式的検証は、ソフトウェアのバグを大幅に削減する可能性があるが、その追加コストが高いため、大規模な採用を妨げている。
Dafnyは、検証プログラムを書く労力を大幅に削減する約束をしているが、検証者を助けるために論理アノテーションを提供する必要があることが多い。
本稿では,大言語モデルと検索を組み合わせたダフニーアノテーションの構築について検討する。
DafnyBench プログラムのコレクションから得られたテストセットでは、LLaMa 3.1 8B でガイドされたgreedy search が15.7%のメソッドに注釈を付けることに成功した。
このデータ駆動型アプローチは大規模トレーニングデータの欠如によって妨げられているため,LLMが高レベルなアイデアを定式化し,実装し,既存のプログラムの変更を段階的に提案するフレキシブルパイプラインにおいて,新しいDafnyプログラムをオープンエンドで合成する手法を提案する。
これによって、DafnyBenchのトレーニングに使用する合成データセットであるDafnySynthが提供されます。
両方のデータセットの微調整により、LLaMa 8Bの成功率は50.6%に向上した。
我々の結果は、大規模な人為的な例がまだない言語のための有能なAIアシスタントへの道のりを示唆している。
逆に、こうしたアシスタントはユーザーの摩擦を減らし、最終的には採用を促進するかもしれない。
関連論文リスト
- SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。
英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
論文 参考訳(メタデータ) (2024-08-28T06:33:03Z) - Laurel: Generating Dafny Assertions Using Large Language Models [2.6942525604796366]
本稿では,大規模な言語モデル(LLM)を用いて,Dafnyプログラムのヘルパーアサーションを自動的に生成するツールであるLaurillを提案する。
Laurelは数回の試行で、必要なヘルパーアサーションの50%以上を生成することができる。
論文 参考訳(メタデータ) (2024-05-27T03:26:01Z) - Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。
このデータセットには、Windows、Linux、Python、Firefoxなど、プロダクションシステムで使用されるソフトウェアが含まれている。
我々は,AIを用いてプログラムとその証明をF*で合成し,有望な結果を得る。
論文 参考訳(メタデータ) (2024-05-03T00:14:33Z) - LESS: Selecting Influential Data for Targeted Instruction Tuning [64.78894228923619]
本稿では,データの影響を推定し,命令データ選択のための低ランクグレーディエント類似度探索を行うアルゴリズムであるLESSを提案する。
LESS選択したデータの5%のトレーニングは、さまざまなダウンストリームタスクにわたる完全なデータセットでのトレーニングよりも優れています。
我々の方法は、意図した下流アプリケーションに必要な推論スキルを識別するために、表面的なフォームキューを超えています。
論文 参考訳(メタデータ) (2024-02-06T19:18:04Z) - Leveraging Large Language Models to Boost Dafny's Developers
Productivity [49.64902130083662]
本稿では、Dafny開発者の生産性を高めるために、LLM(Large Language Models)を活用することを提案する。
新しいDafnyプラグインは、Dafnyが発見および使用できない関連する補題の提案を生成する。
自動的に証明できない補題に対して、プラグインはまた、付随する計算的証明を提供しようとする。
論文 参考訳(メタデータ) (2024-01-01T21:58:13Z) - Uncertainty-aware Parameter-Efficient Self-training for Semi-supervised
Language Understanding [38.11411155621616]
我々は,主に半教師あり学習の手法として,自己学習について研究している。
我々は,新しい不確かさを意識した自己学習フレームワークであるUPETを紹介する。
UPETは性能と効率の面で大幅に向上したことを示す。
論文 参考訳(メタデータ) (2023-10-19T02:18:29Z) - PaD: Program-aided Distillation Can Teach Small Models Reasoning Better than Chain-of-thought Fine-tuning [20.59775450213501]
本稿では, 蒸留データの誤りを抑えるための推論プログラムを導入したPaD(Program-Aided Distillation)を提案する。
算術的推論,記号的推論,一般能力に基づいてPaDを評価する。
論文 参考訳(メタデータ) (2023-05-23T10:11:56Z) - Training Data is More Valuable than You Think: A Simple and Effective
Method by Retrieving from Training Data [82.92758444543689]
検索に基づく手法は,外部知識を導入してNLPタスクに有効であることが示されている。
意外なことに、Retrieving from the training datA (REINA) は複数のNLGおよびNLUタスクにおいて大きな改善をもたらすことが判明した。
実験結果から,本手法は様々なNLUタスクやNLGタスクにおいて,大幅な性能向上が期待できることがわかった。
論文 参考訳(メタデータ) (2022-03-16T17:37:27Z) - Efficient Nearest Neighbor Language Models [114.40866461741795]
非パラメトリックニューラルネットワークモデル(NLM)は、外部データストアを用いてテキストの予測分布を学習する。
比較性能を維持しながら、推論速度の最大6倍の高速化を実現する方法を示す。
論文 参考訳(メタデータ) (2021-09-09T12:32:28Z) - Learning to Count in the Crowd from Limited Labeled Data [109.2954525909007]
我々は,限られた数のラベル付きサンプルから参加者を数えることを学ぶことで,アノテーションの努力を減らすことに重点を置いている。
具体的には,未ラベルデータに対する擬似地下真理推定を含むガウス過程に基づく反復学習機構を提案する。
論文 参考訳(メタデータ) (2020-07-07T04:17:01Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。