論文の概要: Consistent Autoformalization for Constructing Mathematical Libraries
- arxiv url: http://arxiv.org/abs/2410.04194v1
- Date: Sat, 5 Oct 2024 15:13:22 GMT
- ステータス: 処理完了
- システム内更新日: 2024-11-02 13:31:47.831622
- Title: Consistent Autoformalization for Constructing Mathematical Libraries
- Title(参考訳): 数学的ライブラリ構築のための一貫性のあるオートフォーマル化
- Authors: Lan Zhang, Xin Quan, Andre Freitas,
- Abstract要約: オートフォーマル化(Autoformalization)は、自然言語で書かれた数学的内容を自動的に形式言語表現に翻訳するタスクである。
本稿では,MS-RAG(Mult-similar search augmented generation),デノナイズステップ(denoising steps),自動誤りフィードバック(Auto-SEF)による自動補正という3つのメカニズムの協調的利用を提案する。
- 参考スコア(独自算出の注目度): 4.559523879294721
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. The growing language interpretation capabilities of Large Language Models (LLMs), including in formal languages, are lowering the barriers for autoformalization. However, LLMs alone are not capable of consistently and reliably delivering autoformalization, in particular as the complexity and specialization of the target domain grows. As the field evolves into the direction of systematically applying autoformalization towards large mathematical libraries, the need to improve syntactic, terminological and semantic control increases. This paper proposes the coordinated use of three mechanisms, most-similar retrieval augmented generation (MS-RAG), denoising steps, and auto-correction with syntax error feedback (Auto-SEF) to improve autoformalization quality. The empirical analysis, across different models, demonstrates that these mechanisms can deliver autoformalizaton results which are syntactically, terminologically and semantically more consistent. These mechanisms can be applied across different LLMs and have shown to deliver improve results across different model types.
- Abstract(参考訳): オートフォーマル化(Autoformalization)は、自然言語で書かれた数学的内容を自動的に形式言語表現に翻訳するタスクである。
形式言語を含む大言語モデル(LLM)の言語解釈能力の増大は、自動形式化の障壁を低くしている。
しかし、LSMだけでは、特にターゲット領域の複雑さと特殊化が増大するにつれて、一貫して確実にオートフォーマル化を行うことができない。
フィールドが大規模数学的ライブラリーに対して体系的に自己形式化を適用する方向に進化するにつれて、構文、用語、意味制御の改善の必要性が高まっている。
本稿では,MS-RAG(Mult-similar search augmented generation),デノナイズステップ(denoising steps),自動誤りフィードバック(Auto-SEF)による自動補正という3つのメカニズムの協調的利用を提案する。
実験的な分析は、異なるモデルにまたがって、これらのメカニズムが、構文的に、用語的に、意味的により一貫性のあるオートフォーマルなライザトン結果を提供できることを示した。
これらのメカニズムは異なるLLMに適用でき、異なるモデルタイプにまたがって改善結果をもたらすことが示されている。
関連論文リスト
- Unified Generative and Discriminative Training for Multi-modal Large Language Models [88.84491005030316]
生成的トレーニングにより、視覚言語モデル(VLM)は様々な複雑なタスクに取り組むことができる。
CLIPのようなモデルで実証された差別的トレーニングは、ゼロショットイメージテキストの分類と検索に優れています。
本稿では,両パラダイムの強みを統合する統一的アプローチを提案する。
論文 参考訳(メタデータ) (2024-11-01T01:51:31Z) - Self-Healing Machine Learning: A Framework for Autonomous Adaptation in Real-World Environments [50.310636905746975]
実世界の機械学習システムは、基礎となるデータ生成プロセスの分散シフトによって、モデルの性能劣化に遭遇することが多い。
概念のドリフト適応のような既存のシフトへのアプローチは、その理性に依存しない性質によって制限される。
我々はこれらの制限を克服するために自己修復機械学習(SHML)を提案する。
論文 参考訳(メタデータ) (2024-10-31T20:05:51Z) - Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。
MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
論文 参考訳(メタデータ) (2024-10-28T11:37:39Z) - Boosting the Capabilities of Compact Models in Low-Data Contexts with Large Language Models and Retrieval-Augmented Generation [2.9921619703037274]
本稿では,形態素解析の言語タスクにおいて,より小さなモデルの出力を補正するために,大言語モデル(LLM)を基盤とした検索拡張生成(RAG)フレームワークを提案する。
データ不足や訓練可能なパラメータの不足を補うために,言語情報を活用するとともに,LLMを通して解釈・蒸留された記述文法からの入力を許容する。
コンパクトなRAG支援モデルがデータスカース設定に極めて有効であることを示し、このタスクとターゲット言語に対する新しい最先端技術を実現する。
論文 参考訳(メタデータ) (2024-10-01T04:20:14Z) - Explaining Text Similarity in Transformer Models [52.571158418102584]
説明可能なAIの最近の進歩により、トランスフォーマーの説明の改善を活用することで、制限を緩和できるようになった。
両線形類似性モデルにおける2次説明の計算のために開発された拡張であるBiLRPを用いて、NLPモデルにおいてどの特徴相互作用が類似性を促進するかを調べる。
我々の発見は、異なる意味的類似性タスクやモデルに対するより深い理解に寄与し、新しい説明可能なAIメソッドが、どのようにして深い分析とコーパスレベルの洞察を可能にするかを強調した。
論文 参考訳(メタデータ) (2024-05-10T17:11:31Z) - Emergent Linguistic Structures in Neural Networks are Fragile [20.692540987792732]
大規模言語モデル (LLM) は自然言語処理タスクにおいて高い性能を示すと報告されている。
言語表現の一貫性と堅牢性を評価するための枠組みを提案する。
論文 参考訳(メタデータ) (2022-10-31T15:43:57Z) - Autoregressive Structured Prediction with Language Models [73.11519625765301]
本稿では, PLM を用いた自己回帰的手法を用いて, モデル構造を行動列として記述する。
我々のアプローチは、私たちが見てきた全ての構造化予測タスクにおいて、新しい最先端を実現する。
論文 参考訳(メタデータ) (2022-10-26T13:27:26Z) - Unifying Framework for Optimizations in non-boolean Formalisms [0.6853165736531939]
多くの一般的な自動推論パラダイムは最適化文をサポートする言語を提供する。
本稿では,パラダイム間の統語的区別を排除する統一フレームワークを提案する。
本稿では,提案方式の形式的特性を,我々の枠組み内で捉えることができるパラダイムの形式的特性に変換するシステムについて検討する。
論文 参考訳(メタデータ) (2022-06-16T00:38:19Z) - Incorporating Linguistic Knowledge for Abstractive Multi-document
Summarization [20.572283625521784]
ニューラルネットワークに基づく抽象的多文書要約(MDS)モデルを開発した。
依存関係情報を言語誘導型注意機構に処理する。
言語信号の助けを借りて、文レベルの関係を正しく捉えることができる。
論文 参考訳(メタデータ) (2021-09-23T08:13:35Z) - Contextualized Perturbation for Textual Adversarial Attack [56.370304308573274]
逆例は自然言語処理(NLP)モデルの脆弱性を明らかにする。
本稿では,フロートおよび文法的出力を生成するContextualized AdversaRial Example生成モデルであるCLAREを提案する。
論文 参考訳(メタデータ) (2020-09-16T06:53:15Z) - Improve Variational Autoencoder for Text Generationwith Discrete Latent
Bottleneck [52.08901549360262]
変分オートエンコーダ(VAE)は、エンドツーエンドの表現学習において必須のツールである。
VAEは強い自己回帰デコーダで潜伏変数を無視する傾向がある。
よりコンパクトな潜在空間において暗黙的な潜在特徴マッチングを強制する原理的アプローチを提案する。
論文 参考訳(メタデータ) (2020-04-22T14:41:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。