論文の概要: Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience

• arxiv url: http://arxiv.org/abs/2607.14818v1
• Date: Thu, 16 Jul 2026 10:37:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-17 17:01:33.07805
• Title: Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
• Title（参考訳）: LLMは紙からMaxSATソルバーを作れるか?
• Abstract要約: 我々は,大規模言語モデル (LLM) を用いて,研究論文からUnweighted MaxSATソルバを構築する経験について報告する。 このプロジェクトは、満足できないベースのMaxSATアルゴリズムに焦点を当て、紙の議論をChatGPTと組み合わせた反復的なワークフローに従う。 今後のLCM支援ソルバ開発における課題と教訓をまとめた。
• 参考スコア（独自算出の注目度）: 5.812499828391904
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We report on CoreForge, an experience in using large language models (LLMs) to build an unweighted MaxSAT solver from research papers rather than from an existing solver codebase. The project focuses on unsatisfiability-based MaxSAT algorithms and follows an iterative workflow that combines paper discussions with ChatGPT, implementation through Codex prompts, and repeated LLM-assisted code audits and revisions. Although the codebase implements several algorithms and solver components, our evaluation focuses on configurations that combine core-guided optimization, lightweight preprocessing, core minimization, integration with integer linear optimization backends, and a new core-sequence lookahead approach. Our experience suggests that LLMs can support solver implementation from papers, while requiring external validation, benchmarking, and human guidance. In our experiments, fuzzing and MaxSAT Evaluation instances did not reveal wrong answers in the tested configurations, although performance remains below the best hand-engineered MaxSAT solvers. We summarize what worked, what remained difficult, and the lessons for future LLM-assisted solver development.
• Abstract（参考訳）: CoreForgeは,大規模言語モデル(LLM)を使用して,既存の問題解決コードベースからではなく,研究論文からUnweighted MaxSATソルバを構築する経験である。 このプロジェクトは、満足できないベースのMaxSATアルゴリズムに焦点を当てており、紙の議論をChatGPTと組み合わせた反復ワークフロー、Codexプロンプトによる実装、LLM支援コード監査と修正を繰り返している。 コードベースにはいくつかのアルゴリズムとソルバコンポーネントが実装されているが、我々はコア誘導最適化、軽量プリプロセッシング、コア最小化、整数線形最適化バックエンドとの統合、新しいコアシーケンスルックアヘッドアプローチに重点を置いている。 我々の経験から LLM は外部の検証やベンチマーク,人的指導を必要としながら,論文からの解決者実装をサポートできることが示唆されている。 実験では, ファジィリングとMaxSAT評価のインスタンスは, テスト構成において間違った答えを示さなかったが, 性能は手作業で最高のMaxSATソルバ以下である。 今後のLCM支援ソルバ開発における課題と教訓をまとめた。

関連論文リスト

• Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability [19.16962344736341]
  大きな言語モデル(LLM)は、自然言語を理解するのに優れているが、ユーザ定義の好みを含む最適化タスクに苦労する。 本稿では,LLMがコード生成を通じて推論を外部化するハイブリッド推論手法を提案する。 この結果から,LLMによるコード生成と嗜好に基づくMaxSATが組み合わさることで,ソルバ検証の最適化が可能であることが示唆された。
  論文  参考訳（メタデータ） (2026-05-28T09:51:33Z)
• FrontierOR: Benchmarking LLMs' Capacity for Efficient Algorithm Design in Large-Scale Optimization [61.43300970020897]
  大規模言語モデル(LLM)は、最適化モデリングとソルバコード生成にますます使われている。 既存のベンチマークは、実際のスケールと複雑さよりもはるかに低い、小さな、あるいは単純化された例に限られている。 現実的な大規模最適化問題に対して,LLMに基づく効率的なアルゴリズム設計を評価するための最初のベンチマークとしてFrontierORを紹介した。
  論文  参考訳（メタデータ） (2026-05-24T20:10:42Z)
• Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers [52.23061619664667]
  大規模言語モデル(LLM)は直接推論によって複雑な問題を解くのに苦慮しているため、近年のニューロシンボリックシステムは、それを実行可能な解法を合成するためにますます利用している。 我々は,100の問題をベンチマークしたCP-SynC-XL(4,577インスタンス)を導入し,ネイティブアルゴリズム検索(Python),PythonソルバAPI(Python + OR-Tools)による制約モデリング,宣言的制約モデリングという3つのコンストラクションパラダイムを評価した。
  論文  参考訳（メタデータ） (2026-05-12T17:15:45Z)
• Execution-Verified Reinforcement Learning for Optimization Modeling [49.171122807323634]
  実行検証学習フレームワークは、数学的プログラミング解法を決定論的で対話的な検証器として扱う。 NL4OPT, MAMO, IndustryOR, OptiBenchをグロビ, OR-Tools, COPTで行った実験では, EVOMがプロセス管理SFTに適合または優れていた。
  論文  参考訳（メタデータ） (2026-04-01T03:39:11Z)
• Understanding the Challenges in Iterative Generative Optimization with LLMs [19.536425405805957]
  学習ループを設定するには、エンジニアが隠れた設計選択をしなければならない、と私たちは主張する。 本稿では,ほとんどの応用に影響を及ぼす3つの要因について検討する。 ドメイン間で学習ループを設定するためのシンプルで普遍的な方法がないことが、生産化と採用の大きなハードルである、と私たちは結論付けています。
  論文  参考訳（メタデータ） (2026-03-25T06:49:24Z)
• SolverLLM: Leveraging Test-Time Scaling for Optimization Problem via LLM-Guided Search [58.116954449750544]
  多様な最適化問題を解決するために,テスト時間スケーリングを活用したトレーニング不要のフレームワークを導入する。 直接的に解くのではなく、数学的定式化を生成し、新しいモンテカルロ木探索戦略によって導かれる解法対応のコードに変換する。
  論文  参考訳（メタデータ） (2025-10-19T16:21:19Z)
• On LLM-Assisted Generation of Smart Contracts from Business Processes [0.08192907805418582]
  大規模言語モデル(LLM)は、ソフトウェアの生成方法の現実を変えました。 本稿では、ビジネスプロセス記述からスマートコントラクトコードを生成するためのLCMの使用について探索的研究を行う。 以上の結果から,LLMの性能はスマートコントラクト開発に必要な信頼性に劣ることがわかった。
  論文  参考訳（メタデータ） (2025-07-30T20:39:45Z)
• Do LLMs Overthink Basic Math Reasoning? Benchmarking the Accuracy-Efficiency Tradeoff in Language Models [6.312798900093575]
  大規模言語モデル (LLM) は複雑な数学的ベンチマークでは優れた性能を得るが、基本的な数学的推論では失敗することがある。 本稿では,正確さと過度に考えることの基本的なトレードオフに焦点を当てる。 本研究は,総合モデル評価のための高精度とトークン効率を組み合わせた調和平均計量であるOverthinking Scoreを紹介する。
  論文  参考訳（メタデータ） (2025-07-05T12:31:17Z)
• AIME: AI System Optimization via Multiple LLM Evaluators [79.03422337674664]
  AIME は複数の LLM を利用した評価プロトコルであり、それぞれが独立した基準で評価を生成し、結合を通してそれらを結合する。 コード生成タスクにおける AIME のベースラインメソッドのパフォーマンスは,LeetCodeHard と HumanEval データセットの単一 LLM 評価プロトコルよりも最大 62% 高いエラー検出率,最大 16% 高い成功率で向上している。
  論文  参考訳（メタデータ） (2024-10-04T04:03:24Z)
• Code Simulation Challenges for Large Language Models [6.970495767499435]
  この研究は、LLM(Large Language Models)がいかにコーディングやアルゴリズムのタスクをシミュレートできるかを研究する。 我々は、直線プログラムのベンチマーク、クリティカルパスを含むコード、近似命令および冗長命令を導入する。 本稿では,コンパイラのパターンを行/フォローすることで,LLMにコード実行行をシミュレートするように指示する,OFFプロンプト手法であるChain of Simulation(CoSm)を提案する。
  論文  参考訳（メタデータ） (2024-01-17T09:23:59Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)

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

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