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 阅读最新论文
- FinRCA-Bench: Benchmarking Evidence Retrieval and Reasoning for Financial AI SystemsAI经常能说对财务对账出错的原因,却拿不出真正的证据
- Looped Language Models Improve Compositional Tool Calling会反复回想自己答案的AI模型,更擅长按顺序组合调用多个工具
- FACET: Preserving Source Intent and Executable State in Terminal Task SynthesisFACET:让终端命令行任务的“说明书、环境、答案、判分器”自动保持一致
- FM-Bench: A Benchmark for Long-Horizon Management with Competing Agents让AI连续管理一家足球俱乐部20年后发现,胜负关键不在模型大小,而在经营习惯
- Bridging Search and CRM: Productionizing AI Product Research Agents for Customer Re-EngagementAI智能体追着离场用户发WhatsApp,把逛而不买的顾客拉回来
- Adversarial Review: Structured Disagreement for Grounded Agentic Code ReviewAI代码审查:与其堆更多智能体,不如让一个审查者和一个批评者互相较真
- GenEx: A Graph-Based Representational Paradigm for SARS-CoV-2 Variant Detection via Codon Co-occurrence Networks把病毒基因序列变成密码子关系网络图,用来区分新冠变异株
- Alignment Is All You Need: Instruction-Free Training for General Audio-Language Models语言模型全程冻结,只训练一个小连接器,也能做出好用的听觉理解AI