#formal-mathematics News & Analysis

2 articles tagged with #formal-mathematics. AI-curated summaries with sentiment analysis and key takeaways from 50+ sources.

2 articles

AIBullisharXiv – CS AI · 6h ago7/10

🧠

Expected Value Alignment for Generative Reward Modeling in Formal Mathematics Verification

Researchers introduce Expected Value Alignment (EVA), a novel reward-modeling technique that enables Large Language Models to provide continuous numerical scores while maintaining human-readable text output for formal mathematics verification in Lean 4. The method bridges a critical gap between discrete generative outputs and continuous value assessment needed for reinforcement learning in theorem proving systems.

AINeutralarXiv – CS AI · 6h ago6/10

🧠

Formally Solving Answer-Construction Problems in Lean

Researchers introduce Enumerate-Conjecture-Prove (ECP), a neuro-symbolic framework that combines general LLMs and prover LLMs to formally solve mathematical answer-construction problems in Lean. The approach addresses a critical gap where current AI systems struggle with generating both candidate answers and rigorous formal proofs, achieving higher success rates than baseline LLM approaches on competition mathematics benchmarks.