MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's p
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바이러스 유전자 서열을 코돈끼리 서로 옆에 등장하는 관계망(그래프)으로 바꿔 변이를 구분하는 법