論文の概要: 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:数学的構成を伴う大規模言語モデルにおける妥当性創造性の測定
• Authors: Eric Xie, Wenqian Ye, Aidong Zhang,
• 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をフルにリリースします。コーパス、ジェネレータ、自動判断器です。

関連論文リスト

• A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation [59.98516959731531]
  抽象推論能力は、抽象ルールを抽出し適用するためのLLMの知性と能力を反映する。 既存のベンチマークは、高価な手作業のアノテーション、そのスケールの制限、あるいは真の推論ではなく暗記のリスク測定に頼っている。 我々はA2RBenchという名の自動パイプラインを導入し、生成、拡張、評価、分析を行う。
  論文  参考訳（メタデータ） (2026-05-17T06:14:20Z)
• 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)
• 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)

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

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