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

• arxiv url: http://arxiv.org/abs/2410.20936v2
• Date: Fri, 06 Dec 2024 09:06:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-09 15:53:52.651381
• 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倍の相対的な改善が達成されることを示した。

関連論文リスト

• 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)
• Factual Dialogue Summarization via Learning from Large Language Models [35.63037083806503]
  大規模言語モデル(LLM)に基づく自動テキスト要約モデルは、より現実的に一貫した要約を生成する。 ゼロショット学習を用いて、LLMから記号的知識を抽出し、事実整合性(正)および矛盾性(負)の要約を生成する。 各種自動評価指標で確認したように,コヒーレンス,フラレンシ,関連性を保ちながら,より優れた事実整合性を実現する。
  論文  参考訳（メタデータ） (2024-06-20T20:03:37Z)
• 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)
• Semantic Consistency for Assuring Reliability of Large Language Models [9.876355290198639]
  大規模言語モデル(LLM)は、様々な自然言語タスクに対して顕著な流布と能力を示す。 セマンティック一貫性の一般的な尺度を導入し、様々なLLMの性能を評価するために、この指標の複数バージョンを定式化する。 本稿では,Ask-to-Choose (A2C) と呼ばれる新しいプロンプト戦略を提案する。
  論文  参考訳（メタデータ） (2023-08-17T18:11:33Z)
• Enriching Disentanglement: From Logical Definitions to Quantitative Metrics [59.12308034729482]
  複雑なデータにおける説明的要素を遠ざけることは、データ効率の表現学習にとって有望なアプローチである。 論理的定義と量的指標の関連性を確立し, 理論的に根ざした絡み合いの指標を導出する。 本研究では,非交叉表現の異なる側面を分離することにより,提案手法の有効性を実証的に実証する。
  論文  参考訳（メタデータ） (2023-05-19T08:22:23Z)
• Co-Driven Recognition of Semantic Consistency via the Fusion of Transformer and HowNet Sememes Knowledge [6.184249194474601]
  本稿では,Transformer と HowNet のセメム知識の融合に基づく協調型意味的一貫性認識手法を提案する。 BiLSTMは概念的意味情報をエンコードし、意味的一貫性を推測するために利用される。
  論文  参考訳（メタデータ） (2023-02-21T09:53:19Z)
• 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)

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

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