論文の概要: Natural Language to First-Order Logic LLM-based Autoformalization
- arxiv url: http://arxiv.org/abs/2610.12030v1
- Date: Thu, 08 Oct 2026 14:24:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-10 02:36:54.075985
- Title: Natural Language to First-Order Logic LLM-based Autoformalization
- Title（参考訳）: 自然言語から一階論理 LLM によるオートモーダル化
- Abstract要約: まず、論理翻訳からオントロジー抽出を区別することで、FOL自動化タスクの原理的定義を提供する。
我々は既存のデータセット、評価指標、および細調整、プロンプト、検証に基づく改善を含むLCMベースの手法についてレビューする。
- 参考スコア（独自算出の注目度）: 8.516686671273755
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large Language Models (LLMs) have renewed interest in autoformalization. Yet, when First-Order Logic (FOL) is considered as the target formalism, the field still lacks a unified task formulation and a systematic survey. This paper addresses this gap: we first provide a principled definition for the FOL-autoformalization task by distinguishing Ontology Extraction from Logical Translation, showing how their conflation obscures (cross-study) evaluation; we review existing datasets, evaluation metrics, and LLM-based methods, including fine-tuning, prompting, and verification-based refinement; we identify open challenges in benchmarking, semantic evaluation, ontology-aware methods, and end-to-end applications.
- Abstract（参考訳）: LLM(Large Language Models)は、自動形式化に新たな関心を持っている。
しかし、第一次論理(FOL)が対象の形式主義と見なされるとき、この分野は依然として統一されたタスクの定式化と体系的な調査を欠いている。
本稿では、まず、論理翻訳からオントロジー抽出を区別して、FOL自動化タスクの原則的定義を提供し、それらの評価がいかに不明瞭であるかを示し、既存のデータセット、評価指標、LCMベースの手法をレビューし、微調整、プロンプト、検証に基づく改善、ベンチマーク、セマンティック評価、オントロジー認識手法、エンドツーエンドアプリケーションにおいてオープンな課題を特定する。
関連論文リスト
- Towards Autoformalization of LLM-generated Outputs for Requirement Verification [0.6015898117103068]
非公式な文を形式論理に翻訳するプロセスであるオートフォーマル化は、強力な大規模言語モデルの出現により、新たな関心を集めている。
本稿では,LLMをベースとした簡易なオートフォーマライザを用いて,LLM生成した出力を少数の自然言語要求に対して検証する。
この結果から, LLM出力の完全性と論理的整合性を確保する上で, 自己形式化が有意な可能性を示唆した。
論文 参考訳（メタデータ） (2025-11-14T19:45:17Z) - Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning [8.135142928659546]
自動形式化タスクを評価するための,体系的かつ自動的な手法を提案する。
提案手法は,論理的保存(LP),数学的整合性(MC),形式的妥当性(FV),形式的品質(FQ)を基準とした審査員のアンサンブルに基づく。
全体としては,LLM審査員のEFGアンサンブルが評価に好適であることを示す。
論文 参考訳（メタデータ） (2025-06-12T17:09:51Z) - Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。
MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
論文 参考訳（メタデータ） (2024-10-28T11:37:39Z) - Evaluating Human Alignment and Model Faithfulness of LLM Rationale [66.75309523854476]
大規模言語モデル(LLM)が,その世代を理論的にどのように説明するかを考察する。
提案手法は帰属に基づく説明よりも「偽り」が少ないことを示す。
論文 参考訳（メタデータ） (2024-06-28T20:06:30Z) - Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection [44.31755414036022]
自然言語をFOLに自動変換するフレームワークであるNL2FOLについて,Large Language Models (LLMs) を用いて段階的に導入する。
本手法は,暗黙の背景知識の統合など,翻訳プロセスにおける重要な課題に対処する。
ニューロシンボリックなアプローチでは、推論プロセスに対する解釈可能な洞察も提供し、モデル微調整やラベル付きトレーニングデータを必要とせずに堅牢性を示す。
論文 参考訳（メタデータ） (2024-04-18T00:20:48Z) - CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。
このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。
LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
論文 参考訳（メタデータ） (2023-11-29T08:29:54Z) - Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models [56.34029644009297]
大規模言語モデル(LLM)は、形式的知識表現(KR)システムの様々な制限を克服する能力を示した。
LLMは誘導的推論において最も優れているが、誘導的推論では最も効果が低い。
モデルの性能を評価するため,シングルタスクトレーニング,マルチタスクトレーニング,および「チェーンオブ思考」知識蒸留細調整技術について検討した。
論文 参考訳（メタデータ） (2023-10-02T01:00:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。