Why Are Linear RNNs More Parallelizable?
이 논문은 선형 RNN(LRNN) 이 비선형 RNN 보다 병렬화가 용이한 이유를 복잡도 클래스 (Log-depth 회로 대 P-완전 문제) 와 오토마타 이론을 통해 이론적으로 규명하고, 다양한 LRNN 변형 간의 정밀한 표현력 차이를 분석하여 표현력과 병렬성 사이의 균형을 잡는 LLM 아키텍처 설계의 기초를 제공합니다.
💻 Category
cs.FL
28 편의 논문
2-Coloring Cycles in One Round
이 논문은 대형 언어 모델이 증명을 주도하고 Lean 4 로 형식화한 바와 같이, 1 라운드 랜덤화 분산 알고리즘을 사용하여 사이클을 2-색칠할 때 단색 간선의 기대 비율이 0.24118 미만임을 보이고, 동시에 이 비율이 0.23879 이상일 수 없음을 증명하여 기존 상한 및 하한을 개선했습니다.
Reachability in VASS Extended with Integer Counters
이 논문은 정수 카운터가 추가된 VASS(VASS+Z) 모델에서 N-카운터의 개수가 고정되었을 때 도달 가능성 문제의 복잡성을 분석하여, 1-카운터 경우 NP-완전임을 보이고 2-카운터 이상에서는 기존보다 개선된 상한을 제시함과 동시에 Z-카운터의 도입이 문제의 난이도를 높이는 핵심 요인임을 증명합니다.
Algebraic Characterization of Reversible First Degree Cellular Automata over
이 논문은 임의의 격자 크기와 상태 수를 가진 1 차 셀룰러 오토마타 (FDCA) 의 가역성을 상수 시간에 판별하고 모든 가역적 규칙을 생성할 수 있도록 하는 세 가지 필요충분 조건을 대수적으로 제시합니다.
Computational Complexity of Alignments
이 논문은 프로세스 마이닝의 정합성 검사 핵심 기법인 정렬 (alignment) 계산의 알고리즘적 복잡성을 다양한 페트리 넷 클래스에 대해 분석하여, 안전 페트리 넷과 워크플로우 넷에서는 PSPACE-완전임을 증명하고, 일부 하위 클래스에서는 NP-완전임을 보이며, 생동성과 안전성이 보장된 S-시스템에서만 다항 시간 해결이 가능함을 규명했습니다.
History-Deterministic Büchi Automata are Succinct
이 논문은 65 개의 상태로 구성된 히스토리 결정적 뵈치 오토마톤이 언어적으로 동등한 모든 결정적 뵈치 오토마톤보다 상태 수가 적음을 증명하여, 10 년 이상 열린 문제였던 히스토리 결정성의 간결성 문제를 해결했다고 요약할 수 있습니다.
Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
이 논문은 Uppaal 도구를 활용하여 분산 미들웨어 CARE 를 확률적 타이머 자동자 네트워크로 형식화하고, 이를 통해 검증 및 테스트를 수행함으로써 오픈소스 분산 애플리케이션의 신뢰성을 강화하는 방법론을 제시합니다.
SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification
이 논문은 기존 테스트 기반 평가의 한계를 극복하고 생성된 SQL 과 정답 SQL 의 동등성을 형식적 검증 엔진을 통해 엄격하게 검증하는 새로운 평가 파이프라인 'SpotIt'을 제안하며, 이를 통해 기존 평가 방식이 놓칠 수 있는 차이를 포착하고 Text-to-SQL 평가의 복잡성을 재조명합니다.