Fugu-MT 論文翻訳(概要): Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs

論文の概要: Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs

arxiv url: http://arxiv.org/abs/2507.04719v1
Date: Mon, 07 Jul 2025 07:27:45 GMT
ステータス: 翻訳完了
システム内更新日: 2025-07-08 15:46:35.309763
Title: Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
Title（参考訳）: 形式的/インフォーマルな文と形式的/インフォーマルな証明を用いた形式的推論のための完全ベンチマークの提唱
Authors: Roozbeh Yousefzadeh, Xuenan Cao,
Abstract要約: 私たちは、オープンコード、オープンデータ、そして、完全でエラーのないベンチマークがこの分野の進歩を加速する立場を取っています。私たちは、この分野に貢献するための障壁を生み出すプラクティスを特定し、それらを取り除く方法を提案します。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: This position paper provides a critical but constructive discussion of current practices in benchmarking and evaluative practices in the field of formal reasoning and automated theorem proving. We take the position that open code, open data, and benchmarks that are complete and error-free will accelerate progress in this field. We identify practices that create barriers to contributing to this field and suggest ways to remove them. We also discuss some of the practices that might produce misleading evaluative information. We aim to create discussions that bring together people from various groups contributing to automated theorem proving, autoformalization, and informal reasoning.
Abstract（参考訳）: 本稿では,形式的推論と自動定理証明の分野におけるベンチマークと評価の実践に関する,批判的かつ建設的な議論を提供する。オープンコード、オープンデータ、そして完全かつエラーのないベンチマークがこの分野の進歩を加速する位置にある。私たちは、この分野に貢献するための障壁を生み出すプラクティスを特定し、それらを取り除く方法を提案します。また、誤解を招く評価情報を生み出すかもしれないプラクティスについても論じる。我々は, 自動定理証明, 自己形式化, 非公式推論に寄与する様々なグループの人々を集めて議論することを目指している。

関連論文リスト

Translating Informal Proofs into Formal Proofs Using a Chain of States [20.0011959667642]
本稿では,自然言語で表現された非公式な数学的証明を,制約付き計算予算の下でLean4の形式的証明に変換する問題に対処する。まず、中間形式的証明状態の列である状態の連鎖(CoS)を、非公式引数の論理構造に沿って抽出する。次に、CoS内の隣接状態間の遷移戦略を生成し、完全な形式的証明を構築する。
論文参考訳（メタデータ） (2025-12-11T06:08:34Z)
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)
Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
論文参考訳（メタデータ） (2025-09-02T14:16:02Z)
Beyond Agreement: Rethinking Ground Truth in Educational AI Annotation [1.8434042562191815]
我々は、注釈品質ハッパーのゲートキーパーとしての人間間信頼性(IRR)への過度な依存が、データの分類に進展していると論じる。本稿では,マルチラベルアノテーションスキーム,エキスパートベースアプローチ,クローズ・ザ・ループの有効性など,補完的な評価手法の5つの例を紹介する。我々は、アノテーションの品質と基礎的真実を再考し、合意のみに対する妥当性と教育的影響を優先することを求める。
論文参考訳（メタデータ） (2025-07-31T20:05:26Z)
Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning [8.135142928659546]
自動形式化タスクを評価するための,体系的かつ自動的な手法を提案する。提案手法は,論理的保存(LP),数学的整合性(MC),形式的妥当性(FV),形式的品質(FQ)を基準とした審査員のアンサンブルに基づく。全体としては,LLM審査員のEFGアンサンブルが評価に好適であることを示す。
論文参考訳（メタデータ） (2025-06-12T17:09:51Z)
Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
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)
Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文参考訳（メタデータ） (2024-06-14T06:52:08Z)
Improving Autoformalization using Type Checking [15.58948808529849]
我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
論文参考訳（メタデータ） (2024-06-11T13:01:50Z)
DELTA: Pre-train a Discriminative Encoder for Legal Case Retrieval via Structural Word Alignment [55.91429725404988]
判例検索のための識別モデルであるDELTAを紹介する。我々は浅層デコーダを利用して情報ボトルネックを作り、表現能力の向上を目指しています。本手法は, 判例検索において, 既存の最先端手法よりも優れている。
論文参考訳（メタデータ） (2024-03-27T10:40:14Z)
A Unifying Framework for Learning Argumentation Semantics [47.84663434179473]
Inductive Logic Programmingアプローチを用いて、抽象的および構造化された議論フレームワークのアクセシビリティセマンティクスを解釈可能な方法で学習する新しいフレームワークを提案する。提案手法は既存の議論解法よりも優れており,フォーマルな議論や人間と機械の対話の領域において,新たな研究の方向性が開けることになる。
論文参考訳（メタデータ） (2023-10-18T20:18:05Z)
Abductive Commonsense Reasoning Exploiting Mutually Exclusive Explanations [118.0818807474809]
帰納的推論は、イベントのもっともらしい説明を見つけることを目的としている。自然言語処理における帰納的推論のための既存のアプローチは、しばしば監督のために手動で生成されたアノテーションに依存している。この研究は、ある文脈に対して、説明のサブセットのみが正しいという事実を活用する、帰納的コモンセンス推論のアプローチを提案する。
論文参考訳（メタデータ） (2023-05-24T01:35:10Z)
Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。これは、説明に表される論理述語に基づいて、反実仮説を生成する。そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
論文参考訳（メタデータ） (2022-05-25T03:40:59Z)
Probing as Quantifying the Inductive Bias of Pre-trained Representations [99.93552997506438]
本稿では,特定のタスクに対する表現の帰納的バイアスを評価することを目的とした,探索のための新しいフレームワークを提案する。トークン、アーク、文レベルの一連のタスクに我々のフレームワークを適用します。
論文参考訳（メタデータ） (2021-10-15T22:01:16Z)

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