論文の概要: 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（参考訳）: 本稿では,形式的推論と自動定理証明の分野におけるベンチマークと評価の実践に関する,批判的かつ建設的な議論を提供する。
オープンコード、オープンデータ、そして完全かつエラーのないベンチマークがこの分野の進歩を加速する位置にある。
私たちは、この分野に貢献するための障壁を生み出すプラクティスを特定し、それらを取り除く方法を提案します。
また、誤解を招く評価情報を生み出すかもしれないプラクティスについても論じる。
我々は, 自動定理証明, 自己形式化, 非公式推論に寄与する様々なグループの人々を集めて議論することを目指している。
関連論文リスト
- 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) - 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) - A Unifying Framework for Learning Argumentation Semantics [47.84663434179473]
Inductive Logic Programmingアプローチを用いて、抽象的および構造化された議論フレームワークのアクセシビリティセマンティクスを解釈可能な方法で学習する新しいフレームワークを提案する。
提案手法は既存の議論解法よりも優れており,フォーマルな議論や人間と機械の対話の領域において,新たな研究の方向性が開けることになる。
論文 参考訳（メタデータ） (2023-10-18T20:18:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。