Proofs
[Paper Note] AdaBoost Does Not Always Cycle: A Computer-Assisted Counterexample, Erik Y. Wang, arXiv'26, 2026.04
Paper/Blog Link My Issue
#MachineLearning #AI-Human Co-Improvement Issue Date: 2026-04-11 GPT Summary- 全探索型 AdaBoostが有限のサイクルに収束するかという問題に対し、計算機支援で反例を構成。ブロック積ガジェットを用い、周期2の軌道を共有する因子が無理数的な支配的固有値を持つことで、最終的な周期性を排除。主張は有理数算術で証明され、GPT-5.4 ProとClaude Opus 4.6との共同開発によるもの。 Comment
元ポスト:
[Paper Note] On merge-models, Hector Buffière+, arXiv'26, 2026.03
Paper/Blog Link My Issue
#Analysis #MachineLearning #GraphBased Issue Date: 2026-04-05 GPT Summary- 木順序付けられた弱く疎なモデルの枠組みを拡張し、特にtwin-modelsの特性を探求。これにより、クリーク幅を保存できる性質を示し、二項関係を表現する新たなmerge-modelsを導入。merge-modelは定義されたマージ幅に基づいて構築されることから、その性質を明確にし、twin-modelsがmerge-modelsの特例であることを確認した。 Comment
元ポスト:
[Paper Note] Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification, Zenan Li+, arXiv'26, 2026.03
Paper/Blog Link My Issue
#LanguageModel #Coding #SoftwareEngineering #read-later #Verification #Author Thread-Post Issue Date: 2026-03-28 GPT Summary- 大規模言語モデル（LLMs）はコード生成が可能だが、正確性に限界がある。これを克服するために、Lean 4における階層的証明探索フレームワークを提案し、複雑な検証目標を単純なサブゴールに分解する。分解スコアは訓練報酬と推論時の基準として機能し、最適化とデプロイメントの整合性を保証。Goedel-Code-Prover-8Bを利用し、教師あり初期化後にハイブリッド強化学習で訓練。Leanベースのコード検証ベンチマークでは、62.0%の証明成功率を実現し、強力なベースラインを2.6倍上回る成果を達成した。また、推論時のスケーリングによって成功率の向上が観察された。 Comment
元ポスト:
解説:
[Paper Note] Aletheia tackles FirstProof autonomously, Tony Feng+, arXiv'26, 2026.02
Paper/Blog Link My Issue
#NLP #LanguageModel #AIAgents #Mathematics #ScientificDiscovery Issue Date: 2026-02-28 GPT Summary- 数理研究エージェントAletheiaは、Gemini 3 Deep Thinkを活用し、FirstProofチャレンジにおいて10問中6問を自動解決。問題8は専門家の合意が得られなかった。実験の詳細と評価、解釈についても明示し、生データは指定のリンクで入手可能。 Comment
元ポスト:
First Proof:
- [Paper Note] First Proof, Mohammed Abouzaid+, arXiv'26, 2026.02
[Paper Note] First Proof, Mohammed Abouzaid+, arXiv'26, 2026.02
Paper/Blog Link My Issue
#NLP #Dataset #LanguageModel #AIAgents #Evaluation #Mathematics #ScientificDiscovery #Selected Papers/Blogs Issue Date: 2026-02-16 GPT Summary- AIシステムの数学問題回答能力を評価するため、著者が作成した10の未公開の数学問題を共有。答案は著者に知られているが、短期間は非公開とする。 Comment
pj page: https://1stproof.org/
元ポスト:
ポイント解説:
自分たちの研究過程で生じた自分たちは答えを発見しているが世間には未発表な問題と暗号化された解答が公開されている。2月13日時点で鍵が公開されているようだ。果たしてどの程度AIは解答ができたのだろうか？
Google DeepmindのAlethiaは10個中6つの問題を解くことができたようである:
Alethia:
- [Paper Note] Accelerating Mathematical and Scientific Discovery with Gemini Deep Think, Google DeepMin, 2026.02
[Paper Note] Premise Selection for a Lean Hammer, Thomas Zhu+, ICLR'26, 2025.06
Paper/Blog Link My Issue
#MachineLearning #Mathematics Issue Date: 2026-02-05 GPT Summary- Lean向けの初のエンドツーエンドのドメイン一般ハンマー「LeanHammer」を提案。ユーザー固有のコンテキストに適応し、効率的な前提選択システムを導入。評価結果では、LeanHammerが既存の手法より21％多くの目標を解決し、さまざまなドメインでも良好な一般化を示す。形式的検証におけるニューラル検索とシンボリック推論の統合を図る。 Comment
pj page: https://cmu-l3.github.io/lean-hammer/
元ポスト:
Stress-Testing the Reasoning Competence of Language Models With Formal Proofs, Arkoudas+, EMNLP'25 Findings
Paper/Blog Link My Issue
#NLP #Dataset #LanguageModel #Evaluation #Reasoning #Mathematics Issue Date: 2025-11-12 GPT Summary- ProofGridという新しい論理推論タスクを用いて、LLMsとLRMsの性能を広範に評価。タスクは命題論理と方程式論理の証明作成・検証を含み、証明のインペインティングとギャップ埋めも新たに導入。実験ではトップモデルの優れたパフォーマンスが示される一方、体系的な失敗も確認。1万件以上の形式的推論問題と証明からなる新データリソースも公開。 Comment
元ポスト:
[Paper Note] Reliable Fine-Grained Evaluation of Natural Language Math Proofs, Wenjie Ma+, arXiv'25, 2025.10
Paper/Blog Link My Issue
#NLP #Dataset #LanguageModel #Evaluation #Mathematics #read-later #Selected Papers/Blogs Issue Date: 2025-10-18 GPT Summary- 大規模言語モデル（LLMs）による数学的証明の生成と検証における信頼性の高い評価者が不足している問題に対処するため、0から7のスケールで評価する新たな評価者ProofGraderを開発。ProofBenchという専門家注釈付きデータセットを用いて、評価者の設計空間を探求し、低い平均絶対誤差（MAE）0.926を達成。ProofGraderは、最良の選択タスクにおいても高いスコアを示し、下流の証明生成の進展に寄与する可能性を示唆している。 Comment
元ポスト:
これは非常に重要な研究に見える
QED-Nano: Teaching a Tiny Model to Prove Hard Theorems, LM Provers Team, 2026.02
Paper/Blog Link My Issue
#Article #NLP #LanguageModel #Supervised-FineTuning (SFT) #ReinforcementLearning #Blog #Mathematics #SmallModel #PostTraining #Rubric-based #Initial Impression Notes Issue Date: 2026-02-16 Comment
元ポスト:
ポイント解説:
早くもReasoning Cacheが利用されている:
- [Paper Note] Reasoning Cache: Continual Improvement Over Long Horizons via Short-Horizon RL, Ian Wu+, arXiv'26, 2026.02
4B級のモデルで特定タスクに特化したモデルを作りたい場合に非常に役立ちそうなレシピ
ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations, Gu+, 2025.10
Paper/Blog Link My Issue
#Article #NLP #LanguageModel #Mathematics #PostTraining #Simplification Issue Date: 2025-10-22 Comment
pj page: https://proof-optimizer.github.io
LLMの通常利用時の応答も（おそらくベンチマークに最適化されているせいで）長すぎると思っているけど、数学の証明も長いんだなあ、と感じた