Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
이 논문은 대형 언어 모델 (LLM) 의 증명 전략을 추출하여 Rocq(구 Coq) 의 기호적 증명기 (CoqHammer) 에 적용하는 'Strat2Rocq'를 제안함으로써, 자동 증명 성공률을 13.41% 향상시키고 추출된 레마가 LLM 증명 에이전트의 성능도 개선한다는 것을 보여줍니다.
💻 Category
cs.LO
67 편의 논문
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 기반 속성 생성을 결합한 확장 가능한 검증 방법론을 제시합니다.
Upholding Epistemic Agency: A Brouwerian Assertibility Constraint for Responsible AI
이 논문은 고위험 분야에서 AI 가 불확실성을 권위 있는 결론으로 전환하는 것을 방지하고 인간의 인식적 주체성을 보호하기 위해, 공개적으로 검증 가능한 정당성 증빙이 없을 경우 '미결정'으로 응답해야 한다는 브라우어적 주장 제약과 이를 구현하는 3 단계 인터페이스를 제안합니다.
Non-Derivability Results in Polymorphic Dependent Type Theory
이 논문은 P2 체계에서 파라메트릭 몫 타입이 정의 불가능하며, 스트림 타입에 대한 강한 코인덕션 원리가 성립하지 않고 자연수에 대한 인덕션 원리를 증명하려면 함수 확장성이 필수적임을 반모델을 통해 규명합니다.
Continuous Modal Logical Neural Networks: Modal Reasoning via Stochastic Accessibility
이 논문은 신경 확률 미분 방정식 (Neural SDE) 을 활용하여 이산적 크립크 구조를 연속적 다양체로 확장하고, 논리 식을 손실 함수에 직접 통합하여 확률적 확산과 엔트로피 위험 측정을 통해 모달 논리 추론을 가능하게 하는 '유체 논리 (Fluid Logic)' 및 '논리 정보 신경망 (LINNs)' 프레임워크를 제안합니다.
SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints
이 논문은 생성된 SQL 과 정답 SQL 간의 차이를 찾기 위해 제약 조건 마이닝 파이프라인을 도입하여 더 현실적인 차등 데이터베이스를 생성하고 표준 평가 방식이 놓치는 오류를 효율적으로 발견하는 오픈소스 도구 SpotIt+ 를 제안합니다.