論文の概要: TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition
- arxiv url: http://arxiv.org/abs/2510.11944v1
- Date: Mon, 13 Oct 2025 21:09:36 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-15 19:02:32.096613
- Title: TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition
- Title（参考訳）: TopoAlign: トポロジカル分解によるコードから数学への調整フレームワーク
- Authors: Yupei Li, Philipp Borchert, Gerasimos Lampouras,
- Abstract要約: TopoAlignは、広く利用可能なコードリポジトリをMath LLMのトレーニングリソースとしてアンロックするフレームワークである。
TopoAlignはコードをdocstring、main関数、Dependency関数に分解し、これらのコンポーネントを形式的なステートメントを構造的にミラーするアナログに再組み立てする。
我々は、DeepSeek-MathとHeraldの2つの最先端モデルをトレーニングし、minif2f、Patnam、ProofNetベンチマークで評価する。
- 参考スコア（独自算出の注目度）: 9.593530910909363
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large Language Models (LLMs) excel at both informal and formal (e.g. Lean 4) mathematical reasoning but still struggle with autoformalisation, the task of transforming informal into formal mathematical statements. Autoformalisation helps pair the informal reasoning of LLMs with formal proof assistants which enable machine-verifiable generation and mitigate hallucinations. Yet, the performance of current Math LLMs is constrained by the scarcity of large-scale corpora, particularly those containing pairs of informal and formal statements. Although current models are trained to generate code from natural language instructions, structural and syntactic differences between these and formal mathematics limit effective transfer learning. We propose TopoAlign, a framework that unlocks widely available code repositories as training resources for Math LLMs. TopoAlign decomposes code into docstrings, main functions, and dependency functions, and reassembles these components into analogues that structurally mirror formal statements. This produces structurally aligned code data that can be used for training Math LLMs without requiring additional human annotation. We train two state-of-the-art models, DeepSeek-Math and Herald, and evaluate them on the minif2f, Putnam, and ProofNet benchmarks. TopoAlign provides substantial gains for DeepSeek-Math, improving performance by 17.77% on BEq@10 and 68.82% on typecheck@10. Despite introducing no new mathematical knowledge, our framework achieves gains of 0.12% and 1.09% for Herald on BEq@10 and typecheck@10, respectively, demonstrating that training on aligned code data is beneficial even for specialized models.
- Abstract（参考訳）: 大言語モデル(LLMs)は、非公式および形式的(例:Lean 4)数学的推論の両方で優れるが、形式化された数学的ステートメントにフォーマルに変換するタスクであるオートフォーマル化に苦戦している。
オートフォーマル化(Autoformalization)は、LLMの非公式な推論と、マシン検証可能な生成と緩和幻覚を可能にする公式な証明アシスタントとの結合を支援する。
しかし、現在の数学 LLM の性能は、大規模なコーパスの不足、特に非公式な文と形式的な文のペアを含むものによって制約されている。
現在のモデルは、自然言語命令からコードを生成するために訓練されているが、これらと形式数学の間の構造的および構文的差異は、効果的な伝達学習を制限する。
TopoAlignは、広く利用可能なコードリポジトリをMath LLMのトレーニングリソースとしてアンロックするフレームワークである。
TopoAlignはコードをdocstring、main関数、Dependency関数に分解し、これらのコンポーネントを形式的なステートメントを構造的にミラーするアナログに再組み立てする。
これは、追加の人間のアノテーションを必要とせずに、Math LLMのトレーニングに使用できる構造的に整合したコードデータを生成する。
我々は、DeepSeek-MathとHeraldの2つの最先端モデルをトレーニングし、minif2f、Patnam、ProofNetベンチマークで評価する。
TopoAlignはDeepSeek-Mathにかなりの利益をもたらし、BEq@10では17.77%、typecheck@10では68.82%のパフォーマンス向上を実現している。
新たな数学的知識は導入されていないが、私たちのフレームワークは、BEq@10とtypecheck@10でそれぞれHeraldの0.12%と1.09%のゲインを達成している。
関連論文リスト
- DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。
これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。
我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
論文 参考訳（メタデータ） (2025-10-12T21:42:04Z) - 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) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。
LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。
我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
論文 参考訳（メタデータ） (2025-04-23T18:04:38Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
本研究では,自然言語フィードバック型検証器Math-Minosを提案する。
実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
論文 参考訳（メタデータ） (2024-06-20T06:42:27Z) - Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization [45.439933713342256]
大規模言語モデル(LLM)は、数学的な量的推論問題を解く能力がますます高まっている。
LLMのトレーニングコーパスが十分に多くの形式数学の例を含むなら、それらが形式的イザベル符号に翻訳するように促すことができるという事実を活用する。
これは、形式化されたバージョンが内部や形式化された問題ステートメントと矛盾するソリューションを自動的に拒否するメカニズムを提供する。
論文 参考訳（メタデータ） (2024-03-26T22:01:13Z) - InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning [98.53491178426492]
InternLM2から事前学習を継続するILMs InternLM-Mathをオープンソースとして公開する。
我々は、連鎖推論、報酬モデリング、形式推論、データ拡張、コードインタプリタを、統一されたSeq2seqフォーマットで統一する。
我々の事前学習モデルは、微調整なしでMiniF2Fテストセットで30.3を達成する。
論文 参考訳（メタデータ） (2024-02-09T11:22:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。