論文の概要: Certified binary search tree on W-types
- arxiv url: http://arxiv.org/abs/2411.00242v1
- Date: Thu, 31 Oct 2024 22:47:33 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-11-05 14:47:49.188811
- Title: Certified binary search tree on W-types
- Title(参考訳): W型認証二分探索木
- Authors: Gustavo Arengas,
- Abstract要約: 確立された型を使って新しい型を定義する可能性について検討する。
特に,本研究は,本型に基づく新たな除去規則を考案した。
本稿では,これらのアイデアを二分探索木に適用し,手法のパワーを図示する。
- 参考スコア(独自算出の注目度): 0.0
- License:
- Abstract: Software bugs have caused enormous economic and human loss in recent years. Certified programming seeks to solve this problem by developing languages where we can make demonstrations that guarantee that our programs work properly. However, the rapid evolution of modern algorithms constantly forces us to develop new tools for this task. In this article we explore the possibility of defining new types using well-founded types. In particular, we developed a new elimination rule on the terms of the type. We apply these ideas to binary search trees to illustrate the power of the method.
- Abstract(参考訳): 近年、ソフトウェアのバグが経済と人的損失を招いている。
認定プログラミングは、プログラムが適切に動作することを保証するデモを行う言語を開発することで、この問題を解決することを目指している。
しかし、現代のアルゴリズムの急速な進化により、我々は常にこのタスクのための新しいツールを開発することを余儀なくされる。
本稿では、十分に確立された型を使用して新しい型を定義する可能性について検討する。
特に,本研究は,本型に基づく新たな除去規則を考案した。
本稿では,これらのアイデアを二分探索木に適用し,手法のパワーを図示する。
関連論文リスト
- No Man is an Island: Towards Fully Automatic Programming by Code Search, Code Generation and Program Repair [9.562123938545522]
ツールネームは、様々なコード検索、生成、修復ツールを統合することができ、これら3つの研究領域を初めて組み合わせることができる。
例えば、CodeLlamaは62.53%の改善で267のプログラミング問題を解決するのに役立ちます。
論文 参考訳(メタデータ) (2024-09-05T06:24:29Z) - From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models [63.188607839223046]
この調査は、推論中に計算をスケールするメリットに焦点を当てている。
我々はトークンレベルの生成アルゴリズム、メタジェネレーションアルゴリズム、効率的な生成という3つの領域を統一的な数学的定式化の下で探索する。
論文 参考訳(メタデータ) (2024-06-24T17:45:59Z) - Momentum Decoding: Open-ended Text Generation As Graph Exploration [49.812280360794894]
自動回帰言語モデル(LM)を用いたオープンエンドテキスト生成は、自然言語処理における中核的なタスクの1つである。
我々は、新しい視点から、すなわち、有向グラフ内の探索プロセスとして、オープンエンドテキスト生成を定式化する。
本稿では,新しい復号法であるtextitmomentum decodingを提案する。
論文 参考訳(メタデータ) (2022-12-05T11:16:47Z) - Genetic Programming with Local Scoring [0.0]
変異のシーケンスを経たコード進化のための新しい手法をいくつか提示する。
1)プログラムの各表現にスコアを割り当てる局所的なスコア付け方法,(2)if条件を進化させる中間ステップとして機能する仮定表現,(3)拡張と縮小の段階を通じてプログラムを進化させる循環的進化などである。
論文 参考訳(メタデータ) (2022-11-30T18:36:42Z) - A Probabilistic Programming Idiom for Active Knowledge Search [2.8483435983018612]
環境に関する新しい知識を得るために,確率的プログラミングイディオムを考案し,実装する。
能動マッピングとロボット探索の特定の問題に対するアルゴリズムを実装することで,このイディオムの有用性を実証する。
論文 参考訳(メタデータ) (2022-02-19T09:13:14Z) - Searching for More Efficient Dynamic Programs [61.79535031840558]
本稿では,プログラム変換の集合,変換プログラムの効率を評価するための単純な指標,およびこの指標を改善するための探索手順について述べる。
実際に、自動検索は初期プログラムの大幅な改善を見出すことができることを示す。
論文 参考訳(メタデータ) (2021-09-14T20:52:55Z) - Measuring Coding Challenge Competence With APPS [54.22600767666257]
コード生成のベンチマークであるAPPSを紹介する。
私たちのベンチマークには1万の問題が含まれています。
GPT-Neoのような最近のモデルでは、導入問題のテストケースの約15%をパスできる。
論文 参考訳(メタデータ) (2021-05-20T17:58:42Z) - BERT2Code: Can Pretrained Language Models be Leveraged for Code Search? [0.7953229555481884]
我々は,本モデルが埋め込み空間と改良のスコープに対するさらなるプローブの間に固有の関係を学習することを示す。
本稿では,コード埋め込みモデルの品質が,我々のモデルの性能のボトルネックであることを示す。
論文 参考訳(メタデータ) (2021-04-16T10:28:27Z) - MurTree: Optimal Classification Trees via Dynamic Programming and Search [61.817059565926336]
動的プログラミングと探索に基づいて最適な分類木を学習するための新しいアルゴリズムを提案する。
当社のアプローチでは,最先端技術が必要とする時間のごく一部しか使用せず,数万のインスタンスでデータセットを処理することが可能です。
論文 参考訳(メタデータ) (2020-07-24T17:06:55Z) - AutoML-Zero: Evolving Machine Learning Algorithms From Scratch [76.83052807776276]
基本数学的操作をビルディングブロックとして使うだけで,完全な機械学習アルゴリズムを自動的に発見できることが示される。
汎用的な検索空間を通じて人間のバイアスを大幅に低減する新しいフレームワークを導入することでこれを実証する。
機械学習アルゴリズムをゼロから発見する上で、これらの予備的な成功は、この分野における有望な新しい方向性を示していると信じている。
論文 参考訳(メタデータ) (2020-03-06T19:00:04Z) - Bin2vec: Learning Representations of Binary Executable Programs for
Security Tasks [15.780176500971244]
我々は、計算プログラムグラフとともに、GCN(Graph Convolutional Networks)を活用する新しいアプローチであるBin2vecを紹介する。
我々は,2つの意味的に異なるバイナリ解析タスクを解くために,我々の表現を用いることで,このアプローチの汎用性を実証する。
我々は、ソースコードベースのinst2vecアプローチと比較して、分類誤差を40%削減して、新しい最先端結果を設定した。
論文 参考訳(メタデータ) (2020-02-09T15:46:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。