論文の概要: ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction
- arxiv url: http://arxiv.org/abs/2608.15979v1
- Date: Mon, 17 Aug 2026 00:14:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-18 19:59:03.493691
- Title: ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction
- Title（参考訳）: ALPS:数学的構成を伴う大規模言語モデルにおける妥当性創造性の測定
- Abstract要約: ALPS (Austin-Law Proof-Synthesis) は、有効な創造性を測定するためのタスクを設計するベンチマークである。
それぞれの例は単一の方程式法則であり、法則を満たす無限の数学的構造の構築を必要とするか、そのような構造が存在しないという証明を必要とする。
先行する自動プローバーの8つの構成のポートフォリオは、4,141の法則評価プールの2.2%を解決している。
- 参考スコア（独自算出の注目度）: 39.15744753769387
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models produce outputs presented as discoveries - new proofs, conjectures, or molecules. Whether such an output that appears creative is truly original and effective is hard to establish: open-ended outputs require subjective judgment, the output may replicate something seen in training, or the task may be too simple to need creativity. We present ALPS (Austin-Law Proof-Synthesis), a benchmark that designs a task to measure valid creativity: producing a solution that is original and can be proven correct. Each instance is a single equational law, certified to require either the construction of an infinite mathematical structure satisfying the law, or a proof that no such structure exists. Submissions are verified by automated proof checking with no human involvement, and a public generator produces new instances without limit, so LLMs are never evaluated on problems they may have seen. A portfolio of eight configurations of leading automated provers resolves 2.2% of the 4,141-law evaluation pool, and a twentyfold budget increase adds 0.6%: the obstacle is not compute, but the absence of any method that produces the tailored structure each law requires. Under a fixed protocol, the strongest reasoning model we test succeeds in 14% of instances on the proof side, but none on the construction side. The remaining 97.2% of the pool is unresolved at every configuration and budget we test. We release ALPS in full: the corpus, the generator, and the automated judge.
- Abstract（参考訳）: 大規模言語モデルは、新しい証明、予想、または分子として提示される出力を生成する。
オープンエンドのアウトプットは主観的な判断を必要とし、アウトプットはトレーニングで見られるものを再現するかもしれないし、タスクは創造性を必要とするにはあまりにも単純すぎるかもしれない。
提案するALPS(Austin-Law Proof-Synthesis)は,有効性を評価するためのタスクを設計するベンチマークである。
それぞれの例は単一の方程式法則であり、法則を満たす無限の数学的構造の構築を必要とするか、そのような構造が存在しないという証明を必要とする。
サブミッションは人間の関与なしに自動検証によって検証され、パブリックジェネレータは制限なく新しいインスタンスを生成するため、LCMは見た可能性のある問題に対して評価されることはない。
先行する自動プローバーの8つの構成のポートフォリオは、4,141の法則評価プールの2.2%を解決し、20倍の予算増は0.6%増となる。
固定されたプロトコルの下では、我々がテストする最も強い推論モデルは、証明側のインスタンスの14%で成功するが、建設側では成功しない。
残りの97.2%は、テストするすべての構成と予算で未解決です。
ALPSをフルにリリースします。コーパス、ジェネレータ、自動判断器です。
関連論文リスト
- A Machine-Verified Proof of a Quantum-Optimization Conjecture [0.0]
量子最適化における10年以上の課題を,マシンで検証した解決法について報告する。
大規模な言語モデルであるClaude Fable 5を用いて証明し,その正しさをエンドツーエンドで検証した。
この研究は、量子情報科学などにおけるオープンな予想を解決するための道を開いた。
論文 参考訳（メタデータ） (2026-06-29T01:25:40Z) - A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation [59.98516959731531]
抽象推論能力は、抽象ルールを抽出し適用するためのLLMの知性と能力を反映する。
既存のベンチマークは、高価な手作業のアノテーション、そのスケールの制限、あるいは真の推論ではなく暗記のリスク測定に頼っている。
我々はA2RBenchという名の自動パイプラインを導入し、生成、拡張、評価、分析を行う。
論文 参考訳（メタデータ） (2026-05-17T06:14:20Z) - Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。
多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。
自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
論文 参考訳（メタデータ） (2026-02-02T17:42:53Z) - APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。
エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。
この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
論文 参考訳（メタデータ） (2025-05-09T03:38:31Z) - Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。
訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。
トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
論文 参考訳（メタデータ） (2025-04-28T19:25:29Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。
我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。
本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
論文 参考訳（メタデータ） (2023-03-08T22:00:15Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳（メタデータ） (2021-06-02T17:58:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。