論文の概要: Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning

• arxiv url: http://arxiv.org/abs/2606.15972v1
• Date: Sun, 14 Jun 2026 18:52:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-16 16:21:33.968888
• Title: Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning
• Title（参考訳）: 一度形式化し、残りを編集する: 数学推論のための効果的なリーンベースの回答選択
• Abstract要約: 大規模言語モデル(LLM)は、数学的推論にますます応用される。 LLMは、機械チェック可能な厳密さで推論出力を検証するために利用することができる。 既存のリーンベースの回答選択作業では、自動形式化モデルを使用して、各候補の回答を独立してリーンで形式的なステートメントを生成します。 BASEは,問題ごとの1つの基本候補を形式化し,解式を編集して残りのK-1文を導出する,ベース・アンド・エジットパイプラインを提案する。
• 参考スコア（独自算出の注目度）: 7.385162909629646
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: With large language models (LLMs) increasingly applied to mathematical reasoning, formal proof assistants such as Lean can be leveraged to verify reasoning outputs with machine-checkable rigor, enabling use cases such as answer selection in test-time scaling with K sampled candidate answers. However, employing Lean requires that LLM outputs, originally in natural language, first be formalized. Existing Lean-based answer-selection work uses an autoformalization model to generate a formal statement in Lean for each candidate answer independently, incurring a significant computational cost. We propose BASE, a base-and-edit pipeline that formalizes a single base candidate per problem and derives the remaining K-1 statements by editing the answer expression in place. To facilitate this, we train a rewriter model LEANSCRIBE to localize the answer in the base formalization and generate a reusable edit function for the other K-1 candidates. BASE simultaneously improves selection accuracy and reduces formalization cost - a Pareto improvement that holds on all 12 (dataset, solver) configurations across four benchmarks and three solvers, cutting autoformalizer calls by about 5x at K=8, with the reduction expected to become larger as K grows. Code is available at https://github.com/ucr-rai/base-and-edit.
• Abstract（参考訳）: 数学的推論に大規模言語モデル(LLM)がますます適用されるにつれて、Leanのような形式的証明アシスタントは、機械チェック可能な厳密さによる推論出力の検証に活用され、Kサンプルの候補解を用いたテスト時間スケーリングにおける解答選択などのユースケースが実現される。 しかし、リーンを採用するためには、LLMのアウトプットは、元々自然言語で、まずは形式化する必要がある。 既存のリーンベースの回答選択作業では、自動形式化モデルを使用して、候補者の回答ごとにリーンで形式的なステートメントを生成し、かなりの計算コストを発生させます。 BASEは,問題ごとの1つの基本候補を定式化したベース・アンド・エジット・パイプラインであり,解式を編集して残りのK-1文を導出する。 これを容易にするために、リライターモデルLEANSCRIBEをトレーニングし、基本形式化の回答をローカライズし、他のK-1候補に対する再利用可能な編集関数を生成する。 4つのベンチマークと3つのソルバにまたがる12(データセット、ソルバ)構成をすべて保持し、K=8で約5倍のオートフォーマライザ呼び出しを削減し、Kが成長するにつれて減少すると予想されている。 コードはhttps://github.com/ucr-rai/base-and-edit.comで入手できる。

関連論文リスト

• Self-Verified Distillation: Your Language Model Is Secretly Its Own Synthetic Data Pipeline [56.53954182896384]
  大規模言語モデルのための簡単な訓練後改良アルゴリズムである自己検証蒸留を提案する。 自己検証蒸留(Self-Verified Distillation)は、未ラベルの種問に対する候補解を生成する。 プロンプトベースの自己検証を使用してフィルタリングし、結果の自己計算データセットをトレーニングする。 トレーニングデータ構築中に、より多くの候補世代をサンプリングし、より大きな検証予算を使用することで、高品質な自己計算データが得られることがわかった。
  論文  参考訳（メタデータ） (2026-05-20T17:26:10Z)
• Reaching Beyond the Mode: RL for Distributional Reasoning in Language Models [78.68818219506313]
  本稿では,複数解に対する分布推論を行うための多解補足学習手法について述べる。 質問応答, 診断, コーディングベンチマークを通じて, 単一回答学習ベースラインと比較して, 多様性, カバレッジ, 設定レベルの校正スコアが向上した。
  論文  参考訳（メタデータ） (2026-03-25T22:20:25Z)
• Reasoning Planning for Language Models [23.519351730129426]
  本稿では,コントラスト学習フレームワークであるEPICを紹介する。 EPICは、モデル推論能力とクエリメソッド互換性の両方をキャプチャする共有表現空間を学習する。 多様な数学的推論タスクの実験は、EPICが常に最適な推論方法を選択することを示している。
  論文  参考訳（メタデータ） (2025-11-01T11:51:53Z)
• CCQA: Generating Question from Solution Can Improve Inference-Time Reasoning in SLMs [14.97707719362011]
  textbfQuestion textbfAnswering (CCQA)におけるtextbfCycle-textbf一貫性を提案する。 CCQAは、サイクル一貫性に着想を得て、各推論経路から質問を生成し、それぞれが元の質問と類似度で評価し、次に、最も類似度の高い候補解を最終応答として選択する。 CCQAは数学および常識推論ベンチマークにおいて8つのモデルで既存の最先端(SOTA)手法を一貫して上回っていることが確認された。
  論文  参考訳（メタデータ） (2025-09-23T02:01:03Z)
• The Majority is not always right: RL training for solution aggregation [53.1050856072799]
  我々はアグリゲータモデルをトレーニングし、最終的な正解をレビューし、精査し、合成する。 重要な要素は、簡単なトレーニング例と厳しいトレーニング例のバランスを取ることだ。 我々の手法であるAggLMは、強いルールベースと報酬モデルベースラインの両方を上回ります。
  論文  参考訳（メタデータ） (2025-09-08T16:39:38Z)
• Learning to Refine: Self-Refinement of Parallel Reasoning in LLMs [102.48588475875749]
  本稿では,新しい並列テスト時間スケーリングフレームワークであるGenerative Self-Refinement (GSR)を紹介する。 GSRは一連の候補応答を並列に生成し、その後自己精製を行い、新しい優れた解を合成する。 提案手法は,5つの数学ベンチマークにおいて,最先端性能を実現する。
  論文  参考訳（メタデータ） (2025-08-27T06:51:48Z)
• Self-Questioning Language Models [58.73276539661649]
  本稿では,提案者がトピックを与えられ,解答者に対する質問を生成する非対称なセルフプレイフレームワークを提案する。 提案者と解答者はともに強化学習を通じて訓練される。 3桁の乗算、OMEGAベンチマークの代数問題、Codeforcesのプログラミング問題である。
  論文  参考訳（メタデータ） (2025-08-05T17:51:33Z)
• FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4 [14.265023575624008]
  FANS: Lean4を用いた自然言語数学推論のための形式的アンサー選択法を提案する。 LLMの算数推論能力を高めるためにLean4を使用した最初のフレームワークである。 LLMのNL数学能力を強化し、その正解をコンピュータで検証できるソリューションを提供する。
  論文  参考訳（メタデータ） (2025-03-05T07:34:53Z)
• Small Language Models Need Strong Verifiers to Self-Correct Reasoning [69.94251699982388]
  大規模言語モデル(LLM)の推論性能を高めるための有望なソリューションとして自己補正が登場した。 この研究は、小さい(=13B)言語モデル(LM)が、より強いLMから最小の入力で推論タスクを自己補正できるかどうかを考察する。
  論文  参考訳（メタデータ） (2024-04-26T03:41:28Z)
• Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization [45.439933713342256]
  大規模言語モデル(LLM)は、数学的な量的推論問題を解く能力がますます高まっている。 LLMのトレーニングコーパスが十分に多くの形式数学の例を含むなら、それらが形式的イザベル符号に翻訳するように促すことができるという事実を活用する。 これは、形式化されたバージョンが内部や形式化された問題ステートメントと矛盾するソリューションを自動的に拒否するメカニズムを提供する。
  論文  参考訳（メタデータ） (2024-03-26T22:01:13Z)

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

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