FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
이 논문은 대학원 수준을 넘어선 추상 대수학 문제를 포함하는 새로운 벤치마크 'FATE'를 제안하고, 최신 대형 언어 모델들이 수학 경시대회 대비 연구 수준의 형식적 추론에서 극심한 성능 격차와 형식화 과정에서의 한계를 드러냈음을 보고합니다.
💻 Category
cs.FL
28 편의 논문
Complexity of Linear Subsequences of -Automatic Sequences
이 논문은 -자동화 수열의 선형 부분열과 내부 수열의 복잡성 간의 관계를 규명하고, Zantema 와 Bosma 의 최근 질문을 해결하며, Büchi 산술을 기반으로 한 자동화 구성의 상태 및 실행 시간 복잡성을 분석합니다.
Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications
이 논문은 시맨틱 가이드드 합성 (SyGuS) 과 TSL논리를 활용하여 기존 부울 추상화의 한계를 넘어 데이터 변환과 시간적 명세를 동시에 학습하는 새로운 마이닝 기법을 제안하며, 이를 통해 OpenAI-Gymnasium 환경에서 기존 수동 학습 베이스라인보다 훨씬 강력한 성능과 샘플 효율성을 입증했습니다.
Randomise Alone, Reach as a Team
이 논문은 플레이어 간 공유된 무작위성이 없는 분산 무작위화 환경에서 협력하는 동시 그래프 게임의 임계값 및 거의 확실한 도달 문제를 연구하여 메모리 없는 전략의 충분성, 계산 복잡도 결과, 그리고 이를 위한 새로운 논리 IRATL 과 솔버를 제시합니다.
Forgetting Event Order in Higher-Dimensional Automata
이 논문은 고차원 오토마타 (HDA) 의 기존 모델이 가진 인위적인 사건 순서 의존성을 해결하기 위해, 사건 간 선행 관계와 동시성만 보존하는 '구간 ipomset'에 기반한 순서 무관 의미론을 제시하여 HDA 와 다른 동시성 모델 간의 정합성을 확보하고 범주론적 도구의 적용을 가능하게 함을 보여줍니다.
Turn Complexity of Context-free Languages, Pushdown Automata and One-Counter Automata
이 논문은 푸시다운 오토마타와 원-카운터 오토마타의 계산에서 스택 높이가 증가하는 단계에서 감소하는 단계로 전환되는 '턴(turn)'의 수에 대한 복잡성을 분석하여, 턴 수의 유한성 판정 불가능성, 다양한 턴 수 제한에 따른 비재귀적 트레이드오프, 그리고 입력 길이에 대한 부분 선형 함수로 정의된 무한한 계층 구조의 존재를 증명합니다.
Context-Free Trees
이 논문은 Muller 와 Schupp 가 제안한 맥락 자유 그래프의 하위 집합인 진정한 맥락 자유 트리 (bona fide context-free trees) 를 다항 상태 NFA 와 부분 DFA 로 표현 가능함을 보이고, 결정적 맥락 자유 트리의 동형 판별 문제가 루팅 및 비루팅 경우 모두 NL-완전임을 증명합니다.
New properties of the -representation of integers
이 논문은 Walnut 정리 증명 도구와 ChatGPT 5 를 활용하여 -표현의 새로운 성질을 증명하고, 특히 2012 년 Kimberling 의 추측을 해결했습니다.
The Generation-Recognition Asymmetry: Six Dimensions of a Fundamental Divide in Formal Language Theory
이 논문은 생성과 인식이 확장적으로 동등하지만 계산 복잡성, 모호성, 방향성, 정보 가용성, 문법 추론, 시간성 등 여섯 가지 차원에서 근본적인 비대칭성을 보이며, 특히 '생성은 쉽고 구문 분석은 어렵다'는 통념이 생성이 제약받지 않을 때만 성립함을 지적하고 이를 언어 모델의 맥락에서 재해석합니다.
The complexity of finite smooth words over binary alphabets
이 논문은 이진 알파벳을 사용하는 유한 매끄러운 단어 (f-smooth words) 의 복잡도가 로 성장한다는 싱 (Sing) 의 추측에 대한 진전을 이루었으며, 특히 짝수 알파벳의 경우 이를 증명하고 모든 이진 알파벳에 대해 하한을 증명하며 홀수 알파벳에 대한 상한을 개선했습니다.
Formally Verified Linear-Time Invertible Lexing
이 논문은 Stainless 검증기를 사용하여 구현된 ZipLex 프레임워크를 소개하며, 이는 정규식과 최장 일치 semantics 를 충족할 뿐만 아니라 토큰 시퀀스의 역변환 (invertibility) 을 보장하고 검증된 메모이제이션을 통해 Flex 방식의 2 차 시간 복잡도 문제를 해결하는 선형 시간 성능을 달성합니다.
Marking Data-Informativity and Data-Driven Supervisory Control of Discrete-Event Systems
이 논문은 이산 사건 시스템의 모델이 알려지지 않은 상황에서 주어진 사양을 만족하는 비차단 마킹 감독기를 설계하기 위한 조건인 '마킹 데이터 정보성' 개념을 제안하고, 이를 검증하는 알고리즘을 개발하며 데이터가 불충분할 경우를 위한 확장 개념과 알고리즘을 제시합니다.
Attention Meets Reachability: Structural Equivalence and Efficiency in Grammar-Constrained LLM Decoding
이 논문은 문법 제약 하의 LLM 디코딩에서 문법적 동치성이 허용된 다음 토큰 집합에는 영향을 주지 않지만, 컴파일된 상태 공간과 온라인 구조적 모호성 비용 (SAC) 에는 결정적인 차이를 만든다는 것을 증명하고, 이를 기반으로 효율적인 디코딩 엔진의 하한을 규명하며 Transformer 아키텍처와의 통합을 위한 이론적 틀을 제시합니다.
Warm Starting State-Space Models with Automata Learning
이 논문은 모어 기계와 상태 공간 모델 (SSM) 간의 정형적 대응 관계를 규명하고, 기호적 자동자 학습을 통해 SSM 을 초기화함으로써 복잡한 시스템 학습의 수렴 속도와 정확도를 획기적으로 개선하는 방법을 제시합니다.
Online Monitoring of Metric Temporal Logic using Sequential Networks
이 논문은 사이버 - 물리 시스템의 메트릭 시계 논리 (MTL) 명세로부터 이산 및 밀집 시간 행동을 위한 순차적 네트워크를 구축하는 통합 기법을 제안하여, 효율적이고 확장 가능한 온라인 모니터링 프레임워크를 제공하며 기존 접근법 대비 뛰어난 성능과 확장성을 입증합니다.
Module checking of pushdown multi-agent systems
이 논문은 푸시다운 다중 에이전트 시스템 (PMS) 의 모듈 체킹 문제를 연구하여 ATL 에 대해서는 2EXPTIME-완전임을, ATL* 에 대해서는 4EXPTIME-완전임을 증명함으로써 ATL* 의 경우 기존 모델 체킹보다 지수적으로 높은 복잡도를 가짐을 보여줍니다.
The Expansion Problem for Infinite Trees
이 논문은 무한 트리에 대한 램지 유사 정리를 연구하고 이를 트리의 대수적 확장 문제에 적용합니다.
Risk-Aware Autonomous Driving with Linear Temporal Logic Specifications
이 논문은 선형 시간 논리 (LTL) 명세에 위험 정도와 타이밍을 통합하여 인간과 유사한 위험 인식을 구현하고, 이를 선형 계획법 (LP) 문제로 변환해 충돌 위험과 교통 규칙 위반을 모두 고려한 자율 주행 제어 정책을 합성하는 방법을 제시합니다.
On a sequence of Kimberling and its relationship to the Tribonacci word
이 논문은 2017 년 클라크 킴벌링이 제안한 0 과 1 로 이루어진 수열에 대한 여러 추측을 Walnut 자동화 증명기를 활용하여 증명하고, 이 수열이 무한한 트리보나치 단어와 갖는 관계, 부분 단어 복잡도, 그리고 임계 지수를 규명합니다.
Classification of Local Optimization Problems in Directed Cycles
이 논문은 방향성 사이클에서의 국소 최적화 문제들에 대해 결정론적 및 확률적 LOCAL 모델에서의 계산 복잡성을 완전히 분류하고, 주어진 문제에 대한 복잡도 클래스를 자동으로 판별하며 점근적으로 최적의 분산 알고리즘을 효율적으로 생성하는 메타 알고리즘을 제시합니다.