Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving
Theorem proving in real-world Lean 4 projects is challenging because proofs often depend on project-specific context. While iterative refinement can use compiler errors to repair failed proofs, reusing failed attempts requires careful search control: some proofs provide better starting points than others, and later revisions may degrade a partially correct proof. We propose a compiler-guided proof search framework that balances exploration and expl
arXiv에서 원문 보기최신 논문
- FM-Bench: A Benchmark for Long-Horizon Management with Competing AgentsAI에게 축구 구단을 20년간 통째로 맡겨보니, 승패는 계산력이 아니라 '경영 감각'에서 갈렸다
- FinRCA-Bench: Benchmarking Evidence Retrieval and Reasoning for Financial AI SystemsAI가 '정답'을 맞혀도, 정작 증거는 못 찾는 경우가 대부분이었다 - 재무 이상거래 진단 AI의 숨은 약점
- FACET: Preserving Source Intent and Executable State in Terminal Task SynthesisAI 에이전트에게 '터미널 문제집'을 정합성 있게 만들어주는 파이프라인, FACET
- Alignment Is All You Need: Instruction-Free Training for General Audio-Language Models음성·소리를 알아듣는 AI, 지시문 학습 없이 '연결 다리'만 훈련해도 충분하다
- Adversarial Review: Structured Disagreement for Grounded Agentic Code ReviewAI 코딩 에이전트, 에이전트 늘리기보다 '검토자 vs 비판자' 한 쌍이 더 똑똑하게 일한다
- Looped Language Models Improve Compositional Tool Calling생각을 여러 번 되짚는 AI가 여러 개의 도구를 순서대로 엮어 쓰는 일도 더 잘한다
- Bridging Search and CRM: Productionizing AI Product Research Agents for Customer Re-Engagement쇼핑몰 검색에서 이탈한 고객을 AI 에이전트가 다시 카톡(왓츠앱)으로 불러온 이야기
- GenEx: A Graph-Based Representational Paradigm for SARS-CoV-2 Variant Detection via Codon Co-occurrence Networks바이러스 유전자 서열을 코돈끼리 서로 옆에 등장하는 관계망(그래프)으로 바꿔 변이를 구분하는 법