중심 명제
AI4Math의 핵심은 더 많은 문제에서 최종 정답을 맞히는 데 있지 않다. 수학적 아이디어를 생성하고, 명제를 정확하게 형식화하며, 증명을 기계적으로 검증하고, 실패로부터 탐색전략을 개선하며, 새로운 수학·과학 지식을 발견하는 self-evolving verified research system을 구축하는 데 있다.
Formal Proving · Autoformalization · Verification · Discovery · Scientific Agents
AI for Mathematics
AI4Math 2026 논문군을 formal theorem proving, autoformalization, verification-guided search, self-distillation, mathematical memory, discovery, multimodal mathematics, verified machine learning와 scientific agents의 관점에서 통합한다.
210공식 채택 논문
16핵심 연구축
22연구질문
24Open Problems
01
전체 연구 지형
AI4Math를 benchmark answer generation이 아니라 generation, formalization, verification, search, memory와 discovery를 연결하는 research lifecycle로 본다.
Research Question→Conjecture & Retrieval→Informal Search→Autoformalization→Trusted Verification→Counterexample & Repair→Discovery Audit
Self-Evolving Mathematical Intelligence =
Search × Verification × Memory × Discovery
02
Definition
Formal proving, autoformalization, verifier, RLVR, strategy memory, counterexample와 verified ML을 정리한다.
AI for Mathematics
Machine learning, language model, symbolic reasoning과 proof assistant를 사용해 problem solving, theorem proving, formalization, discovery와 verification을 지원하는 연구영역이다.
Formal Theorem Proving
Theorem에 대해 proof assistant의 trusted kernel이 검증할 수 있는 proof term을 찾는 문제다.
Informal Mathematical Reasoning
자연어, 수식과 diagram을 이용해 proof와 solution을 구성하는 과정이다.
Autoformalization
자연어 theorem과 proof를 Lean, Isabelle, Coq·Rocq 등의 formal language로 변환하는 문제다.
Proof Assistant
Formal theorem과 proof를 작은 trusted kernel로 검증하는 software environment다.
Verifier
Candidate proof나 solution의 validity, error location과 diagnostic을 판정하는 component다.
Generator–Verifier Gap
Solution 발견은 어렵지만 주어진 solution의 검증은 상대적으로 쉬운 구조를 의미한다.
Research-Level Discovery
기존 theorem 재현을 넘어 새로운 theorem, bound, algorithm, construction과 counterexample을 생성하는 문제다.
Self-Evolving Scientific Agent
Failure와 verifier feedback으로 자신의 plan, memory, workflow와 strategy를 반복개선하는 agent다.
RL with Verifiable Rewards
Proof kernel, compiler, symbolic checker 등의 자동 verifier에서 reward를 얻는 reinforcement learning이다.
Process Supervision
Final outcome뿐 아니라 reasoning trace의 각 step에 correctness와 usefulness signal을 제공하는 supervision이다.
Self-Distillation
동일 model 또는 이전 version이 생성한 개선된 distribution을 supervision으로 사용하는 학습방식이다.
Mathematical Strategy Memory
개별 answer보다 induction, symmetry, invariant, auxiliary lemma와 repair pattern 같은 reusable schema를 저장한다.
Premise Retrieval
거대한 formal library에서 target theorem에 필요한 definition, lemma와 theorem을 선택하는 문제다.
Counterexample-Guided Reasoning
잘못된 conjecture나 proof에 대해 concrete witness를 생성해 누락된 assumption과 boundary를 찾는다.
Multimodal Mathematical Reasoning
Text와 equation뿐 아니라 geometry diagram, plot, graph, table와 physical image를 함께 사용한다.
Verified Machine Learning
Neural network와 ML algorithm을 executable program이자 formal semantic object로 다룬다.
03
Problem Definition
Informal–formal, generation–verification, proof validity, discovery, diversity, reward, safety와 visual grounding의 간극을 정의한다.
Informal–Formal Gap
자연어 proof가 의미적으로 맞아도 formal detail이 부족할 수 있고, formal proof가 compile되어도 원 theorem과 다른 명제를 증명할 수 있다.
Generation–Verification Gap
현재 model은 candidate 생성능력보다 correct candidate를 선택하고 자기검증하는 능력이 약할 수 있다.
Final Answer–Proof Validity Gap
수치 answer가 맞아도 reasoning이 circular하거나 invalid theorem을 사용할 수 있다.
Compiler Acceptance–Semantic Correctness Gap
Compilation 성공은 semantic alignment와 intended theorem preservation을 보장하지 않는다.
Proof Search–Mathematical Discovery Gap
주어진 theorem을 증명하는 것과 theorem 자체를 발명하는 것은 다른 문제다.
Surface Diversity–Approach Diversity Gap
표현이 달라도 동일 strategy일 수 있고, lexical metric은 genuine approach diversity를 측정하지 못한다.
Sparse Reward–Dense Credit Gap
Binary verifier reward는 긴 reasoning trace에서 어느 token과 step이 오류인지 알려주지 않는다.
Local Step–Global Proof Gap
개별 step이 그럴듯해도 모든 proof obligation이 닫히지 않을 수 있다.
Pass Rate–Agent Attribution Gap
최종 성공률만으로 compiler feedback, retrieval, proof-state inspection과 restart의 기여를 알기 어렵다.
Search Volume–Search Quality Gap
Sample과 tool call을 늘려도 같은 reasoning basin을 반복하면 compute만 낭비한다.
Correctness–Proof Quality Gap
Correct proof라도 장황하고 brittle하며 version change에 취약할 수 있다.
Static Benchmark–Live Research Gap
Public benchmark는 contamination, saturation과 memorized solution 문제를 가진다.
Engineering Tuning–Scientific Invention Gap
Known component tuning과 generalizable method invention은 구분되어야 한다.
Self-Evolution–Safety Gap
Agent가 code와 workflow를 수정할수록 specification violation 위험도 증가한다.
Visual Perception–Symbolic Reasoning Gap
Diagram object를 인식하는 능력과 그것을 proof structure로 변환하는 능력은 다르다.
Tool Availability–Workflow Intelligence Gap
많은 tool이 있어도 언제 검색하고 backtrack하며 commit할지 모르면 성능이 향상되지 않는다.
04
Core Concepts
Proof state, trusted kernel, obligation coverage, strategy schema, guarded generation, provenance와 test-time scaling을 정리한다.
Proof State
아직 해결되지 않은 goal과 local context를 포함하는 formal search state다.
Trusted Kernel
작은 논리규칙 집합으로 final proof term을 검증해 untrusted LLM과 trusted result를 분리한다.
Formalization-Oriented Informal Proof
Diagnosable, repairable, expandable, prunable한 intermediate proof representation이다.
Verification-Guided Search
Verifier feedback을 repair, expand, prune, backtrack, retrieve와 restart action으로 변환한다.
Obligation Coverage
각 문장의 plausibility가 아니라 모든 required proof obligation이 실제로 해결되었는지 측정한다.
Approach-Level Diversity
Algebraic, geometric, induction, generating function 등 genuinely different proof strategy의 coverage다.
Strategy Schema
특정 problem이 아니라 condition, decomposition, useful lemma와 failure mode를 담는 procedural abstraction이다.
Generator–Reviser Distillation
Initial response와 binary reward를 이용해 Reviser가 개선 distribution을 만들고 Generator에 distill한다.
Formally Guarded Generative Model
Output contract를 만족하지 못하면 verified fallback을 반환하는 generation wrapper다.
Multi-Agent Mathematical Reasoning
Decomposer, prover, critic, formalizer, verifier와 synthesizer 역할을 분리한다.
Counterexample-Carrying Verification
Failure label과 함께 concrete witness, failed state 또는 unsatisfied constraint를 반환한다.
Proof Refactoring
Correctness를 유지하며 proof length, compile cost, dependency와 version robustness를 개선한다.
Trace-Level Attribution
Retrieval, compiler call, restart, candidate rejection과 submission timing을 trajectory 수준에서 분석한다.
Live Research Benchmark
최신 theorem, open problem, evolving library와 newly generated task를 지속적으로 추가하는 평가환경이다.
Semantic Invariance
Variable renaming, coordinate transformation과 equivalent assumption에 대해 model behavior가 유지되는 성질이다.
Budget-Aware Test-Time Scaling
Global compute budget을 difficulty, candidate distribution과 verification cost에 따라 problem별 배분한다.
Verified Scientific Workflow
Hypothesis, formal model, computation, candidate result, verification과 robustness test를 연결한다.
05
Introduction
AI4Math는 symbolic proving에서 self-evolving verified scientific agents로 발전한다.
Stage 1 — Symbolic Automated Proving
Hand-crafted search, unification, SAT·SMT와 logic rule을 사용한다.
Stage 2 — Neural Premise Selection
Neural model이 theorem과 lemma relevance를 예측해 symbolic search를 안내한다.
Stage 3 — Language-Model Reasoning
LLM이 자연어와 수식으로 chain-of-thought solution을 생성한다.
Stage 4 — Neural–Symbolic Formal Proving
LLM이 tactic·proof term을 생성하고 Lean·Isabelle kernel이 검증한다.
Stage 5 — Agentic Proof Search
Agent가 compiler, proof state, retrieval와 symbolic tool을 반복사용한다.
Stage 6 — Self-Improving Verifiable Reasoning
Verifier reward, critique, failure memory와 self-distillation로 policy를 개선한다.
Stage 7 — Research-Level Discovery
새 theorem, algorithm, construction과 counterexample을 발견한다.
Stage 8 — Verified Scientific Agents
Math reasoning을 ML, physics, optimization, causality와 program verification으로 확장한다.
06
Motivation and Background
검증가능성, research-level evaluation, scalable supervision, proof maintenance, safe self-evolution과 scientific transfer가 연구를 촉진한다.
수학은 검증 가능한 지능의 핵심 Testbed
Proof kernel, compiler, symbolic execution과 counterexample search로 correctness reward를 자동생성할 수 있다.
Benchmark 성능과 연구능력은 다름
실제 연구에는 problem definition, conjecture selection, long search, literature review와 novelty 판단이 필요하다.
Formal Verification은 Scalable Supervision 제공
Human grading 없이 correctness를 얻지만 binary reward를 richer diagnostic으로 확장해야 한다.
AI-Generated Proof는 유지보수가 어려움
Correct proof도 장황하고 library version 변화에 취약할 수 있다.
Self-Evolution에는 Guardrail 필요
Agent가 자신의 workflow를 바꾸더라도 hard formal constraint를 유지해야 한다.
수학적 Agent는 다른 과학으로 확장 가능
Physics, optimization, causality, ML theory, program verification와 bioinformatics의 기반이 된다.
07
Challenges
Semantic alignment, proof search, verifier reward, self-verification, diversity, proof quality, novelty, safety와 multimodal grounding이 핵심 난제다.
| 도전과제 | 핵심 문제 | 요구되는 방향 |
|---|---|---|
| Informal–formal alignment | Compile되지만 다른 theorem 표현 | Round-trip semantic verification |
| Proof search explosion | Tactic·lemma 조합이 기하급수적 | Hierarchical search·premise retrieval |
| Sparse verifier reward | 성공·실패만 제공 | Step-level diagnostic·self-distillation |
| Self-verification weakness | 좋은 solution 생성 후 선택 실패 | Independent verifier·debate |
| Verifier exploitation | Judge-specific shortcut 최적화 | Adversarial verifier ensemble |
| Surface diversity | 표현만 달라지고 전략 동일 | Approach-level diversity |
| Proof obligation coverage | 일부 step만 검증 | Pessimistic end-to-end checking |
| Counterexample generation | 실패원인 구체화 어려움 | Certified witness search |
| Premise retrieval | 거대 library에서 핵심 lemma 탐색 | Dependency-aware retrieval |
| Library version drift | Lean·Mathlib update로 proof 실패 | Version-aware retrieval·refactoring |
| Proof quality | Correct하지만 장황하고 brittle | Multi-objective optimization |
| Agent attribution | 어떤 tool이 실제 도움됐는지 불명확 | Trace-level ablation |
| Search stopping | 계속 probing하고 commit하지 않음 | Submit·restart policy |
| Research novelty | 올바르지만 이미 알려진 결과 | Literature and novelty audit |
| Benchmark contamination | 기존 solution memorization | Live·unsolved benchmarks |
| Benchmark saturation | Frontier model 차이 구분 어려움 | Continual task generation |
| Scientific significance | Valid result가 중요하다는 보장 없음 | Expert and utility evaluation |
| Self-evolution safety | Agent code 변경이 constraint 위반 | Formally guarded generation |
| Memory pollution | 실패전략이 잘못 저장됨 | Verified memory revision |
| Multi-agent overhead | Debate와 role 분리가 비용 증가 | Cost-aware orchestration |
| Visual reasoning | Diagram perception과 proof inference 분리 | Perception–reasoning decomposition |
| Long deduction | 초기오류가 이후 step 오염 | Sequence-level probabilistic verification |
| RL mode collapse | Reward optimization이 strategy diversity 축소 | Diversity-aware RL |
| Human collaboration | AI output 검증 부담 | Traceable intermediate artifact |
| Cross-domain transfer | Olympiad skill이 연구·과학으로 전이 안 됨 | Research-level scientific tasks |
| Evaluation fragmentation | Formal·informal·multimodal metric 분리 | Unified evaluation framework |
08
Research Questions
Autoformalization, verifier feedback, strategy diversity, memory, discovery, proof quality, multimodal grounding와 human collaboration을 중심으로 정리한다.
RQ1
자연어 theorem과 formal statement의 semantic equivalence를 자동으로 증명할 수 있는가?
RQ2
Formalization 이전에 informal proof를 최적화하면 theorem proving search를 얼마나 줄일 수 있는가?
RQ3
Compiler error, proof state와 counterexample 중 어떤 feedback이 agent 성능에 가장 크게 기여하는가?
RQ4
LLM이 correct proof를 생성하는 능력과 correct proof를 선택하는 능력 사이의 격차를 어떻게 줄일 것인가?
RQ5
Surface-level variation이 아닌 genuinely different mathematical strategy를 어떻게 측정할 것인가?
RQ6
Binary verifier reward를 dense token-level credit assignment로 안정적으로 변환할 수 있는가?
RQ7
Self-distillation 과정에서 잘못된 revision의 반복증폭을 어떻게 방지할 것인가?
RQ8
Agent가 retrieval, backtracking, restart와 submission 중 어떤 action을 선택해야 하는지 학습할 수 있는가?
RQ9
Proof search에 필요한 최소 sufficient tool set은 무엇인가?
RQ10
성공과 실패에서 추출한 strategy memory가 unseen problem에 일반화되는가?
RQ11
Agent memory의 잘못된 schema를 verifier feedback으로 수정·삭제할 수 있는가?
RQ12
Research-level theorem의 novelty와 significance를 automatic verifier만으로 평가할 수 있는가?
RQ13
Unknown solution을 가진 open problem에서 model progress를 안전하게 측정할 수 있는가?
RQ14
Formal correctness를 유지하면서 proof length, compilation cost와 version portability를 공동최적화할 수 있는가?
RQ15
Self-evolving agent가 unseen input에서도 hard specification을 항상 만족하도록 보장할 수 있는가?
RQ16
Formal proof assistant가 neural network implementation과 numerical kernel의 실제 semantics까지 포괄할 수 있는가?
RQ17
Visual diagram에서 인식된 object를 formal proof state와 직접 연결할 수 있는가?
RQ18
RLVR가 mathematical strategy diversity와 compositional reasoning을 실제로 증가시키는가?
RQ19
AI가 발견한 theorem과 algorithm이 controlled benchmark 밖에서도 scale하고 generalize하는가?
RQ20
Human mathematician과 AI agent가 conjecture, proof, verification을 어떻게 분담해야 하는가?
RQ21
수학적 agent를 physics, optimization, software verification과 causal discovery로 확장할 때 어떤 verification layer가 필요한가?
RQ22
정적 leaderboard가 아닌 지속적으로 진화하는 mathematical evaluation platform을 구축할 수 있는가?
09
Approaches / Methods
대표 연구를 formal infrastructure, discovery benchmark, verifier-guided search, self-distillation, proof memory, multimodal reasoning와 verified ML 기준으로 탐색할 수 있다.
AXLE
Strict Lean verification, metadata extraction, semantic source manipulation, proof repair, lemma extraction과 multi-version isolation을 cloud API로 제공한다.
HorizonMath
Unknown-solution research problems와 deterministic verifier를 결합해 contamination-resistant mathematical discovery를 평가한다.
FIPO-Prover
Informal proof를 formalization-oriented intermediate state로 바꾸고 verifier feedback으로 repair, expand, prune와 backtrack을 수행한다.
Approach-Level Diversity
Lexical variation이 아닌 genuine proof strategy diversity를 human-calibrated judge로 측정한다.
MLS-Bench
ML system component의 generalizable method invention과 scale-up validation을 평가한다.
SEVerA
Search–Verify–Learn 과정에서 formal specification을 만족하는 candidate만 agent improvement에 사용한다.
Self-Distillation Zero
Binary verifier reward를 Reviser의 dense token distribution으로 변환해 Generator에 on-policy distill한다.
QED
Research question을 decomposition, multiple proving, verification과 synthesis 역할로 분리한다.
TorchLean
Typed tensor, layer, optimizer, AD, finite-precision semantics와 robustness certificate를 Lean 안에 formalize한다.
Lean Refactor
Version-aware strategy retrieval로 proof length, compile cost와 portability를 동시에 개선한다.
What Helps Agentic Lean Provers?
Compiler feedback, proof-state feedback, retrieval와 tool use를 trace-level ablation으로 분석한다.
ISM
성공·실패 episode에서 verified strategy schema를 추출해 compact memory bank를 갱신한다.
Graffiti3Loop
Graph generation, invariant measurement, conjecture proposal, counterexample search와 refinement를 closed loop로 반복한다.
Formal·Natural-Language Verification
Lean-as-judge, obligation coverage, counterfactual contracts와 debate를 결합해 high-precision verification을 수행한다.
BARSA·Generate-Rank-Verify
Answer distribution 안정성과 verification cost에 따라 recursive aggregation과 extra compute를 배정한다.
PWW-Bench·PRISM·Draw2Think
Diagram perception, auxiliary construction과 symbolic proof를 분리·연결해 multimodal math reasoning을 평가한다.
DafnyProver·VeriBench·Quokka
Test passing을 넘어 invariant, safety property와 universal correctness를 formal proof로 보장한다.
AI-Assisted Scientific Discovery
Convex relaxation, Lyapunov function, PDE architecture, numerical approximation과 causal estimator를 search한다.
10
Key Applications
Formal proof, literature formalization, discovery, verified ML, program verification, scientific ML, education와 collaboration에 적용된다.
Formal Theorem Proving
Lean·Isabelle proof generation, tactic search, premise selection, proof repair와 counterexample search.
Mathematical Literature Formalization
Textbook·paper theorem extraction, dependency graph, formal library construction와 version maintenance.
Research-Level Discovery
Open problem, conjecture, improved bound, combinatorial construction, algorithm과 invariant discovery.
Verified Machine Learning
Neural semantics, AD proofs, robustness certificates, optimizer verification와 ML-theory formalization.
Program Verification
Invariant synthesis, verified code generation, protocol compliance, differential privacy와 memory safety.
Scientific Machine Learning
PDE solver, neural operator, numerical analysis, scientific optimization와 dynamical-system invariant.
Mathematical Education
Student proof feedback, step-level diagnosis, multiple strategy demonstration와 interactive proving.
Benchmark·Dataset Curation
Synthetic proof generation, high-precision filtering, live benchmark, retrieval benchmark와 diversity audit.
Human–AI Mathematical Collaboration
Literature navigation, conjecture assistance, proof critique, formalization과 computational experiment design.
Self-Evolving Scientific Agents
Causality, finance, physics, bioinformatics, automated ML와 software engineering으로 확장한다.
11
Open Problems
Semantic autoformalization, self-verification, novelty, dense credit, memory revision, live evaluation, neural semantics와 governance를 해결해야 한다.
Semantic Autoformalization
Formal statement가 원래 자연어 theorem의 의미를 보존한다는 강한 보장이 필요하다.
Verified Informal Reasoning
Natural-language proof도 obligation coverage 수준으로 검증해야 한다.
Self-Verification Asymmetry
Generator보다 약한 verifier 문제를 해결해야 한다.
Verifier Robustness
LLM judge, reward model과 formalization pipeline이 adversarial candidate에 악용되지 않아야 한다.
Research Novelty Verification
Correct result가 기존 literature에 존재하는지 자동판단하기 어렵다.
Significance Evaluation
새 theorem이 trivial modification인지 중요한 발견인지 평가하기 어렵다.
Strategy-Level Diversity
Approach diversity를 신뢰성 있게 label하고 최적화해야 한다.
Dense Credit Assignment
Binary formal reward에서 error-localized token supervision을 추출해야 한다.
Memory Revision
잘못된 strategy와 false lemma가 장기 memory에 저장되는 것을 막아야 한다.
Search–Commit Policy
Agent가 언제 탐색을 중단하고 final proof를 제출해야 하는지 학습해야 한다.
Long-Horizon Proof Search
수천 step과 여러 subgoal의 trajectory를 안정적으로 관리해야 한다.
Cross-Version Robustness
Lean·Mathlib update 이후에도 proof와 retrieval strategy가 유지되어야 한다.
Cross-Assistant Translation
Lean, Isabelle, Coq 간 translation의 semantic preservation을 검증해야 한다.
Proof Quality Standard
Correctness를 넘어 readability, modularity, reusability와 explanatory value를 평가해야 한다.
Real-World Library Scaling
Mathlib 규모에서 retrieval, compilation과 proof-state management를 효율화해야 한다.
Self-Evolution Guarantees
Agent가 workflow와 code를 수정해도 hard specification을 항상 만족해야 한다.
Scientific Generalization
Benchmark에서 발견한 method가 더 큰 scale과 다른 regime에서도 유지되어야 한다.
Contamination-Proof Evaluation
Public solution에 의존하지 않는 지속적 evaluation이 필요하다.
Multimodal Grounding
Diagram의 line, region과 object가 proof step과 명시적으로 연결되어야 한다.
Physical and Numerical Validity
Symbolic correctness뿐 아니라 unit, precision, conservation과 boundary를 검증해야 한다.
Multi-Agent Cost
Role decomposition과 debate의 latency·token 비용을 정당화해야 한다.
Human Oversight
Research-level output을 효율적으로 감사할 evidence trace와 interface가 필요하다.
Formalized Neural Semantics
GPU kernel, floating point와 fused operator의 실제 semantics를 formal model에 연결해야 한다.
Scientific-Agent Governance
AI-generated theorem, proof와 scientific claim의 provenance, ownership와 책임을 기록해야 한다.
12
Future Directions
미래 AI4Math는 research OS, claim contract, proof provenance, verifier-native models, verified memory와 discovery certificates로 발전한다.
1. Mathematical Research Operating System
Question, literature retrieval, conjecture, informal search, autoformalization, verification, novelty audit와 human review를 통합한다.
2. Machine-Readable Mathematical Claim Contract
Informal·formal statement, assumptions, definitions, proof artifact, kernel, version, dependency와 novelty evidence를 명시한다.
3. Proof Provenance Graph
Proof를 linear text가 아니라 claim dependency, generator, verifier와 revision history를 포함하는 graph로 저장한다.
4. Verifier-Native Foundation Model
Proof state와 verifier feedback을 model hidden state update와 training objective에 직접 통합한다.
5. Counterexample-First Reasoning
Proof search 전에 conjecture의 boundary와 취약 assumption을 counterexample로 탐색한다.
6. Strategy-Diverse Test-Time Scaling
Candidate 수보다 distinct mathematical approach coverage를 compute budget 아래 최적화한다.
7. Verified Continual Strategy Memory
Strategy extraction, validation, insertion, contradiction monitoring과 deletion을 formal workflow로 관리한다.
8. Formal Scientific CI/CD
Agent update를 unit test, formal contract, statistical test, benchmark와 regression gate로 검증한다.
9. Live Discovery Benchmarks
Recent papers, open conjectures, Mathlib pull request와 scientific simulation에서 continual task를 생성한다.
10. Human–AI Proof Studio
Human과 AI가 conjecture, assumption, proof plan, lemma dependency와 exposition을 공동편집한다.
11. Unified Formal–Informal–Visual Reasoning
Natural language와 diagram을 typed scene과 symbolic model로 변환하고 formal obligation과 연결한다.
12. Verified AI for AI Research
AI-generated ML method의 implementation, scaling, robustness, statistics와 formal property를 함께 검증한다.
13. Cross-Prover Mathematical Interlingua
Lean, Isabelle, Coq와 Dafny 사이 proof translation과 cross-validation을 지원하는 중립 IR을 구축한다.
14. Self-Evolving but Formally Bounded Agents
Agent가 strategy와 workflow를 수정하되 safety, proof validity, provenance와 human boundary invariant를 유지한다.
15. Mathematical Discovery Certificate
Exact claim, proof, counterexample scope, literature search, novelty, generalization, reproduction와 expert review를 제공한다.
16. Standard Evaluation Protocol
Correctness, semantic alignment, verification, proof quality, retrieval, search, diversity, memory, discovery, multimodal grounding과 safety를 표준화한다.
13
Conclusion
AI4Math는 answer generation 경쟁에서 verified artifacts, agentic search, dense supervision, live discovery와 formally bounded self-evolution으로 연구중심을 이동시킨다.
정답 생성 → 검증 가능한 Artifact
Natural-language answer보다 kernel-checkable proof, executable verifier와 counterexample이 중요하다.
One-Shot Solving → Agentic Proof Search
Agent가 retrieval, compiler, proof state, symbolic tool과 memory를 반복사용한다.
Binary Reward → Error-Localized Supervision
한 bit reward를 token critique, proof obligation과 revision signal로 변환한다.
Surface Diversity → Approach Diversity
서로 다른 표현이 아니라 실제로 다른 mathematical strategy를 탐색한다.
Static Benchmark → Live Research Evaluation
Known answer 재현보다 open problem과 evolving library에서 progress를 측정한다.
Correct Proof → High-Quality Proof
Length, compile cost, modularity, portability와 explanation을 함께 평가한다.
Tool Availability → Workflow Attribution
많은 tool보다 언제 검색하고 backtrack하며 submit하는지가 중요하다.
Self-Improvement → Verified Self-Evolution
Agent는 strategy와 code를 개선하되 formal contract를 유지해야 한다.
Olympiad Solving → Scientific Discovery
새 theorem, algorithm, invariant와 scientific method 발견이 궁극적 목표다.
AI Mathematician → Verified Scientific Agent
Math verification을 physics, ML research, code verification와 causal discovery로 확장한다.
미래의 AI 수학자는 문제를 보고 긴 풀이를 출력하는 language model이 아니다. 중요한 conjecture를 선택하고, 다양한 strategy를 탐색하며, 실패를 counterexample과 formal feedback으로 분석하고, reusable knowledge를 memory에 축적하며, 핵심 claim을 기계적으로 검증하고, 인간 연구자와 함께 새로운 수학·과학 지식을 생산하는 self-evolving verified research agent다.
14
Sources
공식 워크숍, formal proving, autoformalization, agentic verification, self-improvement, benchmark, multimodal mathematics와 scientific discovery 원문 링크.
ICML 2026 AI4Math 워크숍 페이지원문 및 프로젝트 링크3rd AI for Math Workshop 공식 홈페이지원문 및 프로젝트 링크공식 통계원문 및 프로젝트 링크AI4Math OpenReview원문 및 프로젝트 링크전체 논문 제목·초록 데이터원문 및 프로젝트 링크AXLE원문 및 프로젝트 링크HorizonMath원문 및 프로젝트 링크FIPO-Prover원문 및 프로젝트 링크Approach-Level Diversity원문 및 프로젝트 링크MLS-Bench원문 및 프로젝트 링크SEVerA원문 및 프로젝트 링크Self-Distillation Zero원문 및 프로젝트 링크QED원문 및 프로젝트 링크TorchLean원문 및 프로젝트 링크Lean Refactor원문 및 프로젝트 링크What Helps Agentic Lean Provers?원문 및 프로젝트 링크VOUCH원문 및 프로젝트 링크Lean Disprove원문 및 프로젝트 링크SABER-Math원문 및 프로젝트 링크ISM원문 및 프로젝트 링크LeanFlow원문 및 프로젝트 링크Proof Verification Is Obligation Coverage원문 및 프로젝트 링크DafnyProver원문 및 프로젝트 링크Faithful Autoformalization원문 및 프로젝트 링크VERITAS원문 및 프로젝트 링크PWW-Bench원문 및 프로젝트 링크LemmaBench원문 및 프로젝트 링크MathArena원문 및 프로젝트 링크Re²Math원문 및 프로젝트 링크ITPEval원문 및 프로젝트 링크QEDBENCH원문 및 프로젝트 링크P⁴Bench원문 및 프로젝트 링크BARSA원문 및 프로젝트 링크GRAIL원문 및 프로젝트 링크JURY-RL원문 및 프로젝트 링크Adaptive Generate–Rank–Verify원문 및 프로젝트 링크TEMPO원문 및 프로젝트 링크Probabilistic Chain-of-Thought원문 및 프로젝트 링크PRISM원문 및 프로젝트 링크P1-VL원문 및 프로젝트 링크Draw2Think원문 및 프로젝트 링크BioDimBench원문 및 프로젝트 링크