論文の概要: Formal-Informal Mathematical Alignment through and beyond Human Annotations

• arxiv url: http://arxiv.org/abs/2610.31011v1
• Date: Thu, 22 Oct 2026 09:46:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-24 02:08:44.310643
• Title: Formal-Informal Mathematical Alignment through and beyond Human Annotations
• Title（参考訳）: 人間のアノテーションを通した形式的・非形式的な数学的アライメント
• Abstract要約: 専門家のアノテーションを利用して、Stacksプロジェクトからの非公式なステートメントとtextttmathlibでの形式化をリンクするデータセットを構築します。 形式化された知識の探索と再利用を容易にするため,新たに発見されたアライメントをMaRDI知識グラフに統合した。
• 参考スコア（独自算出の注目度）: 3.9786262195210167
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formalized mathematics libraries such as Lean's \texttt{mathlib} provide machine-verifiable representations of mathematical knowledge, including definitions, theorems, and their relationships. If effectively connected to informal mathematical resources, formal mathematics could help uncover previously implicit links between mathematical concepts and improve access to existing formalizations. However, connections between informal and formal mathematics libraries are currently sparse and unsystematic. In this paper, we make first strides towards better formal integration. We construct a dataset linking informal statements from the Stacks Project to their formalizations in \texttt{mathlib} by exploiting expert annotations. We evaluate retrieval, LLM-based reranking, and LLM-assisted verification to discover new unannotated informal-to-formal links. To facilitate exploration and reuse of formalized knowledge, we integrated the newly discovered alignments into the MaRDI knowledge graph, enabling mathematicians to find formal counterparts to informal mathematical content. We discuss the difficulties and challenges in using LLMs for linking formal and informal mathematical content. All code and data necessary for reproducing this paper can be found at: https://github.com/AnkitSatpute/Formal-Informal-Mathematical-Alignment
• Abstract（参考訳）: Lean's \texttt{mathlib} のような形式化された数学ライブラリは、定義、定理、それらの関係を含む数学的知識の機械的に検証可能な表現を提供する。 仮の数学的資源に効果的に結びつくと、形式数学は、数学的概念の間の以前に暗黙のつながりを発見し、既存の形式化へのアクセスを改善するのに役立つ。 しかし、非公式な数学ライブラリーと形式的な数学ライブラリーのつながりは、現在では疎外であり、体系的ではない。 本稿では,よりフォーマルな統合に向けて第一歩を踏み出す。 専門家のアノテーションを活用して,Stacksプロジェクトからの非公式なステートメントと,それを形式化したデータセットを作成した。 検索, LLMに基づく再分類, LLMによる検証を行い, 未通知の非公式な形式的リンクを新たに発見する。 形式化された知識の探索と再利用を容易にするため、新たに発見されたアライメントをMaRDI知識グラフに統合し、数学者が非公式な数学的内容の形式的な相違を見つけられるようにした。 形式的および形式的な数学的内容のリンクにLLMを使うことの難しさと課題について論じる。 https://github.com/AnkitSatpute/Formal-Informal-Mathematical-Alignment. https://github.com/AnkitSatpute/Formal-Informal-Mathematical-Alignment

関連論文リスト

• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  AI4Mathシステムの次の飛躍は、事前に定義された問題解決者から研究エージェントへの決定的なシフトを必要とする。 この分野の体系的なレビューを行い、データセット、自動形式化、証明合成について紹介する。
  論文  参考訳（メタデータ） (2026-07-08T17:46:36Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。 最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。 汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-06-30T05:05:03Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  数学的民俗補題の発見と形式化を自動化するLLMベースのマルチエージェントシステムであるMathlibLemmaを紹介する。 さらに、幅広い数学的領域にまたがる4,028の型チェックリーンステートメントスイートであるMathlibLemmaベンチマークを構築します。
  論文  参考訳（メタデータ） (2026-01-30T15:24:42Z)
• TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition [9.593530910909363]
  TopoAlignは、広く利用可能なコードリポジトリをMath LLMのトレーニングリソースとしてアンロックするフレームワークである。 TopoAlignはコードをdocstring、main関数、Dependency関数に分解し、これらのコンポーネントを形式的なステートメントを構造的にミラーするアナログに再組み立てする。 我々は、DeepSeek-MathとHeraldの2つの最先端モデルをトレーニングし、minif2f、Patnam、ProofNetベンチマークで評価する。
  論文  参考訳（メタデータ） (2025-10-13T21:09:36Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。 研究論文は大量の背景と文脈を必要とする。 本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
  論文  参考訳（メタデータ） (2023-10-12T00:50:24Z)

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

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