論文の概要: Solving Hard Mizar Problems with Instantiation and Strategy Invention
- arxiv url: http://arxiv.org/abs/2406.17762v1
- Date: Tue, 25 Jun 2024 17:47:13 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-26 13:21:40.365039
- Title: Solving Hard Mizar Problems with Instantiation and Strategy Invention
- Title（参考訳）: InstantiationとStrategy Inventionによる難問の解決
- Authors: Jan Jakubův, Mikoláš Janota, Josef Urban,
- Abstract要約: 複数のATP法とAI法を用いて,これまでATP未承認であったMizar/MPTP問題の3000以上を証明した。
この方法では、これまで未解決だった14163のハード・ミザー問題の3021(21.3%)が解決された。
- 参考スコア（独自算出の注目度）: 2.048226951354646
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75\% to above 80\%. First, we start to experiment with the cvc5 SMT solver which uses several instantiation-based heuristics that differ from the superposition-based systems, that were previously applied to Mizar,and add many new solutions. Then we use automated strategy invention to develop cvc5 strategies that largely improve cvc5's performance on the hard problems. In particular, the best invented strategy solves over 14\% more problems than the best previously available cvc5 strategy. We also show that different clausification methods have a high impact on such instantiation-based methods, again producing many new solutions. In total, the methods solve 3021 (21.3\%) of the 14163 previously unsolved hard Mizar problems. This is a new milestone over the Mizar large-theory benchmark and a large strengthening of the hammer methods for Mizar.
- Abstract（参考訳）: 本研究では, ATP未承認ミザー/MPTP問題の3000以上をいくつかのATP法とAI法を用いて証明し, ATP未解決ミザー問題を75倍から80倍に増やした。
まず,従来Mizarに応用されていた重ね合わせ型システムとは異なるいくつかのインスタンス化ベースのヒューリスティックを用いて,cvc5 SMTソルバを実験し,多くの新しい解を加えた。
次に、自動戦略発明を用いて、難題におけるcvc5の性能を大幅に向上させるcvc5戦略を開発する。
特に、最も優れた発明された戦略は、これまで利用可能な最も優れたcvc5戦略よりも14\%以上の問題を解決している。
また,様々なクラリファイション手法が,このようなインスタンス化に基づく手法に高い影響を与え,多くの新しい解がもたらされることを示す。
この手法は、これまで未解決だった14163のハード・ミザー問題の3021(21.3\%)を解いた。
これはMizarの大規模理論ベンチマークに対する新たなマイルストーンであり、Mizarのハンマーメソッドの大幅な強化である。
関連論文リスト
- Navigating the Labyrinth: Evaluating and Enhancing LLMs' Ability to Reason About Search Problems [59.72548591120689]
我々は,11種類の検索問題を含む新しいベンチマークであるSearchBenchを紹介する。
もっとも先進的なLCMでさえ、これらの問題をエンドツーエンドのテキストで解決することができないことを示す。
LLMにその問題を解決するコードを生成するように指示することは助けになるが、GPT4のパフォーマンスは11.7%向上した。
論文 参考訳（メタデータ） (2024-06-18T00:44:58Z) - MindStar: Enhancing Math Reasoning in Pre-trained LLMs at Inference Time [51.5039731721706]
MindStarは、大言語モデルの純粋に推論に基づく探索手法である。
推論タスクを探索問題として定式化し、最適な推論経路を特定するための2つの探索アイデアを提案する。
Llama-2-13BやMistral-7Bのようなオープンソースモデルの推論能力を大幅に向上させ、GPT-3.5やGrok-1に匹敵する性能を実現している。
論文 参考訳（メタデータ） (2024-05-25T15:07:33Z) - MToP: A MATLAB Optimization Platform for Evolutionary Multitasking [8.51038268410035]
進化的マルチタスク(EMT)のためのMTO-Platform(MTOP)という,オープンソースの初の最適化プラットフォームを紹介する。
MToPには40以上のMTEA、150以上のMTO問題、10以上のパフォーマンスメトリクスが含まれている。
MToPはユーザフレンドリーなグラフィカルインターフェースを備えており、結果分析、データエクスポート、スキーマの可視化を容易にする。
論文 参考訳（メタデータ） (2023-12-13T13:36:14Z) - Monte-Carlo Tree Search for Multi-Agent Pathfinding: Preliminary Results [60.4817465598352]
マルチエージェントパスフィンディングに適したモンテカルロ木探索(MCTS)のオリジナル版を紹介する。
具体的には,エージェントの目標達成行動を支援するために,個別の経路を用いる。
また,木探索手順の分岐係数を低減するために,専用の分解手法を用いる。
論文 参考訳（メタデータ） (2023-07-25T12:33:53Z) - Multi-Method Self-Training: Improving Code Generation With Text, And
Vice Versa [0.0]
本稿では,Multi-Method Self-Training (MMST)を導入し,あるメソッドを他のメソッドのフィルタ出力でトレーニングする。
MMSTは,1) 性能の低い手法(最大30%) を改良し,2) より性能のよい手法(最大32.2%) を改良し,3) 関連性のあるタスク(最大10.3%) を改善できることを示す。
論文 参考訳（メタデータ） (2023-07-20T06:58:55Z) - MizAR 60 for Mizar 50 [3.2322198481646867]
ハンマー設定でミザール定理の約60%を自動証明するAI/TPシステムを開発した。
また、自動プローバーが人間の記述したMizar証明で用いられる前提のみを使用することで助けられる場合、自動的なMizar定理の75%を自動で証明する。
論文 参考訳（メタデータ） (2023-03-12T15:13:05Z) - Learning to Optimize Permutation Flow Shop Scheduling via Graph-based
Imitation Learning [70.65666982566655]
置換フローショップスケジューリング(PFSS)は製造業で広く使われている。
我々は,より安定かつ正確に収束を加速する専門家主導の模倣学習を通じてモデルを訓練することを提案する。
我々のモデルのネットワークパラメータはわずか37%に減少し、エキスパートソリューションに対する我々のモデルの解のギャップは平均6.8%から1.3%に減少する。
論文 参考訳（メタデータ） (2022-10-31T09:46:26Z) - One model Packs Thousands of Items with Recurrent Conditional Query
Learning [8.821298331302563]
本稿では,2次元および3次元のパッキング問題を解決するためにRCQL法を提案する。
RCQLは、オフラインの2D 40-boxケースでは平均ビンギャップ比を1.83%削減し、3Dケースでは7.84%削減する。
論文 参考訳（メタデータ） (2021-11-12T14:00:30Z) - Ranking Cost: Building An Efficient and Scalable Circuit Routing Planner
with Evolution-Based Optimization [49.207538634692916]
そこで我々は、効率よくトレーニング可能なルータを形成するための新しい回路ルーティングアルゴリズム、Randing Costを提案する。
提案手法では,A*ルータが適切な経路を見つけるのに役立つコストマップと呼ばれる新しい変数群を導入する。
我々のアルゴリズムはエンドツーエンドで訓練されており、人工データや人間の実演は一切使用しない。
論文 参考訳（メタデータ） (2021-10-08T07:22:45Z) - Efficient Active Search for Combinatorial Optimization Problems [1.6543719822033436]
能動探索により、学習したモデルが、トレーニング中に見られたものよりもはるかに大きいインスタンスを効果的に解決できることが示される。
提案手法は、与えられたモデルの探索性能を大幅に向上する簡単な方法を提供し、ルーティング問題に対する最先端の機械学習手法より優れている。
論文 参考訳（メタデータ） (2021-06-09T15:08:03Z) - GACEM: Generalized Autoregressive Cross Entropy Method for Multi-Modal
Black Box Constraint Satisfaction [69.94831587339539]
本稿では,マスク付き自己回帰ニューラルネットワークを用いて解空間上の均一分布をモデル化するクロスエントロピー法(CEM)を提案する。
我々のアルゴリズムは複雑な解空間を表現でき、様々な異なる解領域を追跡できる。
論文 参考訳（メタデータ） (2020-02-17T20:21:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。