論文の概要: 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におけるメタ言語開発のための公式な数学的基礎を提供する。
私たちの研究は、我々の知る限り、非常に自動化された証明アシスタント内のオペラッドの最初の公式化や、ホモトピー型理論の知識なしに複製できるモデルも提供しています。
関連論文リスト
- A Coq Formalization of Unification Modulo Exclusive-Or [0.0]
我々は、XOR-ユニフィケーション、すなわち排他的あるいは排他的理論の統一化に焦点をあてる。
証明アシスタントCoqでは,XOR統一問題を解くアルゴリズムを実装している。
我々はプログラミング言語OCamlの実装を得る。
論文 参考訳（メタデータ） (2025-02-13T11:51:37Z) - Learning Task Representations from In-Context Learning [73.72066284711462]
大規模言語モデル(LLM)は、文脈内学習において顕著な習熟性を示している。
ICLプロンプトにおけるタスク情報をアテンションヘッドの関数として符号化するための自動定式化を導入する。
提案手法の有効性は,最後の隠れ状態の分布と最適に実行されたテキスト内学習モデルとの整合性に起因していることを示す。
論文 参考訳（メタデータ） (2025-02-08T00:16:44Z) - Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
形式言語理論は、特に認識者に関するものである。
代わりに、非公式な意味でのみ類似したプロキシタスクを使用するのが一般的である。
ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価することで、このミスマッチを補正する。
論文 参考訳（メタデータ） (2024-11-11T16:33:25Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳（メタデータ） (2024-06-14T06:52:08Z) - Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code [0.0]
Coqの証明アシスタントは、数学的アサーションとソフトウェアの正確性を検証するための厳格なアプローチで際立っている。
人工知能と機械学習の進歩にもかかわらず、Coq構文と意味論の特殊性は大規模言語モデル(LLM)に固有の課題をもたらす。
このデータセットは、10,000以上のCoqソースファイルのコレクションから派生したもので、幅広い命題、証明、定義を含んでいる。
論文 参考訳（メタデータ） (2024-03-19T10:53:40Z) - Molly: A Verified Compiler for Cryptoprotocol Roles [0.0]
Mollyは暗号プロトコルロールを直線プログラムにコンパイルする。
我々は,ランタイムの公理化に基づいて,プロトコルの役割を意味論的に定義する。
論文 参考訳（メタデータ） (2023-11-22T21:04:07Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳（メタデータ） (2023-01-05T17:56:00Z) - 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) - Procedures as Programs: Hierarchical Control of Situated Agents through
Natural Language [81.73820295186727]
エージェント命令と制御のための階層的な手続き的知識を表現する強力な手法である,プログラムとしての手続きの形式化を提案する。
NL命令に対するIQAおよびALFREDデータセット上で、このフレームワークをインスタンス化する。
論文 参考訳（メタデータ） (2021-09-16T20:36:21Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。