Commutativity and Kleisli laws of codensity monads of probability measures
이 논문은 확률 측도의 코디던스 (codensity) 단위를 통해 Giry 단위와의 클라이슬리 (Kleisli) 법칙 존재성, 마르코프 범주와 관련된 라크 단조성 및 아핀성 조건, 그리고 데이 컨볼루션을 통한 텐서곱의 특징화 등 확률 단위의 세 가지 핵심 성질을 체계적으로 분석하고 증명합니다.
💻 Category
cs.LO
64 편의 논문
Dependent Directed Wiring Diagrams for Composing Instantaneous Systems
이 논문은 입력에 따라 출력이 즉시 결정되는 시스템 (Mealy 머신) 과 보조 변수가 입력에 의해 매개변수화되는 재고 및 흐름 다이어그램을 구성하기 위해 종속 방향 와이어링 다이어그램의 연산자와 그 대수를 도입하고, 이를 Mealy 머신으로 해석하는 의미론을 제시합니다.
A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
본 논문은 정적 분석과 LLM 기반 추론을 결합한 모듈형 프레임워크인 Preguss 를 통해 대규모 프로그램의 잠재적 런타임 오류를 기반으로 인터프로시저 명세를 자동 생성 및 정제함으로써, 기존 LLM 기반 접근법보다 우수한 확장성을 보이며 수천 줄 규모의 프로그램에 대한 검증 노력을 80.6%~88.9% 감소시킨다고 제안합니다.
Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits
이 논문은 양자 위상 추정 (QPE) 회로의 기능적 정확성을 보장하기 위해 양자 현상을 비트 벡터 논리로 추상화하는 확장 가능한 형식 검증 방법론을 제시하며, 이를 통해 1,024 개의 위상 큐비트를 포함하는 대규모 회로를 제한된 메모리 내에서 성공적으로 검증할 수 있음을 보여줍니다.
A Simple Constructive Bound on Circuit Size Change Under Truth Table Perturbation
이 논문은 최소 회로 크기 문제의 암시적 관찰을 명시적으로 정립하여 진리표의 한 점 변경 시 최적 회로 크기가 이내로만 변함을 증명하고, 이를 일반화하며 에서의 AIG 기반 실험을 통해 이 상한이 최적임을 확인했습니다.
Declarative Scenario-based Testing with RoadLogic
이 논문은 자율주행차의 시나리오 기반 테스트를 위해 선언적 OpenSCENARIO 명세를 실행 가능한 시뮬레이션으로 자동 변환하는 오픈소스 도구 'RoadLogic'을 제안하고, 이를 통해 명세 준수성과 다양한 행동 변형을 효율적으로 검증할 수 있음을 입증합니다.
d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries
이 논문은 SMT(Satisfiability Modulo Theories) 문제를 부울 논리 문제로 변환하여 d-DNNF(결정적 분해 부정 정규형) 컴파일을 통해 오프라인에서 계산 비용을 치르고 온라인에서 다항 시간 내에 다양한 SMT 쿼리를 효율적으로 처리할 수 있는 새로운 일반 프레임워크를 제안합니다.
BemaGANv2: Discriminator Combination Strategies for GAN-based Vocoders in Long-Term Audio Generation
이 논문은 AMP 모듈과 Multi-Envelope Discriminator(MED) 를 도입하여 장기간 오디오 생성의 일관성과 고음질을 향상시키고, 다양한 판별자 조합 전략을 체계적으로 평가한 BemaGANv2 를 제안합니다.
FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
이 논문은 대학원 수준을 넘어선 추상 대수학 문제를 포함하는 새로운 벤치마크 'FATE'를 제안하고, 최신 대형 언어 모델들이 수학 경시대회 대비 연구 수준의 형식적 추론에서 극심한 성능 격차와 형식화 과정에서의 한계를 드러냈음을 보고합니다.
Classifying covering types in homotopy type theory
이 논문은 호모토피 타입 이론에서 갈루아 대응을 형식화하고 n 차원 피복 공간의 일반화를 개발하며 렌즈 공간의 피복을 분류하고 포인카레 호몰로지 구를 구성하는 방법을 제시합니다.
Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications
이 논문은 시맨틱 가이드드 합성 (SyGuS) 과 TSL논리를 활용하여 기존 부울 추상화의 한계를 넘어 데이터 변환과 시간적 명세를 동시에 학습하는 새로운 마이닝 기법을 제안하며, 이를 통해 OpenAI-Gymnasium 환경에서 기존 수동 학습 베이스라인보다 훨씬 강력한 성능과 샘플 효율성을 입증했습니다.
Three Fixed-Dimension Satisfiability Semantics for Quantum Logic: Implications and an Explicit Separator
이 논문은 유한 차원 힐베르트 공간에서 정의된 세 가지 양자 논리 만족도 개념 (표준 힐베르트 격자, 전역 가환 투영자, 국소 부분-부울) 을 비교하여, 특정 논리식이 표준 의미론에서는 만족 가능하지만 나머지 두 의미론에서는 만족 불가능함을 보여주는 명시적 분리자 (SEP-1) 를 제시하고 세 개념 간의 포함 관계를 규명합니다.
Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
이 논문은 대규모 LLM 에이전트들이 정적 계획 대신 보너스 기반 시장 메커니즘을 활용하여 상호작용적 정리 증명 (ITP) 환경에서 대수적 위상수학의 자동 형식화와 증명 탐색을 분산 협력적으로 수행하는 실험을 다룹니다.
Twitch: Learning Abstractions for Equational Theorem Proving
이 논문은 자동 추론에서 인간이 제공하는 지침 없이도 관련 증명에서 반복적으로 나타나는 흥미로운 항 패턴(추상화) 을 자동으로 발견하는 도구 'Twitch'를 제안하고, 이를 등식 정리 증명기 Twee 에 통합하여 TPTP 의 단위 등식 문제 해결 성능과 속도를 크게 향상시켰음을 보여줍니다.
LLM2SMT: Building an SMT Solver with Zero Human-Written Code
이 논문은 인간이 작성한 코드가 전혀 없이 LLM 코딩 에이전트가 QF_UF 문제를 해결하는 완전한 SMT 솔버를 구축하고 벤치마크에서 경쟁력 있는 성능을 보였음을 보여주는 사례 연구입니다.
Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues
이 논문은 대형 언어 모델을 화자 (Prover) 와 반박자 (Skeptic) 로 활용하여 전문가와의 대화를 통해 지식을 추출하는 것이 아니라 명시화하는 'Elenchus' 시스템을 제안하고, 이를 비단조 다결 (NMMS) 논리에 매핑하여 W3C PROV-O 온톨로지의 설계 근거를 대화에서 추출하고 형식적으로 검증하는 방법을 제시합니다.
Learning to Rank the Initial Branching Order of SAT Solvers
이 논문은 그래프 신경망 (GNN) 을 활용해 SAT 솔버의 초기 분기 순서를 예측함으로써 무작위 및 준-산업적 벤치마크에서 상당한 속도 향상을 보이지만, 복잡한 산업적 인스턴스에서는 솔버의 동적 휴리스틱이 초기화를 즉시 덮어쓰는 등의 한계를 발견했다고 요약할 수 있습니다.
Sketch-Oriented Databases
이 논문은 데이터베이스 패러다임을 유한 극한 스케치로, 개별 데이터베이스와 스키마를 집합 값 모델로 인코딩하는 범주론적 프레임워크인 '스케치 지향 데이터베이스'를 제안하며, 그래프 기반 특징을 포착하고 경로를 효율적으로 추론하며 모듈화된 확장을 가능하게 하는 '더듬기 스케치'를 도입합니다.
A method for the automated generation of proof exercises with comparable levels of proving complexity
이 논문은 첫 번째 논리 언어로 표현된 수학적 증명 연습문제의 난이도를 통제하여, 입력된 연습문제와 동등한 증명 복잡도를 가진 새로운 연습문제들을 자동으로 생성하는 방법을 제안합니다.
Proceedings Eighth International Conference on Applied Category Theory
이 논문은 2025 년 6 월 플로리다 대학교에서 개최된 제 8 회 응용 범주론 국제 학술대회 (ACT2025) 의 개요와 컴퓨터 과학, 양자 계산 등 다양한 분야의 연구 결과를 담은 Proceedings 의 내용을 소개합니다.