Fugu-MT 論文翻訳(概要): GFLean: An Autoformalisation Framework for Lean via GF

論文の概要: GFLean: An Autoformalisation Framework for Lean via GF

arxiv url: http://arxiv.org/abs/2404.01234v1
Date: Mon, 1 Apr 2024 16:51:50 GMT
ステータス: 処理完了
システム内更新日: 2024-04-03 21:36:17.812505
Title: GFLean: An Autoformalisation Framework for Lean via GF
Title（参考訳）: GFLean:GFによるリーンの自動化フレームワーク
Authors: Shashank Pathak,
Abstract要約: 本稿では,GFLeanと呼ばれる,リーン定理証明のための自己形式化フレームワークを提案する。 GFLeanは文法的フレームワーク(GF)と呼ばれる高レベルの文法記述ツールを使用して解析と線形化を行っている。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We present an autoformalisation framework for the Lean theorem prover, called GFLean. GFLean uses a high-level grammar writing tool called Grammatical Framework (GF) for parsing and linearisation. GFLean is implemented in Haskell. We explain the functionalities of GFLean, its inner working and discuss its limitations. We also discuss how we can use neural network based translation programs and rule based translation programs together complimenting each other to build robust autoformalisation frameworks.
Abstract（参考訳）: 本稿では,GFLeanと呼ばれる,リーン定理証明のための自己形式化フレームワークを提案する。 GFLeanは文法的フレームワーク(GF)と呼ばれる高レベルの文法記述ツールを使用して解析と線形化を行っている。 GFLeanはHaskellで実装されている。 GFLeanの内部動作の機能を説明し、その限界について議論する。また、ニューラルネットワークベースの翻訳プログラムとルールベースの翻訳プログラムを相互に補完し、堅牢な自動形式化フレームワークを構築する方法について論じる。

関連論文リスト

XGrammar: Flexible and Efficient Structured Generation Engine for Large Language Models [3.9417976759908573]
文脈自由文法は制約付き復号化による構造化生成を可能にするフレキシブルなアプローチである。 XGrammarは、大規模言語モデルのための柔軟で効率的な構造生成エンジンである。 XGrammarは、既存のソリューションで最大100倍のスピードアップを達成することができる。
論文参考訳（メタデータ） (2024-11-22T18:01:37Z)
Can LLMs Reason with Rules? Logic Scaffolding for Stress-Testing and Improving LLMs [87.34281749422756]
大規模言語モデル(LLM)は、様々な推論タスクにおいて、印象的な人間的なパフォーマンスを実現している。しかし、その根底にある推論規則の熟達性は、人間の能力に欠ける。本稿では,推論ルールベースであるULogicを構築するための,推論ルール生成フレームワークを提案する。
論文参考訳（メタデータ） (2024-02-18T03:38:51Z)
Understanding In-Context Learning with a Pelican Soup Framework [27.144616560712493]
本稿では,自然言語処理における文脈内学習の理論的枠組みを提案する。本研究は,文脈内学習におけるフレームワークの有効性を実証するものである。
論文参考訳（メタデータ） (2024-02-16T03:20:14Z)
LILO: Learning Interpretable Libraries by Compressing and Documenting Code [71.55208585024198]
LILOは、反復的に合成、圧縮、文書化を行う、ニューロシンボリックなフレームワークである。 LILOは、LLM誘導プログラム合成と、Stitchから自動化された最近のアルゴリズムの進歩を組み合わせたものである。 LILOのシンセサイザーが学習した抽象化を解釈し、デプロイするのを手助けすることで、AutoDocがパフォーマンスを向上させることが分かりました。
論文参考訳（メタデータ） (2023-10-30T17:55:02Z)
Technical report: Graph Neural Networks go Grammatical [4.029787149512632]
本稿では,代数言語の一部とグラフニューラルネットワーク(GNN)との接続を正式に確立する枠組みを提案する。このフレームワークは、文脈自由文法(CFG)を利用して、代数演算をGNN層モデルに変換可能な生成規則に整理する。
論文参考訳（メタデータ） (2023-03-02T21:27:54Z)
Data types as a more ergonomic frontend for Grammar-Guided Genetic Programming [0.0]
本稿では,フレームワークのホスト言語に内在するドメイン特化言語として文法を組み込むことを提案する。このアプローチはホスト言語型システムを使用しながらBNFやEBNFと同じ表現力を持つ。木生成システムのユーザ定義オーバーライドであるメタハンドラーも提示する。
論文参考訳（メタデータ） (2022-10-10T16:38:16Z)
Verification of Locally Tight Programs [8.005641341294732]
プログラム完了は、論理プログラムの言語から一階理論の言語への変換である。この定理の厳密性条件は、より制限の少ない「局所的厳密性」要件に置き換えることができることを示す。証明アシスタントAnthem-p2pは、局所的に密なプログラム間の等価性を検証できると結論付ける。
論文参考訳（メタデータ） (2022-04-18T23:22:54Z)
GL-CLeF: A Global-Local Contrastive Learning Framework for Cross-lingual Spoken Language Understanding [74.39024160277809]
この問題に対処するために,グローバルローカルコントラスト学習フレームワーク(GL-CLeF)を提案する。具体的には、比較学習を採用し、二言語辞書を活用して、同じ発話の多言語ビューを構築する。 GL-CLeFは最高のパフォーマンスを達成し、言語間の類似した文の表現をうまくプルする。
論文参考訳（メタデータ） (2022-04-18T13:56:58Z)
Infusing Finetuning with Semantic Dependencies [62.37697048781823]
シンタックスとは異なり、セマンティクスは今日の事前訓練モデルによって表面化されないことを示す。次に、畳み込みグラフエンコーダを使用して、タスク固有の微調整にセマンティック解析を明示的に組み込む。
論文参考訳（メタデータ） (2020-12-10T01:27:24Z)
The Return of Lexical Dependencies: Neural Lexicalized PCFGs [103.41187595153652]
語彙化PCFGのニューラルモデルを提案する。実験により、この統一されたフレームワークは、いずれかの形式主義単独で達成されるよりも、両方の表現に対してより強い結果をもたらすことが示された。
論文参考訳（メタデータ） (2020-07-29T22:12:49Z)
Coreferential Reasoning Learning for Language Representation [88.14248323659267]
本稿では,コンテキスト内でコアファーデンシャル関係をキャプチャ可能な新しい言語表現モデルCorefBERTを提案する。実験の結果,既存のベースラインモデルと比較して,CorefBERTは下流のNLPタスクにおいて一貫した大幅な改善を達成できることがわかった。
論文参考訳（メタデータ） (2020-04-15T03:57:45Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。