論文の概要: SITA: A Framework for Structure-to-Instance Theorem Autoformalization

• arxiv url: http://arxiv.org/abs/2511.10356v1
• Date: Fri, 14 Nov 2025 01:47:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-14 22:53:22.825767
• Title: SITA: A Framework for Structure-to-Instance Theorem Autoformalization
• Title（参考訳）: SITA: 構造化からインスタンスへの定理自動化のためのフレームワーク
• Authors: Chenyi Li, Wanli Ma, Zichen Wang, Zaiwen Wen,
• Abstract要約: 我々は、SITA(Structure-to-instance theorem autoformalization)の枠組みを開発する。 SITAは抽象数学的理論と、リーン証明アシスタントにおける具体的な応用のギャップを埋める。 対応するリーンの定義とインスタンス宣言を生成し、それらをリーンのタイプクラスメカニズムを使って統合し、構造的な仮定をチェックして検証済みの定理を構築します。
• 参考スコア（独自算出の注目度）: 20.941850622174236
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While large language models (LLMs) have shown progress in mathematical reasoning, they still face challenges in formalizing theorems that arise from instantiating abstract structures in concrete settings. With the goal of auto-formalizing mathematical results at the research level, we develop a framework for structure-to-instance theorem autoformalization (SITA), which systematically bridges the gap between abstract mathematical theories and their concrete applications in Lean proof assistant. Formalized abstract structures are treated as modular templates that contain definitions, assumptions, operations, and theorems. These templates serve as reusable guides for the formalization of concrete instances. Given a specific instantiation, we generate corresponding Lean definitions and instance declarations, integrate them using Lean's typeclass mechanism, and construct verified theorems by checking structural assumptions. We incorporate LLM-based generation with feedback-guided refinement to ensure both automation and formal correctness. Experiments on a dataset of optimization problems demonstrate that SITA effectively formalizes diverse instances grounded in abstract structures.
• Abstract（参考訳）: 大規模言語モデル(LLM)は数学的推論の進歩を示しているが、具体的な設定で抽象構造をインスタンス化することによって生じる定理を定式化する際の課題に直面している。 研究レベルでの数学的結果の自動形式化を目標とし,抽象数学的理論とリーン証明アシスタントにおける具体的な応用とのギャップを体系的に橋渡しする構造-インスタンス定理自動形式化(SITA)の枠組みを開発する。 形式化された抽象構造は、定義、仮定、演算、定理を含むモジュラーテンプレートとして扱われる。 これらのテンプレートは、具体例の形式化のための再利用可能なガイドとして機能する。 特定のインスタンス化が与えられたら、対応するリーン定義とインスタンス宣言を生成し、それらをリーンの型クラスメカニズムを使って統合し、構造的な仮定をチェックして検証済みの定理を構築します。 自動と形式的正当性の両方を保証するために, LLM ベースの生成にフィードバック誘導の洗練を取り入れた。 最適化問題のデータセットに関する実験は、SITAが抽象構造に基づく多様なインスタンスを効果的に形式化することを示した。

関連論文リスト

• Structure-R1: Dynamically Leveraging Structural Knowledge in LLM Reasoning through Reinforcement Learning [29.722512436773638]
  本稿では,検索したコンテンツを推論に最適化した構造化表現に変換するフレームワークであるtextscStructure-R1を提案する。 textscStructure-R1は、7Bスケールのバックボーンモデルとの競合性能を一貫して達成していることを示す。 我々の理論的分析は,情報密度と文脈的明瞭度を向上させることによって,構造化表現が推論をいかに促進するかを示す。
  論文  参考訳（メタデータ） (2025-10-16T23:19:28Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。 最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。 本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
  論文  参考訳（メタデータ） (2025-09-02T14:16:02Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Steering LLMs for Formal Theorem Proving [1.083373217040891]
  我々は,非公式な推論トレースに関連する残効活性化における線形方向を同定する推論時間介入を開発する。 このメカニズムはまた、大規模言語モデルのアクティベーション空間において、推論がどのように内部的にエンコードされているかについての解釈可能な情報を与える。 1) LLM の証明合成を導くための新しいアクティベーションベースの介入,(2) この介入が2つの復号化戦略の下で性能を向上させることの実証である。
  論文  参考訳（メタデータ） (2025-02-21T15:04:48Z)
• Exploring the Role of Reasoning Structures for Constructing Proofs in Multi-Step Natural Language Reasoning with Large Language Models [30.09120709652445]
  本稿では,現在最先端のジェネラリスト LLM がいくつかの例でこれらの構造を活用でき,テキスト・コンテクスト・ラーニングによる証明構造をより良く構築できるかどうかという,焦点を絞った研究に焦点をあてる。
  論文  参考訳（メタデータ） (2024-10-11T00:45:50Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• Parrot Mind: Towards Explaining the Complex Task Reasoning of Pretrained Large Language Models with Template-Content Structure [66.33623392497599]
  テンプレート・コンテント構造(T-C構造)と呼ばれる構造は指数レベルから線形レベルへの可能な空間を減少させることができることを示す。 モデルがタスク構成を達成でき、線形から対数への学習に必要なスペースをさらに削減できることを実証する。
  論文  参考訳（メタデータ） (2023-10-09T06:57:45Z)
• Unifying Structure Reasoning and Language Model Pre-training for Complex Reasoning [26.811507121199323]
  本稿では,明示的な構造推論と言語事前学習を組み合わせ,PLMと構造推論のスキルを融合した統合学習フレームワークを提案する。 まず、コンテクスト内のいくつかの基本構造を識別し、構造化されたクエリを構築し、クエリに沿ってステップバイステップの推論を行い、回答エンティティを識別する。 4つのデータセットに対する実験結果から,提案モデルが多様構造を含む複雑な推論タスクにおいて,大幅な改善を達成できることが示されている。
  論文  参考訳（メタデータ） (2023-01-21T08:18:11Z)
• Autoregressive Structured Prediction with Language Models [73.11519625765301]
  本稿では, PLM を用いた自己回帰的手法を用いて, モデル構造を行動列として記述する。 我々のアプローチは、私たちが見てきた全ての構造化予測タスクにおいて、新しい最先端を実現する。
  論文  参考訳（メタデータ） (2022-10-26T13:27:26Z)

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

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