論文の概要: KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment

• arxiv url: http://arxiv.org/abs/2507.08665v1
• Date: Fri, 11 Jul 2025 15:05:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-14 18:03:54.399485
• Title: KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment
• Title（参考訳）: KELPS:セマンティック・シンタクティックアライメントによる多言語自動生成の検証フレームワーク
• Authors: Jiyao Zhang, Chengli Zhong, Hui Xu, Qige Li, Yi Zhou,
• Abstract要約: KELPSは、非公式データを形式言語に翻訳、合成、フィルタリングするための反復的なフレームワークである。 まず、自然言語を知識方程式(KEs)に翻訳する。 次に、構文構造と意味的意味の両方を保持する厳密に定義された規則により、ターゲット言語に変換する。 このプロセスは6万以上の問題からなる並列コーパスを生み出した。
• 参考スコア（独自算出の注目度）: 5.295540405828356
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Modern large language models (LLMs) show promising progress in formalizing informal mathematics into machine-verifiable theorems. However, these methods still face bottlenecks due to the limited quantity and quality of multilingual parallel corpora. In this paper, we propose a novel neuro-symbolic framework KELPS (Knowledge-Equation based Logical Processing System) to address these problems. KELPS is an iterative framework for translating, synthesizing, and filtering informal data into multiple formal languages (Lean, Coq, and Isabelle). First, we translate natural language into Knowledge Equations (KEs), a novel language that we designed, theoretically grounded in assertional logic. Next, we convert them to target languages through rigorously defined rules that preserve both syntactic structure and semantic meaning. This process yielded a parallel corpus of over 60,000 problems. Our framework achieves 88.9% syntactic accuracy (pass@1) on MiniF2F, outperforming SOTA models such as Deepseek-V3 (81%) and Herald (81.3%) across multiple datasets. All datasets and codes are available in the supplementary materials.
• Abstract（参考訳）: 現代の大言語モデル (LLMs) は、形式的な数学を機械検証可能な定理に定式化する上で、有望な進歩を示している。 しかし、これらの手法は多言語並列コーパスの限られた量と品質のために依然としてボトルネックに直面している。 本稿では,これらの問題に対処する新しいニューロシンボリック・フレームワークKELPS(Knowledge-Equation based Logical Processing System)を提案する。 KELPSは、非公式データを複数の形式言語(Lean、Coq、Isabelle)に翻訳、合成、フィルタリングするための反復的なフレームワークである。 まず、自然言語を知識方程式(KEs)に翻訳する。 次に、構文構造と意味的意味の両方を保持する厳密に定義された規則により、ターゲット言語に変換する。 このプロセスは6万以上の問題からなる並列コーパスを生み出した。 我々のフレームワークは、MiniF2F上で88.9%の構文精度(pass@1)を実現し、複数のデータセットにわたってDeepseek-V3 (81%)やHerald (81.3%)といったSOTAモデルを上回っている。 すべてのデータセットとコードは補足資料で利用可能である。

関連論文リスト

• The Unreasonable Effectiveness of Model Merging for Cross-Lingual Transfer in LLMs [54.59207567677249]
  大規模言語モデル(LLM)は、ハイソース言語以外のタスクで依然として苦戦している。 本研究では,タスク固有のポストトレーニングデータが不足している低リソース言語への言語間移動について検討する。
  論文  参考訳（メタデータ） (2025-05-23T20:28:31Z)
• Towards Typologically Aware Rescoring to Mitigate Unfaithfulness in Lower-Resource Languages [9.426642998924724]
  多言語大言語モデルは、資源制約言語で非忠実な出力を生成する。 このような設定における不誠実さを軽減するため、我々は計算学的に軽量な補助モデルを用いて、より大きなアーキテクチャの出力を再評価する。 我々は,700MB未満のデータに対して,スクラッチから事前訓練した単言語4層BERTモデルにより,忠実な要約を88.33%の平均精度で識別可能であることを示した。
  論文  参考訳（メタデータ） (2025-02-24T21:22:19Z)
• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価する。 3つのニューラルアーキテクチャに対して、チョムスキー階層の様々な言語について結果を提供する。 我々の貢献は、将来の研究において、言語認識の主張を理論的に健全に検証するのに役立つだろう。
  論文  参考訳（メタデータ） (2024-11-11T16:33:25Z)
• In-Context Language Learning: Architectures and Algorithms [73.93205821154605]
  我々は、文脈言語学習(ICLL)において、私たちが用語する新しいモデル問題群(英語版)のレンズを通してICLを研究する。 我々は,通常のICLLタスクにおいて,多種多様なニューラルシーケンスモデルを評価する。
  論文  参考訳（メタデータ） (2024-01-23T18:59:21Z)
• Automatic Model Selection with Large Language Models for Reasoning [33.93807127935167]
  Chain-of-Thought (CoT) と Program-Aided Language Models (PAL) は2つの異なる推論方法を表す。 本稿では,大言語モデルを用いて両世界の長所を結合するモデル選択手法を提案する。 提案手法は,8つの推論データセット間で有意な性能向上を示す。
  論文  参考訳（メタデータ） (2023-05-23T17:57:59Z)
• Learning Disentangled Semantic Representations for Zero-Shot Cross-Lingual Transfer in Multilingual Machine Reading Comprehension [40.38719019711233]
  マルチリンガル事前学習モデルは、機械読取理解(MRC)において、リッチリソース言語から低リソース言語への移行知識をゼロショットで得ることができる 本稿では,シメセマンティック・ディスタングルメント・モデル(SSDM)を用いた,多言語事前学習モデルで学習した表現の構文から意味論を解離させる新しい多言語MRCフレームワークを提案する。
  論文  参考訳（メタデータ） (2022-04-03T05:26:42Z)
• Zero-Shot Cross-lingual Semantic Parsing [56.95036511882921]
  7つのテスト言語に対する並列データを持たないゼロショット問題として,言語間セマンティックパーシングについて検討した。 英文論理形式ペアデータのみを用いて解析知識を付加言語に転送するマルチタスクエンコーダデコーダモデルを提案する。 このシステムは、ゼロショット解析を潜時空間アライメント問題としてフレーム化し、事前訓練されたモデルを改善し、最小のクロスリンガル転送ペナルティで論理形式を生成することができる。
  論文  参考訳（メタデータ） (2021-04-15T16:08:43Z)
• SML: a new Semantic Embedding Alignment Transformer for efficient cross-lingual Natural Language Inference [71.57324258813674]
  トランスフォーマーが質問応答、自然言語推論(NLI)、要約といった様々なタスクを精度良く実行できることは、現在この種のタスクに対処するための最良のパラダイムの1つとしてランク付けすることができる。 nliは、複雑な文を理解するための知識が必要であり、仮説と前提の関係を確立するため、これらのアーキテクチャをテストする最良のシナリオの1つである。 本稿では,自然言語推論のための多言語組込みを効率的にアライメントするための新しいアーキテクチャ siamese multilingual transformer を提案する。
  論文  参考訳（メタデータ） (2021-03-17T13:23:53Z)
• XCOPA: A Multilingual Dataset for Causal Commonsense Reasoning [68.57658225995966]
  XCOPA (Cross-lingual Choice of Plausible Alternatives) は11言語における因果コモンセンス推論のための多言語データセットである。 提案手法は,翻訳に基づく転送と比較して,現在の手法の性能が低下していることを明らかにする。
  論文  参考訳（メタデータ） (2020-05-01T12:22:33Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。