論文の概要: NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry
- arxiv url: http://arxiv.org/abs/2608.28481v1
- Date: Fri, 28 Aug 2026 16:07:16 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-31 17:16:04.39046
- Title: NL2AGBench: Benchmarking LLM Auto-Formalization for AlphaGeometry
- Title（参考訳）: NL2AGBench:AlphaGeometryのためのLLMオートフォーマライゼーションのベンチマーク
- Abstract要約: そこで我々は,AlphaGeometry Benchmark (NL2AGBench) に自然言語を導入し,幾何学的問題を形式的表現に変換するための大規模言語モデル (LLM) を評価する。
我々は、複数のパラメータスケールで10の最先端のオープン・クローズド・ソースLCMを評価し、実行可能な翻訳精度、構文的正確性、エラー特性を分析した。
- 参考スコア（独自算出の注目度）: 1.8959297902766956
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Recent advances in large language models (LLMs) have demonstrated strong capabilities in natural language understanding and mathematical reasoning. However, their ability to translate informal mathematical problems into formal representations remains underexplored. This limitation is particularly important for neuro-symbolic geometry systems such as AlphaGeometry, whose theorem-proving engine requires inputs in a specialized domain-specific language (DSL). Although AlphaGeometry achieves near-IMO gold-medalist performance, manually converting natural-language problems into its formal syntax remains a significant usability bottleneck. To address this challenge, we introduce the Natural Language to AlphaGeometry Benchmark (NL2AGBench), which evaluates LLMs in translating English geometry problems into AlphaGeometry-compatible formal representations. NL2AGBench uses execution-based verification within AlphaGeometry to assess translation quality rather than relying solely on textual similarity. We evaluate ten state-of-the-art open- and closed-source LLMs across multiple parameter scales and analyze executable translation accuracy, syntactic correctness, and error characteristics. Our experiments reveal a substantial performance gap between closed- and open-source models: leading closed-source models achieve executable translation rates above 80%, while even the largest open-source models struggle to consistently preserve geometric constraints and produce valid formalizations. We introduce an error taxonomy distinguishing syntax and logic errors and investigate mitigation strategies, including few-shot prompting, fine-tuning, and human-guided hinting, which yield measurable improvements across multiple model families.
- Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩は、自然言語の理解と数学的推論において強力な能力を示している。
しかし、非公式な数学的問題を形式的な表現に翻訳する能力はいまだ未定である。
この制限は、特別なドメイン固有言語(DSL)の入力を必要とするAlphaGeometryのような神経記号幾何学システムにおいて特に重要である。
AlphaGeometryは、IMOに近いゴールドメダリストのパフォーマンスを達成しているが、自然言語問題をその形式構文に変換することは、依然として重要なユーザビリティボトルネックである。
この課題に対処するために、英語の幾何学的問題をAlphaGeometry互換の形式表現に変換する際のLLMを評価する自然言語 to AlphaGeometry Benchmark (NL2AGBench) を導入する。
NL2AGBenchは、AlphaGeometry内での実行ベースの検証を使用して、テキストの類似性のみに頼るのではなく、翻訳品質を評価する。
我々は,複数のパラメータスケールにまたがる10種類のオープンソースLCMを評価し,実行可能な翻訳精度,構文的正確性,エラー特性を解析した。
我々の実験は、クローズドソースモデルとオープンソースモデルの間にかなりの性能差があることを明らかにしている: クローズドソースモデルが80%以上の実行可能翻訳率を達成する一方で、最大のオープンソースモデルでさえ、幾何的制約を一貫して保存し、有効な形式化を作成するのに苦労している。
本稿では,構文と論理的誤りを区別する誤り分類を導入し,複数のモデルファミリに対して測定可能な改善をもたらす,数発のプロンプト,微調整,人為的ヒントなどの緩和策を検討する。
関連論文リスト
- The Geometry of Low-Resource Language Representations [11.09360259927697]
LLMにおける低リソース言語と高リソース言語のパフォーマンスギャップは広く知られているが、どの内部モデル要素がこれらの違いを駆動しているのかは定かではない。
隠れ表現の幾何学的性質を30言語で比較する。
9基のLDMを10のアフリカ言語に単言語で適応させる実験は、幾何学的正規化が表現退化を効果的に減少させることを示した。
論文 参考訳（メタデータ） (2026-08-24T15:06:58Z) - LLM Probe: Evaluating LLMs for Low-Resource Languages [6.177998679139308]
本稿では,低リソース言語における大規模言語モデル (LLM) の言語能力を評価するための語彙ベースアセスメントフレームワークを提案する。
このフレームワークは、語彙アライメント、音声認識、モルフォシンタクティック・プロービング、翻訳精度の4つの領域にわたるモデルを分析する。
論文 参考訳（メタデータ） (2026-03-31T10:03:38Z) - TangramPuzzle: Evaluating Multimodal Large Language Models with Compositional Spatial Reasoning [104.66714520975837]
古典的タングラムゲームのレンズを通して構成空間推論を評価するために,幾何グラウンドのベンチマークを導入する。
本稿では,タングラム集合を正確に機械で検証可能な座標仕様でグルーピングする記号幾何学的枠組みであるタングラム構成式(TCE)を提案する。
MLLMは、幾何学的制約を無視しながら、ターゲットのシルエットとのマッチングを優先する傾向がある。
論文 参考訳（メタデータ） (2026-01-23T07:35:05Z) - GeoRef: Referring Expressions in Geometry via Task Formulation, Synthetic Supervision, and Reinforced MLLM-based Solutions [45.70578816057097]
本稿では,幾何学的問題に対するReferring Expression (REC) の課題を紹介する。
RECは、テキストのプロンプトに応じて図形の点、形、空間関係をローカライズできるかどうかを評価する。
構造化幾何形式言語を用いた大規模合成学習データセットを生成する。
論文 参考訳（メタデータ） (2025-09-25T12:00:52Z) - Bridging Formal Language with Chain-of-Thought Reasoning to Geometry Problem Solving [9.550050299909184]
我々はChain-of-Thought(CoT)とフォーマル言語を統合する新しいアプローチを提案する。
このモデルは、ソルバ実行可能コードの漸進的な排出を伴う自然言語推論をインターリーブする。
Qwen2.5-VL-7Bに基づいて構築された新しいモデルGF-Reasonerは、標準GPSベンチマークで最大15%の精度向上を実現している。
論文 参考訳（メタデータ） (2025-08-12T17:26:23Z) - OMEGA: Can LLMs Reason Outside the Box in Math? Evaluating Exploratory, Compositional, and Transformative Generalization [88.76091817642963]
最近の大規模言語モデル (LLMs) は、DeepSeek-R1-のような長い鎖の推論を持ち、オリンピアード級数学において印象的な成果を上げている。
本稿では,3つの分布外一般化の軸を評価するために設計された3つの一般化 Axes-a ベンチマークを用いた OMEGA-Out-of-distriion Math Problems Evaluation を提案する。
論文 参考訳（メタデータ） (2025-06-23T17:51:40Z) - HELM: Hyperbolic Large Language Models via Mixture-of-Curvature Experts [29.365614317331932]
我々はHypErbolic Large Language ModelsのファミリーであるHELMを紹介する。
HELM-MICEでは,双曲型マルチヘッド潜在注意法を開発した。
両方のモデルに対して、回転位置符号化と RMS 正規化の本質的な双曲的等価性を開発する。
論文 参考訳（メタデータ） (2025-05-30T15:42:42Z) - Mechanistic Understanding and Mitigation of Language Confusion in English-Centric Large Language Models [56.61984030508691]
言語混乱に関する最初の機械論的解釈可能性研究について述べる。
混乱点(CP)がこの現象の中心であることを示す。
比較分析によって同定された少数の臨界ニューロンを多言語で調整したニューロンで編集すると、混乱が著しく軽減されることがわかった。
論文 参考訳（メタデータ） (2025-05-22T11:29:17Z) - Enhancing the Geometric Problem-Solving Ability of Multimodal LLMs via Symbolic-Neural Integration [57.95306827012784]
幾何学図のステップワイズ推論パスを自動的に生成するパイプラインであるGeoGenを提案する。
正確なシンボリック推論を活用することで、textbfGeoGenは大規模で高品質な質問応答ペアを生成する。
GeoGen が生成した合成データを用いて,Large Language Model (LLM) である textbfGeoLogic を訓練する。
論文 参考訳（メタデータ） (2025-04-17T09:13:46Z) - SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。
英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
論文 参考訳（メタデータ） (2024-08-28T06:33:03Z) - G-LLaVA: Solving Geometric Problem with Multi-Modal Large Language Model [121.07873620883322]
大規模言語モデル(LLM)は、人間レベルの推論と生成能力に顕著な習熟性を示している。
G-LLaVAは幾何学的問題の解法において例外的な性能を示し、7Bパラメータしか持たないMathVistaベンチマークにおいて GPT-4-V を著しく上回っている。
論文 参考訳（メタデータ） (2023-12-18T17:36:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。