論文の概要: h1: A Taste of the Bitter Lesson in Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2610.35962v1
• Date: Sun, 25 Oct 2026 11:07:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-28 21:04:31.37364
• Title: h1: A Taste of the Bitter Lesson in Automated Theorem Proving
• Title（参考訳）: h1: 自動定理証明におけるビターレッスンの味覚
• Abstract要約: h1は単純なハーネスで、モデルにLean 4.0への効率的なインターフェースを提供する。 ひとつの試み(pass@1)が、オープンな問題を解決するためにスケールできることがよく示されます。
• 参考スコア（独自算出の注目度）: 13.45095779297246
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While progress in informal mathematics has come largely from scaling the chain-of-thought and agentic reasoning of frontier language models, formal theorem proving has increasingly relied on human-designed workflows around these models, such as planning, decomposition, and orchestrating specialized provers. This raises a bitter-lesson question: can a simple agentic loop that scales test-time compute match these workflows? The answer matters as formal verification must scale to keep up with frontier models producing research mathematics, yet new workflows rarely settle it, as their gains are often confounded with stronger models or more compute. We study this question with h1, a simple harness that gives a model an efficient interface to Lean 4 and keeps it working through verifier feedback and self-reflection, without imposing a decomposition or search structure. h1 reaches state-of-the-art results on PutnamBench, FATE-X, and FormalConjectures100-Solved, settles eight open problems in FormalConjectures, and, at matched models, matches or outperforms specialized workflows such as Goedel-Architect and AlphaProof Nexus, surprisingly showing that a single attempt (pass@1) can often scale to solve open problems. Through ablations and matched-model comparisons with Claude Code and AxProverBase, we find that simplicity alone is not enough: an efficient Lean interface largely determines cost and solve rate. We thus recommend that future work evaluate frontier models with efficient execution feedback before prescribing workflows, at the risk of bitter lessons.
• Abstract（参考訳）: フォーマルな数学の進歩は、主にフロンティア言語モデルのチェーン・オブ・シンキングとエージェント的推論のスケールから来ているが、フォーマルな定理証明は、計画、分解、特殊プローバーのオーケストレーションなど、これらのモデルを取り巻く人間設計のワークフローにますます依存している。 単純なエージェントループは、これらのワークフローに一致するテスト時間計算をスケールできますか? この答えは、研究数学を生み出すフロンティアモデルに追いつくために形式的検証をスケールしなければならないが、より強力なモデルやより多くの計算で得られるため、新しいワークフローが解決されることは滅多にない。 私たちはこの質問を、モデルにLean 4への効率的なインターフェースを与えるシンプルなハーネスであるh1を使って研究し、検証者からのフィードバックと自己回帰を通じて、分解や検索構造を課すことなく、モデルを動作させ続けます。 18.h1はPutnamBench、FATE-X、FormalConjectures100-Solvedの最先端の結果に達し、FormalConjecturesの8つのオープンな問題を解決し、マッチしたモデルではGoedel-ArchitectやAlphaProof Nexusのような特別なワークフローにマッチしたり、性能が良くなった。 Claude CodeやAxProverBaseとマッチしたモデルの比較を通じて、シンプルさだけでは十分ではないことが分かりました。 したがって、ワークフローを規定する前に効率的な実行フィードバックでフロンティアモデルを評価し、苦しい教訓のリスクを負うことを推奨する。

関連論文リスト

• HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs [32.234133057592935]
  Hermesはツール支援エージェントで、リーンシステムにおける検証段階と非公式な推論をインターリーブする。 パラメータスケールの異なる LLM を用いて,Hermes を4つの挑戦的数学的推論ベンチマークで評価する。
  論文  参考訳（メタデータ） (2025-11-24T04:50:18Z)
• Code-driven Number Sequence Calculation: Enhancing the inductive Reasoning Abilities of Large Language Models [44.17697803306198]
  textitCodeSeqは,数列から構築した合成後トレーニングデータセットである。 パイプラインは、失敗したテストケースを反映し、反復的な修正を取り入れることで、教師付き微妙なデータを生成する。 実験の結果,textitCodeSeqでトレーニングしたモデルでは,様々な推論タスクが改善され,OOD性能が保たれることがわかった。
  論文  参考訳（メタデータ） (2025-10-16T12:29:40Z)
• Bridging Formal Language with Chain-of-Thought Reasoning to Geometry Problem Solving [9.550050299909184]
  我々はChain-of-Thought(CoT)とフォーマル言語を統合する新しいアプローチを提案する。 このモデルは、ソルバ実行可能コードの漸進的な排出を伴う自然言語推論をインターリーブする。 Qwen2.5-VL-7Bに基づいて構築された新しいモデルGF-Reasonerは、標準GPSベンチマークで最大15%の精度向上を実現している。
  論文  参考訳（メタデータ） (2025-08-12T17:26:23Z)
• Frontier LLMs Still Struggle with Simple Reasoning Tasks [53.497499123166804]
  この研究は、フロンティア言語モデルの性能を、幅広い「容易」推論問題に対して研究する。 計算,一階述語論理,証明木,旅行計画など,手続き的に生成された単純な推論タスクのスイートを作成します。 最先端の思考モデルでさえ、このような問題や同様の理由で一貫して失敗することを示します。
  論文  参考訳（メタデータ） (2025-07-09T22:22:49Z)
• Model Utility Law: Evaluating LLMs beyond Performance through Mechanism Interpretable Metric [99.56567010306807]
  大規模言語モデル(LLM)は、学術、産業、そして日々のアプリケーションに欠かせないものになっている。 大規模言語モデル (LLM) 時代における評価の課題の1つは一般化問題である。 従来の性能スコアを補完するメカニズムの解釈可能性向上指標であるモデル利用指数(MUI)を提案する。
  論文  参考訳（メタデータ） (2025-04-10T04:09:47Z)
• Universality of the $π^2/6$ Pathway in Avoiding Model Collapse [0.0]
  π-2乗オーバ6の増大リスクの普遍性は、正準統計モデルの大群にまたがることを示した。 さまざまな拡張プロセスに対応可能なフレームワークを提供しています。
  論文  参考訳（メタデータ） (2024-10-30T08:44:10Z)
• A Comparative Study on Reasoning Patterns of OpenAI's o1 Model [69.08287909042421]
  OpenAIのo1モデルは、ほとんどのデータセットで最高のパフォーマンスを実現しています。 また、いくつかの推論ベンチマークについて詳細な分析を行う。
  論文  参考訳（メタデータ） (2024-10-17T15:09:03Z)
• LoRanPAC: Low-rank Random Features and Pre-trained Models for Bridging Theory and Practice in Continual Learning [103.45785408116146]
  連続学習(CL)は、連続的に提示される複数のタスクを解決できるモデルを訓練することを目的としている。 最近のCLアプローチは、ダウンストリームタスクをうまく一般化する大規模な事前学習モデルを活用することで、強力なパフォーマンスを実現している。 しかし、これらの手法には理論的保証がなく、予期せぬ失敗をしがちである。 理論的に健全で高性能な単純なCL法を設計することで,このギャップを埋めることを目指している。
  論文  参考訳（メタデータ） (2024-10-01T12:58:37Z)
• Understanding prompt engineering may not require rethinking generalization [56.38207873589642]
  言語モデルによって与えられるPAC-Bayesと組み合わさったプロンプトの離散的性質は、文献の標準によって非常に厳密な一般化境界をもたらすことを示す。 この研究は、プロンプトエンジニアリングの広範な実践を正当化する可能性がある。
  論文  参考訳（メタデータ） (2023-10-06T00:52:48Z)

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

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