論文の概要: FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean

• arxiv url: http://arxiv.org/abs/2604.23002v1
• Date: Fri, 24 Apr 2026 20:47:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-28 17:12:07.093599
• Title: FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean
• Title（参考訳）: FormalScience: リーンのエージェントコード生成による、スケーラブルなヒューマン・イン・ザ・ループの科学オートフォーマル化
• Authors: Jordan Meadows, Lan Zhang, Andre Freitas,
• Abstract要約: FormalScienceは、人為的なエージェントパイプラインで、テキストシンタクティックに正確で、テキスト的に整列された、低い経済コストに対する非公式な推論の形式的証明を生成する。 我々は、Lean4の公式表現とともに200の物理問題と解(主に量子力学と電磁磁性)のデータセットであるFormalPhysicsを構築した。 我々は、ゼロショットプロンプト、エラーフィードバックによる自己抑制、新しいマルチステージエージェントアプローチを通じて、データセット上のステートメントの自動形式化タスクに基づいて、オープンソースモデルとプロプライエタリシステムを評価する。
• 参考スコア（独自算出の注目度）: 7.11696910077237
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formalising informal mathematical reasoning into formally verifiable code is a significant challenge for large language models. In scientific fields such as physics, domain-specific machinery (\textit{e.g.} Dirac notation, vector calculus) imposes additional formalisation challenges that modern LLMs and agentic approaches have yet to tackle. To aid autoformalisation in scientific domains, we present FormalScience; a domain-agnostic human-in-the-loop agentic pipeline that enables a single domain expert (without deep formal language experience) to produce \textit{syntactically correct} and \textit{semantically aligned} formal proofs of informal reasoning for low economic cost. Applying FormalScience to physics, we construct FormalPhysics, a dataset of 200 university-level (LaTeX) physics problems and solutions (primarily quantum mechanics and electromagnetism), along with their Lean4 formal representations. Compared to existing formal math benchmarks, FormalPhysics achieves perfect formal validity and exhibits greater statement complexity. We evaluate open-source models and proprietary systems on a statement autoformalisation task on our dataset via zero-shot prompting, self-refinement with error feedback, and a novel multi-stage agentic approach, and explore autoformalisation limitations in modern LLM-based approaches. We provide the first systematic characterisation of semantic drift in physics autoformalisation in terms of concepts such as notational collapse and abstraction elevation which reveals what formal language verifies when full semantic preservation is unattainable. We release the codebase together with an interactive UI-based FormalScience system which facilitates autoformalisation and theorem proving in scientific domains beyond physics.https://github.com/jmeadows17/formal-science
• Abstract（参考訳）: 形式化された検証可能なコードへの非公式な数学的推論の形式化は、大きな言語モデルにとって重要な課題である。 物理学などの科学分野において、ドメイン固有機械(\textit{e g } Dirac notation, vector calculus)は、現代のLLMやエージェント的アプローチがまだ取り組まなかったさらなる形式化課題を課す。 科学領域における自己形式化を支援するために,我々は,単一ドメインの専門家が(深い形式的な言語経験を伴わずに)低経済コストの非公式推論の形式的証明を生成できる,ドメインに依存しないエージェント型パイプラインであるFormalScienceを提案する。 FormalScienceを物理学に適用し、Lean4の公式表現とともに200の大学レベルの(LaTeX)物理問題と解(主に量子力学と電磁磁性)のデータセットであるFormalPhysicsを構築した。 既存のフォーマルな数学ベンチマークと比較すると、FormalPhysicsは完全な形式的妥当性を達成し、文の複雑さを増大させる。 我々は、ゼロショットプロンプト、エラーフィードバックによる自己修正、新しい多段階エージェントアプローチを通じて、データセット上のステートメントの自動形式化タスクに基づいて、オープンソースモデルとプロプライエタリシステムを評価し、現代のLCMベースのアプローチにおける自動形式化の限界を探求する。 本稿では,物理の自己形式化における意味的ドリフトの体系的特徴付けとして,完全意味的保存が不可能な場合に形式言語がどのような検証を行うかを明らかにする,記法的崩壊や抽象的高揚といった概念を用いて,意味的ドリフトの体系的特徴付けを行う。 物理以外の科学領域における自己形式化と定理の証明を容易にする,インタラクティブなUIベースのFormalScienceシステムとともに,コードベースをリリースする。

関連論文リスト

• MMFormalizer: Multimodal Autoformalization in the Wild [79.24853896733154]
  MMFormalizerは、適応グラウンドを現実の数学的および物理的ドメインのエンティティと統合することにより、テキスト以外の自動形式化を拡張する。 MMFormalizerを新しいベンチマークであるPhyX-AFで評価し,MathVerse,PhyX,Synthetic Geometry,Analytic Geometryから115個のキュレートされたサンプルを作成した。 その結果, GPT-5 と Gemini-3-Pro が最も高いコンパイル精度と意味的精度が得られ, GPT-5 は物理的推論に優れていた。
  論文  参考訳（メタデータ） (2026-01-06T13:42:51Z)
• Automated Formalization via Conceptual Retrieval-Augmented LLMs [19.328918823576153]
  CRAMFは概念駆動のRetrieval-Augmented Mathematical Formalizationフレームワークである。 概念定義知識ベースをMathlib4から自動構築するフレームワークを提案する。 miniF2F, ProofNet, そして新たに提案したAdvancedMathベンチマークでは, CRAMF を LLM ベースのオートフォーマライザにシームレスに統合できることが示されている。
  論文  参考訳（メタデータ） (2025-08-09T10:54:25Z)
• 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)
• SciInstruct: a Self-Reflective Instruction Annotated Dataset for Training Scientific Language Models [57.96527452844273]
  我々はSciInstructを紹介した。SciInstructは、大学レベルの科学的推論が可能な科学言語モデルを訓練するための科学指導スイートである。 我々は、物理学、化学、数学、公式な証明を含む多種多様な高品質なデータセットをキュレートした。 SciInstructの有効性を検証するため、SciInstruct、すなわちChatGLM3(6Bと32B)、Llama3-8B-Instruct、Mistral-7B: MetaMathを用いて言語モデルを微調整した。
  論文  参考訳（メタデータ） (2024-01-15T20:22:21Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。 研究論文は大量の背景と文脈を必要とする。 本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
  論文  参考訳（メタデータ） (2023-10-12T00:50:24Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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