論文の概要: Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency

• arxiv url: http://arxiv.org/abs/2410.20936v1
• Date: Mon, 28 Oct 2024 11:37:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-29 12:14:25.274967
• Title: Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
• Title（参考訳）: 記号等価性と意味的整合性による自動数学的ステートメント
• Authors: Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, Xiaoxing Ma,
• Abstract要約: そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。 MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
• 参考スコア（独自算出の注目度）: 22.86318578119266
• License:
• Abstract: Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@1 and pass@k accuracies in LLM-generated formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k autoformalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Elaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using automated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings of the original and informalized texts. Our extensive experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.35x relative improvements across various LLMs and baseline methods.
• Abstract（参考訳）: 自然言語記述を形式言語に自動翻訳するタスクであるオートフォーマル化は、特に数学において、様々な分野において重要な課題となる。 大規模言語モデル(LLM)の最近の進歩は、競合レベルの数学問題さえも形式化する有望な能力を明らかにしている。 しかし LLM 生成の形式化では pass@1 と pass@k の精度にかなりの差がある。 このギャップに対処するために、シンボリック等価性とセマンティック一貫性という2つの相補的自己整合性手法に基づいて、k個の自己形式化候補から最良の結果をスコアし、選択する新しいフレームワークを導入する。 記号同値性は自動定理プロバーを用いて自己形式化候補間の論理的均一性を識別し、意味的整合性は、候補を非公式にし、元のテキストと非公式なテキストの埋め込みの類似性を計算することによって、元の意味の保存を評価する。 MATHとminiF2Fデータセットに関する広範な実験により、我々のアプローチはオートフォーマライゼーションの精度を大幅に向上し、様々なLLMおよびベースライン法で最大0.22-1.35倍の相対的な改善が達成されることを示した。

関連論文リスト

• Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers [4.897782942277061]
  本稿では,SSV(Semantic Self-Verification)を導入し,自然言語から解法の形式言語への推論問題を正確に定式化する手法を提案する。 SSVは一貫性に基づくアプローチを用いて、モデルによって生成され、解決者によって検証される具体的なインスタンス化を用いて、問題の強力な抽象的な形式化を生成する。 このような*ほぼ確実な推論*は、多くの場合、手動検証の必要性を減らすための新しいアプローチとして提案され、より信頼性が高く自律的なAI推論システムに近づきます。
  論文  参考訳（メタデータ） (2025-01-28T14:04:49Z)
• Emergence of Self-Identity in AI: A Mathematical Framework and Empirical Study with Generative Large Language Models [4.036530158875673]
  本稿では,AIシステムにおける自己同一性の定義と定量化のための数学的枠組みを提案する。 我々の枠組みは、2つの数学的に定量化された条件から自己同一性が生じることを示唆している。 本研究の意義は、ヒューマノイドロボット工学や自律システムの分野に即時に関係している。
  論文  参考訳（メタデータ） (2024-11-27T17:23:47Z)
• Unified Generative and Discriminative Training for Multi-modal Large Language Models [88.84491005030316]
  生成的トレーニングにより、視覚言語モデル(VLM)は様々な複雑なタスクに取り組むことができる。 CLIPのようなモデルで実証された差別的トレーニングは、ゼロショットイメージテキストの分類と検索に優れています。 本稿では,両パラダイムの強みを統合する統一的アプローチを提案する。
  論文  参考訳（メタデータ） (2024-11-01T01:51:31Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [91.981439746404]
  本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。 まず,人間のアノテーションに対するQASemConsistency法の有効性を示す。 そこで我々は,局所的な事実の不整合を自動的に検出するいくつかの手法を実装した。
  論文  参考訳（メタデータ） (2024-10-09T22:53:48Z)
• Consistent Autoformalization for Constructing Mathematical Libraries [4.559523879294721]
  オートフォーマル化(Autoformalization)は、自然言語で書かれた数学的内容を自動的に形式言語表現に翻訳するタスクである。 本稿では,MS-RAG(Mult-similar search augmented generation),デノナイズステップ(denoising steps),自動誤りフィードバック(Auto-SEF)による自動補正という3つのメカニズムの協調的利用を提案する。
  論文  参考訳（メタデータ） (2024-10-05T15:13:22Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  本研究では,自然言語フィードバック型検証器Math-Minosを提案する。 実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2024-06-20T06:42:27Z)
• Improving Autoformalization using Type Checking [15.58948808529849]
  我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• Enriching Disentanglement: From Logical Definitions to Quantitative Metrics [59.12308034729482]
  複雑なデータにおける説明的要素を遠ざけることは、データ効率の表現学習にとって有望なアプローチである。 論理的定義と量的指標の関連性を確立し, 理論的に根ざした絡み合いの指標を導出する。 本研究では,非交叉表現の異なる側面を分離することにより,提案手法の有効性を実証的に実証する。
  論文  参考訳（メタデータ） (2023-05-19T08:22:23Z)
• A Latent-Variable Model for Intrinsic Probing [93.62808331764072]
  固有プローブ構築のための新しい潜在変数定式化を提案する。 我々は、事前訓練された表現が言語間交互に絡み合ったモルフォシンタクスの概念を発達させる経験的証拠を見出した。
  論文  参考訳（メタデータ） (2022-01-20T15:01:12Z)
• Joint Contextual Modeling for ASR Correction and Language Understanding [60.230013453699975]
  言語理解(LU)と協調してASR出力の文脈的言語補正を行うマルチタスクニューラルアプローチを提案する。 そこで本研究では,市販のASRおよびLUシステムの誤差率を,少量のドメイン内データを用いてトレーニングしたジョイントモデルと比較して14%削減できることを示した。
  論文  参考訳（メタデータ） (2020-01-28T22:09:25Z)

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

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