論文の概要: Theory-Scale Auto-Formalization of Logics for Computer Science

• arxiv url: http://arxiv.org/abs/2606.26525v1
• Date: Thu, 25 Jun 2026 01:59:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-26 18:46:32.142578
• Title: Theory-Scale Auto-Formalization of Logics for Computer Science
• Title（参考訳）: コンピュータ科学のための論理理論の大規模自動定式化
• Abstract要約: LCS-Bench は Logics for Computer Science に基づく理論スケールのベンチマークである。 アーティファクトには327の教科書項目,4,076以上のリーン宣言,85万行以上のリーンコードが含まれています。 LCS-Benchは高品質で一貫性があり、忠実であることを示す。
• 参考スコア（独自算出の注目度）: 36.45195518081978
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Auto-formalization is critical for scalable formal verification, but existing progress largely focuses on isolated statements, while theory-scale auto-formalization, which coherently translates hundreds of interdependent definitions, lemmas, and theorems, remains open due to challenges in consistency, faithfulness, scalability, and correctness. In this paper, we introduce LCS-Bench, a stand-alone, theory-scale benchmark based on Logics for Computer Science. LCS-Bench is built through a novel semi-automated agentic pipeline that leverages concept graphs, formal signature planning, issue tracking, sorry-filling with counter-example search, complemented by faithfulness review from human experts. The resulting artifact covers 327 textbook items, over 4,076 Lean declarations, and more than 85K lines of Lean code. The dataset supports broad evaluation through a data engine that automatically derives five tracks of evaluation benchmarks, measuring different aspects of auto-formalization and theorem-proving capabilities. We also introduce a novel evaluation protocol featuring definitional equivalence checkers, enabling more fine-grained and faithful assessment. Through extensive evaluation on 14 models, we demonstrate that (1) LCS-Bench is of high quality, consistent, and faithful; (2) the benchmark is challenging, with state-of-the-art models achieving only 20.1% on auto-formalization tasks; and (3) our analysis reveals key findings regarding theory-scale auto-formalization and suggests promising directions for future work.
• Abstract（参考訳）: 自動形式化は、スケーラブルな形式検証には不可欠であるが、既存の進歩は主に孤立したステートメントに焦点を当て、理論スケールのオート形式化は、一貫性、忠実性、スケーラビリティ、正確性の課題のために、何百もの相互依存の定義、補題、定理を一貫性を持って翻訳する。 本稿では,計算機科学のための論理に基づくスタンドアローン理論スケールのベンチマークであるLCS-Benchを紹介する。 LCS-Benchは、概念グラフ、正式な署名計画、問題追跡、反例探索による謝罪の埋め合わせ、人間の専門家による忠実なレビューによって補完される、新しい半自動エージェントパイプラインを通じて構築されている。 成果物には327の教科書項目,4,076以上のリーン宣言,85万行以上のリーンコードが含まれています。 このデータセットは、自動形式化と定理証明能力の異なる側面を計測し、5つの評価ベンチマークを自動的に導出するデータエンジンを通じて幅広い評価をサポートする。 また、定義等価チェッカーを特徴とする新しい評価プロトコルを導入し、よりきめ細やかで忠実な評価を可能にする。 その結果,(1)LCS-Benchは高品質で一貫性があり,忠実である,(2)最先端のモデルでは,自動形式化タスクで20.1%しか達成できない,(3)理論スケールの自己形式化に関する重要な知見が得られ,今後の作業に向けて有望な方向性が示唆される,という結果が得られた。

関連論文リスト

• FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models [53.68149869349268]
  大規模言語モデル(LLM)は、自動理論計算機科学(TCS)研究の可能性を増大させている。 我々は、最前線のエンドツーエンドのTCS研究でLSMを評価するための専門家検証ベンチマークである ourbenchmarkを紹介した。
  論文  参考訳（メタデータ） (2026-08-20T15:13:41Z)
• From Reasoning to Agentic: Credit Assignment in Reinforcement Learning for Large Language Models [3.651838585096184]
  大規模言語モデルの強化学習(RL)は、スパースで結果レベルの報酬にますます依存している。 我々は2024年から2026年にかけて発行された47のCA法を調査し,それらの分類を課題別に2次元分類で整理した。 我々は,(1)分類ラベル,ベースラインファミリー,エビデンスレベルを備えた構造化機械可読紙の在庫,(2)組織的方法論的ギャップを特定するための将来のCA論文の報告チェックリスト,(3)タスクファミリ,メタデータ要件,管理された分岐タスクを備えたベンチマークプロトコル仕様の3つの再利用可能な資源をコントリビュートする。
  論文  参考訳（メタデータ） (2026-04-10T16:17:44Z)
• SciMDR: Benchmarking and Advancing Scientific Multimodal Document Reasoning [59.93568326270048]
  集中セグメント上での忠実で孤立したQAペアを生成する合成合成フレームワークを提案する。 クロスモーダル理解のための大規模トレーニングデータセットであるSciMDRを構築した。 実験により、SciMDRモデルは複数の科学的QAベンチマークで大幅に改善されていることが示された。
  論文  参考訳（メタデータ） (2026-03-12T17:57:52Z)
• Beyond Holistic Scores: Automatic Trait-Based Quality Scoring of Argumentative Essays [15.895792302323883]
  教育の文脈では、教師と学習者は解釈可能な特性レベルのフィードバックを必要とする。 本稿では,2つの相補的モデリングパラダイムを用いた特徴量に基づく自動弁別評価手法について検討する。 スコア・オーディナリティを明示的にモデル化することは、人間のレーダとの合意を著しく改善することを示します。
  論文  参考訳（メタデータ） (2026-02-04T14:30:52Z)
• RPC-Bench: A Fine-grained Benchmark for Research Paper Comprehension [65.81339691942757]
  RPC-Bench(RPC-Bench)は、高品質なコンピュータサイエンス論文のレビュー・リビューの交換から構築された大規模質問応答ベンチマークである。 我々は、科学研究の流れに沿ったきめ細かい分類を設計し、モデルがなぜ、何、どのように学術的な文脈で質問するかを理解し、答える能力を評価する。
  論文  参考訳（メタデータ） (2026-01-14T11:37:00Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• 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)
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。 MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
  論文  参考訳（メタデータ） (2024-10-28T11:37:39Z)

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

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