論文の概要: MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization
- arxiv url: http://arxiv.org/abs/2610.35269v1
- Date: Mon, 26 Oct 2026 11:44:26 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-27 22:27:13.846744
- Title: MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization
- Title（参考訳）: MechAlign: 数学的形式化におけるプロジェクトレベルでの意味的アライメントの評価
- Abstract要約: プロジェクトレベルのセマンティックアライメントレビューのためのフレームワークであるMechAlignを紹介します。
我々は173のOpenAI Mathプロジェクトから201の主要な成果の予備的なレビューを行う。
また、OpenAI Math、FermatのLast Theorem、Kakeyaの501の固定クレームステートメント-コンテキストトリプルで構成されたLeanReviewBenchを構築します。
- 参考スコア（独自算出の注目度）: 18.986093919008827
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Lean verifies that a formal proof establishes its stated proposition under declared assumptions, but does not check whether that proposition faithfully expresses the mathematical claim in a manuscript. Assessing this correspondence requires interpreting the main theorem through its project dependencies, which may be scattered throughout a large development. We introduce MechAlign, a framework for project-level semantic alignment review that combines formal dependency extraction with LLM-based assessment. Its extraction tool, LeanTrace, constructs a statement dependency graph from elaborated declarations, retaining definition bodies and structure constraints while excluding proof bodies and stopping at an explicit library boundary. The reviewer uses this context to investigate alignment and report discrepancies with localized evidence. We conduct a preliminary review of 201 main results from 173 OpenAI Math projects, using supplied informal descriptions and available paper context. A hyperbolic-group case illustrates how dependency inspection localizes a missing dimensional constraint relative to the manuscript, consistent with the upstream declaration of formalization scope. We also construct LeanReviewBench, comprising 501 fixed claim-statement-context triples from OpenAI Math, Fermat's Last Theorem, and Kakeya, with description provenance recorded. The resource supports controlled comparisons of more project-level semantic alignment evaluations.
- Abstract（参考訳）: リーンは、形式的な証明が宣言された前提の下でその命題を確立することを検証するが、その命題が原稿の数学的主張を忠実に表現しているかどうかを確認しない。
この対応を評価するには、プロジェクトの依存関係を通じて主定理を解釈する必要がある。
我々は,プロジェクトレベルのセマンティックアライメントレビューのためのフレームワークであるMechAlignを紹介した。
その抽出ツールであるLeanTraceは、詳細な宣言からステートメント依存グラフを構築し、定義ボディと構造制約を維持しながら、証明ボディを除外し、明示的なライブラリ境界で停止する。
この文脈を利用して、アライメントを調査し、局所的な証拠で不一致を報告する。
我々は173のOpenAI Mathプロジェクトから得られた201の主要な成果を、提供された非公式な記述と利用可能な論文コンテキストを用いて予備的なレビューを行う。
ハイパーボリック・グループ・ケースは、依存関係検査が、形式化スコープの上流宣言と一致して、原稿に対して欠落した次元的制約をローカライズする方法を示している。
また、OpenAI Math、FermatのLast Theorem、Kakeyaの501の固定クレーム-ステートメント-コンテキストトリプルで構成されたLeanReviewBenchを構築しました。
このリソースは、プロジェクトレベルのセマンティックアライメント評価の制御された比較をサポートする。
関連論文リスト
- Autoformalizing Argumentative Material Inferences [26.35292656634472]
我々は、ガード補完として議論材料推論のための自己形式化を開発する。
GUARDは、証明された信条を大幅に改善する。
シンボル的ソフトな批判と明示的な仮定層がこれらの利益の大部分を担っていることを示す。
論文 参考訳（メタデータ） (2026-09-15T11:05:26Z) - Structuring Semantic Embeddings for Principle Evaluation: A Prototype-Guided Contrastive Learning Approach [58.15427952222424]
汎用的なテキスト埋め込みはそのようなタスクに広くデプロイされているが、意味的類似性は意味的に似ているがタスク固有の例を示すことができる。
本稿では,凍結したテキスト埋め込み上に構築された幾何正規化モジュールであるPGCL(Prototype-Guided Contrastive Learning)を紹介する。
論文 参考訳（メタデータ） (2026-08-15T13:19:25Z) - Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。
ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
論文 参考訳（メタデータ） (2026-06-30T00:27:53Z) - Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
T は形式定理の意味的正しさを評価する枠組みである。
5つの実世界のLean 4リポジトリからベンチマークを構築します。
実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
論文 参考訳（メタデータ） (2026-04-26T13:24:20Z) - Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。
我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。
我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-13T01:33:20Z) - SITA: A Framework for Structure-to-Instance Theorem Autoformalization [20.941850622174236]
我々は、SITA(Structure-to-instance theorem autoformalization)の枠組みを開発する。
SITAは抽象数学的理論と、リーン証明アシスタントにおける具体的な応用のギャップを埋める。
対応するリーンの定義とインスタンス宣言を生成し、それらをリーンのタイプクラスメカニズムを使って統合し、構造的な仮定をチェックして検証済みの定理を構築します。
論文 参考訳（メタデータ） (2025-11-13T14:33:51Z) - 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) - DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。
DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。
我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
論文 参考訳（メタデータ） (2025-05-29T17:59:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。