Finding Connections via Satisfiability Solving
이 논문은 연결 계산법 (connection calculi) 의 증명 검색 구조를 부호화하고 대칭성 깨기를 적용한 SAT 기반 방법을 제안하여 1 차 논리 증명 자동화를 향상시키고, 이를 위해 세 가지 SAT 부호화를 제시하고 이론적 분석을 수행하며 새로운 솔버 upCoP 를 구현하여 실용성을 입증합니다.
💻 Category
cs.LO
64 편의 논문
Commutation Groups and State-Independent Contextuality
이 논문은 퍼스 - 메르민 마법 정사각형과 같은 상태 독립적 문맥성 논증을 연구하기 위해 교환군과 문자 재작성 시스템을 도입하고, 이를 통해 문맥적 단어를 특징짓는 대수적 구조를 제시합니다.
Online Monitoring of Metric Temporal Logic using Sequential Networks
이 논문은 사이버 - 물리 시스템의 메트릭 시계 논리 (MTL) 명세로부터 이산 및 밀집 시간 행동을 위한 순차적 네트워크를 구축하는 통합 기법을 제안하여, 효율적이고 확장 가능한 온라인 모니터링 프레임워크를 제공하며 기존 접근법 대비 뛰어난 성능과 확장성을 입증합니다.
Module checking of pushdown multi-agent systems
이 논문은 푸시다운 다중 에이전트 시스템 (PMS) 의 모듈 체킹 문제를 연구하여 ATL 에 대해서는 2EXPTIME-완전임을, ATL* 에 대해서는 4EXPTIME-완전임을 증명함으로써 ATL* 의 경우 기존 모델 체킹보다 지수적으로 높은 복잡도를 가짐을 보여줍니다.
The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness
이 논문은 스텝-복제 재귀자를 갖는 1 차원 재작성 시스템에서 직접적 구성적 측정의 불가능성을 기계적으로 검증하고, 투영 기반 방법이 이를 우회하는 방식을 규명하며, 안전한 부분 집합에 대해 기계화된 종료성 증명과 인증 체인을 제시합니다.
MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
이 논문은 그래프 신경망 (GNN) 임베딩과 런타임 설계 통계를 결합하여 다중 속성 검증 (MPV) 에서 속성 클러스터링을 지능화하고 경계 모델 검사 (BMC) 의 성능을 획기적으로 개선하는 새로운 하이브리드 접근법인 MPBMC 를 제안합니다.
Fusions of One-Variable First-Order Modal Logics
이 논문은 한 변수 일차 모달 논리의 독립적 융합에 대한 보존 결과를 연구하여, 등호가 없는 경우 Kripke 완전성과 결정성이 보존되지만 등호와 비강성 상수가 있는 경우 디오판토스 방정식 인코딩을 통해 보존되지 않음을 증명하고, 이를 S5 모달리티를 공유하는 명제 모달 논리의 융합으로 해석하여 Kripke 완전성과 결정성의 전파를 위한 일반적 충분 조건을 제시합니다.
Complete Diagrammatic Axiomatisations of Relative Entropy
이 논문은 확률 분포 간의 거리인 상대 엔트로피를 확률 행렬 범주의 양적 확대로 간주하여, 크로네커 곱과 직접 합이라는 두 가지 단위원 구조에 대해 클리바크-라이블러 발산 및 일반화된 렌지 발산을 완전하게 공리화한 결과를 제시합니다.
Modal Fragments
이 논문은 포스트의 격자 (Post's lattice) 를 기반으로 명제 논리 및 모달 논리의 연산자 제한 조각들을 체계적으로 조사하여 표현력과 계산 복잡성 간의 관계를 규명하고, 학습 가능성에 대한 기존 결과를 확장하며 미해결 문제들을 제시합니다.
The Complexity of the Constructive Master Modality
이 논문은 구성적 마스터 모달리티 논리 와 를 도입하고 이를 의 단편과 번역하여 두 논리가 모두 EXPTIME-완전하며 지수 크기 유한 모델 성질을 가진다는 것을 증명하고, 이를 통해 아프샤리 (Afshari) 등이 제기한 다이아몬드-프리 단편에 대한 추측을 해결하며 와 를 이 논리에 내포시켜 그 유효성 문제가 EXPTIME 에 속함을 보여줍니다.
Constraint Learning for Non-confluent Proof Search
이 논문은 연결 계산법 (connection calculus) 에서의 불완전한 백트래킹 문제를 해결하기 위해 제약 학습을 도입하여, 완전성을 유지하면서 실제 백트래킹을 크게 줄이는 방법을 제안합니다.
On Solving String Equations via Powers and Parikh Images
이 논문은 문자열을 위한 거듭제곱 연산자, 일반화된 파라키 이미지, 그리고 등식 분해 기법을 니켈 변환의 확장으로 결합하여 복잡한 문자열 방정식 및 SMT 입력을 해결하는 새로운 접근법을 제시합니다.
NL2GDS: LLM-aided interface for Open Source Chip Design
이 논문은 대규모 언어 모델 (LLM) 을 활용하여 자연어 설명을 RTL 과 GDSII 레이아웃으로 자동 변환하는 NL2GDS 프레임워크를 제안하며, 이를 통해 ASIC 설계의 접근성을 높이고 면적, 지연, 전력 효율을 크게 개선할 수 있음을 입증합니다.
Reversible Computation with Stacks and "Reversible Management of Failures"
이 논문은 스택 연산을 부분 전단사 함수가 아닌 전 전단사 함수로 해석하여 계산 복잡성 연구에 필수적인 총전단사성 (total bijectivity) 을 보장하는 새로운 역계산 언어 SCORE 를 제안하고, 증명 보조기구를 통해 그 정확성을 검증합니다.
Ohana trees, linear approximation and multi-types for the I-calculus: No variable gets left behind or forgotten!
이 논문은 I-계산에서 소실되거나 무한히 밀려난 자유 변수까지도 기억하는 '오하나 트리 (Ohana trees)'를 도입하여, 기존 연구에서 간과되었던 I-계산의 새로운 등식 이론을 정립하고 이를 타일러 전개 및 비-idempotent 타입 시스템을 통해 검증하는 방법을 제시합니다.
LeanTutor: Towards a Verified AI Mathematical Proof Tutor
이 논문은 자연어 처리가 가능한 대형 언어 모델 (LLM) 과 엄밀한 증명 검증이 가능한 Lean 정리를 결합하여, 오류가 없는 수학적 증명 튜터 'LeanTutor'를 개발하고 PeanoBench 데이터셋을 통해 이를 평가하는 방법을 제시합니다.
The Geometry of Reasoning: Flowing Logics in Representation Space
이 논문은 대규모 언어 모델의 추론을 표현 공간 내의 기하학적 흐름으로 모델링하여, 다음 토큰 예측 학습만으로도 모델이 논리적 불변성을 내재화할 수 있음을 증명하고 기계적 이해와 인간 언어 규칙 사이의 보편적 표현 법칙을 제시합니다.
Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
이 논문은 대형 언어 모델 (LLM) 의 증명 전략을 추출하여 Rocq(구 Coq) 의 기호적 증명기 (CoqHammer) 에 적용하는 'Strat2Rocq'를 제안함으로써, 자동 증명 성공률을 13.41% 향상시키고 추출된 레마가 LLM 증명 에이전트의 성능도 개선한다는 것을 보여줍니다.
SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification
이 논문은 기존 테스트 기반 평가의 한계를 극복하고 생성된 SQL 과 정답 SQL 의 동등성을 형식적 검증 엔진을 통해 엄격하게 검증하는 새로운 평가 파이프라인 'SpotIt'을 제안하며, 이를 통해 기존 평가 방식이 놓칠 수 있는 차이를 포착하고 Text-to-SQL 평가의 복잡성을 재조명합니다.
Formal that "Floats" High: Formal Verification of Floating Point Arithmetic
이 논문은 비선형 연산과 제어/데이터 경로 결합으로 인해 어려운 부동소수점 연산의 형식 검증을 위해, 직접적인 RTL 대 RTL 모델 체킹과 분할 정복 전략, 그리고 인간-인-루프 (HITL) 가이드를 통한 AI 기반 속성 생성을 결합한 확장 가능한 검증 방법론을 제시합니다.