論文の概要: A Formalization of Operads in Coq
- arxiv url: http://arxiv.org/abs/2303.08894v1
- Date: Wed, 15 Mar 2023 19:29:40 GMT
- ステータス: 処理完了
- システム内更新日: 2023-03-17 18:08:29.220397
- Title: A Formalization of Operads in Coq
- Title（参考訳）: coqにおけるオペラの形式化
- Authors: Zachary Flores, Angelo Taranto, Eric Bond, Yakir Forman
- Abstract要約: 本稿では,証明アシスタントであるCoqで操作された関数の形式化について論じる。
CoqはV-SPELLS内でのメタ言語開発のための公式な数学的基盤を提供する。
私たちの研究は、私たちの知る限りでは、重要な自動化を備えた証明アシスタント内でのオペラッドの初めての公式化も提供しています。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: What provides the highest level of assurance for correctness of execution
within a programming language? One answer, and our solution in particular, to
this problem is to provide a formalization for, if it exists, the denotational
semantics of a programming language. Achieving such a formalization provides a
gold standard for ensuring a programming language is correct-by-construction.
In our effort on the DARPA V-SPELLS program, we worked to provide a foundation
for the denotational semantics of a meta-language using a mathematical object
known as an operad. This object has compositional properties which are vital to
building languages from smaller pieces. In this paper, we discuss our
formalization of an operad in the proof assistant Coq. Moreover, our definition
within Coq is capable of providing proofs that objects specified within Coq are
operads. This work within Coq provides a formal mathematical basis for our
meta-language development within V-SPELLS. Our work also provides, to our
knowledge, the first known formalization of operads within a proof assistant
that has significant automation, as well as a model that can be replicated
without knowledge of Homotopy Type Theory.
- Abstract（参考訳）: プログラミング言語における実行の正確性に対する最高レベルの保証を提供するものは何か?
この問題に対する私たちの解決策は、プログラミング言語の表記意味論(denotational semantics)が存在する場合、形式化を提供することです。
このような形式化を実現することは、プログラミング言語が正しい構成であることを保証するための金の標準を提供する。
DARPA V-SPELLSプログラムの取り組みとして,オペラッドとして知られる数学的対象を用いたメタ言語の意味論の基盤を提供する。
このオブジェクトは、小さな部品から言語を構築するのに不可欠な合成特性を持っています。
本稿では,証明アシスタントcoqにおける操作の形式化について述べる。
さらに、Coq内での定義は、Coq内で指定されたオブジェクトが操作可能であるという証明を提供することができる。
この研究は、V-SPELLSにおけるメタ言語開発のための公式な数学的基礎を提供する。
私たちの研究は、我々の知る限り、非常に自動化された証明アシスタント内のオペラッドの最初の公式化や、ホモトピー型理論の知識なしに複製できるモデルも提供しています。
関連論文リスト
- Formalizing Piecewise Affine Activation Functions of Neural Networks in
Coq [0.0]
本稿では,Coq内のニューラルネットワークの検証に適した対話型定理証明器として,pwaアクティベーション関数の最初の形式化を提案する。
概念実証として、一般的なpwaアクティベーション関数ReLUを構築する。
私たちのフォーマル化は、自動証明が失敗する際のフォールバック証明として、ニューラルネットワーク検証のフレームワークにCoqを統合するための道を開くものです。
論文 参考訳（メタデータ） (2023-01-30T13:53:52Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳（メタデータ） (2023-01-05T17:56:00Z) - Towards a Mathematics Formalisation Assistant using Large Language
Models [5.485439959027125]
リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。
コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。
新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
論文 参考訳（メタデータ） (2022-11-14T16:52:32Z) - Q# as a Quantum Algorithmic Language [0.0]
我々はQ#の形式的な言語定義を提供することを目標とし、言語をしっかりとした数学的基礎の上に置きます。
$lambda_Q#$は、Q#を量子言語(アルゴリズム言語)と見なす方法を示している。
論文 参考訳（メタデータ） (2022-06-07T18:42:50Z) - ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。
我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
論文 参考訳（メタデータ） (2022-03-15T08:25:08Z) - Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。
本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。
提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文 参考訳（メタデータ） (2021-11-23T17:49:00Z) - Hierarchical Control of Situated Agents through Natural Language [97.90229625072696]
エージェント命令と制御のための階層的な手続き的知識を表現する強力な手法である,プログラムとしての手続きの形式化を提案する。
NL命令に対するIQAおよびALFREDデータセット上で、このフレームワークをインスタンス化する。
論文 参考訳（メタデータ） (2021-09-16T20:36:21Z) - Hierarchical Poset Decoding for Compositional Generalization in Language [52.13611501363484]
出力が部分的に順序付けられた集合(命題)である構造化予測タスクとして人間の言語理解を形式化する。
現在のエンコーダ・デコーダアーキテクチャは意味論のポーズ構造を適切に考慮していない。
本稿では,言語における合成一般化のための新しい階層型ポーズデコーディングパラダイムを提案する。
論文 参考訳（メタデータ） (2020-10-15T14:34:26Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z) - Deep Generation of Coq Lemma Names Using Elaborated Terms [35.21093297227429]
我々はCoqプロジェクトのための新しい生成モデルを提案し、補題名を提案する。
マルチインプットニューラルネットワークをベースとした当社のモデルは,コクのレキサートケンからの構文情報と意味情報をレムマ文で活用する最初のモデルです。
以上の結果から,Roosterizeは補題名を提案するベースラインを大幅に上回ることがわかった。
論文 参考訳（メタデータ） (2020-04-16T16:54:21Z) - Lexical Sememe Prediction using Dictionary Definitions by Capturing
Local Semantic Correspondence [94.79912471702782]
セメムは人間の言語の最小の意味単位として定義されており、多くのNLPタスクで有用であることが証明されている。
本稿では,このようなマッチングを捕捉し,セメムを予測できるセメム対応プールモデルを提案する。
我々は,有名なSememe KB HowNetのモデルとベースライン手法を評価し,そのモデルが最先端のパフォーマンスを実現することを発見した。
論文 参考訳（メタデータ） (2020-01-16T17:30:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。