論文の概要: Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees

• arxiv url: http://arxiv.org/abs/2604.19000v1
• Date: Tue, 21 Apr 2026 02:36:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-22 22:41:49.579088
• Title: Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees
• Title（参考訳）: 分解, 構造, 修復: オペレータツリーによるオートモーフィゼーションのためのニューロシンボリックフレームワーク
• Authors: Xiaoyang Liu, Zineng Dong, Yifan Bai, Yantao Li, Yuntian Liu, Tao Luo,
• Abstract要約: ステートメント自己形式化は数学と形式数学の間に重要な橋渡しとなる。 本稿では,自己形式化をモジュールパイプラインに再構成する神経象徴的フレームワークであるDecompose, Structure, and repair(DSR)を紹介する。
• 参考スコア（独自算出の注目度）: 10.346796782214485
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Statement autoformalization acts as a critical bridge between human mathematics and formal mathematics by translating natural language problems into formal language. While prior works have focused on data synthesis and diverse training paradigms to optimize end-to-end Large Language Models (LLMs), they typically treat formal code as flat sequences, neglecting the hierarchical logic inherent in mathematical statements. In this work, we introduce Decompose, Structure, and Repair (DSR), a neuro-symbolic framework that restructures autoformalization into a modular pipeline. DSR decomposes statements into logical components and maps them to structured operator trees, leveraging this topological blueprint to precisely localize and repair errors via sub-tree refinement. Furthermore, we introduce PRIME, a benchmark of 156 undergraduate and graduate-level theorems selected from canonical textbooks and expertly annotated in Lean 4. Experimental results demonstrate that DSR establishes a new state-of-the-art, consistently outperforming baselines under equivalent computational budgets. The datasets, model, and code will be released to the public soon.
• Abstract（参考訳）: ステートメント自己形式化は、自然言語問題を形式言語に翻訳することで、人間の数学と形式数学の間に重要な橋渡しとなる。 従来の研究は、エンドツーエンドのLarge Language Models (LLM) を最適化するためのデータ合成と多様な訓練パラダイムに重点を置いていたが、形式的なコードを平らなシーケンスとして扱い、数学的ステートメントに固有の階層論理を無視した。 本稿では, 自己形式化をモジュールパイプラインに再構成する神経象徴的フレームワークである分解, 構造, 修復(DSR)を紹介する。 DSRは、ステートメントを論理成分に分解し、構造化されたオペレータツリーにマッピングし、このトポロジカルブループリントを利用して、サブツリーの精細化によってエラーを正確にローカライズし、修復する。 さらに、標準教科書から選択された156の学部・大学院レベルの定理のベンチマークであるPRIMEを紹介します。 実験の結果、DSRは同等の計算予算の下で、新しい最先端の、一貫して優れたベースラインを確立することが示されている。 データセット、モデル、コードはまもなく一般公開される予定だ。

関連論文リスト

• NED-Tree: Bridging the Semantic Gap with Nonlinear Element Decomposition Tree for LLM Nonlinear Optimization Modeling [6.424862571179283]
  NED-Treeは意味的ギャップを埋めるための体系的なフレームワークである。 NED-Treeは、堅牢なパラメータマッピングとトレーサビリティを保証するために文ごとの抽出戦略を採用している。 NEXTORは、複雑な非線形で広範囲に制約のあるOR問題に特化して設計された新しいベンチマークである。
  論文  参考訳（メタデータ） (2026-04-02T03:59:37Z)
• LSRIF: Logic-Structured Reinforcement Learning for Instruction Following [56.517329105764475]
  命令論理を明示的にモデル化するロジック構造化学習フレームワーク LSRIF を提案する。 実験の結果、LSRIFは命令追従と一般的な推論に大きな改善をもたらすことが示された。
  論文  参考訳（メタデータ） (2026-01-10T05:11:38Z)
• SITA: A Framework for Structure-to-Instance Theorem Autoformalization [20.941850622174236]
  我々は、SITA(Structure-to-instance theorem autoformalization)の枠組みを開発する。 SITAは抽象数学的理論と、リーン証明アシスタントにおける具体的な応用のギャップを埋める。 対応するリーンの定義とインスタンス宣言を生成し、それらをリーンのタイプクラスメカニズムを使って統合し、構造的な仮定をチェックして検証済みの定理を構築します。
  論文  参考訳（メタデータ） (2025-11-13T14:33:51Z)
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。 これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。 我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
  論文  参考訳（メタデータ） (2025-10-12T21:42:04Z)
• Enhancing Systematic Decompositional Natural Language Inference Using Informal Logic [51.967603572656266]
  我々は,分解包含を注釈付けするための一貫した理論的なアプローチを導入する。 我々の新しいデータセットRDTEは、前回の分解エンターメントデータセットよりもかなり高い内部整合性(+9%)を持つことがわかった。 また,RDTE による知識蒸留によるエンテーメント分類器の訓練や,エンテーメントツリー推論エンジンへの導入により,精度と検証精度が向上することが確認された。
  論文  参考訳（メタデータ） (2024-02-22T18:55:17Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。 線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。 2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
  論文  参考訳（メタデータ） (2023-05-23T01:25:29Z)

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

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