論文の概要: Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
- arxiv url: http://arxiv.org/abs/2606.13925v1
- Date: Thu, 11 Jun 2026 21:33:50 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-15 16:00:42.657132
- Title: Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
- Title（参考訳）: Sorries is not the Hard Part: an Expert-Review Case Study of a Semi-Autonomous Formalization
- Authors: Vasily Ilin, Brian Nugent,
- Abstract要約: グロタンディークの消滅定理の半自己形式化について研究する。
最初のバージョンは、心配なくコンパイルされるが、専門家のレビューでは、定義、定理の一般性、ファイルの整理、APIに深刻な問題があることが判明した。
自己形式化は、閉じた悲しみだけでなく、結果の形式化が専門家のレビューに残るかどうかによって評価されるべきである。
- 参考スコア（独自算出の注目度）: 0.47745223151611654
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models can often close proof gaps in interactive theorem provers, but a verified theorem is not the same thing as a reusable library contribution. We study this distinction through a detailed case study: a semi-autonomous formalization of Grothendieck's vanishing theorem. The initial version compiles with no sorries, but an expert review found serious problems in definitions, theorem generality, file organization, and the API. We then ran a review-driven refactor and compression process and obtained a second expert review. The before-and-after comparison shows a sharp split: agents adapted well to local, mechanically checkable feedback, but remained weak at choosing definitions and designing APIs. We argue that autoformalization should be evaluated not only by closed sorries, but by whether the resulting formalization survives expert review.
- Abstract（参考訳）: 大規模言語モデルは、しばしばインタラクティブな定理プローバーの証明ギャップを閉じるが、検証された定理は再利用可能なライブラリの寄与と同じものではない。
この区別は、Grothendieckの消滅定理の半自明な形式化(英語版)という詳細なケーススタディを通して研究する。
最初のバージョンは、心配なくコンパイルされるが、専門家のレビューでは、定義、定理の一般性、ファイルの整理、APIに深刻な問題があることが判明した。
その後、レビュー駆動のリファクタリングと圧縮プロセスを実行し、2つ目の専門家レビューを取得しました。
エージェントはローカルで機械的にチェック可能なフィードバックに順応するが、定義の選択やAPIの設計には弱いままである。
自己形式化は、閉じた悲しみだけでなく、結果の形式化が専門家のレビューに残るかどうかによって評価されるべきである。
関連論文リスト
- TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics [6.168228844241134]
TheoremBenchは、コンテストの設定を超えて定理の証明者を評価するために設計されたLean4ベンチマークである。
このベンチマークは100近い古典的定理から構築され、2つの相補的な形式で解放される。
我々の実験は、明示的な前提がLean4対応の証明モデルの性能を大幅に改善していることを示している。
論文 参考訳（メタデータ） (2026-06-08T12:57:18Z) - Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
T は形式定理の意味的正しさを評価する枠組みである。
5つの実世界のLean 4リポジトリからベンチマークを構築します。
実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
論文 参考訳（メタデータ） (2026-04-26T13:24:20Z) - The Myhill-Nerode Theorem for Bounded Interaction: Canonical Abstractions via Agent-Bounded Indistinguishability [0.0]
有限状態コントローラの固定プローブ族は、観測履歴に擬似的に閉ループのワッサーシュタインを誘導し、家族内のコントローラが区別できないようなプローブ・エクサクタントなマージ履歴を誘導する。
時計を意識したプローブでは、エージェントの観察と行動にのみ依存する目的に対して、決定に十分である。
スケーラブルな決定論的定常実験は、小さな精度のケースで測定されたギャップで引き込み可能な粗大化を研究し、より大きなスケールで経験的に探索した。
論文 参考訳（メタデータ） (2026-03-22T20:59:31Z) - Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium [0.564046562677526]
本稿では、VML(Vlasov-Maxwell-Landau)システムにおける平衡特性の完全式化について述べる。
プロジェクトはAIによる数学的研究の完全なループを実証する。
論文 参考訳（メタデータ） (2026-03-16T21:21:53Z) - Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。
我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。
我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-13T01:33:20Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。