論文の概要: FMC: Formalization of Natural Language Mathematical Competition Problems
- arxiv url: http://arxiv.org/abs/2507.11275v1
- Date: Tue, 15 Jul 2025 12:52:47 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-16 19:46:03.116082
- Title: FMC: Formalization of Natural Language Mathematical Competition Problems
- Title（参考訳）: FMC:自然言語の数学的競合問題の形式化
- Authors: Jiaxuan Xie, Chengwu Liu, Ye Yuan, Siqi Li, Zhiping Xiao, Ming Zhang,
- Abstract要約: 本稿では,誤りフィードバックを伴う大規模言語モデルに基づく自動形式化パイプラインを提案する。
Olympiadレベルのデータセットを、自然言語の問題をリーンの形式化と整合させます。
少数ショット学習,エラーフィードバック,サンプリング数の増加により,自動形式化プロセスが促進されることを示す。
- 参考スコア（独自算出の注目度）: 12.86616278136374
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Efficient and accurate autoformalization methods, which leverage large-scale datasets of extensive natural language mathematical problems to construct formal language datasets, are key to advancing formal mathematical reasoning. In this paper, we propose an autoformalization pipeline based on large language models with error feedback, achieving a fully automatic and training-free formalization approach. Using this pipeline, we curate an Olympiad-level dataset aligning natural language problems with Lean formalizations. The dataset comprises $3,922$ mathematical problems in natural language and $9,787$ in Lean, of which $64.46\%$ were assessed as at least above-average quality, making it suitable as a benchmark for automated theorem provers. Additionally, we investigate the formalization and reasoning capabilities of various LLMs and empirically demonstrate that few-shot learning, error feedback, and increasing sampling numbers enhance the autoformalization process. Experiments of three automated theorem provers on the \dataset\ dataset also highlight its challenging nature and its value as a benchmark for formal reasoning tasks.
- Abstract（参考訳）: 自然言語の数学的問題からなる大規模データセットを活用して形式的な言語データセットを構築する、効率的で正確な自動形式化手法は、形式的な数学的推論を前進させる鍵となる。
本稿では,誤りフィードバックを伴う大規模言語モデルに基づく自動形式化パイプラインを提案し,完全自動およびトレーニング不要な形式化アプローチを実現する。
このパイプラインを使用して、自然言語問題とリーンの形式を整合させるOlympiadレベルのデータセットをキュレートします。
このデータセットは、自然言語で3,922ドル、リーンで9,787ドルからなり、そのうち6,4.46セントは少なくとも平均以上の品質で評価され、自動定理証明器のベンチマークとして適している。
さらに, 各種LLMの形式化と推論能力について検討し, 少数ショット学習, エラーフィードバック, サンプリング数の増加が自己形式化プロセスの促進を実証した。
\dataset\データセット上の3つの自動定理証明器の実験では、その挑戦的な性質と、公式な推論タスクのベンチマークとしての価値も強調されている。
関連論文リスト
- Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。
本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。
現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文 参考訳（メタデータ） (2025-05-05T15:37:00Z) - Autoformulation of Mathematical Optimization Models Using LLMs [50.030647274271516]
本稿では,自然言語問題記述から解法対応最適化モデルを自動生成する,$textitautoformulation$の問題にアプローチする。
オートフォーミュレーションの3つの主要な課題を識別する: $textit(1)$ 巨大で問題に依存した仮説空間、および$textit(2)$ 不確実性の下でこの空間を効率的かつ多様に探索する。
我々は,$textitLarge Language Models$と$textitMonte-Carlo Tree Search$を併用した新しい手法を提案する。
論文 参考訳（メタデータ） (2024-11-03T20:41:38Z) - Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。
MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
論文 参考訳（メタデータ） (2024-10-28T11:37:39Z) - SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。
英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
論文 参考訳（メタデータ） (2024-08-28T06:33:03Z) - 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) - Lean Workbook: A large-scale Lean problem set formalized from natural language math problems [51.15420267178]
大規模な言語モデルは、リーンのような形式言語を使って証明する数学の定理が得意ではありません。
この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。
本稿では,自然言語の数学的問題をリーン4文に変換するために,合成データを反復的に生成・フィルタリングするパイプラインを提案する。
論文 参考訳（メタデータ） (2024-06-06T08:25:43Z) - 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) - Multilingual Mathematical Autoformalization [14.433478397963123]
オートフォーマル化(Autoformalization)は、自然言語を機械で検証可能な形式に変換するタスクである。
既存の方法は、手動で小さなコーパスをキュレートすることで、この課題を回避する傾向がある。
本研究では,大容量でフレキシブルで多言語で多ドメインのデータセットである$textttMMA$を作成する。
論文 参考訳（メタデータ） (2023-11-07T06:42:15Z) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳（メタデータ） (2023-10-16T08:42:39Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳（メタデータ） (2022-05-25T09:53:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。