論文の概要: Monotonic Reference-Free Refinement for Autoformalization

• arxiv url: http://arxiv.org/abs/2601.23166v1
• Date: Fri, 30 Jan 2026 16:48:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-02 18:28:15.571066
• Title: Monotonic Reference-Free Refinement for Autoformalization
• Title（参考訳）: オートフォーマライゼーションのためのモノトニック参照フリーリファインメント
• Authors: Lan Zhang, Marco Valentino, André Freitas,
• Abstract要約: 完全定理自動形式化のための参照フリー反復単調過程を導入する。 我々は,形式的妥当性,論理的保存,数学的整合性,形式的品質よりもマスクされた複合目標を最適化する。 実験により、提案プロセスは複数の次元にまたがって同時に改善できることを示した。
• 参考スコア（独自算出の注目度）: 38.81622317169746
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While statement autoformalization has advanced rapidly, full-theorem autoformalization remains largely unexplored. Existing iterative refinement methods in statement autoformalization typicall improve isolated aspects of formalization, such as syntactic correctness, but struggle to jointly optimizing multiple quality dimensions, which is critical for full-theorem autoformalization. We introduce a reference-free iterative monotonic process for full-theorem autoformalization that leverages complementary feedback from theorem provers and LLM-based judges, without access to ground-truth proofs or existing formalizations at inference time. Our approach optimizes a masked composite objective over Formal Validity, Logical Preservation, Mathematical Consistency, and Formal Quality, guided by a responsiveness map that indicates how different LLMs acting as different roles preferentially improve each dimension. We further propose an acceptance policy that guarantees certified monotonic improvement, and provide conditions ensuring convergence and termination. Empirical experiments demonstrate the proposed process enables simultaneous improvement across multiple dimensions, achieving 93.44% formal validity and a 78.22% overall score on miniF2F, and 44.09% formal validity and a 29.79% overall score on ProofNet.
• Abstract（参考訳）: ステートメントの自己形式化は急速に進んでいるが、完全理論の自己形式化は未解明のままである。 文の自動形式化における既存の反復的洗練法は、構文的正しさのような形式化の分離的な側面を改善するが、完全理論の自動形式化にとって重要な複数の品質次元を共同最適化することに苦労する。 本研究では,定理証明やLLMに基づく判断の相補的フィードバックを利用する完全定理自動定式化のための基準自由反復単調プロセスを提案する。 本手法は,異なる役割として機能するLCMがそれぞれの次元を優先的に改善することを示す応答性マップによって導かれる,形式的妥当性,論理的保存,数学的一貫性,形式的品質よりもマスクされた複合目的を最適化する。 さらに,認定された単調改善を保証し,収束と終了を確実にする条件を提供する受理政策を提案する。 実験的な実験は、提案されたプロセスが複数の次元で同時に改善できることを示し、93.44%の正式な妥当性と、MiniF2Fの78.22%の総合スコア、44.09%の正式な妥当性、ProofNetの29.79%の総合スコアを達成した。

関連論文リスト

• Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
  大規模言語モデル(LLM)は、現実のファクトチェックシステムにますます多くデプロイされている。 FactArenaは、完全に自動化されたアリーナスタイルの評価フレームワークである。 本研究では,静的クレーム検証精度とエンドツーエンドのファクトチェック能力の相違点を明らかにした。
  論文  参考訳（メタデータ） (2026-01-06T02:51:56Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• Conjecturing: An Overlooked Step in Formal Mathematical Reasoning [10.398167568549924]
  結論を導かない限り、多くの数学的問題は直接形式化できない。 本研究では,大規模言語モデルの導出能力を測定するためにConjectureBenchを開発した。 提案手法は,GPT-4.1と7とDeepSeek-V3.1の13のPutnamBench問題において,最初のエンドツーエンドの自動形式化を実現する。
  論文  参考訳（メタデータ） (2025-10-13T22:29:49Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。 その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。 VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
  論文  参考訳（メタデータ） (2025-05-17T04:16:36Z)
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。 MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
  論文  参考訳（メタデータ） (2024-10-28T11:37:39Z)
• Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
  改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。 まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。 ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)

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

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