論文の概要: Symbolic Informalization: Fluent, Productive, Multilingual
- arxiv url: http://arxiv.org/abs/2606.16893v1
- Date: Mon, 15 Jun 2026 16:06:21 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-16 16:21:34.748712
- Title: Symbolic Informalization: Fluent, Productive, Multilingual
- Title（参考訳）: シンボリック・インフォーマル化:フルーレント・プロダクティブ・マルチリンガル
- Authors: Aarne Ranta,
- Abstract要約: 記号的非公式化は、形式数学を自然言語に信頼できる変換を可能にする。
本稿では,象徴的非公式化がいかに流動的なテキストを生成できるかを示すプロジェクトInformathの概要を紹介する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Symbolic informalization enables a reliable conversion of formal mathematics to natural language. It has the potential to make machine-checked content human-readable without loss of precision. In a traditional proof system usage, symbolic informalization generalizes the limited mechanisms of syntactic sugar into the ordinary language of mathematics. In a setting where proofs are constructed by artificial intelligence and autoformalization, symbolic informalization can explain what precisely has been constructed. This paper outlines the project Informath, which aims to show how symbolic informalization can produce fluent text with a reasonable development effort and address multiple formal and natural languages. Informath is based on an interlingual architecture, where Dedukti works as a hub between different proof systems (Agda, Lean, Rocq) and Grammatical Framework (GF) takes care of linguistic correctness and variation in different natural languages.
- Abstract（参考訳）: 記号的非公式化は、形式数学を自然言語に信頼できる変換を可能にする。
精度を損なうことなく、マシンチェックされたコンテンツを人間に読まれる可能性がある。
伝統的な証明システムでは、記号的非公式化は、構文的糖の限られたメカニズムを数学の通常の言語に一般化する。
人工知能とオートフォーマル化によって証明が構築される場合、記号的非公式化は正確に何を構築したかを説明することができる。
本稿では,記号的非公式化が合理的な開発努力を伴い,複数の形式言語と自然言語に対処できることを示すプロジェクトInformathの概要を述べる。
Informathは言語間アーキテクチャに基づいており、Deduktiは異なる証明システム(Agda、Lean、Rocq)と文法フレームワーク(GF)の間のハブとして働く。
関連論文リスト
- Coherency through formalisations of Structured Natural Language, A case study on FRETish [0.0]
形式化とは、システム要件を形式言語で記述するプロセスである。
本稿では,ホルマライゼーションによるコヒーレンシ(コヒーレンシー)の新たなガイドラインを提案する。
本稿では,NASA の形式的要求抽出ツール FRET を分析し,制御された自然言語 FRETish を MTL の形式言語に自動翻訳する手法を提案する。
論文 参考訳（メタデータ） (2026-05-11T12:30:53Z) - Data2Concept2Text: An Explainable Multilingual Framework for Data Analysis Narration [42.95840730800478]
本稿では,データの集合を解釈し,基礎となる特徴を抽象化し,それを自然言語で記述する,完全な説明可能なシステムを提案する。
このシステムは、2つの重要な段階に依存している: (i)データから出現する特性を識別し、それらを抽象概念に変換する、(ii)これらの概念を自然言語に変換する。
論文 参考訳（メタデータ） (2025-02-13T11:49:48Z) - From Word Models to World Models: Translating from Natural Language to
the Probabilistic Language of Thought [124.40905824051079]
言語インフォームド・シンキングのための計算フレームワークである「構成」を合理的に提案する。
我々は、自然言語から確率論的思考言語への文脈感応的なマッピングとして、言語の意味を定式化する。
LLMは、現実的に適切な言語的意味をキャプチャする文脈依存翻訳を生成することができることを示す。
認知的なモチベーションを持つシンボリックモジュールを統合するために、我々のフレームワークを拡張します。
論文 参考訳（メタデータ） (2023-06-22T05:14:00Z) - Geometry of Language [0.0]
様々なソースからのアイデアを組み合わせながら、新しい合成で混ざり合った言語について、新しい視点を提示する。
問題は、エレガントな形式主義、普遍文法、あるいは人間の言語学の重要な側面を説明するメカニズムを定式化できるかどうかである。
このようなメカニズムは、その幾何学的性質によって、既存の論理的・文法的アプローチとは異なる。
論文 参考訳（メタデータ） (2023-03-09T12:22:28Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳（メタデータ） (2023-01-05T17:56:00Z) - Language Models as Inductive Reasoners [125.99461874008703]
本稿では,帰納的推論のための新しいパラダイム(タスク)を提案し,自然言語の事実から自然言語規則を誘導する。
タスクのための1.2kルールファクトペアを含むデータセットDEERを作成し,ルールと事実を自然言語で記述する。
我々は、事前訓練された言語モデルが自然言語の事実から自然言語規則をいかに誘導できるかを、初めてかつ包括的な分析を行う。
論文 参考訳（メタデータ） (2022-12-21T11:12:14Z) - A Latent-Variable Model for Intrinsic Probing [93.62808331764072]
固有プローブ構築のための新しい潜在変数定式化を提案する。
我々は、事前訓練された表現が言語間交互に絡み合ったモルフォシンタクスの概念を発達させる経験的証拠を見出した。
論文 参考訳（メタデータ） (2022-01-20T15:01:12Z) - Probing Linguistic Information For Logical Inference In Pre-trained
Language Models [2.4366811507669124]
本稿では,事前学習した言語モデル表現における論理推論のための言語情報探索手法を提案する。
i)事前学習された言語モデルは、推論のためにいくつかの種類の言語情報を符号化するが、弱符号化された情報もいくつか存在する。
シンボリック推論支援のためのセマンティックおよび背景知識基盤としての言語モデルの可能性を実証した。
論文 参考訳（メタデータ） (2021-12-03T07:19:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。