Fugu-MT 論文翻訳(概要): Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

論文の概要: Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

arxiv url: http://arxiv.org/abs/2607.13292v1
Date: Tue, 14 Jul 2026 21:58:52 GMT
ステータス: 翻訳完了
システム内更新日: 2026-07-16 16:39:12.595688
Title: Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
Title（参考訳）: 理論レベルオートフォーマル化:独立したステートメントから統一された形式的知識ベースへ
Abstract要約: 我々は、理論レベルの自己形式化について論じる: 完全な理論を形式化し、すべての依存関係を構造化ライブラリとして含む。我々は,このシフトの重要性を検証し,代替の見解に対処し,オープンな課題を特定し,将来性のある3つの経路を提案する。
参考スコア（独自算出の注目度）: 32.96018876882992
License: http://creativecommons.org/licenses/by-nc-sa/4.0/
Abstract: Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual statements, real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target theorems can even be stated. In this position paper, we argue for theory-level autoformalization: formalizing complete theories, including all their inter-dependencies, as structured libraries. We examine the significance of this shift, address alternative views, identify open challenges, and propose three promising paths forward. Our survey of autoformalization is available at https://github.com/marcusm117/Awesome-Autoformalization.
Abstract（参考訳）: オートフォーマル化(Autoformalization)は、非公式な自然言語を形式的で機械で検証可能な言語に翻訳する。ほとんどの研究は個々の言明に焦点を当てているが、真の形式化の努力は本質的に理論レベルであり、対象定理が記述される前に公理、定義、補題の網全体を必要とする。本稿では,すべての依存関係を含む完全理論を構造化ライブラリとして定式化する,理論レベルの自己形式化を論じる。我々は,このシフトの重要性を検証し,代替の見解に対処し,オープンな課題を特定し,将来性のある3つの経路を提案する。自動形式化に関する私たちの調査はhttps://github.com/marcusm117/Awesome-Autoformalizationで公開されています。

関連論文リスト

Coherency through formalisations of Structured Natural Language, A case study on FRETish [0.0]
形式化とは、システム要件を形式言語で記述するプロセスである。本稿では,ホルマライゼーションによるコヒーレンシ(コヒーレンシー)の新たなガイドラインを提案する。本稿では,NASA の形式的要求抽出ツール FRET を分析し,制御された自然言語 FRETish を MTL の形式言語に自動翻訳する手法を提案する。
論文参考訳（メタデータ） (2026-05-11T12:30:53Z)
FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean [7.11696910077237]
FormalScienceは、人為的なエージェントパイプラインで、テキストシンタクティックに正確で、テキスト的に整列された、低い経済コストに対する非公式な推論の形式的証明を生成する。我々は、Lean4の公式表現とともに200の物理問題と解(主に量子力学と電磁磁性)のデータセットであるFormalPhysicsを構築した。我々は、ゼロショットプロンプト、エラーフィードバックによる自己抑制、新しいマルチステージエージェントアプローチを通じて、データセット上のステートメントの自動形式化タスクに基づいて、オープンソースモデルとプロプライエタリシステムを評価する。
論文参考訳（メタデータ） (2026-04-24T20:47:22Z)
From Specification to Architecture: A Theory Compiler for Knowledge-Guided Machine Learning [6.365277569082624]
理論誘導型機械学習は、モデル設計に直接ドメイン知識を組み込むことで、性能が向上することを示した。しかし、形式的ドメイン理論がアーキテクチャ上の制約に変換されるプロセスは完全に手作業のままである。本稿では,型付き機械可読なドメイン理論を入力として受け入れ,アーキテクチャを自動生成するシステムである理論コンパイラを提案する。
論文参考訳（メタデータ） (2026-03-15T13:15:31Z)
ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文参考訳（メタデータ） (2025-10-28T16:22:54Z)
Subject-Event Ontology Without Global Time: Foundations and Execution Semantics [51.56484100374058]
形式化は9つの公理(A1-A9)を含み、実行可能性の正しさを保証する:履歴の単調性(I1)、因果性の非巡回性(I2)、トレーサビリティ(I3)である。フォーマル化は、分散システム、マイクロサービスアーキテクチャ、DLTプラットフォーム、およびマルチパースペクティビティシナリオ(異なる主題から事実を分解する)に適用できる。モデルに基づくアプローチ(A9): スキーマによるイベント検証、アクター認可、グローバル時間なしで因果連鎖の自動構築(W3)。
論文参考訳（メタデータ） (2025-10-20T19:26:44Z)
Towards a Common Framework for Autoformalization [2.487142846438629]
オートフォーマル化(Autoformalization)は、フォーマル化の自動化を指す用語として登場した。本稿の目的は、オートフォーマライゼーション(autoformalization)と見なせるものの-明示的または暗黙的な-インスタンスをレビューすることである。
論文参考訳（メタデータ） (2025-09-11T19:28:56Z)
StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion [30.51794514312176]
効果的な自己形式化のための2つの重要な能力を特定する。我々は、両方の能力を改善するデータ合成およびトレーニングパイプラインであるThinkingFを紹介します。結果の7Bと32Bモデルは、包括的な形式的知識と強い形式的・形式的推論の両方を示す。
論文参考訳（メタデータ） (2025-08-06T13:28:22Z)
Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。自己形式化定理文の自動意味評価を行う。
論文参考訳（メタデータ） (2024-05-27T14:35:10Z)
How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
知識ベース質問回答(KBQA)は,知識ベースにおける事実に基づいた自然言語質問への回答を目的としている。最近の研究は、論理形式生成のための大規模言語モデル(LLM)の機能を活用して性能を向上させる。
論文参考訳（メタデータ） (2024-01-11T09:27:50Z)
Provable Limitations of Acquiring Meaning from Ungrounded Form: What will Future Language Models Understand? [87.20342701232869]
未知のシステムが意味を習得する能力について検討する。アサーションによってシステムが等価性のような意味関係を保存する表現をエミュレートできるかどうか検討する。言語内のすべての表現が参照的に透明であれば,アサーションによってセマンティックエミュレーションが可能になる。しかし、言語が変数バインディングのような非透過的なパターンを使用する場合、エミュレーションは計算不能な問題になる可能性がある。
論文参考訳（メタデータ） (2021-04-22T01:00:17Z)

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