Fugu-MT 論文翻訳(概要): A SAT-based Resolution of Lam's Problem

論文の概要: A SAT-based Resolution of Lam's Problem

arxiv url: http://arxiv.org/abs/2012.04715v1
Date: Tue, 8 Dec 2020 20:06:25 GMT
ステータス: 処理完了
システム内更新日: 2021-05-16 20:56:18.401382
Title: A SAT-based Resolution of Lam's Problem
Title（参考訳）: SATによるラム問題の解法
Authors: Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh
Abstract要約: 1989年、Lam, Thiel と Swiercz によるコンピュータサーチは、10個の独立した証明書が存在する場合、Lam の問題を実験的に解決した。 2011年の最初の検索と発見の両方で、そのようなカスタムな検証コードが見つからなかった。
参考スコア（独自算出の注目度）: 16.745129897429315
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: In 1989, computer searches by Lam, Thiel, and Swiercz experimentally resolved Lam's problem from projective geometry$\unicode{x2014}$the long-standing problem of determining if a projective plane of order ten exists. Both the original search and an independent verification in 2011 discovered no such projective plane. However, these searches were each performed using highly specialized custom-written code and did not produce nonexistence certificates. In this paper, we resolve Lam's problem by translating the problem into Boolean logic and use satisfiability (SAT) solvers to produce nonexistence certificates that can be verified by a third party. Our work uncovered consistency issues in both previous searches$\unicode{x2014}$highlighting the difficulty of relying on special-purpose search code for nonexistence results.
Abstract（参考訳）: 1989年、lam、thiel、swiierczによるコンピュータによる探索により、10階の射影平面が存在するかどうかを判定する長年の問題である射影幾何学$\unicode{x2014} からラムの問題を実験的に解いた。 2011年のオリジナル検索と独立検証の両方でそのような射影平面は見つからなかった。しかし、これらの検索はそれぞれ高度に専門化されたカスタムコードを使用して行われ、存在しない証明書は生成されなかった。本稿では,問題をブール論理に翻訳し,SAT(SAT)ソルバを用いて第三者が検証可能な非存在証明を生成することにより,Lamの問題を解決する。我々の研究は、両方の検索で一貫性の問題を発見した。$\unicode{x2014}$highlighting the difficulty of relying special-purpose search code for nonistence results。

関連論文リスト

Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects [1.6727186769396274]
満足度に基づく自動推論は、ソフトウェア工学において複雑なソフトウェアを検証するのに成功している。我々は、FOL*不満足な結果の正しさを検証するという課題に取り組む。我々は,不満足の原因を説明するために,証明に基づく診断法を開発した。
論文参考訳（メタデータ） (2024-09-13T22:25:58Z)
Solving for X and Beyond: Can Large Language Models Solve Complex Math Problems with More-Than-Two Unknowns? [57.80779199039929]
大規模言語モデル (LLM) は数学問題の解法において顕著な性能を示した。本稿では,複数の未知の問題を組み込むことで,これらの制約に対処する新しいベンチマークであるBeyondXを紹介する。 BeyondXに関する実証的な研究によると、数学のタスクに特化して調整された既存のLLMの性能は、未知の数が増えるにつれて著しく低下する。
論文参考訳（メタデータ） (2024-07-06T17:01:04Z)
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)
Extending the Frontier of ChatGPT: Code Generation and Debugging [0.0]
OpenAIが開発したChatGPTは,さまざまな問題領域に取り組むために人工知能(AI)を活用することによって,新たな時代を迎えている。本稿では,ChatGPTのプログラミング問題に対する有効性について検討し,時間とメモリの複雑さの観点から,その解の正しさと効率性について検討する。この研究は、ChatGPTが正しいソリューションを提供することができた問題の割合を示すため、総成功率は71.875%であることを示した。
論文参考訳（メタデータ） (2023-07-17T06:06:58Z)
Explaining SAT Solving Using Causal Reasoning [30.469229388827443]
本稿では、因果推論を用いて、現代のSATソルバの機能に関する洞察を得るCausalSATを紹介する。われわれはCausalSATを用いて,これまで「親指のルール」や経験的発見と考えられていた仮説を定量的に検証した。
論文参考訳（メタデータ） (2023-06-09T22:53:16Z)
An Exploratory Study on the Evidence of Hackathons' Role in Solving OSS Newcomers' Challenges [54.56931759953522]
我々はOSSプロジェクトに参加する際、新参者が直面する課題を理解し、議論することを目指している。これらの課題にどのようにハッカソンが使われたかを示す証拠を収集する。
論文参考訳（メタデータ） (2023-05-16T15:40:19Z)
Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。 ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
論文参考訳（メタデータ） (2022-03-02T05:14:12Z)
Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
本稿では,最小長の制約付き混合被覆アレイを構築するためのSAT(Satifiability)に基づくアプローチを提案する。この問題はシステム障害検出のためのコンビネータテストの中心である。
論文参考訳（メタデータ） (2021-05-26T14:00:56Z)
Addressing the Multiplicity of Solutions in Optical Lens Design as a Niching Evolutionary Algorithms Computational Challenge [0.0]
本研究は,Niching-CMA-ESを用いて,シミュレーションに基づく設計問題に対処する。 1回のランで21個のミニマのうち19個が検出された。ニッチ機構はこの問題領域に対処するのに適しており、達成された新しい解によって形成される見かけの多次元構造を仮定する。
論文参考訳（メタデータ） (2021-05-21T19:10:54Z)
AdaVQA: Overcoming Language Priors with Adapted Margin Cosine Loss [73.65872901950135]
本研究は,特徴空間学習の観点から,言語先行問題に挑戦する試みである。適応したマージンコサイン損失は、頻繁でスパースな回答特徴空間を区別するように設計されている。実験の結果, 適応したマージンコサイン損失はベースラインモデルを大きく向上できることがわかった。
論文参考訳（メタデータ） (2021-05-05T11:41:38Z)
If beam search is the answer, what was the question? [78.71330480725668]
ビームサーチは、認知科学に動機づけられた特性であるテキストの均一な情報密度を強制する。この特性を明示的に強制する復号対象のセットを提案し、これらの目的による正確な復号化は、校正の不十分な言語生成モデルの復号時に発生する問題を緩和する。
論文参考訳（メタデータ） (2020-10-06T11:57:03Z)

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