論文の概要: From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

• arxiv url: http://arxiv.org/abs/2605.15445v1
• Date: Thu, 14 May 2026 22:02:31 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-18 21:22:26.115838
• Title: From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
• Title（参考訳）: LLM生成概念からリーン形式化へ: 正方形証明による自動多項式不等式証明
• Authors: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang,
• Abstract要約: 本稿では,LLMの相補的強度と計算不等式証明のための記号計算を組み合わせた,ニューロシンボリックなフレームワークNSPIを提案する。 私たちはリーンの不平等をさらに証明し、発見からマシンチェックされた証明までエンドツーエンドのパイプラインを作ります。
• 参考スコア（独自算出の注目度）: 9.397847333441417
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search space hinder scalability. Purely symbolic approaches provide strong guarantees but often scale poorly as the number of variables or the degree increases, due to expensive algebraic manipulations and rapidly growing intermediate expressions. In parallel, LLM-guided methods have made notable progress, particularly on competition-style inequalities with a small number of variables. To address the remaining scalability challenges, we propose NSPI, a neuro-symbolic framework that combines the complementary strengths of LLMs and symbolic computation for polynomial-inequality proving. Concretely, an LLM proposes a conjecture in the form of an approximate polynomial Sum-Of-Squares (SOS) decomposition; we refine it via symbolic computation to obtain an exact polynomial SOS representation, which directly proves the target inequality, and we further certify the proof in Lean, yielding an end-to-end pipeline from heuristic discovery to machine-checked proof. Experiments on challenging benchmarks involving polynomials with up to 10 variables demonstrate the effectiveness and scalability of the proposed method.
• Abstract（参考訳）: 多項式の不等式の自動証明は、リッチ代数構造と急速に増加する証明検索空間がスケーラビリティを妨げるような、自動数学的推論の基本的な課題である。 純粋に象徴的なアプローチは強い保証を提供するが、高額な代数的操作と急速に増加する中間表現のため、変数の数や次数が増加するにつれて、しばしばスケールが低下する。 並行して、LSM誘導法は、特に少数の変数を持つ競合スタイルの不等式において顕著な進歩を遂げている。 そこで我々は,LLMの相補的強みと多項式不等式証明のための記号計算を組み合わせた,ニューロシンボリック・フレームワークNSPIを提案する。 具体的には、LLM は近似多項式 Sum-Of-Squares (SOS) 分解の形での予想を提案し、これを記号計算により洗練して、目的の不等式を直接証明する正確な多項式 SOS 表現を得る。 最大10変数の多項式を含む挑戦的ベンチマーク実験は,提案手法の有効性と拡張性を示す。

関連論文リスト

• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• Provable Benefit of Curriculum in Transformer Tree-Reasoning Post-Training [76.12556589212666]
  学習後のカリキュラムは指数関数的複雑性のボトルネックを回避していることを示す。 結果のみの報酬信号の下では、強化学習の微調整は、サンプルの複雑さを高い精度で達成する。 カリキュラムを意識したクエリにより、報奨託書の呼び出しとサンプリングコストの両方を指数関数的に削減するテストタイムスケーリングの保証を確立する。
  論文  参考訳（メタデータ） (2025-11-10T18:29:54Z)
• Automated Proof of Polynomial Inequalities via Reinforcement Learning [4.246350085706678]
  本稿では,強化学習に基づく不等式証明のためのKrivine-Basis表現の探索手法を提案する。 APPIRL(Reinforcementによる多項式不等式の自動証明)というツールも実装している。
  論文  参考訳（メタデータ） (2025-03-09T12:50:28Z)
• Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning [27.562284768743694]
  大規模言語モデル(LLM)は、証明システム内で証明ステップを生成することによって、数学的定理を正式に証明することができる。 本稿では,LLMが学習した数学的直観と,記号的手法によって符号化された領域固有の洞察を相乗化する,ニューロシンボリック・戦術生成器を提案する。 複数の数学コンペティションから161の挑戦的不等式を評価する。
  論文  参考訳（メタデータ） (2025-02-19T15:54:21Z)
• Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization [4.2518927441106]
  既存の手法の主なボトルネックは計算コストのかかる定量化器の除去ステップである。 テンプレートに基づく Skolemization 手法を提案し,線形/ポリノミカルな Skolem 関数を自動的に合成し,式中の量化子を除去する。 提案手法は, 高性能な実用性能と相まって, 魅力的な理論特性を提供する。
  論文  参考訳（メタデータ） (2024-12-18T14:37:15Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAPは、それらの算術的証明構造に関する仕様に従って、問題文と連鎖推論トレースを生成する。 MathGAP を用いて, LLM はより深く, より広くなるにつれて, 性能が著しく低下することがわかった。
  論文  参考訳（メタデータ） (2024-10-17T12:48:14Z)
• Deep Generative Symbolic Regression [83.04219479605801]
  記号回帰は、データから簡潔な閉形式数学的方程式を発見することを目的としている。 既存の手法は、探索から強化学習まで、入力変数の数に応じてスケールできない。 本稿では,我々のフレームワークであるDeep Generative Symbolic Regressionのインスタンス化を提案する。
  論文  参考訳（メタデータ） (2023-12-30T17:05:31Z)
• Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
  PAC-セマンティックスにおける暗黙学習を拡張し、線形算術の言語における間隔としきい値の不確実性を扱う。 最適線形プログラミング対象制約の学習に対する我々の暗黙的アプローチは、実際的な明示的アプローチよりも著しく優れていることを示す。
  論文  参考訳（メタデータ） (2020-10-23T19:08:46Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  本稿では,リアプノフ関数の自動合成法を提案する。 我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。 提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
  論文  参考訳（メタデータ） (2020-03-19T17:21:02Z)

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

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