Fugu-MT 論文翻訳(概要): Reformalization of the Jordan Curve Theorem

論文の概要: Reformalization of the Jordan Curve Theorem

arxiv url: http://arxiv.org/abs/2607.01734v1
Date: Thu, 02 Jul 2026 05:44:10 GMT
ステータス: 翻訳完了
システム内更新日: 2026-07-03 19:45:08.687075
Title: Reformalization of the Jordan Curve Theorem
Title（参考訳）: ヨルダン曲線理論の改革
Abstract要約: 本稿では、入力証明が自然言語ではなく、異なる証明アシスタントにおける形式的発達である自己形式化の変種である改革におけるケーススタディを提案する。私たちは、Jordan Curve Theoremの3つの改革について報告します。MizarからLeanへ、HOL LightからLeanへ、HOL LightからAgdaへ。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by-nc-sa/4.0/
Abstract: We present a case study in reformalization, a variant of autoformalization in which the input proof is not natural language but a formal development in a different proof assistant. Concretely, we report three reformalizations of the Jordan Curve Theorem: from Mizar to Lean, from HOL Light to Lean, and from HOL Light to Agda. We analyse the results and identify pipeline design choices that matter for practical reformalization tasks.
Abstract（参考訳）: 本稿では、入力証明が自然言語ではなく、異なる証明アシスタントにおける形式的発達である自己形式化の変種である改革におけるケーススタディを提案する。具体的には、MizarからLean、HOL LightからLean、HOL LightからAgdaまで、Jordan Curve Theoremの3つの改革について報告します。結果を分析し、実践的な改革作業において重要なパイプライン設計の選択を特定します。

関連論文リスト

(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs [0.20305676256390937]
本稿では,LLMエージェントを決定論的に制約されたワークフローで活用して,リーンの自己形式化タスクの漸進的な進歩を実現する自動形式化システムを提案する。我々のアプローチは、まず第一に厳密な証明を持つことの意味についての一般数学者の考えに動機づけられている。プロセスによって生み出された最近のRamsey理論のブレークスルーを、エンドツーエンドのリーン形式化にリンクします。
論文参考訳（メタデータ） (2026-06-08T15:57:14Z)
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems [3.1963549333419388]
本稿では,PDF-to-La Algebra前処理,Lean 4への自動形式化,非公式な形式対応の検証などからなるスケーラブルなパイプラインを開発する。コントリビューションには、(i)形式化された演習の構造化データセットの構築、(ii)教科書数学の形式化のための体系的方法論、(iii)形式化過程における繰り返しの課題の分析が含まれる。
論文参考訳（メタデータ） (2026-05-20T08:15:43Z)
Variational Reasoning for Language Models [93.08197299751197]
本稿では,思考トレースを潜在変数として扱う言語モデルのための変分推論フレームワークを提案する。 GRPOを含むリジェクションサンプリングとバイナリリワードRLは局所的なフォワードKLの目的と解釈できることを示す。
論文参考訳（メタデータ） (2025-09-26T17:58:10Z)
Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
論文参考訳（メタデータ） (2025-09-02T14:16:02Z)
CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
我々は,系統的かつ包括的な推論プロセスを実行するためのモデルを導くことで,モデルがよりきめ細やかで正確な絞り込み決定を実行できることを提案する。我々は,(i)クレームの分解,(ii)サブクレームの属性と包含分類,および(iii)集約分類から成る3段階の推論プロセスを定義し,そのような導出推論が実際に幻覚検出の改善をもたらすことを示す。
論文参考訳（メタデータ） (2025-06-05T17:02:52Z)
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文参考訳（メタデータ） (2025-06-05T03:16:08Z)
Steering LLMs for Formal Theorem Proving [1.083373217040891]
我々は,非公式な推論トレースに関連する残効活性化における線形方向を同定する推論時間介入を開発する。このメカニズムはまた、大規模言語モデルのアクティベーション空間において、推論がどのように内部的にエンコードされているかについての解釈可能な情報を与える。 1) LLM の証明合成を導くための新しいアクティベーションベースの介入,(2) この介入が2つの復号化戦略の下で性能を向上させることの実証である。
論文参考訳（メタデータ） (2025-02-21T15:04:48Z)
Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
Evidence-Focused Fact Summarization for Knowledge-Augmented Zero-Shot Question Answering [14.389264346634507]
本稿では,QA(Quesetion Answering)の性能向上を目的とした,エビデンスに着目したFact SummarizationフレームワークであるEFSumを提案する。実験の結果,EFSumはLDMのゼロショットQA性能を向上することがわかった。
論文参考訳（メタデータ） (2024-03-05T13:43:58Z)
Lyra: Orchestrating Dual Correction in Automated Theorem Proving [63.115422781158934]
Lyraは新しいフレームワークで、ツール補正とConjecture Correctionという2つの異なる補正メカニズムを採用している。ツール補正は幻覚の緩和に寄与し、それによって証明の全体的な精度が向上する。 Conjecture Correctionは命令で生成を洗練させるが、ペア化された(生成、エラー、改善)プロンプトは収集しない。
論文参考訳（メタデータ） (2023-09-27T17:29:41Z)

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