論文の概要: FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse and Prover-Effective Autoformalization

• arxiv url: http://arxiv.org/abs/2603.19828v2
• Date: Mon, 23 Mar 2026 06:21:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-24 14:46:12.198141
• Title: FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse and Prover-Effective Autoformalization
• Title（参考訳）: FormalEvolve: ダイバージョンとプロバーエフェクティブオートフォーマライゼーションのためのニューロ・シンボリック進化探索
• Authors: Haijian Lu, Wei Wang, Jing Liu,
• Abstract要約: 我々は、意味的に一貫性のあるレパートリーの予算付きテストタイム検索として、オートフォーマル化を定式化する。 本稿では,コンパイル型ニューロシンボリック進化フレームワークであるFormalEvolveを提案する。 CombiBenchとProofNetでは、FormalEvolveは58.0%と84.9%のセマンティックヒット率(SH@100)に達し、セマンティック成功のクロスプロブレム濃度を低下させる。
• 参考スコア（独自算出の注目度）: 7.641987396532518
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Autoformalization aims to translate natural-language mathematics into compilable, machine-checkable statements. However, semantic consistency does not imply prover effectiveness: even semantically consistent formalizations can differ substantially in proof-search cost and success rate. In this work, we formulate autoformalization as a budgeted, test-time search for semantically consistent repertoires, and propose FormalEvolve, a compilation-gated neuro-symbolic evolutionary framework. FormalEvolve generates diverse candidates via LLM-driven mutation and crossover with bounded patch repair, while symbolic Abstract Syntax Tree (AST) rewrite operations further inject structural diversity. On CombiBench and ProofNet, under a strict generator-call budget of T = 100, FormalEvolve reaches semantic hit rates (SH@100) of 58.0% and 84.9%, and reduces cross-problem concentration of semantic successes(lower Gini). Under a fixed prover budget, FormalEvolve also improves downstream proving performance on CombiBench. Code will be released publicly.
• Abstract（参考訳）: オートフォーマル化は、自然言語数学をコンパイル可能な機械チェック可能な文に変換することを目的としている。 しかし、意味的整合性は証明効果を示さない: 意味的整合性のある形式化でさえ、実証研究のコストと成功率において著しく異なることがある。 本研究では,自己形式化を,意味論的に一貫性のあるレパートリーのための予算付きテストタイム検索として定式化し,コンパイル型ニューラルシンボリック進化フレームワークであるFormalEvolveを提案する。 FormalEvolve は LLM による突然変異と有界パッチ修復によるクロスオーバーによって多様な候補を生成するが、シンボリックな抽象構文木 (AST) の書き換え操作は構造的多様性をさらに注入する。 CombiBenchとProofNetでは、T = 100の厳格なジェネレータコール予算の下で、FormalEvolveは58.0%と84.9%のセマンティックヒット率(SH@100)に達し、セマンティック成功のクロスプロブレム濃度を低下させる(より低いGini)。 一定の証明予算の下で、FormalEvolveはCombiBenchの下流での証明性能も改善した。 コードは公開されます。

関連論文リスト

• Monotonic Reference-Free Refinement for Autoformalization [38.81622317169746]
  完全定理自動形式化のための参照フリー反復単調過程を導入する。 我々は,形式的妥当性,論理的保存,数学的整合性,形式的品質よりもマスクされた複合目標を最適化する。 実験により、提案プロセスは複数の次元にまたがって同時に改善できることを示した。
  論文  参考訳（メタデータ） (2026-01-30T16:48:33Z)
• Decompose-and-Formalise: Recursively Verifiable Natural Language Inference [34.505373718498014]
  ニューロシンボリックパイプラインにおける定理プロバー(TP)を持つ大言語モデル(LLM)は、自然言語推論(NLI)の検証と証明誘導による説明の洗練に役立つ 本稿では,前提と仮説のペアを包含木に分解する分解・形式化フレームワークを提案する。 また、一貫性のある引数-ロールバインディングを強制するために、イベントベースの論理形式に$-substitutionを導入します。
  論文  参考訳（メタデータ） (2026-01-27T13:43:30Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity [9.337443482551356]
  ASSESS (Semantic and Structure Evaluation Framework for Statement similarity) を導入し、セマンティックおよび構造情報を総合的に統合し、連続的な類似度スコアを提供する。 厳密な検証のために,ミニF2F と ProofNet から派生した 524 のエキスパート注釈付き形式文ペアの新しいベンチマーク EPLA を提案する。 EPLAの実験では、TransTEDの類似性は既存の手法よりも優れており、最先端の精度と最高カッパ係数が達成されている。
  論文  参考訳（メタデータ） (2025-09-26T12:02:58Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
  改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。 まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。 ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• Equivariant Transduction through Invariant Alignment [71.45263447328374]
  グループ内ハードアライメント機構を組み込んだ,新しいグループ同変アーキテクチャを提案する。 我々のネットワーク構造は、既存のグループ同変アプローチよりも強い同変特性を発達させることができる。 また、SCANタスクにおいて、従来のグループ同変ネットワークよりも経験的に優れていたことが判明した。
  論文  参考訳（メタデータ） (2022-09-22T11:19:45Z)

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

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