最新の論文記事を読みやすく整理。保存・タグ検索に加え、Plus/Proでは研究ノートと知識グラフで理解を積み上げられます。
Cog AI Archive
大規模言語モデル（LLM）は、計算機科学の難問である「停止問題」の予測において、専門的な検証ツールに匹敵する極めて高い性能を示した。特にGPT-5やClaude Sonnet-4.5は、国際的なソフトウェア検証コンペティション（SV-Comp 2025）のトップクラスのツールに次ぐスコアを記録し、その推論能力の高さが証明された。 一方で、プログラムが終了しないことの数学的な証明となる「証拠（ウィットネス）」の生成には依然として課題があり、コードの長さや複雑さが増すにつれて予測精度が低下する傾向も確認された。 信頼性を高めるために導入された「テストタイム・スケーリング（TTS）」による合意形成アルゴリズムは、モデルの不確実性を適切に管理し、誤判定によるペナルティを回避してスコアを劇的に向上させる有効な手段であることが明らかになった。
現代の深層学習ワークロードのスケールアップに伴い、デバイスメッシュやメモリ階層、異種アクセラレータ間でのデータと計算の調整が不可欠となっていますが、本論文は論理的なテンソル座標を「名前付き軸」を介して多軸物理空間にマッピングする、ハードウェアを意識した抽象化「Axe Layout」を提案しています。
Magellanは、大規模言語モデル（LLM）と進化的探索、自動チューニングを組み合わせることで、コンパイラの最適化パスを制御するC++の意思決定ロジックを自律的に生成するエージェント型フレームワークである。 LLVMの関数インライニングにおいて、数十年にわたる手動エンジニアリングを凌駕する5.
現代のコンパイラが依存する手動設計のヒューリスティクスは、複雑なソフトウェアや多様なハードウェアへの適応が困難で保守負担も大きいという課題がありますが、本研究ではLLMと進化探索、自動チューニングを組み合わせたエージェント型フレームワーク「Magellan」を提案し、実行可能なC++の決定ロジックを直接合成することでこの問題を解決します。 LLVMの関数インライニングにおいて、Magellanは数十年にわたる専門家の手動設計を上回る新しいヒューリスティクスを合成し、バイナリサイズの削減率で5.23%の向上を達成したほか、生成されたコードは手動実装の約15分の1という極めて簡潔な記述でありながら、既存のコンパイラに直接統合して運用できる高い実用性を備えていることが確認されました。 この手法はレジスタ割り当てやXLAなどの異なる最適化タスクやコンパイラ基盤にも適用可能であり、特定のベンチマークへの過学習を避けつつ、時間の経過や異なるアプリケーション領域に対しても高い汎用性を示すことが実証されており、ニューラルネットワークを直接コンパイラに組み込む手法に代わる、保守性と性能を両立した新しい自動設計の道を切り拓いています。
自然言語の問題記述を数理最適化モデルへ変換する際、独自のコンパイラ「PyOPL」からの詳細な診断フィードバックをループに組み込み、AIが自己修正を行うエンドツーエンドのシステム「SyntAGM」を開発した。
EvolVEは、大規模言語モデル（LLM）を活用してハードウェア記述言語であるVerilogのコード生成と最適化を自動化する、進化的探索アルゴリズムに基づいた革新的なフレームワークである。 機能的正当性を最大化するモンテカルロ木探索（MCTS）と、設計の最適化に特化したアイデア主導型洗練（IGR）という二つの異なる戦略を使い分け、さらに検証プロセスを高速化する構造化テストベンチ生成（STG）を導入している。 評価の結果、既存のベンチマークで世界最高水準の正解率を達成しただけでなく、産業規模の課題を含むIC-RTLベンチマークにおいて、人間による設計を大幅に上回る電力・性能・面積（PPA）の削減に成功した。
ソフトウェアの信頼性を数学的に保証するプログラム検証において、最大の難所である「検証条件（VC）」の自動証明を解決するため、機械学習を用いたニューラル定理証明（NTP）を実世界の複雑なコードに適用する初のベンチマーク「NTP4VC」を構築した。
本研究は、計算機科学の根幹的な未解決問題である「停止問題」に対し、GPT-5やClaude Sonnet-4.5といった最新の大規模言語モデル（LLM）が、国際ソフトウェア検証コンペティション（SV-Comp）2025の基準で専門ツールに匹敵する予測能力を持つことを実証した。
Axeは、論理的なテンソル座標をデバイス、メモリ、スレッドなどのハードウェア軸にマッピングする、ハードウェアを意識した新しい抽象化手法である。 この手法は、デバイス間のデータ分散（シャーディング、複製）とデバイス内のメモリレイアウト（タイリング、オフセット）を単一の形式で統一し、一貫した記述を可能にする。